model: add read-write coherence for promise nodes
authorBrian Norris <banorris@uci.edu>
Thu, 7 Feb 2013 00:39:52 +0000 (16:39 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 7 Feb 2013 00:52:30 +0000 (16:52 -0800)
Promises must be ordered after any other loads from the same thread.

model.cc

index 15718e1..3d89dc3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1619,6 +1619,14 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                }
        }
 
+       /*
+        * All compatible, thread-exclusive promises must be ordered after any
+        * concrete loads from the same thread
+        */
+       for (unsigned int i = 0; i < promises->size(); i++)
+               if ((*promises)[i]->is_compatible_exclusive(curr))
+                       added = mo_graph->addEdge(rf, (*promises)[i]) || added;
+
        return added;
 }