while (!thread_system_next());
}
+static void parse_options(struct model_params *params, int argc, char **argv) {
+}
+
+int main_argc;
+char **main_argv;
/** The real_main function contains the main model checking loop. */
static void real_main() {
thrd_t user_thread;
ucontext_t main_context;
+ struct model_params params;
+
+ parse_options(¶ms, main_argc, main_argv);
//Initialize race detector
initRaceDetector();
//Create the singleton SnapshotStack object
snapshotObject = new SnapshotStack();
- model = new ModelChecker();
+ model = new ModelChecker(params);
if (getcontext(&main_context))
return;
DEBUG("Exiting\n");
}
-int main_numargs;
-char ** main_args;
-
/**
* Main function. Just initializes snapshotting library and the
* snapshotting library calls the real_main function.
*/
-int main(int numargs, char ** args) {
- /* Stash this stuff in case someone wants it eventually */
- main_numargs=numargs;
- main_args=args;
+int main(int argc, char ** argv) {
+ main_argc = argc;
+ main_argv = argv;
/* Let's jump in quickly and start running stuff */
initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main);
ModelChecker *model;
/** @brief Constructor */
-ModelChecker::ModelChecker() :
+ModelChecker::ModelChecker(struct model_params params) :
/* Initialize default scheduler */
scheduler(new Scheduler()),
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
num_executions(0),
+ params(params),
current_action(NULL),
diverge(NULL),
nextThread(THREAD_ID_T_NONE),
class CycleGraph;
class Promise;
+/**
+ * Model checker parameter structure. Holds run-time configuration options for
+ * the model checker.
+ */
+struct model_params {
+};
+
/** @brief The central structure for model-checking */
class ModelChecker {
public:
- ModelChecker();
+ ModelChecker(struct model_params params);
~ModelChecker();
/** The scheduler to use: tracks the running/ready Threads */
modelclock_t used_sequence_numbers;
int num_executions;
+ const model_params params;
+
/**
* Stores the ModelAction for the current thread action. Call this
* immediately before switching from user- to system-context to pass