From b99c0d78b25704a61225be8a8b5c47b246afe22a Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 22 Jan 2017 22:27:33 +0100 Subject: [PATCH 1/1] cosmetics --- include/simgrid/modelchecker.h | 4 ++-- src/include/mc/mc.h | 2 +- src/mc/Process.hpp | 2 +- src/mc/VisitedState.cpp | 2 +- src/mc/checker/CommunicationDeterminismChecker.cpp | 6 +++--- src/mc/checker/LivenessChecker.cpp | 4 ++-- src/mc/checker/SafetyChecker.cpp | 2 +- src/mc/mc_base.cpp | 2 +- src/mc/mc_checkpoint.cpp | 2 +- src/mc/mc_config.cpp | 4 ++-- src/mc/mc_state.cpp | 11 +++-------- 11 files changed, 18 insertions(+), 23 deletions(-) diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 0579ca6e2a..a09795351b 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -31,10 +31,10 @@ XBT_PUBLIC(int) MC_random(int min, int max); * * Please don't use directly: you should use MC_is_active. */ extern XBT_PUBLIC(int) _sg_do_model_check; -extern XBT_PUBLIC(int) _sg_mc_visited; +extern XBT_PUBLIC(int) _sg_mc_max_visited_states; #define MC_is_active() _sg_do_model_check -#define MC_visited_reduction() _sg_mc_visited +#define MC_visited_reduction() _sg_mc_max_visited_states /** Assertion for the model-checker * diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 39213e1bd1..2d37e156a9 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -39,7 +39,7 @@ extern XBT_PUBLIC(char*) _sg_mc_property_file; extern XBT_PRIVATE int _sg_mc_timeout; extern XBT_PRIVATE int _sg_mc_hash; extern XBT_PRIVATE int _sg_mc_max_depth; -extern XBT_PUBLIC(int) _sg_mc_visited; +extern XBT_PUBLIC(int) _sg_mc_max_visited_states; extern XBT_PRIVATE char* _sg_mc_dot_output_file; extern XBT_PUBLIC(int) _sg_mc_comms_determinism; extern XBT_PUBLIC(int) _sg_mc_send_determinism; diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp index a109f83142..07f510c931 100644 --- a/src/mc/Process.hpp +++ b/src/mc/Process.hpp @@ -147,7 +147,7 @@ public: this->refresh_heap(); return this->heap.get(); } - malloc_info* get_malloc_info() + const malloc_info* get_malloc_info() { if (!(this->cache_flags_ & Process::cache_malloc)) this->refresh_malloc_info(); diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index c57bf9c056..a2348a80ad 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -60,7 +60,7 @@ VisitedState::~VisitedState() void VisitedStates::prune() { - while (states_.size() > (std::size_t) _sg_mc_visited) { + while (states_.size() > (std::size_t)_sg_mc_max_visited_states) { XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)"); auto min_element = boost::range::min_element(states_, [](std::unique_ptr& a, std::unique_ptr& b) { diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index fa5ab40612..e8999908e5 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -512,9 +512,9 @@ void CommunicationDeterminismChecker::main(void) bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done; - if (_sg_mc_visited == 0 - || (visited_state = visitedStates_.addVisitedState( - expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) { + if (_sg_mc_max_visited_states == 0 || + (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) == + nullptr) { /* Get enabled actors and insert them in the interleave set of the next state */ for (auto& actor : mc_model_checker->process().actors()) diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index a28aa518cd..a505e097e4 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -220,7 +220,7 @@ void LivenessChecker::replay() */ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair) { - if (_sg_mc_visited == 0) + if (_sg_mc_max_visited_states == 0) return -1; if (visited_pair == nullptr) @@ -258,7 +258,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair void LivenessChecker::purgeVisitedPairs() { - if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) { + if (_sg_mc_max_visited_states != 0 && visitedPairs_.size() > (std::size_t)_sg_mc_max_visited_states) { // Remove the oldest entry with a linear search: visitedPairs_.erase(boost::min_element(visitedPairs_, [](std::shared_ptr const a, std::shared_ptr const& b) { diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 52e1e70831..21855771d7 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -158,7 +158,7 @@ void SafetyChecker::run() this->checkNonTermination(next_state.get()); /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */ - if (_sg_mc_visited == true) + if (_sg_mc_max_visited_states == true) visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true); /* If this is a new state (or if we don't care about state-equality reduction) */ diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index f5530bd3ee..e6e2a7797d 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -113,8 +113,8 @@ bool request_is_enabled(smx_simcall_t req) #if HAVE_MC // Fetch from MCed memory: // HACK, type puning - simgrid::mc::Remote temp_comm; if (mc_model_checker != nullptr) { + simgrid::mc::Remote temp_comm; mc_model_checker->process().read(temp_comm, remote(act)); act = static_cast(temp_comm.getBuffer()); } diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp index 6deee1c5a2..37169199f7 100644 --- a/src/mc/mc_checkpoint.cpp +++ b/src/mc/mc_checkpoint.cpp @@ -578,7 +578,7 @@ std::shared_ptr take_snapshot(int num_state) snapshot->to_ignore = mc_model_checker->process().ignored_heap(); - if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) { + if (_sg_mc_max_visited_states > 0 || strcmp(_sg_mc_property_file, "")) { snapshot->stacks = take_snapshot_stacks(snapshot.get()); if (_sg_mc_hash) snapshot->hash = simgrid::mc::hash(*snapshot); diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 84b8b07dbc..67bebd4e6b 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -55,7 +55,7 @@ int _sg_mc_ksm = 0; char *_sg_mc_property_file = nullptr; int _sg_mc_hash = 0; int _sg_mc_max_depth = 1000; -int _sg_mc_visited = 0; +int _sg_mc_max_visited_states = 0; char *_sg_mc_dot_output_file = nullptr; int _sg_mc_comms_determinism = 0; int _sg_mc_send_determinism = 0; @@ -144,7 +144,7 @@ void _mc_cfg_cb_visited(const char *name) xbt_die ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - _sg_mc_visited = xbt_cfg_get_int(name); + _sg_mc_max_visited_states = xbt_cfg_get_int(name); } void _mc_cfg_cb_dot_output(const char *name) diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 861e399698..e85574f899 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -165,11 +165,10 @@ static inline smx_simcall_t MC_state_get_request_for_process( if (!req) return nullptr; - // Fetch the data of the request and translate it: - state->transition.pid = process->pid; - state->executed_req = *req; + // Fetch the data of the request and translate it: + state->internal_req = *req; /* The waitany and testany request are transformed into a wait or test request * over the corresponding communication action so it can be treated later by @@ -177,7 +176,6 @@ static inline smx_simcall_t MC_state_get_request_for_process( switch (req->call) { case SIMCALL_COMM_WAITANY: { state->internal_req.call = SIMCALL_COMM_WAIT; - state->internal_req.issuer = req->issuer; smx_activity_t remote_comm; read_element(mc_model_checker->process(), &remote_comm, remote(simcall_comm_waitany__get__comms(req)), @@ -191,7 +189,6 @@ static inline smx_simcall_t MC_state_get_request_for_process( case SIMCALL_COMM_TESTANY: state->internal_req.call = SIMCALL_COMM_TEST; - state->internal_req.issuer = req->issuer; if (state->transition.argument > 0) { smx_activity_t remote_comm = mc_model_checker->process().read( @@ -205,7 +202,6 @@ static inline smx_simcall_t MC_state_get_request_for_process( break; case SIMCALL_COMM_WAIT: - state->internal_req = *req; mc_model_checker->process().read_bytes(&state->internal_comm , sizeof(state->internal_comm), remote(simcall_comm_wait__get__comm(req))); simcall_comm_wait__set__comm(&state->executed_req, state->internal_comm.getBuffer()); @@ -213,7 +209,6 @@ static inline smx_simcall_t MC_state_get_request_for_process( break; case SIMCALL_COMM_TEST: - state->internal_req = *req; mc_model_checker->process().read_bytes(&state->internal_comm, sizeof(state->internal_comm), remote(simcall_comm_test__get__comm(req))); simcall_comm_test__set__comm(&state->executed_req, state->internal_comm.getBuffer()); @@ -221,7 +216,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( break; default: - state->internal_req = *req; + /* No translation needed */ break; } -- 2.20.1