model: privatize, move isfinalfeasible()

This function should go with all the other "feasible" functions.

diff --git a/model.cc b/model.cc
index 0e650a3c5b3c530d1fc398c4a07964e59b65dd64..8453f2e51a0c7866da57db9e6b65560442bb1905 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1217,6 +1217,15 @@ bool ModelChecker::isfeasibleprefix() const
        return promises->size() == 0 && pending_rel_seqs->size() == 0 && !is_infeasible();
 }
 
        return promises->size() == 0 && pending_rel_seqs->size() == 0 && !is_infeasible();
 }
 

+/** Returns whether the current completed trace is feasible. */
+bool ModelChecker::isfinalfeasible() const
+{
+       if (DBG_ENABLED() && promises->size() != 0)
+               DEBUG("Infeasible: unrevolved promises\n");
+
+       return !is_infeasible() && promises->size() == 0;
+}
+

 /**
  * Check if the current partial trace is infeasible. Does not check any
  * end-of-execution flags, which might rule out the execution. Thus, this is
 /**
  * Check if the current partial trace is infeasible. Does not check any
  * end-of-execution flags, which might rule out the execution. Thus, this is


@@ -1258,15 +1267,6 @@ bool ModelChecker::is_infeasible_ignoreRMW() const
                promises_expired();
 }
 
                promises_expired();
 }
 

-/** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() const
-{
-       if (DBG_ENABLED() && promises->size() != 0)
-               DEBUG("Infeasible: unrevolved promises\n");
-
-       return !is_infeasible() && promises->size() == 0;
-}
-

 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
        ModelAction *lastread = get_last_action(act->get_tid());
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
        ModelAction *lastread = get_last_action(act->get_tid());

diff --git a/model.h b/model.h
index 432399ea22eb7124557cb8cdc9bcfa8b38b6d605..3f1103e543fa987164cc8d75f7c0c92779a6ff86 100644 (file)
--- a/model.h
+++ b/model.h
@@ -116,7 +116,6 @@ public:
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);
        ModelAction * get_parent_action(thread_id_t tid);
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);
        ModelAction * get_parent_action(thread_id_t tid);

-       bool isfinalfeasible() const;

        void check_promises_thread_disabled();
        void mo_check_promises(thread_id_t tid, const ModelAction *write);
        void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
        void check_promises_thread_disabled();
        void mo_check_promises(thread_id_t tid, const ModelAction *write);
        void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);


@@ -244,6 +243,7 @@ private:
        struct execution_stats stats;
        void record_stats();
 
        struct execution_stats stats;
        void record_stats();
 

+       bool isfinalfeasible() const;

        bool is_infeasible_ignoreRMW() const;
        bool is_infeasible() const;
        bool is_deadlocked() const;
        bool is_infeasible_ignoreRMW() const;
        bool is_infeasible() const;
        bool is_deadlocked() const;