From 10536d9feee27d20b8022ff4fde8000a2cbb3a38 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 5 Oct 2012 00:07:10 -0700
Subject: [PATCH] model: add process_relseq_fixup()

This performs the bulk of the release sequence finalization step.
---
 model.cc | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 model.h  |  1 +
 2 files changed, 60 insertions(+)

diff --git a/model.cc b/model.cc
index e46a18cb..c5e41ab7 100644
--- a/model.cc
+++ b/model.cc
@@ -544,6 +544,62 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 	return updated;
 }
 
+/**
+ * @brief Process the current action for release sequence fixup activity
+ *
+ * Performs model-checker release sequence fixups for the current action,
+ * forcing a single pending release sequence to break (with a given, potential
+ * "loose" write) or to complete (i.e., synchronize). If a pending release
+ * sequence forms a complete release sequence, then we must perform the fixup
+ * synchronization, mo_graph additions, etc.
+ *
+ * @param curr The current action; must be a release sequence fixup action
+ * @param work_queue The work queue to which to add work items as they are
+ * generated
+ */
+void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
+{
+	const ModelAction *write = curr->get_node()->get_relseq_break();
+	struct release_seq *sequence = pending_rel_seqs->back();
+	pending_rel_seqs->pop_back();
+	ASSERT(sequence);
+	ModelAction *acquire = sequence->acquire;
+	const ModelAction *rf = sequence->rf;
+	const ModelAction *release = sequence->release;
+	ASSERT(acquire);
+	ASSERT(release);
+	ASSERT(rf);
+	ASSERT(release->same_thread(rf));
+
+	if (write == NULL) {
+		/* Must synchronize */
+		if (!acquire->synchronize_with(release)) {
+			set_bad_synchronization();
+			return;
+		}
+		/* Re-check all pending release sequences */
+		work_queue->push_back(CheckRelSeqWorkEntry(NULL));
+		/* Re-check act for mo_graph edges */
+		work_queue->push_back(MOEdgeWorkEntry(acquire));
+
+		/* propagate synchronization to later actions */
+		action_list_t::reverse_iterator rit = action_trace->rbegin();
+		for (; (*rit) != acquire; rit++) {
+			ModelAction *propagate = *rit;
+			if (acquire->happens_before(propagate)) {
+				propagate->synchronize_with(acquire);
+				/* Re-check 'propagate' for mo_graph edges */
+				work_queue->push_back(MOEdgeWorkEntry(propagate));
+			}
+		}
+	} else {
+		/* Break release sequence with new edges:
+		 *   release --mo--> write --mo--> rf */
+		mo_graph->addEdge(release, write);
+		mo_graph->addEdge(write, rf);
+	}
+}
+
 /**
  * Initialize the current action by performing one or more of the following
  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
@@ -684,6 +740,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			if (act->is_mutex_op() && process_mutex(act))
 				update_all = true;
 
+			if (act->is_relseq_fixup())
+				process_relseq_fixup(curr, &work_queue);
+
 			if (update_all)
 				work_queue.push_back(CheckRelSeqWorkEntry(NULL));
 			else if (update)
diff --git a/model.h b/model.h
index a8268cf8..4032ef12 100644
--- a/model.h
+++ b/model.h
@@ -140,6 +140,7 @@ private:
 	bool process_write(ModelAction *curr);
 	bool process_mutex(ModelAction *curr);
 	bool process_thread_action(ModelAction *curr);
+	void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);
 	bool check_action_enabled(ModelAction *curr);
 
 	bool take_step();
-- 
2.34.1