From: Brian Norris Date: Tue, 6 Nov 2012 00:00:18 +0000 (-0800) Subject: model: refactor build_reads_from_past X-Git-Tag: oopsla2013~539^2^2~16 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=da5263cb595ee0440b27a757f3293715c3e7371a;p=model-checker.git model: refactor build_reads_from_past A couple of if-else conditions can be merged to a single if block. Also, I move the DBG prints for the may_read_from set into the correct part of the if, to avoid printing false messages about the may_read_from set. --- diff --git a/model.cc b/model.cc index 9dcc06c..94620ea 100644 --- a/model.cc +++ b/model.cc @@ -2022,17 +2022,14 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) /* Don't consider more than one seq_cst write if we are a seq_cst read. */ if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } - - if (curr->get_sleep_flag() && ! curr->is_seqcst()) { - if (sleep_can_read_from(curr, act)) - curr->get_node()->add_read_from(act); - } else + 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); + } } /* Include at most one act per-thread that "happens before" curr */