2 * @brief Entry point for the model checker.
7 #include "libthreads.h"
13 /* global "model" object */
15 #include "snapshot-interface.h"
17 static void param_defaults(struct model_params * params) {
19 params->maxfuturedelay = 100;
22 static void print_usage(struct model_params *params) {
24 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
27 "-h Display this help message and exit\n"
28 "-m Maximum times a thread can read from the same write while other writes exist. Default: %d\n"
29 "-s Maximum actions that the model checker will wait for a write from the future past the expected number of actions. Default: %d\n"
30 "-- Program arguments follow.\n\n", params->maxreads, params->maxfuturedelay);
34 static void parse_options(struct model_params *params, int *argc, char ***argv) {
35 const char *shortopts = "hm:s:";
38 while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
44 params->maxfuturedelay = atoi(optarg);
47 params->maxreads = atoi(optarg);
64 /** The real_main function contains the main model checking loop. */
65 static void real_main() {
67 struct model_params params;
69 param_defaults(¶ms);
71 parse_options(¶ms, &main_argc, &main_argv);
73 //Initialize race detector
76 //Create the singleton SnapshotStack object
77 snapshotObject = new SnapshotStack();
79 model = new ModelChecker(params);
81 snapshotObject->snapshotStep(0);
83 /* Start user program */
84 model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
86 /* Wait for all threads to complete */
87 model->finish_execution();
88 } while (model->next_execution());
96 * Main function. Just initializes snapshotting library and the
97 * snapshotting library calls the real_main function.
99 int main(int argc, char ** argv) {
103 /* Let's jump in quickly and start running stuff */
104 initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main);