From 3b3533a76db06884f44b3e70ccdbad647275fcc4 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 24 Jan 2013 17:18:06 -0800
Subject: [PATCH] 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 4ccdbce..9e611fa 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 960e9e1..c76a289 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