X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=9d2dbb61ef577c43421f6ab071fe5fc7c9323004;hb=939c3e18d1214e60cfc680244f8ab3e9bd5404af;hp=1711e1a002b6d105cb413efec6c20e644f51f0f8;hpb=9c02def96200170715f28557ba36ab94b4f956a6;p=c11tester.git

diff --git a/model.cc b/model.cc
index 1711e1a0..9d2dbb61 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. */