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 while other writes exist. Default: %d\n"
  29 "-s                    Maximum actions that the model checker will wait for a write from the future past the expected number of actions.  Default: %d\n"
  30 "--                    Program arguments follow.\n\n", params->maxreads, params->maxfuturedelay);
  31         exit(EXIT_SUCCESS);
  32 }
  33
  34 static void parse_options(struct model_params *params, int *argc, char ***argv) {
  35         const char *shortopts = "hm:s:";
  36         int opt;
  37         bool error = false;
  38         while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
  39                 switch (opt) {
  40                 case 'h':
  41                         print_usage(params);
  42                         break;
  43                 case 's':
  44                         params->maxfuturedelay = atoi(optarg);
  45                         break;
  46                 case 'm':
  47                         params->maxreads = atoi(optarg);
  48                         break;
  49                 default: /* '?' */
  50                         error = true;
  51                         break;
  52                 }
  53         }
  54         (*argc) -= optind;
  55         (*argv) += optind;
  56
  57         if (error)
  58                 print_usage(params);
  59 }
  60
  61 int main_argc;
  62 char **main_argv;
  63
  64 /** The real_main function contains the main model checking loop. */
  65 static void real_main() {
  66         thrd_t user_thread;
  67         struct model_params params;
  68
  69         param_defaults(&params);
  70
  71         parse_options(&params, &main_argc, &main_argv);
  72
  73         //Initialize race detector
  74         initRaceDetector();
  75
  76         //Create the singleton SnapshotStack object
  77         snapshotObject = new SnapshotStack();
  78
  79         model = new ModelChecker(params);
  80
  81         snapshotObject->snapshotStep(0);
  82         do {
  83                 /* Start user program */
  84                 model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
  85
  86                 /* Wait for all threads to complete */
  87                 model->finish_execution();
  88         } while (model->next_execution());
  89
  90         delete model;
  91
  92         DEBUG("Exiting\n");
  93 }
  94
  95 /**
  96  * Main function.  Just initializes snapshotting library and the
  97  * snapshotting library calls the real_main function.
  98  */
  99 int main(int argc, char ** argv) {
 100         main_argc = argc;
 101         main_argv = argv;
 102
 103         /* Let's jump in quickly and start running stuff */
 104         initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main);
 105 }