/** This method changes an existing read part of an RMW action into either:
* (1) a full RMW action in case of the completed write or
* (2) a READ action in case a failed action.
+ * @todo If the memory_order changes, we may potentially need to update our
+ * clock vector.
*/
-
-//TODO: If the memory_order changes, we may potentially need to update our
-//clock vector.
-
void ModelAction::process_rmw(ModelAction * act) {
this->order=act->order;
if (act->is_rmwc())
* @param act is the action to consider exploring a reordering.
* @return tells whether we have to explore a reordering.
*/
-
bool ModelAction::is_synchronizing(const ModelAction *act) const
{
//Same thread can't be reordered
void ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
- if (act->is_release() && this->is_acquire())
+ if (act->is_release() && this->is_acquire()) {
+ synchronized(act);
cv->merge(act->cv);
+ }
reads_from = act;
}
+
+/** Synchronize the current thread with the thread corresponding to
+ * the ModelAction parameter. */
+
+void ModelAction::synchronized(const ModelAction *act) {
+ model->check_promises(cv, act->cv);
+ cv->merge(act->cv);
+}
+
/**
* Check whether 'this' happens before act, according to the memory-model's
* happens before relation. This is checked via the ClockVector constructs.