2 * @brief Entry point for the model checker.
14 /* global "model" object */
17 #include "snapshot-interface.h"
18 #include "scanalysis.h"
21 static void param_defaults(struct model_params *params)
24 params->maxfuturedelay = 6;
25 params->fairwindow = 0;
26 params->yieldon = false;
27 params->yieldblock = false;
28 params->enabledcount = 1;
30 params->maxfuturevalues = 0;
31 params->expireslop = 4;
32 params->verbose = !!DBG_ENABLED();
33 params->uninitvalue = 0;
34 params->maxexecutions = 0;
37 static void print_usage(const char *program_name, struct model_params *params)
39 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
40 /* Reset defaults before printing */
41 param_defaults(params);
44 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
45 "Distributed under the GPLv2\n"
46 "Written by Brian Norris and Brian Demsky\n"
48 "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
50 "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
51 "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
53 "Model-checker options:\n"
54 "-h, --help Display this help message and exit\n"
55 "-m, --liveness=NUM Maximum times a thread can read from the same write\n"
56 " while other writes exist.\n"
58 "-M, --maxfv=NUM Maximum number of future values that can be sent to\n"
61 "-s, --maxfvdelay=NUM Maximum actions that the model checker will wait for\n"
62 " a write from the future past the expected number\n"
65 "-S, --fvslop=NUM Future value expiration sloppiness.\n"
67 "-y, --yield Enable CHESS-like yield-based fairness support\n"
68 " (requires thrd_yield() in test program).\n"
70 "-Y, --yieldblock Prohibit an execution from running a yield.\n"
72 "-f, --fairness=WINDOW Specify a fairness window in which actions that are\n"
73 " enabled sufficiently many times should receive\n"
74 " priority for execution (not recommended).\n"
76 "-e, --enabled=COUNT Enabled count.\n"
78 "-b, --bound=MAX Upper length bound.\n"
80 "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
81 " 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
84 "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
85 " uninitialized atomic.\n"
87 "-t, --analysis=NAME Use Analysis Plugin.\n"
88 "-o, --options=NAME Option for previous analysis plugin. \n"
89 "-x, --maxexec=NUM Maximum number of executions.\n"
91 " -o help for a list of options\n"
92 " -- Program arguments follow.\n\n",
95 params->maxfuturevalues,
96 params->maxfuturedelay,
98 params->yieldon ? "enabled" : "disabled",
99 params->yieldblock ? "enabled" : "disabled",
101 params->enabledcount,
105 params->maxexecutions);
106 model_print("Analysis plugins:\n");
107 for(unsigned int i=0;i<registeredanalysis->size();i++) {
108 TraceAnalysis * analysis=(*registeredanalysis)[i];
109 model_print("%s\n", analysis->name());
114 bool install_plugin(char * name) {
115 ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
116 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
118 for(unsigned int i=0;i<registeredanalysis->size();i++) {
119 TraceAnalysis * analysis=(*registeredanalysis)[i];
120 if (strcmp(name, analysis->name())==0) {
121 installedanalysis->push_back(analysis);
125 model_print("Analysis %s Not Found\n", name);
129 static void parse_options(struct model_params *params, int argc, char **argv)
131 const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:x:v::";
132 const struct option longopts[] = {
133 {"help", no_argument, NULL, 'h'},
134 {"liveness", required_argument, NULL, 'm'},
135 {"maxfv", required_argument, NULL, 'M'},
136 {"maxfvdelay", required_argument, NULL, 's'},
137 {"fvslop", required_argument, NULL, 'S'},
138 {"fairness", required_argument, NULL, 'f'},
139 {"yield", no_argument, NULL, 'y'},
140 {"yieldblock", no_argument, NULL, 'Y'},
141 {"enabled", required_argument, NULL, 'e'},
142 {"bound", required_argument, NULL, 'b'},
143 {"verbose", optional_argument, NULL, 'v'},
144 {"uninitialized", required_argument, NULL, 'u'},
145 {"analysis", required_argument, NULL, 't'},
146 {"options", required_argument, NULL, 'o'},
147 {"maxexecutions", required_argument, NULL, 'x'},
148 {0, 0, 0, 0} /* Terminator */
152 while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
155 print_usage(argv[0], params);
158 params->maxexecutions = atoi(optarg);
161 params->maxfuturedelay = atoi(optarg);
164 params->expireslop = atoi(optarg);
167 params->fairwindow = atoi(optarg);
170 params->enabledcount = atoi(optarg);
173 params->bound = atoi(optarg);
176 params->maxreads = atoi(optarg);
179 params->maxfuturevalues = atoi(optarg);
182 params->verbose = optarg ? atoi(optarg) : 1;
185 params->uninitvalue = atoi(optarg);
188 params->yieldon = true;
191 if (install_plugin(optarg))
196 ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
197 if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
202 params->yieldblock = true;
210 /* Pass remaining arguments to user program */
211 params->argc = argc - (optind - 1);
212 params->argv = argv + (optind - 1);
214 /* Reset program name */
215 params->argv[0] = argv[0];
217 /* Reset (global) optind for potential use by user program */
221 print_usage(argv[0], params);
227 static void install_trace_analyses(ModelExecution *execution)
229 ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
230 for(unsigned int i=0;i<installedanalysis->size();i++) {
231 TraceAnalysis * ta=(*installedanalysis)[i];
232 ta->setExecution(execution);
233 model->add_trace_analysis(ta);
234 /** Call the installation event for each installed plugin */
235 ta->actionAtInstallation();
239 /** The model_main function contains the main model checking loop. */
240 static void model_main()
242 struct model_params params;
244 param_defaults(¶ms);
247 parse_options(¶ms, main_argc, main_argv);
249 //Initialize race detector
252 snapshot_stack_init();
254 model = new ModelChecker(params);
255 install_trace_analyses(model->get_execution());
265 * Main function. Just initializes snapshotting library and the
266 * snapshotting library calls the model_main function.
268 int main(int argc, char **argv)
274 * If this printf statement is removed, CDSChecker will fail on an
275 * assert on some versions of glibc. The first time printf is
276 * called, it allocated internal buffers. We can't easily snapshot
277 * libc since we also use it.
280 printf("CDSChecker\n"
281 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
282 "Distributed under the GPLv2\n"
283 "Written by Brian Norris and Brian Demsky\n\n");
285 /* Configure output redirection for the model-checker */
288 /* Let's jump in quickly and start running stuff */
289 snapshot_system_init(10000, 1024, 1024, 4000, &model_main);