model: add release_seq structure definition

diff --git a/model.h b/model.h
index dfc8e36c2be5e775ec82dab1e81a8adcfdaa2697..c5d85a42f8010f55e47105802ef71e72083bd810 100644 (file)
--- a/model.h
+++ b/model.h
@@ -55,6 +55,19 @@ struct model_snapshot_members {
        ModelAction *next_backtrack;
 };
 
        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<const ModelAction *> writes;
+};
+

 /** @brief The central structure for model-checking */
 class ModelChecker {
 public:
 /** @brief The central structure for model-checking */
 class ModelChecker {
 public: