X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;h=2a7e0dadd1e0918ac21b5f43dd4e3608935b8f18;hp=01a5fa442b0905b522f05714d95dc7eaf5fa56a2;hb=88fb5522811e0bd481ad3e60b70fe40fbc9c3e0f;hpb=a2e32839cc2d45b6f8f559061ac4315acc628396

diff --git a/execution.cc b/execution.cc
index 01a5fa4..2a7e0da 100644
--- a/execution.cc
+++ b/execution.cc
@@ -34,6 +34,7 @@ struct model_snapshot_members {
 		too_many_reads(false),
 		no_valid_reads(false),
 		bad_synchronization(false),
+		bad_sc_read(false),
 		asserted(false)
 	{ }
 
@@ -53,6 +54,7 @@ struct model_snapshot_members {
 	bool no_valid_reads;
 	/** @brief Incorrectly-ordered synchronization was made */
 	bool bad_synchronization;
+	bool bad_sc_read;
 	bool asserted;
 
 	SNAPSHOTALLOC
@@ -202,6 +204,13 @@ void ModelExecution::set_bad_synchronization()
 	priv->bad_synchronization = true;
 }
 
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelExecution::set_bad_sc_read()
+{
+	priv->bad_sc_read = true;
+}
+
 bool ModelExecution::assert_bug(const char *msg)
 {
 	priv->bugs.push_back(new bug_message(msg));
@@ -1306,6 +1315,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 				if (rf) {
 					if (r_modification_order(act, rf))
 						updated = true;
+					if (act->is_seqcst()) {
+						ModelAction *last_sc_write = get_last_seq_cst_write(act);
+						if (last_sc_write != NULL && rf->happens_before(last_sc_write)) {
+							set_bad_sc_read();
+						}
+					}
 				} else if (promise) {
 					if (r_modification_order(act, promise))
 						updated = true;
@@ -1385,6 +1400,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 		ptr += sprintf(ptr, "[no valid reads-from]");
 	if (priv->bad_synchronization)
 		ptr += sprintf(ptr, "[bad sw ordering]");
+	if (priv->bad_sc_read)
+		ptr += sprintf(ptr, "[bad sc read]");
 	if (promises_expired())
 		ptr += sprintf(ptr, "[promise expired]");
 	if (promises.size() != 0)
@@ -1415,6 +1432,7 @@ bool ModelExecution::is_infeasible() const
 		priv->no_valid_reads ||
 		priv->too_many_reads ||
 		priv->bad_synchronization ||
+		priv->bad_sc_read ||
 		priv->hard_failed_promise ||
 		promises_expired();
 }
@@ -1616,12 +1634,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
 				}
 			}
 
-			/* C++, Section 29.3 statement 3 (second subpoint) */
-			if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
-				added = mo_graph->addEdge(act, rf) || added;
-				break;
-			}
-
 			/*
 			 * Include at most one act per-thread that "happens
 			 * before" curr