From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 5 Oct 2012 02:44:14 +0000 (-0700)
Subject: 1) more comments
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=80ab61e4168b993a319788c70fd41e63a34ba627

1) more comments
2) rename is_synchronizing with
3) realize that reordering is only necessary if we create a synchronization...not needed to break one...
---

diff --git a/action.cc b/action.cc
index c6504cd3..b4f4e434 100644
--- a/action.cc
+++ b/action.cc
@@ -184,7 +184,7 @@ void ModelAction::process_rmw(ModelAction * act) {
  *  @param act is the action to consider exploring a reordering.
  *  @return tells whether we have to explore a reordering.
  */
-bool ModelAction::is_synchronizing(const ModelAction *act) const
+bool ModelAction::could_synchronize_with(const ModelAction *act) const
 {
 	//Same thread can't be reordered
 	if (same_thread(act))
@@ -196,14 +196,12 @@ bool ModelAction::is_synchronizing(const ModelAction *act) const
 
 	// Explore interleavings of seqcst writes to guarantee total order
 	// of seq_cst operations that don't commute
-	if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
+	if ((is_write() || act->is_write()) && is_seqcst() && act->is_seqcst())
 		return true;
 
 	// Explore synchronizing read/write pairs
 	if (is_read() && is_acquire() && act->is_write() && act->is_release())
 		return true;
-	if (is_write() && is_release() && act->is_read() && act->is_acquire())
-		return true;
 
 	// Otherwise handle by reads_from relation
 	return false;
diff --git a/action.h b/action.h
index d178976a..96ea6fa9 100644
--- a/action.h
+++ b/action.h
@@ -101,7 +101,7 @@ public:
 	bool same_var(const ModelAction *act) const;
 	bool same_thread(const ModelAction *act) const;
 	bool is_conflicting_lock(const ModelAction *act) const;
-	bool is_synchronizing(const ModelAction *act) const;
+	bool could_synchronize_with(const ModelAction *act) const;
 
 	void create_cv(const ModelAction *parent = NULL);
 	ClockVector * get_cv() const { return cv; }
diff --git a/model.cc b/model.cc
index bcc4298b..c3f63725 100644
--- a/model.cc
+++ b/model.cc
@@ -236,7 +236,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
-			if (act->is_synchronizing(prev))
+			if (prev->could_synchronize_with(act))
 				return prev;
 		}
 		break;
@@ -1114,7 +1114,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				}
 				added = true;
 				break;
-			} else if (act->is_read() && !act->is_synchronizing(curr) &&
+			} else if (act->is_read() && !act->could_synchronize_with(curr) &&
 			                             !act->same_thread(curr)) {
 				/* We have an action that:
 				   (1) did not happen before us
@@ -1562,7 +1562,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
 		const ModelAction *act = promise->get_action();
 		if (!act->happens_before(curr) &&
 				act->is_read() &&
-				!act->is_synchronizing(curr) &&
+				!act->could_synchronize_with(curr) &&
 				!act->same_thread(curr) &&
 				promise->get_value() == curr->get_value()) {
 			curr->get_node()->set_promise(i);