5 #include "clockvector.h"
8 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value) :
16 Thread *t = thread_current();
17 this->tid = t->get_id();
18 this->seq_number = model->get_next_seq_num();
21 ModelAction::~ModelAction()
27 bool ModelAction::is_read() const
29 return type == ATOMIC_READ;
32 bool ModelAction::is_write() const
34 return type == ATOMIC_WRITE || type == ATOMIC_INIT;
37 bool ModelAction::is_rmw() const
39 return type == ATOMIC_RMW;
42 bool ModelAction::is_initialization() const
44 return type == ATOMIC_INIT;
47 bool ModelAction::is_acquire() const
50 case memory_order_acquire:
51 case memory_order_acq_rel:
52 case memory_order_seq_cst:
59 bool ModelAction::is_release() const
62 case memory_order_release:
63 case memory_order_acq_rel:
64 case memory_order_seq_cst:
71 bool ModelAction::is_seqcst() const
73 return order==memory_order_seq_cst;
76 bool ModelAction::same_var(const ModelAction *act) const
78 return location == act->location;
81 bool ModelAction::same_thread(const ModelAction *act) const
83 return tid == act->tid;
86 /** The is_synchronizing method should only explore interleavings if:
87 * (1) the operations are seq_cst and don't commute or
88 * (2) the reordering may establish or break a synchronization relation.
89 * Other memory operations will be dealt with by using the reads_from
92 * @param act is the action to consider exploring a reordering.
93 * @return tells whether we have to explore a reordering.
96 bool ModelAction::is_synchronizing(const ModelAction *act) const
98 //Same thread can't be reordered
102 // Different locations commute
106 // Explore interleavings of seqcst writes to guarantee total order
107 // of seq_cst operations that don't commute
108 if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
111 // Explore synchronizing read/write pairs
112 if (is_read() && is_acquire() && act->is_write() && act->is_release())
114 if (is_write() && is_release() && act->is_read() && act->is_acquire())
117 // Otherwise handle by reads_from relation
121 void ModelAction::create_cv(const ModelAction *parent)
126 cv = new ClockVector(parent->cv, this);
128 cv = new ClockVector(NULL, this);
131 void ModelAction::read_from(const ModelAction *act)
134 if (act->is_release() && this->is_acquire())
141 * Check whether 'this' happens before act, according to the memory-model's
142 * happens before relation. This is checked via the ClockVector constructs.
143 * @return true if this action's thread has synchronized with act's thread
144 * since the execution of act, false otherwise.
146 bool ModelAction::happens_before(const ModelAction *act) const
148 return act->cv->synchronized_since(this);
151 void ModelAction::print(void) const
153 const char *type_str;
154 switch (this->type) {
156 type_str = "thread create";
159 type_str = "thread start";
162 type_str = "thread yield";
165 type_str = "thread join";
168 type_str = "atomic read";
171 type_str = "atomic write";
174 type_str = "atomic rmw";
177 type_str = "init atomic";
180 type_str = "unknown type";
183 printf("(%3d) Thread: %-2d Action: %-13s MO: %d Loc: %14p Value: %-4d",
184 seq_number, id_to_int(tid), type_str, order, location, value);
186 printf(" Rf: %d", reads_from->get_seq_number());