action.cc

   1 #include <stdio.h>
   2 #define __STDC_FORMAT_MACROS
   3 #include <inttypes.h>
   4
   5 #include "model.h"
   6 #include "action.h"
   7 #include "clockvector.h"
   8 #include "common.h"
   9
  10 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) :
  11         type(type),
  12         order(order),
  13         location(loc),
  14         value(value),
  15         reads_from(NULL),
  16         cv(NULL)
  17 {
  18         Thread *t = thread_current();
  19         this->tid = t->get_id();
  20         this->seq_number = model->get_next_seq_num();
  21 }
  22
  23 ModelAction::~ModelAction()
  24 {
  25         if (cv)
  26                 delete cv;
  27 }
  28
  29 bool ModelAction::is_read() const
  30 {
  31         return type == ATOMIC_READ || type == ATOMIC_RMW;
  32 }
  33
  34 bool ModelAction::is_write() const
  35 {
  36         return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT;
  37 }
  38
  39 bool ModelAction::is_rmw() const
  40 {
  41         return type == ATOMIC_RMW;
  42 }
  43
  44 bool ModelAction::is_initialization() const
  45 {
  46         return type == ATOMIC_INIT;
  47 }
  48
  49 bool ModelAction::is_acquire() const
  50 {
  51         switch (order) {
  52         case memory_order_acquire:
  53         case memory_order_acq_rel:
  54         case memory_order_seq_cst:
  55                 return true;
  56         default:
  57                 return false;
  58         }
  59 }
  60
  61 bool ModelAction::is_release() const
  62 {
  63         switch (order) {
  64         case memory_order_release:
  65         case memory_order_acq_rel:
  66         case memory_order_seq_cst:
  67                 return true;
  68         default:
  69                 return false;
  70         }
  71 }
  72
  73 bool ModelAction::is_seqcst() const
  74 {
  75         return order==memory_order_seq_cst;
  76 }
  77
  78 bool ModelAction::same_var(const ModelAction *act) const
  79 {
  80         return location == act->location;
  81 }
  82
  83 bool ModelAction::same_thread(const ModelAction *act) const
  84 {
  85         return tid == act->tid;
  86 }
  87
  88 void ModelAction::upgrade_rmw(ModelAction * act) {
  89         ASSERT(is_read());
  90         ASSERT(act->is_rmw());
  91         //Upgrade our type to the act's type
  92         this->type=act->type;
  93         this->order=act->order;
  94         this->value=act->value;
  95 }
  96
  97 /** The is_synchronizing method should only explore interleavings if:
  98  *  (1) the operations are seq_cst and don't commute or
  99  *  (2) the reordering may establish or break a synchronization relation.
 100  *  Other memory operations will be dealt with by using the reads_from
 101  *  relation.
 102  *
 103  *  @param act is the action to consider exploring a reordering.
 104  *  @return tells whether we have to explore a reordering.
 105  */
 106
 107 bool ModelAction::is_synchronizing(const ModelAction *act) const
 108 {
 109         //Same thread can't be reordered
 110         if (same_thread(act))
 111                 return false;
 112
 113         // Different locations commute
 114         if (!same_var(act))
 115                 return false;
 116
 117         // Explore interleavings of seqcst writes to guarantee total order
 118         // of seq_cst operations that don't commute
 119         if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
 120                 return true;
 121
 122         // Explore synchronizing read/write pairs
 123         if (is_read() && is_acquire() && act->is_write() && act->is_release())
 124                 return true;
 125         if (is_write() && is_release() && act->is_read() && act->is_acquire())
 126                 return true;
 127
 128         // Otherwise handle by reads_from relation
 129         return false;
 130 }
 131
 132 void ModelAction::create_cv(const ModelAction *parent)
 133 {
 134         ASSERT(cv == NULL);
 135
 136         if (parent)
 137                 cv = new ClockVector(parent->cv, this);
 138         else
 139                 cv = new ClockVector(NULL, this);
 140 }
 141
 142 void ModelAction::read_from(const ModelAction *act)
 143 {
 144         ASSERT(cv);
 145         if (act->is_release() && this->is_acquire())
 146                 cv->merge(act->cv);
 147         reads_from = act;
 148 }
 149
 150 /**
 151  * Check whether 'this' happens before act, according to the memory-model's
 152  * happens before relation. This is checked via the ClockVector constructs.
 153  * @return true if this action's thread has synchronized with act's thread
 154  * since the execution of act, false otherwise.
 155  */
 156 bool ModelAction::happens_before(const ModelAction *act) const
 157 {
 158         return act->cv->synchronized_since(this);
 159 }
 160
 161 void ModelAction::print(void) const
 162 {
 163         const char *type_str;
 164         switch (this->type) {
 165         case THREAD_CREATE:
 166                 type_str = "thread create";
 167                 break;
 168         case THREAD_START:
 169                 type_str = "thread start";
 170                 break;
 171         case THREAD_YIELD:
 172                 type_str = "thread yield";
 173                 break;
 174         case THREAD_JOIN:
 175                 type_str = "thread join";
 176                 break;
 177         case ATOMIC_READ:
 178                 type_str = "atomic read";
 179                 break;
 180         case ATOMIC_WRITE:
 181                 type_str = "atomic write";
 182                 break;
 183         case ATOMIC_RMW:
 184                 type_str = "atomic rmw";
 185                 break;
 186         case ATOMIC_INIT:
 187                 type_str = "init atomic";
 188                 break;
 189         default:
 190                 type_str = "unknown type";
 191         }
 192
 193         uint64_t valuetoprint=type==ATOMIC_READ?reads_from->value:value;
 194
 195         printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %-12" PRIu64,
 196                         seq_number, id_to_int(tid), type_str, order, location, valuetoprint);
 197         if (reads_from)
 198                 printf(" Rf: %d", reads_from->get_seq_number());
 199         if (cv) {
 200                 printf("\t");
 201                 cv->print();
 202         } else
 203                 printf("\n");
 204 }