model: avoid infinite loop in release_seq_head()

To understand the problem I'm solving here, note that resolve_promises()
calls ModelAction::read_from() which calls ModelChecker::release_seq_head().

Now, release_seq_head() has the basic assumption that the mo_graph
doesn't have cycles (or specifically, in this case it's important that
sequences of RMW's don't form loops in the reads-from relation).
Unfortunately, resolve_promises() can create such a cycle (by assigning
the "reads-from" value) before checking if that would create a cycle.
This will trigger a check to release_seq_head, which gets stuck in an
infinite loop...

The solution, at least for this targeted portion of code, is to:
(1) First add the relevant RMW edge, if possible
(2) If (1) didn't create mo_graph cycles:
       Then assign reads-from, check release sequences, update
       synchronization
(3) Calculate other normal mo_graph edges

This way, (2) will simply be skipped if we have cycles, avoiding the
problem.

diff --git a/model.cc b/model.cc
index fdefcc2bcf390dd4a2615a411920466a8f901022..ea7b657c3f34c03b8839c3e09be7dbcc6a6ae3a7 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1413,16 +1413,22 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                Promise *promise = (*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
                        ModelAction *read = promise->get_action();
                Promise *promise = (*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
                        ModelAction *read = promise->get_action();

-                       read->read_from(write);

                        if (read->is_rmw()) {
                                mo_graph->addRMWEdge(write, read);
                        }
                        if (read->is_rmw()) {
                                mo_graph->addRMWEdge(write, read);
                        }

+
+                       /* Only read (and check for release sequences) if this
+                        * write (esp. RMW) doesn't create cycles */
+                       if (!mo_graph->checkForCycles())
+                               read->read_from(write);
+

                        //First fix up the modification order for actions that happened
                        //before the read
                        r_modification_order(read, write);
                        //Next fix up the modification order for actions that happened
                        //after the read.
                        post_r_modification_order(read, write);
                        //First fix up the modification order for actions that happened
                        //before the read
                        r_modification_order(read, write);
                        //Next fix up the modification order for actions that happened
                        //after the read.
                        post_r_modification_order(read, write);

+

                        promises->erase(promises->begin() + promise_index);
                        resolved = true;
                } else
                        promises->erase(promises->begin() + promise_index);
                        resolved = true;
                } else