From 43144df37c0f1bb5b4efc4cf1bd2908b6cf440b9 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 3 Dec 2012 13:05:55 -0800 Subject: [PATCH 1/1] model: refactor build_reads_from_past Just rearrange the logic a little, to prepare for some other additions. --- model.cc | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/model.cc b/model.cc index fc86d5c7..d6ebfe5a 100644 --- a/model.cc +++ b/model.cc @@ -2289,15 +2289,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) continue; /* Don't consider more than one seq_cst write if we are a seq_cst read. */ - if (!curr->is_seqcst() || (!act->is_seqcst() && (last_sc_write == NULL || !act->happens_before(last_sc_write))) || act == last_sc_write) { - if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } - curr->get_node()->add_read_from(act); + bool allow_read = true; + + if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write) + allow_read = false; + else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act)) + allow_read = false; + + if (allow_read) { + DEBUG("Adding action to may_read_from:\n"); + if (DBG_ENABLED()) { + act->print(); + curr->print(); } + curr->get_node()->add_read_from(act); } /* Include at most one act per-thread that "happens before" curr */ -- 2.34.1