From 939c3e18d1214e60cfc680244f8ab3e9bd5404af Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Mon, 1 Oct 2012 13:29:00 -0700
Subject: [PATCH] model: add "bad synchronization" flag

Can be used for aborting a trace when an incorrectly-ordered
synchronization occurs.
---
 model.cc | 8 ++++++--
 model.h  | 7 +++++++
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/model.cc b/model.cc
index 1711e1a..9d2dbb6 100644
--- a/model.cc
+++ b/model.cc
@@ -38,7 +38,8 @@ ModelChecker::ModelChecker(struct model_params params) :
 	mo_graph(new CycleGraph()),
 	failed_promise(false),
 	too_many_reads(false),
-	asserted(false)
+	asserted(false),
+	bad_synchronization(false)
 {
 	/* Allocate this "size" on the snapshotting heap */
 	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -80,6 +81,7 @@ void ModelChecker::reset_to_initial_state()
 	node_stack->reset_execution();
 	failed_promise = false;
 	too_many_reads = false;
+	bad_synchronization = false;
 	reset_asserted();
 	snapshotObject->backTrackBeforeStep(0);
 }
@@ -740,10 +742,12 @@ bool ModelChecker::isfeasibleotherthanRMW() {
 			DEBUG("Infeasible: failed promise\n");
 		if (too_many_reads)
 			DEBUG("Infeasible: too many reads\n");
+		if (bad_synchronization)
+			DEBUG("Infeasible: bad synchronization ordering\n");
 		if (promises_expired())
 			DEBUG("Infeasible: promises expired\n");
 	}
-	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
+	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
diff --git a/model.h b/model.h
index 4a1fcf4..4b9e3ff 100644
--- a/model.h
+++ b/model.h
@@ -91,6 +91,11 @@ public:
 	void finish_execution();
 	bool isfeasibleprefix();
 	void set_assert() {asserted=true;}
+
+	/** @brief Alert the model-checker that an incorrectly-ordered
+	 * synchronization was made */
+	void set_bad_synchronization() { bad_synchronization = true; }
+
 	const model_params params;
 
 	MEMALLOC
@@ -196,6 +201,8 @@ private:
 	bool failed_promise;
 	bool too_many_reads;
 	bool asserted;
+	/** @brief Incorrectly-ordered synchronization was made */
+	bool bad_synchronization;
 };
 
 extern ModelChecker *model;
-- 
2.34.1