main.cc

   1 /** @file main.cc
   2  *  @brief Entry point for the model checker.
   3  */
   4
   5 #include <unistd.h>
   6
   7 #include "libthreads.h"
   8 #include "common.h"
   9 #include "threads.h"
  10
  11 #include "datarace.h"
  12
  13 /* global "model" object */
  14 #include "model.h"
  15 #include "snapshot-interface.h"
  16
  17 static void param_defaults(struct model_params * params) {
  18         params->maxreads = 0;
  19         params->maxfuturedelay = 100;
  20 }
  21
  22 static void print_usage(struct model_params *params) {
  23         printf(
  24 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
  25 "\n"
  26 "Options:\n"
  27 "-h                    Display this help message and exit\n"
  28 "-m                    Maximum times a thread can read from the same write\n"
  29 "                      while other writes exist. Default: %d\n"
  30 "-s                    Maximum actions that the model checker will wait for\n"
  31 "                      a write from the future past the expected number of\n"
  32 "                      actions. Default: %d\n"
  33 "--                    Program arguments follow.\n\n",
  34                         params->maxreads, params->maxfuturedelay);
  35         exit(EXIT_SUCCESS);
  36 }
  37
  38 static void parse_options(struct model_params *params, int *argc, char ***argv) {
  39         const char *shortopts = "hm:s:";
  40         int opt;
  41         bool error = false;
  42         while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
  43                 switch (opt) {
  44                 case 'h':
  45                         print_usage(params);
  46                         break;
  47                 case 's':
  48                         params->maxfuturedelay = atoi(optarg);
  49                         break;
  50                 case 'm':
  51                         params->maxreads = atoi(optarg);
  52                         break;
  53                 default: /* '?' */
  54                         error = true;
  55                         break;
  56                 }
  57         }
  58         (*argc) -= optind;
  59         (*argv) += optind;
  60
  61         if (error)
  62                 print_usage(params);
  63 }
  64
  65 int main_argc;
  66 char **main_argv;
  67
  68 /** The real_main function contains the main model checking loop. */
  69 static void real_main() {
  70         thrd_t user_thread;
  71         struct model_params params;
  72
  73         param_defaults(&params);
  74
  75         parse_options(&params, &main_argc, &main_argv);
  76
  77         //Initialize race detector
  78         initRaceDetector();
  79
  80         //Create the singleton SnapshotStack object
  81         snapshotObject = new SnapshotStack();
  82
  83         model = new ModelChecker(params);
  84
  85         snapshotObject->snapshotStep(0);
  86         do {
  87                 /* Start user program */
  88                 model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
  89
  90                 /* Wait for all threads to complete */
  91                 model->finish_execution();
  92         } while (model->next_execution());
  93
  94         delete model;
  95
  96         DEBUG("Exiting\n");
  97 }
  98
  99 /**
 100  * Main function.  Just initializes snapshotting library and the
 101  * snapshotting library calls the real_main function.
 102  */
 103 int main(int argc, char ** argv) {
 104         main_argc = argc;
 105         main_argv = argv;
 106
 107         /* Let's jump in quickly and start running stuff */
 108         initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main);
 109 }