From: Brian Norris <banorris@uci.edu>
Date: Tue, 19 Mar 2013 02:23:21 +0000 (-0700)
Subject: model: note how we support seq-cst fences
X-Git-Tag: oopsla2013~134
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=cfbcbb33437af392cea2a5092d89cfed47506b75

model: note how we support seq-cst fences
---

diff --git a/model.cc b/model.cc
index d9ff365..3ed2fb2 100644
--- a/model.cc
+++ b/model.cc
@@ -1128,6 +1128,7 @@ bool ModelChecker::process_fence(ModelAction *curr)
 	 *   use in later synchronization
 	 * fence-acquire (this function): search for hypothetical release
 	 *   sequences
+	 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
 	 */
 	bool updated = false;
 	if (curr->is_acquire()) {