5 #include "clockvector.h"
8 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value) :
15 Thread *t = thread_current();
16 this->tid = t->get_id();
17 this->seq_number = model->get_next_seq_num();
20 ModelAction::~ModelAction()
26 bool ModelAction::is_read() const
28 return type == ATOMIC_READ;
31 bool ModelAction::is_write() const
33 return type == ATOMIC_WRITE || type == ATOMIC_INIT;
36 bool ModelAction::is_rmw() const
38 return type == ATOMIC_RMW;
41 bool ModelAction::is_initialization() const
43 return type == ATOMIC_INIT;
46 bool ModelAction::is_acquire() const
49 case memory_order_acquire:
50 case memory_order_acq_rel:
51 case memory_order_seq_cst:
58 bool ModelAction::is_release() const
61 case memory_order_release:
62 case memory_order_acq_rel:
63 case memory_order_seq_cst:
70 bool ModelAction::is_seqcst() const
72 return order==memory_order_seq_cst;
75 bool ModelAction::same_var(const ModelAction *act) const
77 return location == act->location;
80 bool ModelAction::same_thread(const ModelAction *act) const
82 return tid == act->tid;
85 /** The is_synchronizing method should only explore interleavings if:
86 * (1) the operations are seq_cst and don't commute or
87 * (2) the reordering may establish or break a synchronization relation.
88 * Other memory operations will be dealt with by using the reads_from
91 * @param act is the action to consider exploring a reordering.
92 * @return tells whether we have to explore a reordering.
95 bool ModelAction::is_synchronizing(const ModelAction *act) const
97 //Same thread can't be reordered
101 // Different locations commute
105 // Explore interleavings of seqcst writes to guarantee total order
106 // of seq_cst operations that don't commute
107 if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
110 // Explore synchronizing read/write pairs
111 if (is_read() && is_acquire() && act->is_write() && act->is_release())
113 if (is_write() && is_release() && act->is_read() && act->is_acquire())
116 // Otherwise handle by reads_from relation
120 void ModelAction::create_cv(const ModelAction *parent)
125 cv = new ClockVector(parent->cv, this);
127 cv = new ClockVector(NULL, this);
130 void ModelAction::read_from(const ModelAction *act)
133 if (act->is_release() && this->is_acquire())
139 * Check whether 'this' happens before act, according to the memory-model's
140 * happens before relation. This is checked via the ClockVector constructs.
141 * @return true if this action's thread has synchronized with act's thread
142 * since the execution of act, false otherwise.
144 bool ModelAction::happens_before(const ModelAction *act) const
146 return act->cv->synchronized_since(this);
149 void ModelAction::print(void) const
151 const char *type_str;
152 switch (this->type) {
154 type_str = "thread create";
157 type_str = "thread yield";
160 type_str = "thread join";
163 type_str = "atomic read";
166 type_str = "atomic write";
169 type_str = "atomic rmw";
172 type_str = "init atomic";
175 type_str = "unknown type";
178 printf("(%3d) Thread: %-2d Action: %-13s MO: %d Loc: %14p Value: %d",
179 seq_number, id_to_int(tid), type_str, order, location, value);