model: remove ModelChecker::is_infeasible_ignoreRMW()
authorBrian Norris <banorris@uci.edu>
Fri, 25 Jan 2013 01:18:06 +0000 (17:18 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 25 Jan 2013 01:18:06 +0000 (17:18 -0800)
We don't make any special exceptions for this condition anymore, so drop
the function.

model.cc
model.h

index 4ccdbce..9e611fa 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1407,21 +1407,11 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() 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();
 }
 
                promises_expired();
 }
 
diff --git a/model.h b/model.h
index 960e9e1..c76a289 100644 (file)
--- 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;
 
        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;
        bool is_infeasible() const;
        bool is_deadlocked() const;
        bool is_complete_execution() const;