From 74d93da009212a1d375b4fd5baede4dde82f3115 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 4 Oct 2012 11:15:39 -0700 Subject: [PATCH] model: add release_seq structure definition --- model.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/model.h b/model.h index dfc8e36..c5d85a4 100644 --- a/model.h +++ b/model.h @@ -55,6 +55,19 @@ struct model_snapshot_members { ModelAction *next_backtrack; }; +/** @brief Records information regarding a single pending release sequence */ +struct release_seq { + /** @brief The acquire operation */ + ModelAction *acquire; + /** @brief The head of the RMW chain from which 'acquire' reads; may be + * equal to 'release' */ + const ModelAction *rf; + /** @brief The head of the potential longest release sequence chain */ + const ModelAction *release; + /** @brief The write(s) that may break the release sequence */ + std::vector writes; +}; + /** @brief The central structure for model-checking */ class ModelChecker { public: -- 2.34.1