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