From 3b3533a76db06884f44b3e70ccdbad647275fcc4 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 24 Jan 2013 17:18:06 -0800 Subject: [PATCH 1/1] model: remove ModelChecker::is_infeasible_ignoreRMW() We don't make any special exceptions for this condition anymore, so drop the function. --- model.cc | 20 +++++--------------- model.h | 1 - 2 files changed, 5 insertions(+), 16 deletions(-) diff --git a/model.cc b/model.cc index 4ccdbce2..9e611fae 100644 --- a/model.cc +++ b/model.cc @@ -1407,21 +1407,11 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const */ bool ModelChecker::is_infeasible() const { - return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW(); -} - -/** - * Check If the current partial trace is infeasible, while ignoring - * infeasibility related to 2 RMW's reading from the same store. It does not - * check end-of-execution feasibility. - * @see ModelChecker::is_infeasible - * @return whether the current partial trace is infeasible, ignoring multiple - * RMWs reading from the same store. - * */ -bool ModelChecker::is_infeasible_ignoreRMW() const -{ - return mo_graph->checkForCycles() || priv->failed_promise || - priv->too_many_reads || priv->bad_synchronization || + return mo_graph->checkForRMWViolation() || + mo_graph->checkForCycles() || + priv->failed_promise || + priv->too_many_reads || + priv->bad_synchronization || promises_expired(); } diff --git a/model.h b/model.h index 960e9e1a..c76a2897 100644 --- a/model.h +++ b/model.h @@ -257,7 +257,6 @@ private: void print_infeasibility(const char *prefix) const; bool is_feasible_prefix_ignore_relseq() const; - bool is_infeasible_ignoreRMW() const; bool is_infeasible() const; bool is_deadlocked() const; bool is_complete_execution() const; -- 2.34.1