model: move flags to private 'model_snapshot_members'

diff --git a/model.cc b/model.cc
index 4fdd8602d71b99f2c084cab4fa9d71ebade6d68e..fd893c78b42a85cec0bc2668102600f1a4fa63c8 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -45,7 +45,11 @@ struct model_snapshot_members {
                nextThread(NULL),
                next_backtrack(NULL),
                bugs(),
-               stats()
+               stats(),
+               failed_promise(false),
+               too_many_reads(false),
+               bad_synchronization(false),
+               asserted(false)
        { }
 
        ~model_snapshot_members() {
@@ -61,6 +65,11 @@ struct model_snapshot_members {
        ModelAction *next_backtrack;
        std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
        struct execution_stats stats;
+       bool failed_promise;
+       bool too_many_reads;
+       /** @brief Incorrectly-ordered synchronization was made */
+       bool bad_synchronization;
+       bool asserted;
 
        SNAPSHOTALLOC
 };
@@ -84,11 +93,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
        node_stack(new NodeStack()),
        priv(new struct model_snapshot_members()),
-       mo_graph(new CycleGraph()),
-       failed_promise(false),
-       too_many_reads(false),
-       asserted(false),
-       bad_synchronization(false)
+       mo_graph(new CycleGraph())
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
@@ -147,10 +152,6 @@ void ModelChecker::reset_to_initial_state()
 {
        DEBUG("+++ Resetting to initial state +++\n");
        node_stack->reset_execution();
-       failed_promise = false;
-       too_many_reads = false;
-       bad_synchronization = false;
-       reset_asserted();
 
        /* Print all model-checker output before rollback */
        fflush(model_out);
@@ -308,6 +309,23 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
        }
 }
 
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelChecker::set_bad_synchronization()
+{
+       priv->bad_synchronization = true;
+}
+
+bool ModelChecker::has_asserted() const
+{
+       return priv->asserted;
+}
+
+void ModelChecker::set_assert()
+{
+       priv->asserted = true;
+}
+
 /**
  * Check if we are in a deadlock. Should only be called at the end of an
  * execution, although it should not give false positives in the middle of an
@@ -679,7 +697,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 
                        if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
                                mo_graph->rollbackChanges();
-                               too_many_reads = false;
+                               priv->too_many_reads = false;
                                continue;
                        }
 
@@ -1215,16 +1233,16 @@ bool ModelChecker::isfeasibleotherthanRMW() const
        if (DBG_ENABLED()) {
                if (mo_graph->checkForCycles())
                        DEBUG("Infeasible: modification order cycles\n");
-               if (failed_promise)
+               if (priv->failed_promise)
                        DEBUG("Infeasible: failed promise\n");
-               if (too_many_reads)
+               if (priv->too_many_reads)
                        DEBUG("Infeasible: too many reads\n");
-               if (bad_synchronization)
+               if (priv->bad_synchronization)
                        DEBUG("Infeasible: bad synchronization ordering\n");
                if (promises_expired())
                        DEBUG("Infeasible: promises expired\n");
        }
-       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
+       return !mo_graph->checkForCycles() && !priv->failed_promise && !priv->too_many_reads && !priv->bad_synchronization && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -1333,7 +1351,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
                                }
                        }
                        if (feasiblewrite) {
-                               too_many_reads = true;
+                               priv->too_many_reads = true;
                                return;
                        }
                }
@@ -2075,7 +2093,7 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
                                merge_cv->synchronized_since(act)) {
                        if (promise->increment_threads(tid)) {
                                //Promise has failed
-                               failed_promise = true;
+                               priv->failed_promise = true;
                                return;
                        }
                }
@@ -2086,7 +2104,7 @@ void ModelChecker::check_promises_thread_disabled() {
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
                if (promise->check_promise()) {
-                       failed_promise = true;
+                       priv->failed_promise = true;
                        return;
                }
        }
@@ -2137,12 +2155,12 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
                                promise->set_write(write);
                                //The pwrite cannot happen before the promise
                                if (write->happens_before(act) && (write != act)) {
-                                       failed_promise = true;
+                                       priv->failed_promise = true;
                                        return;
                                }
                        }
                        if (mo_graph->checkPromise(write, promise)) {
-                               failed_promise = true;
+                               priv->failed_promise = true;
                                return;
                        }
                }
@@ -2153,7 +2171,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
 
                if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
                        if (promise->increment_threads(tid)) {
-                               failed_promise = true;
+                               priv->failed_promise = true;
                                return;
                        }
                }

diff --git a/model.h b/model.h
index f92c8bdf75679b1cd8b9c0915f210e1d6f667b23..5473e52c2c78b3613ca5f0013c29f5a41f895dd4 100644 (file)
--- a/model.h
+++ b/model.h
@@ -126,9 +126,7 @@ public:
        bool is_complete_execution() const;
        void print_stats() const;
 
-       /** @brief Alert the model-checker that an incorrectly-ordered
-        * synchronization was made */
-       void set_bad_synchronization() { bad_synchronization = true; }
+       void set_bad_synchronization();
 
        const model_params params;
        Node * get_curr_node();
@@ -141,9 +139,8 @@ private:
        bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
        bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
        bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
-       bool has_asserted() {return asserted;}
-       void reset_asserted() { asserted = false; }
-       void set_assert() { asserted = true; }
+       bool has_asserted() const;
+       void set_assert();
        bool promises_expired() const;
        void execute_sleep_set();
        void wake_up_sleeping_actions(ModelAction * curr);
@@ -241,11 +238,6 @@ private:
         * <tt>b</tt>.
         */
        CycleGraph *mo_graph;
-       bool failed_promise;
-       bool too_many_reads;
-       bool asserted;
-       /** @brief Incorrectly-ordered synchronization was made */
-       bool bad_synchronization;
 
        /** @brief The cumulative execution stats */
        struct execution_stats stats;