+
+ // Explore synchronizing read/write pairs
+ if (is_read() && is_acquire() && act->is_write() && act->is_release())
+ return true;
+ if (is_write() && is_release() && act->is_read() && act->is_acquire())
+ return true;
+
+ // Otherwise handle by reads_from relation
+ return false;
+}
+
+bool ModelAction::is_conflicting_lock(const ModelAction *act) const
+{
+ //Must be different threads to reorder
+ if (same_thread(act))
+ return false;
+
+ //Try to reorder a lock past a successful lock
+ if (act->is_success_lock())
+ return true;
+
+ //Try to push a successful trylock past an unlock
+ if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
+ return true;
+
+ return false;
+}
+
+/**
+ * Create a new clock vector for this action. Note that this function allows a
+ * user to clobber (and leak) a ModelAction's existing clock vector. A user
+ * should ensure that the vector has already either been rolled back
+ * (effectively "freed") or freed.
+ *
+ * @param parent A ModelAction from which to inherit a ClockVector
+ */
+void ModelAction::create_cv(const ModelAction *parent)
+{
+ if (parent)
+ cv = new ClockVector(parent->cv, this);
+ else
+ cv = new ClockVector(NULL, this);
+}
+
+void ModelAction::set_try_lock(bool obtainedlock) {
+ if (obtainedlock)
+ value=VALUE_TRYSUCCESS;
+ else
+ value=VALUE_TRYFAILED;
+}
+
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ * @return True if this read established synchronization
+ */
+bool ModelAction::read_from(const ModelAction *act)
+{
+ ASSERT(cv);
+ reads_from = act;
+ if (act != NULL && this->is_acquire()) {
+ rel_heads_list_t release_heads;
+ model->get_release_seq_heads(this, &release_heads);
+ int num_heads = release_heads.size();
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ if (!synchronize_with(release_heads[i])) {
+ model->set_bad_synchronization();
+ num_heads--;
+ }
+ return num_heads > 0;
+ }