1 /* Copyright (c) 2016. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
15 #include <xbt/sysdep.h>
17 #include "src/mc/mc_state.h"
18 #include "src/mc/mc_request.h"
19 #include "src/mc/mc_safety.h"
20 #include "src/mc/mc_private.h"
21 #include "src/mc/mc_record.h"
22 #include "src/mc/mc_smx.h"
23 #include "src/mc/Client.hpp"
24 #include "src/mc/mc_exit.h"
25 #include "src/mc/Checker.hpp"
26 #include "src/mc/SafetyChecker.hpp"
27 #include "src/mc/VisitedState.hpp"
29 #include "src/xbt/mmalloc/mmprivate.h"
31 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
32 "Logging specific to MC safety verification ");
36 static void MC_show_non_termination(void)
38 XBT_INFO("******************************************");
39 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
40 XBT_INFO("******************************************");
41 XBT_INFO("Counter-example execution trace:");
42 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
43 XBT_INFO("%s", s.c_str());
44 MC_print_statistics(mc_stats);
47 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
49 simgrid::mc::Snapshot* s1 = state1->system_state.get();
50 simgrid::mc::Snapshot* s2 = state2->system_state.get();
51 int num1 = state1->num;
52 int num2 = state2->num;
53 return snapshot_compare(num1, s1, num2, s2);
56 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
58 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
59 if (snapshot_compare(i->get(), current_state) == 0){
60 XBT_INFO("Non-progressive cycle : state %d -> state %d",
61 (*i)->num, current_state->num);
67 RecordTrace SafetyChecker::getRecordTrace() // override
70 for (auto const& state : stack_) {
72 smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
73 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
74 const int pid = issuer->pid;
75 res.push_back(RecordTraceElement(pid, value));
80 std::vector<std::string> SafetyChecker::getTextualTrace() // override
82 std::vector<std::string> trace;
83 for (auto const& state : stack_) {
85 smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
87 trace.push_back(simgrid::mc::request_to_string(
88 req, value, simgrid::mc::RequestType::executed));
93 int SafetyChecker::run()
99 while (!stack_.empty()) {
101 /* Get current state */
102 simgrid::mc::State* state = stack_.back().get();
104 XBT_DEBUG("**************************************************");
106 "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
107 stack_.size(), state, state->num,
108 state->interleaveSize());
110 mc_stats->visited_states++;
112 // The interleave set is empty or the maximum depth is reached,
114 smx_simcall_t req = nullptr;
115 if (stack_.size() > (std::size_t) _sg_mc_max_depth
116 || (req = MC_state_get_request(state, &value)) == nullptr
117 || visitedState_ != nullptr) {
118 int res = this->backtrack();
125 // If there are processes to interleave and the maximum depth has not been
126 // reached then perform one step of the exploration algorithm.
127 XBT_DEBUG("Execute: %s",
128 simgrid::mc::request_to_string(
129 req, value, simgrid::mc::RequestType::simix).c_str());
132 if (dot_output != nullptr)
133 req_str = simgrid::mc::request_get_dot_output(req, value);
135 mc_stats->executed_transitions++;
137 // TODO, bundle both operations in a single message
138 // MC_execute_transition(req, value)
140 /* Answer the request */
141 simgrid::mc::handle_simcall(req, value);
142 mc_model_checker->wait_for_requests();
144 /* Create the new expanded state */
145 std::unique_ptr<simgrid::mc::State> next_state =
146 std::unique_ptr<simgrid::mc::State>(MC_state_new());
148 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
149 MC_show_non_termination();
150 return SIMGRID_MC_EXIT_NON_TERMINATION;
153 if (_sg_mc_visited == 0
154 || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
156 /* Get an enabled process and insert it in the interleave set of the next state */
157 for (auto& p : mc_model_checker->process().simix_processes())
158 if (simgrid::mc::process_is_enabled(&p.copy)) {
159 next_state->interleave(&p.copy);
160 if (reductionMode_ != simgrid::mc::ReductionMode::none)
164 if (dot_output != nullptr)
165 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
166 state->num, next_state->num, req_str.c_str());
168 } else if (dot_output != nullptr)
169 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
171 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
173 stack_.push_back(std::move(next_state));
176 XBT_INFO("No property violation found.");
177 MC_print_statistics(mc_stats);
178 initial_global_state = nullptr;
179 return SIMGRID_MC_EXIT_SUCCESS;
182 int SafetyChecker::backtrack()
184 if (stack_.size() > (std::size_t) _sg_mc_max_depth
185 || visitedState_ != nullptr) {
186 if (visitedState_ == nullptr)
187 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
189 XBT_DEBUG("State already visited (equal to state %d),"
190 " exploration stopped on this path.",
191 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
193 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
198 visitedState_ = nullptr;
200 /* Check for deadlocks */
201 if (mc_model_checker->checkDeadlock()) {
203 return SIMGRID_MC_EXIT_DEADLOCK;
206 /* Traverse the stack backwards until a state with a non empty interleave
207 set is found, deleting all the states that have it empty in the way.
208 For each deleted state, check if the request that has generated it
209 (from it's predecesor state), depends on any other previous request
210 executed before it. If it does then add it to the interleave set of the
211 state that executed that previous request. */
213 while (!stack_.empty()) {
214 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
216 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
217 smx_simcall_t req = MC_state_get_internal_request(state.get());
218 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
219 xbt_die("Mutex is currently not supported with DPOR, "
220 "use --cfg=model-check/reduction:none");
221 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
222 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
223 simgrid::mc::State* prev_state = i->get();
224 if (reductionMode_ != simgrid::mc::ReductionMode::none
225 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
226 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
227 XBT_DEBUG("Dependent Transitions:");
229 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
230 XBT_DEBUG("%s (state=%d)",
231 simgrid::mc::request_to_string(
232 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
234 prev_req = MC_state_get_executed_request(state.get(), &value);
235 XBT_DEBUG("%s (state=%d)",
236 simgrid::mc::request_to_string(
237 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
241 if (!prev_state->processStates[issuer->pid].isDone())
242 prev_state->interleave(issuer);
244 XBT_DEBUG("Process %p is in done set", req->issuer);
248 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
250 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
255 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
256 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
257 req->call, issuer->pid, state->num,
258 MC_state_get_internal_request(prev_state)->call,
259 previous_issuer->pid,
266 if (state->interleaveSize()
267 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
268 /* We found a back-tracking point, let's loop */
269 XBT_DEBUG("Back-tracking to state %d at depth %zi",
270 state->num, stack_.size() + 1);
271 stack_.push_back(std::move(state));
272 simgrid::mc::replay(stack_);
273 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
274 stack_.back()->num, stack_.size());
277 XBT_DEBUG("Delete state %d at depth %zi",
278 state->num, stack_.size() + 1);
281 return SIMGRID_MC_EXIT_SUCCESS;
284 void SafetyChecker::init()
286 reductionMode_ = simgrid::mc::reduction_mode;
287 if( _sg_mc_termination)
288 reductionMode_ = simgrid::mc::ReductionMode::none;
289 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
290 reductionMode_ = simgrid::mc::ReductionMode::dpor;
292 if (_sg_mc_termination)
293 XBT_INFO("Check non progressive cycles");
295 XBT_INFO("Check a safety property");
296 mc_model_checker->wait_for_requests();
298 XBT_DEBUG("Starting the safety algorithm");
300 std::unique_ptr<simgrid::mc::State> initial_state =
301 std::unique_ptr<simgrid::mc::State>(MC_state_new());
303 XBT_DEBUG("**************************************************");
304 XBT_DEBUG("Initial state");
306 /* Wait for requests (schedules processes) */
307 mc_model_checker->wait_for_requests();
309 /* Get an enabled process and insert it in the interleave set of the initial state */
310 for (auto& p : mc_model_checker->process().simix_processes())
311 if (simgrid::mc::process_is_enabled(&p.copy)) {
312 initial_state->interleave(&p.copy);
313 if (reductionMode_ != simgrid::mc::ReductionMode::none)
317 stack_.push_back(std::move(initial_state));
319 /* Save the initial state */
320 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
321 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
324 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
328 SafetyChecker::~SafetyChecker()
332 Checker* createSafetyChecker(Session& session)
334 return new SafetyChecker(session);