+ reads_from = act;
+ if (act != NULL && this->is_acquire()) {
+ std::vector<const ModelAction *> release_heads;
+ model->get_release_seq_heads(this, &release_heads);
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ synchronize_with(release_heads[i]);
+ }
+}
+
+/**
+ * Synchronize the current thread with the thread corresponding to the
+ * ModelAction parameter.
+ * @param act The ModelAction to synchronize with
+ */
+void ModelAction::synchronize_with(const ModelAction *act) {
+ ASSERT(*act < *this);
+ model->check_promises(cv, act->cv);
+ cv->merge(act->cv);
+}
+
+bool ModelAction::has_synchronized_with(const ModelAction *act) const
+{
+ return cv->has_synchronized_with(act->cv);
+}
+
+/**
+ * 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(const ModelAction *act) const
+{
+ return act->cv->synchronized_since(this);