model: avoid infinite loop in release_seq_head()
authorBrian Norris <banorris@uci.edu>
Wed, 26 Sep 2012 02:23:51 +0000 (19:23 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 26 Sep 2012 19:30:44 +0000 (12:30 -0700)
commitec01a46ce69f58f219b59a4148bc833cd5aa07c6
tree511106cac866fc1c64cbce68c6f52884848172c3
parent53a4f1f5edbe67d4cb5c47c1faa687deccc04610
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.
model.cc