model: add read-acquire/fence-release support
[c11tester.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 "snapshot-interface.h"
15
16 static void param_defaults(struct model_params * params) {
17         params->maxreads = 0;
18         params->maxfuturedelay = 100;
19         params->fairwindow = 0;
20         params->enabledcount = 1;
21         params->bound = 0;
22         params->maxfuturevalues = 0;
23         params->expireslop = 10;
24         params->verbose = 0;
25 }
26
27 static void print_usage(struct model_params *params) {
28         /* Reset defaults before printing */
29         param_defaults(params);
30
31         model_print(
32 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
33 "\n"
34 "Options:\n"
35 "-h                    Display this help message and exit\n"
36 "-m                    Maximum times a thread can read from the same write\n"
37 "                      while other writes exist. Default: %d\n"
38 "-M                    Maximum number of future values that can be sent to\n"
39 "                      the same read. Default: %d\n"
40 "-s                    Maximum actions that the model checker will wait for\n"
41 "                      a write from the future past the expected number of\n"
42 "                      actions. Default: %d\n"
43 "-S                    Future value expiration sloppiness. Default: %u\n"
44 "-f                    Specify a fairness window in which actions that are\n"
45 "                      enabled sufficiently many times should receive\n"
46 "                      priority for execution. Default: %d\n"
47 "-e                    Enabled count. Default: %d\n"
48 "-b                    Upper length bound. Default: %d\n"
49 "-v                    Print verbose execution information.\n"
50 "--                    Program arguments follow.\n\n",
51 params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->enabledcount, params->bound);
52         exit(EXIT_SUCCESS);
53 }
54
55 static void parse_options(struct model_params *params, int argc, char **argv) {
56         const char *shortopts = "hm:M:s:S:f:e:b:v";
57         int opt;
58         bool error = false;
59         while (!error && (opt = getopt(argc, argv, shortopts)) != -1) {
60                 switch (opt) {
61                 case 'h':
62                         print_usage(params);
63                         break;
64                 case 's':
65                         params->maxfuturedelay = atoi(optarg);
66                         break;
67                 case 'S':
68                         params->expireslop = atoi(optarg);
69                         break;
70                 case 'f':
71                         params->fairwindow = atoi(optarg);
72                         break;
73                 case 'e':
74                         params->enabledcount = atoi(optarg);
75                         break;
76                 case 'b':
77                         params->bound = atoi(optarg);
78                         break;
79                 case 'm':
80                         params->maxreads = atoi(optarg);
81                         break;
82                 case 'M':
83                         params->maxfuturevalues = atoi(optarg);
84                         break;
85                 case 'v':
86                         params->verbose = 1;
87                         break;
88                 default: /* '?' */
89                         error = true;
90                         break;
91                 }
92         }
93
94         /* Pass remaining arguments to user program */
95         params->argc = argc - (optind - 1);
96         params->argv = argv + (optind - 1);
97
98         /* Reset program name */
99         params->argv[0] = argv[0];
100
101         /* Reset (global) optind for potential use by user program */
102         optind = 1;
103
104         if (error)
105                 print_usage(params);
106 }
107
108 int main_argc;
109 char **main_argv;
110
111 /** The model_main function contains the main model checking loop. */
112 static void model_main() {
113         struct model_params params;
114
115         param_defaults(&params);
116
117         parse_options(&params, main_argc, main_argv);
118
119         //Initialize race detector
120         initRaceDetector();
121
122         //Create the singleton SnapshotStack object
123         snapshotObject = new SnapshotStack();
124
125         model = new ModelChecker(params);
126         snapshotObject->snapshotStep(0);
127         model->run();
128         delete model;
129
130         DEBUG("Exiting\n");
131 }
132
133 /**
134  * Main function.  Just initializes snapshotting library and the
135  * snapshotting library calls the model_main function.
136  */
137 int main(int argc, char ** argv) {
138         main_argc = argc;
139         main_argv = argv;
140
141         /* Configure output redirection for the model-checker */
142         redirect_output();
143
144         /* Let's jump in quickly and start running stuff */
145         initSnapshotLibrary(10000, 1024, 1024, 4000, &model_main);
146 }