From: Brian Norris <banorris@uci.edu>
Date: Thu, 4 Oct 2012 18:15:39 +0000 (-0700)
Subject: model: add release_seq structure definition
X-Git-Tag: pldi2013~102^2~4
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=74d93da009212a1d375b4fd5baede4dde82f3115;hp=38b76fe373e538f275cb3a864a6e919664dc9bda

model: add release_seq structure definition
---

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<const ModelAction *> writes;
+};
+
 /** @brief The central structure for model-checking */
 class ModelChecker {
 public: