5 #include "clockvector.h"
8 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
10 Thread *t = thread_current();
11 ModelAction *act = this;
16 act->tid = t->get_id();
18 act->seq_number = model->get_next_seq_num();
23 ModelAction::~ModelAction()
29 bool ModelAction::is_read() const
31 return type == ATOMIC_READ;
34 bool ModelAction::is_write() const
36 return type == ATOMIC_WRITE;
39 bool ModelAction::is_rmw() const
41 return type == ATOMIC_RMW;
44 bool ModelAction::is_acquire() const
47 case memory_order_acquire:
48 case memory_order_acq_rel:
49 case memory_order_seq_cst:
56 bool ModelAction::is_release() const
59 case memory_order_release:
60 case memory_order_acq_rel:
61 case memory_order_seq_cst:
68 bool ModelAction::is_seqcst() const
70 return order==memory_order_seq_cst;
73 bool ModelAction::same_var(const ModelAction *act) const
75 return location == act->location;
78 bool ModelAction::same_thread(const ModelAction *act) const
80 return tid == act->tid;
83 /** The is_synchronizing method should only explore interleavings if:
84 * (1) the operations are seq_cst and don't commute or
85 * (2) the reordering may establish or break a synchronization relation.
86 * Other memory operations will be dealt with by using the reads_from
89 * @param act is the action to consider exploring a reordering.
90 * @return tells whether we have to explore a reordering.
93 bool ModelAction::is_synchronizing(const ModelAction *act) const
95 //Same thread can't be reordered
99 // Different locations commute
103 // Explore interleavings of seqcst writes to guarantee total order
104 // of seq_cst operations that don't commute
105 if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
108 // Explore synchronizing read/write pairs
109 if (is_read() && is_acquire() && act->is_write() && act->is_release())
111 if (is_write() && is_release() && act->is_read() && act->is_acquire())
114 // Otherwise handle by reads_from relation
118 void ModelAction::create_cv(ModelAction *parent)
123 cv = new ClockVector(parent->cv, this);
125 cv = new ClockVector(NULL, this);
128 void ModelAction::read_from(ModelAction *act)
131 if (act->is_release() && this->is_acquire())
137 * Check whether 'this' happens before act, according to the memory-model's
138 * happens before relation. This is checked via the ClockVector constructs.
139 * @return true if this action's thread has synchronized with act's thread
140 * since the execution of act, false otherwise.
142 bool ModelAction::happens_before(ModelAction *act)
144 return act->cv->synchronized_since(this);
147 void ModelAction::print(void)
149 const char *type_str;
150 switch (this->type) {
152 type_str = "thread create";
155 type_str = "thread yield";
158 type_str = "thread join";
161 type_str = "atomic read";
164 type_str = "atomic write";
167 type_str = "atomic rmw";
170 type_str = "unknown type";
173 printf("(%3d) Thread: %-2d Action: %-13s MO: %d Loc: %14p Value: %d",
174 seq_number, id_to_int(tid), type_str, order, location, value);