X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=c5d85a42f8010f55e47105802ef71e72083bd810;hb=74d93da009212a1d375b4fd5baede4dde82f3115;hp=dfc8e36c2be5e775ec82dab1e81a8adcfdaa2697;hpb=38b76fe373e538f275cb3a864a6e919664dc9bda;p=model-checker.git

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: