From 7a0167d52294a9707f81a54d74009c6f82346d18 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
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