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