From ec01a46ce69f58f219b59a4148bc833cd5aa07c6 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 25 Sep 2012 19:23:51 -0700 Subject: [PATCH] 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 | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index fdefcc2..ea7b657 100644 --- 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(); - read->read_from(write); 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); + promises->erase(promises->begin() + promise_index); resolved = true; } else -- 2.34.1