From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Dec 2012 02:14:55 +0000 (-0800)
Subject: model/action: move complicated read_from logic into model.cc
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=39c0de028fe3b1c1d229ecf715007c751ddab445

model/action: move complicated read_from logic into model.cc

The release sequence wrapper logic will only get more complicated, so
rather than spreading across two files and exporting more interfaces,
just integrate into ModelChecker.
---

diff --git a/action.cc b/action.cc
index 5ecc1f0e..41a025ab 100644
--- a/action.cc
+++ b/action.cc
@@ -337,24 +337,10 @@ void ModelAction::set_try_lock(bool obtainedlock) {
 /**
  * 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)
+void ModelAction::set_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])) {
-				model->set_bad_synchronization();
-				num_heads--;
-			}
-		return num_heads > 0;
-	}
-	return false;
 }
 
 /**
diff --git a/action.h b/action.h
index 4c40bd9b..82b8532d 100644
--- a/action.h
+++ b/action.h
@@ -85,6 +85,8 @@ public:
 	Node * get_node() const { return node; }
 	void set_node(Node *n) { node = n; }
 
+	void set_read_from(const ModelAction *act);
+
 	/** Store the most recent fence-release from the same thread
 	 *  @param fence The fence-release that occured prior to this */
 	void set_last_fence_release(const ModelAction *fence) { last_fence_release = fence; }
@@ -123,7 +125,6 @@ public:
 
 	void create_cv(const ModelAction *parent = NULL);
 	ClockVector * get_cv() const { return cv; }
-	bool read_from(const ModelAction *act);
 	bool synchronize_with(const ModelAction *act);
 
 	bool has_synchronized_with(const ModelAction *act) const;
diff --git a/model.cc b/model.cc
index f96249fc..2f9ec63f 100644
--- a/model.cc
+++ b/model.cc
@@ -705,7 +705,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 				continue;
 			}
 
-			curr->read_from(reads_from);
+			read_from(curr, reads_from);
 			mo_graph->commitChanges();
 			mo_check_promises(curr->get_tid(), reads_from);
 
@@ -714,7 +714,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			/* Read from future value */
 			value = curr->get_node()->get_future_value();
 			modelclock_t expiration = curr->get_node()->get_future_value_expiration();
-			curr->read_from(NULL);
+			read_from(curr, NULL);
 			Promise *valuepromise = new Promise(curr, value, expiration);
 			promises->push_back(valuepromise);
 		}
@@ -1047,6 +1047,34 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
 	}
 }
 
+/**
+ * @brief Establish reads-from relation between two actions
+ *
+ * Perform basic operations involved with establishing a concrete rf relation,
+ * including setting the ModelAction data and checking for release sequences.
+ *
+ * @param act The action that is reading (must be a read)
+ * @param rf The action from which we are reading (must be a write)
+ *
+ * @return True if this read established synchronization
+ */
+bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
+{
+	act->set_read_from(rf);
+	if (rf != NULL && act->is_acquire()) {
+		rel_heads_list_t release_heads;
+		get_release_seq_heads(act, &release_heads);
+		int num_heads = release_heads.size();
+		for (unsigned int i = 0; i < release_heads.size(); i++)
+			if (!act->synchronize_with(release_heads[i])) {
+				set_bad_synchronization();
+				num_heads--;
+			}
+		return num_heads > 0;
+	}
+	return false;
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -2154,7 +2182,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			if (read->is_rmw()) {
 				mo_graph->addRMWEdge(write, read);
 			}
-			read->read_from(write);
+			read_from(read, write);
 			//First fix up the modification order for actions that happened
 			//before the read
 			r_modification_order(read, write);
diff --git a/model.h b/model.h
index fd99700a..6bb4788c 100644
--- a/model.h
+++ b/model.h
@@ -153,6 +153,7 @@ private:
 	bool process_mutex(ModelAction *curr);
 	bool process_thread_action(ModelAction *curr);
 	void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);
+	bool read_from(ModelAction *act, const ModelAction *rf);
 	bool check_action_enabled(ModelAction *curr);
 
 	bool take_step();