+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;
+
+ // Try to push a successful trylock past a wait
+ if (act->is_wait() && 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)
+{
+ value = obtainedlock ? VALUE_TRYSUCCESS : VALUE_TRYFAILED;
+}
+
+/**
+ * @brief Get the value read by this load
+ *
+ * We differentiate this function from ModelAction::get_write_value and
+ * ModelAction::get_value for the purpose of RMW's, which may have both a
+ * 'read' and a 'write' value.
+ *
+ * Note: 'this' must be a load.
+ *
+ * @return The value read by this load
+ */
+uint64_t ModelAction::get_reads_from_value() const
+{
+ ASSERT(is_read());
+ if (reads_from)
+ return reads_from->get_write_value();
+ else if (reads_from_promise)
+ return reads_from_promise->get_value();
+ return VALUE_NONE; /* Only for new actions with no reads-from */
+}
+
+/**
+ * @brief Get the value written by this store
+ *
+ * We differentiate this function from ModelAction::get_reads_from_value and
+ * ModelAction::get_value for the purpose of RMW's, which may have both a
+ * 'read' and a 'write' value.
+ *
+ * Note: 'this' must be a store.
+ *
+ * @return The value written by this store
+ */
+uint64_t ModelAction::get_write_value() const
+{
+ ASSERT(is_write());
+ return value;
+}
+
+/**
+ * @brief Get the value returned by this action
+ *
+ * For atomic reads (including RMW), an operation returns the value it read.
+ * For atomic writes, an operation returns the value it wrote. For other
+ * operations, the return value varies (sometimes is a "don't care"), but the
+ * value is simply stored in the "value" field.
+ *
+ * @return This action's return value
+ */
+uint64_t ModelAction::get_return_value() const
+{
+ if (is_read())
+ return get_reads_from_value();
+ else if (is_write())
+ return get_write_value();
+ else
+ return value;
+}
+
+/** @return The Node associated with this ModelAction */
+Node * ModelAction::get_node() const
+{
+ /* UNINIT actions do not have a Node */
+ ASSERT(!is_uninitialized());
+ return node;
+}
+
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ */
+void ModelAction::set_read_from(const ModelAction *act)
+{
+ ASSERT(act);
+ reads_from = act;
+ reads_from_promise = NULL;
+ if (act->is_uninitialized())
+ model->assert_bug("May read from uninitialized atomic:\n"
+ " action %d, thread %d, location %p (%s, %s)",
+ seq_number, id_to_int(tid), location,
+ get_type_str(), get_mo_str());
+}
+
+/**
+ * Set this action's read-from promise
+ * @param promise The promise to read from
+ */
+void ModelAction::set_read_from_promise(Promise *promise)
+{
+ ASSERT(is_read());
+ reads_from_promise = promise;
+ reads_from = NULL;
+}
+
+/**
+ * Synchronize the current thread with the thread corresponding to the
+ * ModelAction parameter.
+ * @param act The ModelAction to synchronize with
+ * @return True if this is a valid synchronization; false otherwise
+ */
+bool ModelAction::synchronize_with(const ModelAction *act)
+{
+ if (*this < *act)
+ return false;
+ cv->merge(act->cv);
+ return true;
+}
+
+bool ModelAction::has_synchronized_with(const ModelAction *act) const
+{
+ return cv->synchronized_since(act);
+}
+
+/**
+ * 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);
+}
+
+const char * ModelAction::get_type_str() const