From: Brian Norris <banorris@uci.edu>
Date: Mon, 8 Oct 2012 06:24:21 +0000 (-0700)
Subject: model: add todo synchronization comment
X-Git-Tag: pldi2013~97^2~1^2
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=9b894e117ad1090ad6f54753cde7fd9b6ea60ab7

model: add todo synchronization comment
---

diff --git a/model.cc b/model.cc
index e23e9ec..8267377 100644
--- a/model.cc
+++ b/model.cc
@@ -576,6 +576,16 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 	ASSERT(release->same_thread(rf));
 
 	if (write == NULL) {
+		/**
+		 * @todo Forcing a synchronization requires that we set
+		 * modification order constraints. For instance, we can't allow
+		 * a fixup sequence in which two separate read-acquire
+		 * operations read from the same sequence, where the first one
+		 * synchronizes and the other doesn't. Essentially, we can't
+		 * allow any writes to insert themselves between 'release' and
+		 * 'rf'
+		 */
+
 		/* Must synchronize */
 		if (!acquire->synchronize_with(release)) {
 			set_bad_synchronization();