execution: improve documentation
[model-checker.git] / main.cc
1 /** @file main.cc
2  *  @brief Entry point for the model checker.
3  */
4
5 #include <unistd.h>
6
7 #include "common.h"
8 #include "output.h"
9
10 #include "datarace.h"
11
12 /* global "model" object */
13 #include "model.h"
14 #include "params.h"
15 #include "snapshot-interface.h"
16 #include "scanalysis.h"
17
18 static void param_defaults(struct model_params *params)
19 {
20         params->maxreads = 0;
21         params->maxfuturedelay = 6;
22         params->fairwindow = 0;
23         params->yieldon = false;
24         params->yieldblock = false;
25         params->sc_trace_analysis = false;
26         params->enabledcount = 1;
27         params->bound = 0;
28         params->maxfuturevalues = 0;
29         params->expireslop = 4;
30         params->verbose = !!DBG_ENABLED();
31         params->uninitvalue = 0;
32 }
33
34 static void print_usage(struct model_params *params)
35 {
36         /* Reset defaults before printing */
37         param_defaults(params);
38
39         model_print(
40 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
41 "Distributed under the GPLv2\n"
42 "Written by Brian Norris and Brian Demsky\n"
43 "\n"
44 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
45 "\n"
46 "Options:\n"
47 "-h                    Display this help message and exit\n"
48 "-m                    Maximum times a thread can read from the same write\n"
49 "                      while other writes exist. Default: %d\n"
50 "-M                    Maximum number of future values that can be sent to\n"
51 "                      the same read. Default: %d\n"
52 "-s                    Maximum actions that the model checker will wait for\n"
53 "                      a write from the future past the expected number of\n"
54 "                      actions. Default: %d\n"
55 "-S                    Future value expiration sloppiness. Default: %u\n"
56 "-f                    Specify a fairness window in which actions that are\n"
57 "                      enabled sufficiently many times should receive\n"
58 "                      priority for execution. Default: %d\n"
59 "-y                    Turn on CHESS yield-based fairness support.\n"
60 "                      Default: %d\n"
61 "-Y                    Prohibit an execution from running a yield.\n"
62 "                      Default: %d\n"
63 "-e                    Enabled count. Default: %d\n"
64 "-b                    Upper length bound. Default: %d\n"
65 "-v                    Print verbose execution information.\n"
66 "-u                    Value for uninitialized reads. Default: %u\n"
67 "-c                    Use SC Trace Analysis.\n"
68 "--                    Program arguments follow.\n\n",
69 params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->yieldblock, params->enabledcount, params->bound, params->uninitvalue);
70         exit(EXIT_SUCCESS);
71 }
72
73 static void parse_options(struct model_params *params, int argc, char **argv)
74 {
75         const char *shortopts = "hyYcm:M:s:S:f:e:b:u:v";
76         int opt;
77         bool error = false;
78         while (!error && (opt = getopt(argc, argv, shortopts)) != -1) {
79                 switch (opt) {
80                 case 'h':
81                         print_usage(params);
82                         break;
83                 case 's':
84                         params->maxfuturedelay = atoi(optarg);
85                         break;
86                 case 'S':
87                         params->expireslop = atoi(optarg);
88                         break;
89                 case 'f':
90                         params->fairwindow = atoi(optarg);
91                         break;
92                 case 'e':
93                         params->enabledcount = atoi(optarg);
94                         break;
95                 case 'b':
96                         params->bound = atoi(optarg);
97                         break;
98                 case 'm':
99                         params->maxreads = atoi(optarg);
100                         break;
101                 case 'M':
102                         params->maxfuturevalues = atoi(optarg);
103                         break;
104                 case 'v':
105                         params->verbose = 1;
106                         break;
107                 case 'u':
108                         params->uninitvalue = atoi(optarg);
109                         break;
110                 case 'c':
111                         params->sc_trace_analysis = true;
112                         break;
113                 case 'y':
114                         params->yieldon = true;
115                         break;
116                 case 'Y':
117                         params->yieldblock = true;
118                         break;
119                 default: /* '?' */
120                         error = true;
121                         break;
122                 }
123         }
124
125         /* Pass remaining arguments to user program */
126         params->argc = argc - (optind - 1);
127         params->argv = argv + (optind - 1);
128
129         /* Reset program name */
130         params->argv[0] = argv[0];
131
132         /* Reset (global) optind for potential use by user program */
133         optind = 1;
134
135         if (error)
136                 print_usage(params);
137 }
138
139 int main_argc;
140 char **main_argv;
141
142 static void install_trace_analyses(const ModelExecution *execution)
143 {
144         if (model->params.sc_trace_analysis)
145                 model->add_trace_analysis(new SCAnalysis(execution));
146 }
147
148 /** The model_main function contains the main model checking loop. */
149 static void model_main()
150 {
151         struct model_params params;
152
153         param_defaults(&params);
154
155         parse_options(&params, main_argc, main_argv);
156
157         //Initialize race detector
158         initRaceDetector();
159
160         snapshot_stack_init();
161
162         model = new ModelChecker(params);
163         install_trace_analyses(model->get_execution());
164
165         snapshot_record(0);
166         model->run();
167         delete model;
168
169         DEBUG("Exiting\n");
170 }
171
172 /**
173  * Main function.  Just initializes snapshotting library and the
174  * snapshotting library calls the model_main function.
175  */
176 int main(int argc, char **argv)
177 {
178         main_argc = argc;
179         main_argv = argv;
180
181         /* Configure output redirection for the model-checker */
182         redirect_output();
183
184         /* Let's jump in quickly and start running stuff */
185         snapshot_system_init(10000, 1024, 1024, 4000, &model_main);
186 }