model.cc

   1 #include <stdio.h>
   2
   3 #include "model.h"
   4 #include "schedule.h"
   5
   6 ModelChecker *model;
   7
   8 ModelChecker::ModelChecker()
   9 {
  10         /* First thread created (system_thread) will have id 1 */
  11         this->used_thread_id = 0;
  12         /* Initialize default scheduler */
  13         this->scheduler = new DefaultScheduler();
  14
  15         this->current_action = NULL;
  16 }
  17
  18 ModelChecker::~ModelChecker()
  19 {
  20         delete this->scheduler;
  21 }
  22
  23 void ModelChecker::assign_id(struct thread *t)
  24 {
  25         t->id = ++this->used_thread_id;
  26 }
  27
  28 void ModelChecker::add_system_thread(struct thread *t)
  29 {
  30         this->system_thread = t;
  31 }
  32
  33 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
  34 {
  35         struct thread *t = thread_current();
  36         ModelAction *act = this;
  37
  38         act->type = type;
  39         act->order = order;
  40         act->location = loc;
  41         act->tid = t->id;
  42         act->value = value;
  43 }
  44
  45 void ModelAction::print(void)
  46 {
  47         const char *type_str;
  48         switch (this->type) {
  49         case THREAD_CREATE:
  50                 type_str = "thread create";
  51                 break;
  52         case THREAD_YIELD:
  53                 type_str = "thread yield";
  54                 break;
  55         case THREAD_JOIN:
  56                 type_str = "thread join";
  57                 break;
  58         case ATOMIC_READ:
  59                 type_str = "atomic read";
  60                 break;
  61         case ATOMIC_WRITE:
  62                 type_str = "atomic write";
  63                 break;
  64         default:
  65                 type_str = "unknown type";
  66         }
  67
  68         printf("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);
  69 }