From: Brian Norris <banorris@uci.edu>
Date: Fri, 14 Sep 2012 20:11:08 +0000 (-0700)
Subject: model: add some mo_graph fixup code to work_queue
X-Git-Tag: pldi2013~177^2^2~11
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=942ca53513b4c50f3f73bc4b123c3552dbc71ca6

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.
---

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;