model: add write-to-promise edges

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 6739d2c85ee2ca51dd3963c471c811e12f0711b3..691ab832519d11dff2515dfe313884da05ef7382 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1808,6 +1808,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                }
        }
 
+       /*
+        * All compatible, thread-exclusive promises must be ordered after any
+        * concrete stores to the same thread, or else they can be merged with
+        * this store later
+        */
+       for (unsigned int i = 0; i < promises->size(); i++)
+               if ((*promises)[i]->is_compatible_exclusive(curr))
+                       added = mo_graph->addEdge(curr, (*promises)[i]) || added;
+
        return added;
 }