2 * @brief Entry point for the model checker.
14 /* global "model" object */
17 #include "snapshot-interface.h"
19 static void param_defaults(struct model_params *params)
22 params->fairwindow = 0;
23 params->yieldon = false;
24 params->yieldblock = false;
25 params->enabledcount = 1;
27 params->verbose = !!DBG_ENABLED();
28 params->uninitvalue = 0;
29 params->maxexecutions = 0;
32 static void print_usage(const char *program_name, struct model_params *params)
34 /* Reset defaults before printing */
35 param_defaults(params);
38 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
39 "Distributed under the GPLv2\n"
40 "Written by Brian Norris and Brian Demsky\n"
42 "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
44 "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
45 "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
47 "Model-checker options:\n"
48 "-h, --help Display this help message and exit\n"
49 "-m, --liveness=NUM Maximum times a thread can read from the same write\n"
50 " while other writes exist.\n"
52 "-y, --yield Enable CHESS-like yield-based fairness support\n"
53 " (requires thrd_yield() in test program).\n"
55 "-Y, --yieldblock Prohibit an execution from running a yield.\n"
57 "-f, --fairness=WINDOW Specify a fairness window in which actions that are\n"
58 " enabled sufficiently many times should receive\n"
59 " priority for execution (not recommended).\n"
61 "-e, --enabled=COUNT Enabled count.\n"
63 "-b, --bound=MAX Upper length bound.\n"
65 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
66 " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
69 "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
70 " uninitialized atomic.\n"
72 "-t, --analysis=NAME Use Analysis Plugin.\n"
73 "-o, --options=NAME Option for previous analysis plugin. \n"
74 "-x, --maxexec=NUM Maximum number of executions.\n"
76 " -o help for a list of options\n"
77 " -- Program arguments follow.\n\n",
80 params->yieldon ? "enabled" : "disabled",
81 params->yieldblock ? "enabled" : "disabled",
87 params->maxexecutions);
92 static void parse_options(struct model_params *params, int argc, char **argv)
94 const char *shortopts = "hyYt:o:m:f:e:b:u:x:v::";
95 const struct option longopts[] = {
96 {"help", no_argument, NULL, 'h'},
97 {"liveness", required_argument, NULL, 'm'},
98 {"fairness", required_argument, NULL, 'f'},
99 {"yield", no_argument, NULL, 'y'},
100 {"yieldblock", no_argument, NULL, 'Y'},
101 {"enabled", required_argument, NULL, 'e'},
102 {"bound", required_argument, NULL, 'b'},
103 {"verbose", optional_argument, NULL, 'v'},
104 {"uninitialized", required_argument, NULL, 'u'},
105 {"analysis", required_argument, NULL, 't'},
106 {"options", required_argument, NULL, 'o'},
107 {"maxexecutions", required_argument, NULL, 'x'},
108 {0, 0, 0, 0} /* Terminator */
112 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
115 print_usage(argv[0], params);
118 params->maxexecutions = atoi(optarg);
121 params->fairwindow = atoi(optarg);
124 params->enabledcount = atoi(optarg);
127 params->bound = atoi(optarg);
130 params->maxreads = atoi(optarg);
133 params->verbose = optarg ? atoi(optarg) : 1;
136 params->uninitvalue = atoi(optarg);
139 params->yieldon = true;
142 if (install_plugin(optarg))
147 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
148 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
154 params->yieldblock = true;
162 /* Pass remaining arguments to user program */
163 params->argc = argc - (optind - 1);
164 params->argv = argv + (optind - 1);
166 /* Reset program name */
167 params->argv[0] = argv[0];
169 /* Reset (global) optind for potential use by user program */
173 print_usage(argv[0], params);
179 /** The model_main function contains the main model checking loop. */
180 static void model_main()
182 struct model_params params;
184 param_defaults(¶ms);
186 parse_options(¶ms, main_argc, main_argv);
188 //Initialize race detector
191 snapshot_stack_init();
193 model = new ModelChecker(params); // L: Model thread is created
194 // install_trace_analyses(model->get_execution()); L: disable plugin
204 * Main function. Just initializes snapshotting library and the
205 * snapshotting library calls the model_main function.
207 int main(int argc, char **argv)
213 * If this printf statement is removed, CDSChecker will fail on an
214 * assert on some versions of glibc. The first time printf is
215 * called, it allocated internal buffers. We can't easily snapshot
216 * libc since we also use it.
219 printf("CDSChecker\n"
220 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
221 "Distributed under the GPLv2\n"
222 "Written by Brian Norris and Brian Demsky\n\n");
224 /* Configure output redirection for the model-checker */
227 /* Let's jump in quickly and start running stuff */
228 snapshot_system_init(10000, 1024, 1024, 4000, &model_main);