From 1af30302f46d984b38a02a3f21ec53a5a9de0f71 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 4 Oct 2012 22:38:37 -0700 Subject: [PATCH 1/1] action: add MODEL_FIXUP_RELSEQ action_type This type will be used as a special model-checker action for fixing up release sequences. Each action corresponds to "finalizing" one release sequence: either force a particular write to break the sequence or else allow the synchronization to occur. Currently, this action_type won't do anything, as it's not hooked up in ModelChecker. --- action.cc | 8 ++++++++ action.h | 3 +++ 2 files changed, 11 insertions(+) diff --git a/action.cc b/action.cc index b4f4e43..c12165b 100644 --- a/action.cc +++ b/action.cc @@ -50,6 +50,11 @@ void ModelAction::set_seq_number(modelclock_t num) seq_number = num; } +bool ModelAction::is_relseq_fixup() const +{ + return type == MODEL_FIXUP_RELSEQ; +} + bool ModelAction::is_mutex_op() const { return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK; @@ -305,6 +310,9 @@ void ModelAction::print() const { const char *type_str, *mo_str; switch (this->type) { + case MODEL_FIXUP_RELSEQ: + type_str = "relseq fixup"; + break; case THREAD_CREATE: type_str = "thread create"; break; diff --git a/action.h b/action.h index 96ea6fa..dfe2102 100644 --- a/action.h +++ b/action.h @@ -37,6 +37,8 @@ using std::memory_order_seq_cst; /** @brief Represents an action type, identifying one of several types of * ModelAction */ typedef enum action_type { + MODEL_FIXUP_RELSEQ, /**< Special ModelAction: finalize a release + * sequence */ THREAD_CREATE, /**< A thread creation action */ THREAD_START, /**< First action in each thread */ THREAD_YIELD, /**< A thread yield action */ @@ -82,6 +84,7 @@ public: void copy_from_new(ModelAction *newaction); void set_seq_number(modelclock_t num); void set_try_lock(bool obtainedlock); + bool is_relseq_fixup() const; bool is_mutex_op() const; bool is_lock() const; bool is_trylock() const; -- 2.34.1