From 90342c146c207107ec0bf05cb70b2d7defbeaa3e Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 5 Feb 2013 14:10:06 -0800 Subject: [PATCH] model: add write-to-promise edges Assume that any time a promise exists, is compatible with a store, and is exclusive to the same thread as the store, that it is mod-ordered after that store. This should never produce cycles, until we decide to begin satisfying promises. At that point, if there's a cycle, then we must either merge nodes (i.e., the store must satisfy that promise) or else we discard the execution for the moment and perform the satisfaction at a later point in the search space. --- model.cc | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/model.cc b/model.cc index 6739d2c8..691ab832 100644 --- 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; } -- 2.34.1