model.cc

   1 #include <stdio.h>
   2
   3 #include "model.h"
   4 #include "schedule.h"
   5 #include "common.h"
   6
   7 ModelChecker *model;
   8
   9 ModelChecker::ModelChecker()
  10 {
  11         /* First thread created (system_thread) will have id 1 */
  12         this->used_thread_id = 0;
  13         /* Initialize default scheduler */
  14         this->scheduler = new Scheduler();
  15
  16         this->current_action = NULL;
  17 }
  18
  19 ModelChecker::~ModelChecker()
  20 {
  21         delete this->scheduler;
  22 }
  23
  24 void ModelChecker::assign_id(Thread *t)
  25 {
  26         t->set_id(++used_thread_id);
  27 }
  28
  29 void ModelChecker::add_system_thread(Thread *t)
  30 {
  31         this->system_thread = t;
  32 }
  33
  34 void ModelChecker::check_current_action(void)
  35 {
  36         if (this->current_action)
  37                 this->action_trace.push_back(this->current_action);
  38         else
  39                 DEBUG("trying to push NULL action...\n");
  40 }
  41
  42 void ModelChecker::print_trace(void)
  43 {
  44         std::list<class ModelAction *>::iterator it;
  45
  46         for (it = action_trace.begin(); it != action_trace.end(); it++) {
  47                 DBG();
  48                 (*it)->print();
  49         }
  50 }
  51
  52 int ModelChecker::add_thread(Thread *t)
  53 {
  54         thread_map[t->get_id()] = t;
  55         return 0;
  56 }
  57
  58 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
  59 {
  60         Thread *t = thread_current();
  61         ModelAction *act = this;
  62
  63         act->type = type;
  64         act->order = order;
  65         act->location = loc;
  66         act->tid = t->get_id();
  67         act->value = value;
  68 }
  69
  70 void ModelAction::print(void)
  71 {
  72         const char *type_str;
  73         switch (this->type) {
  74         case THREAD_CREATE:
  75                 type_str = "thread create";
  76                 break;
  77         case THREAD_YIELD:
  78                 type_str = "thread yield";
  79                 break;
  80         case THREAD_JOIN:
  81                 type_str = "thread join";
  82                 break;
  83         case ATOMIC_READ:
  84                 type_str = "atomic read";
  85                 break;
  86         case ATOMIC_WRITE:
  87                 type_str = "atomic write";
  88                 break;
  89         default:
  90                 type_str = "unknown type";
  91         }
  92
  93         printf("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);
  94 }