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->maxfuturedelay = 6;
23 params->fairwindow = 0;
24 params->yieldon = false;
25 params->yieldblock = false;
26 params->enabledcount = 1;
28 params->maxfuturevalues = 0;
29 params->expireslop = 4;
30 params->verbose = !!DBG_ENABLED();
31 params->uninitvalue = 0;
32 params->maxexecutions = 0;
35 static void print_usage(const char *program_name, struct model_params *params)
37 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
38 /* Reset defaults before printing */
39 param_defaults(params);
42 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
43 "Distributed under the GPLv2\n"
44 "Written by Brian Norris and Brian Demsky\n"
46 "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
48 "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
49 "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
51 "Model-checker options:\n"
52 "-h, --help Display this help message and exit\n"
53 "-m, --liveness=NUM Maximum times a thread can read from the same write\n"
54 " while other writes exist.\n"
56 "-M, --maxfv=NUM Maximum number of future values that can be sent to\n"
59 "-s, --maxfvdelay=NUM Maximum actions that the model checker will wait for\n"
60 " a write from the future past the expected number\n"
63 "-S, --fvslop=NUM Future value expiration sloppiness.\n"
65 "-y, --yield Enable CHESS-like yield-based fairness support\n"
66 " (requires thrd_yield() in test program).\n"
68 "-Y, --yieldblock Prohibit an execution from running a yield.\n"
70 "-f, --fairness=WINDOW Specify a fairness window in which actions that are\n"
71 " enabled sufficiently many times should receive\n"
72 " priority for execution (not recommended).\n"
74 "-e, --enabled=COUNT Enabled count.\n"
76 "-b, --bound=MAX Upper length bound.\n"
78 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
79 " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
82 "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
83 " uninitialized atomic.\n"
85 "-t, --analysis=NAME Use Analysis Plugin.\n"
86 "-o, --options=NAME Option for previous analysis plugin. \n"
87 "-x, --maxexec=NUM Maximum number of executions.\n"
89 " -o help for a list of options\n"
90 " -- Program arguments follow.\n\n",
93 params->maxfuturevalues,
94 params->maxfuturedelay,
96 params->yieldon ? "enabled" : "disabled",
97 params->yieldblock ? "enabled" : "disabled",
103 params->maxexecutions);
104 model_print("Analysis plugins:\n");
105 for(unsigned int i=0;i<registeredanalysis->size();i++) {
106 TraceAnalysis * analysis=(*registeredanalysis)[i];
107 model_print("%s\n", analysis->name());
112 bool install_plugin(char * name) {
113 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
114 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
116 for(unsigned int i=0;i<registeredanalysis->size();i++) {
117 TraceAnalysis * analysis=(*registeredanalysis)[i];
118 if (strcmp(name, analysis->name())==0) {
119 installedanalysis->push_back(analysis);
123 model_print("Analysis %s Not Found\n", name);
127 static void parse_options(struct model_params *params, int argc, char **argv)
129 const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:x:v::";
130 const struct option longopts[] = {
131 {"help", no_argument, NULL, 'h'},
132 {"liveness", required_argument, NULL, 'm'},
133 {"maxfv", required_argument, NULL, 'M'},
134 {"maxfvdelay", required_argument, NULL, 's'},
135 {"fvslop", required_argument, NULL, 'S'},
136 {"fairness", required_argument, NULL, 'f'},
137 {"yield", no_argument, NULL, 'y'},
138 {"yieldblock", no_argument, NULL, 'Y'},
139 {"enabled", required_argument, NULL, 'e'},
140 {"bound", required_argument, NULL, 'b'},
141 {"verbose", optional_argument, NULL, 'v'},
142 {"uninitialized", required_argument, NULL, 'u'},
143 {"analysis", required_argument, NULL, 't'},
144 {"options", required_argument, NULL, 'o'},
145 {"maxexecutions", required_argument, NULL, 'x'},
146 {0, 0, 0, 0} /* Terminator */
150 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
153 print_usage(argv[0], params);
156 params->maxexecutions = atoi(optarg);
159 params->maxfuturedelay = atoi(optarg);
162 params->expireslop = atoi(optarg);
165 params->fairwindow = atoi(optarg);
168 params->enabledcount = atoi(optarg);
171 params->bound = atoi(optarg);
174 params->maxreads = atoi(optarg);
177 params->maxfuturevalues = atoi(optarg);
180 params->verbose = optarg ? atoi(optarg) : 1;
183 params->uninitvalue = atoi(optarg);
186 params->yieldon = true;
189 if (install_plugin(optarg))
194 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
195 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
200 params->yieldblock = true;
208 /* Pass remaining arguments to user program */
209 params->argc = argc - (optind - 1);
210 params->argv = argv + (optind - 1);
212 /* Reset program name */
213 params->argv[0] = argv[0];
215 /* Reset (global) optind for potential use by user program */
219 print_usage(argv[0], params);
225 static void install_trace_analyses(ModelExecution *execution)
227 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
228 for(unsigned int i=0;i<installedanalysis->size();i++) {
229 TraceAnalysis * ta=(*installedanalysis)[i];
230 ta->setExecution(execution);
231 model->add_trace_analysis(ta);
232 /** Call the installation event for each installed plugin */
233 ta->actionAtInstallation();
237 /** The model_main function contains the main model checking loop. */
238 static void model_main()
240 struct model_params params;
242 param_defaults(¶ms);
245 parse_options(¶ms, main_argc, main_argv);
247 //Initialize race detector
250 snapshot_stack_init();
252 model = new ModelChecker(params); // L: Model thread is created
253 // install_trace_analyses(model->get_execution()); L: disable plugin
263 * Main function. Just initializes snapshotting library and the
264 * snapshotting library calls the model_main function.
266 int main(int argc, char **argv)
272 * If this printf statement is removed, CDSChecker will fail on an
273 * assert on some versions of glibc. The first time printf is
274 * called, it allocated internal buffers. We can't easily snapshot
275 * libc since we also use it.
278 printf("CDSChecker\n"
279 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
280 "Distributed under the GPLv2\n"
281 "Written by Brian Norris and Brian Demsky\n\n");
283 /* Configure output redirection for the model-checker */
286 /* Let's jump in quickly and start running stuff */
287 snapshot_system_init(10000, 1024, 1024, 4000, &model_main);