From 942ca53513b4c50f3f73bc4b123c3552dbc71ca6 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 14 Sep 2012 13:11:08 -0700
Subject: [PATCH] model: add some mo_graph fixup code to work_queue

The work queue has all its work items implemented now. But I haven't fully
verified that this is complete yet.
---
 model.cc | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/model.cc b/model.cc
index 9faf4e2..7f1e49d 100644
--- a/model.cc
+++ b/model.cc
@@ -447,8 +447,24 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		case WORK_CHECK_RELEASE_SEQ:
 			resolve_release_sequences(work.location, &work_queue);
 			break;
-		case WORK_CHECK_MO_EDGES:
-			/** @todo Perform follow-up mo_graph checks */
+		case WORK_CHECK_MO_EDGES: {
+			/** @todo Complete verification of work_queue */
+			ModelAction *act = work.action;
+			bool updated = false;
+
+			if (act->is_read()) {
+				if (r_modification_order(act, act->get_reads_from()))
+					updated = true;
+			}
+			if (act->is_write()) {
+				if (w_modification_order(act))
+					updated = true;
+			}
+
+			if (updated)
+				work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+			break;
+		}
 		default:
 			ASSERT(false);
 			break;
-- 
2.34.1