From 7a0167d52294a9707f81a54d74009c6f82346d18 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 19 Nov 2012 20:33:53 -0800 Subject: [PATCH] model: rename isfinalfeasible -> is_feasible_prefix_ignore_relseq This more accurately reflects its use case and the fact that it is a slightly-weaker version of isfeasibleprefix(). Also, I integrate it into isfeasibleprefix(), to avoid re-writing the same conditions. --- model.cc | 13 ++++++++----- model.h | 2 +- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/model.cc b/model.cc index d829582..da68074 100644 --- a/model.cc +++ b/model.cc @@ -1214,14 +1214,17 @@ bool ModelChecker::promises_expired() const * This is the strongest feasibility check available. * @return whether the current trace (partial or complete) must be a prefix of * a feasible trace. - * */ + */ bool ModelChecker::isfeasibleprefix() const { - return promises->size() == 0 && pending_rel_seqs->size() == 0 && !is_infeasible(); + return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); } -/** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() const +/** + * Returns whether the current completed trace is feasible, except for pending + * release sequences. + */ +bool ModelChecker::is_feasible_prefix_ignore_relseq() const { if (DBG_ENABLED() && promises->size() != 0) DEBUG("Infeasible: unrevolved promises\n"); @@ -2498,7 +2501,7 @@ bool ModelChecker::take_step() { * (4) no pending promises */ if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) && - isfinalfeasible() && !unrealizedraces.empty()) { + is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) { model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", pending_rel_seqs->size()); ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, diff --git a/model.h b/model.h index 3f1103e..74866c6 100644 --- a/model.h +++ b/model.h @@ -243,7 +243,7 @@ private: struct execution_stats stats; void record_stats(); - bool isfinalfeasible() const; + bool is_feasible_prefix_ignore_relseq() const; bool is_infeasible_ignoreRMW() const; bool is_infeasible() const; bool is_deadlocked() const; -- 2.34.1