From 3323cca9507640ddc9e38cf93c2e737ca2df9fd7 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 27 Sep 2012 10:53:59 -0700 Subject: [PATCH] model: push mo_graph cycle check into release_seq code Release sequences traveral should only be undertaken if the mo_graph has no cycles. Instead of just making this check a hack within resolve_promises(), make it part of every release sequence exploration. --- model.cc | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/model.cc b/model.cc index fd906858..cf58e9c0 100644 --- a/model.cc +++ b/model.cc @@ -1111,6 +1111,10 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con */ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const { + /* Only check for release sequences if there are no cycles */ + if (mo_graph->checkForCycles()) + return false; + while (rf) { ASSERT(rf->is_write()); @@ -1419,12 +1423,7 @@ bool ModelChecker::resolve_promises(ModelAction *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); - + read->read_from(write); //First fix up the modification order for actions that happened //before the read r_modification_order(read, write); -- 2.34.1