delete cv;
}
-bool ModelAction::is_read()
+bool ModelAction::is_read() const
{
return type == ATOMIC_READ;
}
-bool ModelAction::is_write()
+bool ModelAction::is_write() const
{
return type == ATOMIC_WRITE;
}
-bool ModelAction::is_rmw()
+bool ModelAction::is_rmw() const
{
return type == ATOMIC_RMW;
}
-bool ModelAction::is_acquire()
+bool ModelAction::is_acquire() const
{
switch (order) {
case memory_order_acquire:
}
}
-bool ModelAction::is_release()
+bool ModelAction::is_release() const
{
switch (order) {
case memory_order_release:
}
}
-bool ModelAction::is_seqcst()
+bool ModelAction::is_seqcst() const
{
return order==memory_order_seq_cst;
}
-bool ModelAction::same_var(ModelAction *act)
+bool ModelAction::same_var(const ModelAction *act) const
{
return location == act->location;
}
-bool ModelAction::same_thread(ModelAction *act)
+bool ModelAction::same_thread(const ModelAction *act) const
{
return tid == act->tid;
}
* @return tells whether we have to explore a reordering.
*/
-bool ModelAction::is_synchronizing(ModelAction *act)
+bool ModelAction::is_synchronizing(const ModelAction *act) const
{
//Same thread can't be reordered
if (same_thread(act))
value = act->value;
}
-void ModelAction::print(void)
+/**
+ * Check whether 'this' happens before act, according to the memory-model's
+ * happens before relation. This is checked via the ClockVector constructs.
+ * @return true if this action's thread has synchronized with act's thread
+ * since the execution of act, false otherwise.
+ */
+bool ModelAction::happens_before(ModelAction *act)
+{
+ return act->cv->synchronized_since(this);
+}
+
+void ModelAction::print(void) const
{
const char *type_str;
switch (this->type) {