From: Brian Norris <banorris@uci.edu>
Date: Tue, 25 Sep 2012 23:29:14 +0000 (-0700)
Subject: action: return synchronization status for ModelAction::read_from()
X-Git-Tag: pldi2013~107^2~1
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=5ead9124f62d38a96f606ddbcfc8a62c8d5f8335

action: return synchronization status for ModelAction::read_from()

The ModelChecker may need to know if any synchronization was performed in
read_from().

Note that the return status is not used yet.
---

diff --git a/action.cc b/action.cc
index 08fe106..20777f9 100644
--- a/action.cc
+++ b/action.cc
@@ -249,18 +249,27 @@ void ModelAction::set_try_lock(bool obtainedlock) {
 		value=VALUE_TRYFAILED;
 }
 
-/** Update the model action's read_from action */
-void ModelAction::read_from(const ModelAction *act)
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ * @return True if this read established synchronization
+ */
+bool ModelAction::read_from(const ModelAction *act)
 {
 	ASSERT(cv);
 	reads_from = act;
 	if (act != NULL && this->is_acquire()) {
 		rel_heads_list_t release_heads;
 		model->get_release_seq_heads(this, &release_heads);
+		int num_heads = release_heads.size();
 		for (unsigned int i = 0; i < release_heads.size(); i++)
-			if (!synchronize_with(release_heads[i]))
+			if (!synchronize_with(release_heads[i])) {
 				model->set_bad_synchronization();
+				num_heads--;
+			}
+		return num_heads > 0;
 	}
+	return false;
 }
 
 /**
diff --git a/action.h b/action.h
index 32cada2..d178976 100644
--- a/action.h
+++ b/action.h
@@ -105,7 +105,7 @@ public:
 
 	void create_cv(const ModelAction *parent = NULL);
 	ClockVector * get_cv() const { return cv; }
-	void read_from(const ModelAction *act);
+	bool read_from(const ModelAction *act);
 	bool synchronize_with(const ModelAction *act);
 
 	bool has_synchronized_with(const ModelAction *act) const;