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.