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 int ModelChecker::switch_to_master(ModelAction *act)
  59 {
  60         Thread *old, *next;
  61
  62         DBG();
  63         old = thread_current();
  64         set_current_action(act);
  65         old->set_state(THREAD_READY);
  66         next = system_thread;
  67         return old->swap(next);
  68 }
  69
  70 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
  71 {
  72         Thread *t = thread_current();
  73         ModelAction *act = this;
  74
  75         act->type = type;
  76         act->order = order;
  77         act->location = loc;
  78         act->tid = t->get_id();
  79         act->value = value;
  80 }
  81
  82 void ModelAction::print(void)
  83 {
  84         const char *type_str;
  85         switch (this->type) {
  86         case THREAD_CREATE:
  87                 type_str = "thread create";
  88                 break;
  89         case THREAD_YIELD:
  90                 type_str = "thread yield";
  91                 break;
  92         case THREAD_JOIN:
  93                 type_str = "thread join";
  94                 break;
  95         case ATOMIC_READ:
  96                 type_str = "atomic read";
  97                 break;
  98         case ATOMIC_WRITE:
  99                 type_str = "atomic write";
 100                 break;
 101         default:
 102                 type_str = "unknown type";
 103         }
 104
 105         printf("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);
 106 }