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
  16 ModelChecker::~ModelChecker()
  17 {
  18         delete this->scheduler;
  19 }
  20
  21 void ModelChecker::assign_id(struct thread *t)
  22 {
  23         t->id = ++this->used_thread_id;
  24 }
  25
  26 void ModelChecker::add_system_thread(struct thread *t)
  27 {
  28         this->system_thread = t;
  29 }
  30
  31 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
  32 {
  33         struct thread *t = thread_current();
  34         ModelAction *act = this;
  35
  36         act->type = type;
  37         act->order = order;
  38         act->location = loc;
  39         act->tid = t->id;
  40         act->value = value;
  41 }
  42
  43 void ModelAction::print(void)
  44 {
  45         const char *type_str;
  46         switch (this->type) {
  47         case THREAD_CREATE:
  48                 type_str = "thread create";
  49                 break;
  50         case THREAD_YIELD:
  51                 type_str = "thread yield";
  52                 break;
  53         case THREAD_JOIN:
  54                 type_str = "thread join";
  55                 break;
  56         case ATOMIC_READ:
  57                 type_str = "atomic read";
  58                 break;
  59         case ATOMIC_WRITE:
  60                 type_str = "atomic write";
  61                 break;
  62         default:
  63                 type_str = "unknown type";
  64         }
  65
  66         printf("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);
  67 }