model.cc

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #include "model.h"
  11 #include "snapshot-interface.h"
  12 #include "mcschedule.h"
  13 #include "output.h"
  14 #include "planner.h"
  15
  16 MC * model;
  17
  18 MC::MC(struct model_params params) :
  19         params(params),
  20         execution(new MCExecution())
  21 {
  22 }
  23
  24 MC::~MC() {
  25         delete execution;
  26 }
  27
  28 /** Wrapper to run the user's main function, with appropriate arguments */
  29 void user_main_wrapper(void *) {
  30         user_main(model->params.argc, model->params.argv);
  31 }
  32
  33 /** Implements the main loop for model checking test case
  34  */
  35 void MC::check() {
  36         snapshot_record(0);
  37         do {
  38                 run_execution();
  39                 execution->get_planner()->plan();
  40                 print_program_output();
  41 #if SUPPORT_MOD_ORDER_DUMP
  42                 execution->dumpExecution();
  43 #endif
  44                 execution->reset();
  45                 snapshot_backtrack_before(0);
  46         } while(!execution->get_planner()->is_finished());
  47         dprintf(2, "Finished!\n");
  48 }
  49
  50
  51 /** Executes a single execution. */
  52
  53 void MC::run_execution() {
  54         thrd_t user_thread;
  55         Thread *t = new Thread(execution->get_next_tid(), &user_thread, &user_main_wrapper, NULL, NULL, NULL);
  56         execution->add_thread(t);
  57         execution->get_scheduler()->swap_threads(NULL, t);
  58 }
  59
  60