From: Brian Norris Date: Tue, 20 Nov 2012 03:15:47 +0000 (-0800) Subject: model: move flags to private 'model_snapshot_members' X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=4e707deed378c162acd933d7d7b7c190d341543a;ds=sidebyside model: move flags to private 'model_snapshot_members' --- diff --git a/model.cc b/model.cc index 4fdd8602..fd893c78 100644 --- 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 > 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 >(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 f92c8bdf..5473e52c 100644 --- 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: * b. */ 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;