From 88fb5522811e0bd481ad3e60b70fe40fbc9c3e0f Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Fri, 18 Jul 2014 14:59:59 -0700
Subject: [PATCH] SC Reads can read from things mo'd before the last sc write,
 they just can't happen before it

---
 execution.cc | 24 ++++++++++++++++++------
 execution.h  |  1 +
 2 files changed, 19 insertions(+), 6 deletions(-)

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
diff --git a/execution.h b/execution.h
index 2ca2513..3635657 100644
--- a/execution.h
+++ b/execution.h
@@ -132,6 +132,7 @@ private:
 	bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
 	bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
 	void set_bad_synchronization();
+	void set_bad_sc_read();
 	bool promises_expired() const;
 	bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
 	void wake_up_sleeping_actions(ModelAction *curr);
-- 
2.34.1