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. */
13 #include <xbt/sysdep.h>
15 #include "src/mc/mc_state.h"
16 #include "src/mc/mc_request.h"
17 #include "src/mc/mc_safety.h"
18 #include "src/mc/mc_private.h"
19 #include "src/mc/mc_record.h"
20 #include "src/mc/mc_smx.h"
21 #include "src/mc/Client.hpp"
22 #include "src/mc/mc_exit.h"
23 #include "src/mc/Checker.hpp"
24 #include "src/mc/SafetyChecker.hpp"
25 #include "src/mc/VisitedState.hpp"
27 #include "src/xbt/mmalloc/mmprivate.h"
29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
30 "Logging specific to MC safety verification ");
34 static void MC_show_non_termination(void)
36 XBT_INFO("******************************************");
37 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
38 XBT_INFO("******************************************");
39 XBT_INFO("Counter-example execution trace:");
40 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
41 XBT_INFO("%s", s.c_str());
42 MC_print_statistics(mc_stats);
45 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
47 simgrid::mc::Snapshot* s1 = state1->system_state.get();
48 simgrid::mc::Snapshot* s2 = state2->system_state.get();
49 int num1 = state1->num;
50 int num2 = state2->num;
51 return snapshot_compare(num1, s1, num2, s2);
54 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
56 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
57 if (snapshot_compare(i->get(), current_state) == 0){
58 XBT_INFO("Non-progressive cycle : state %d -> state %d",
59 (*i)->num, current_state->num);
65 RecordTrace SafetyChecker::getRecordTrace() // override
68 for (auto const& state : stack_) {
70 smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
71 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
72 const int pid = issuer->pid;
73 res.push_back(RecordTraceElement(pid, value));
78 std::vector<std::string> SafetyChecker::getTextualTrace() // override
80 std::vector<std::string> trace;
81 for (auto const& state : stack_) {
83 smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
85 char* req_str = simgrid::mc::request_to_string(
86 req, value, simgrid::mc::RequestType::executed);
87 trace.push_back(req_str);
94 int SafetyChecker::run()
100 while (!stack_.empty()) {
102 /* Get current state */
103 simgrid::mc::State* state = stack_.back().get();
105 XBT_DEBUG("**************************************************");
107 "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
108 stack_.size(), state, state->num,
109 MC_state_interleave_size(state));
111 mc_stats->visited_states++;
113 // The interleave set is empty or the maximum depth is reached,
115 smx_simcall_t req = nullptr;
116 if (stack_.size() > (std::size_t) _sg_mc_max_depth
117 || (req = MC_state_get_request(state, &value)) == nullptr
118 || visitedState_ != nullptr) {
119 int res = this->backtrack();
126 // If there are processes to interleave and the maximum depth has not been
127 // reached then perform one step of the exploration algorithm.
129 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
130 char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
131 XBT_DEBUG("Execute: %s", req_str);
135 char* req_str = nullptr;
136 if (dot_output != nullptr)
137 req_str = simgrid::mc::request_get_dot_output(req, value);
139 MC_state_set_executed_request(state, req, value);
140 mc_stats->executed_transitions++;
142 // TODO, bundle both operations in a single message
143 // MC_execute_transition(req, value)
145 /* Answer the request */
146 simgrid::mc::handle_simcall(req, value);
147 mc_model_checker->wait_for_requests();
149 /* Create the new expanded state */
150 std::unique_ptr<simgrid::mc::State> next_state =
151 std::unique_ptr<simgrid::mc::State>(MC_state_new());
153 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
154 MC_show_non_termination();
155 return SIMGRID_MC_EXIT_NON_TERMINATION;
158 if (_sg_mc_visited == 0
159 || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
161 /* Get an enabled process and insert it in the interleave set of the next state */
162 for (auto& p : mc_model_checker->process().simix_processes())
163 if (simgrid::mc::process_is_enabled(&p.copy)) {
164 MC_state_interleave_process(next_state.get(), &p.copy);
165 if (reductionMode_ != simgrid::mc::ReductionMode::none)
169 if (dot_output != nullptr)
170 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
172 } else if (dot_output != nullptr)
173 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str);
175 stack_.push_back(std::move(next_state));
177 if (dot_output != nullptr)
181 XBT_INFO("No property violation found.");
182 MC_print_statistics(mc_stats);
183 initial_global_state = nullptr;
184 return SIMGRID_MC_EXIT_SUCCESS;
187 int SafetyChecker::backtrack()
189 if (stack_.size() > (std::size_t) _sg_mc_max_depth
190 || visitedState_ != nullptr) {
191 if (visitedState_ == nullptr)
192 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
194 XBT_DEBUG("State already visited (equal to state %d),"
195 " exploration stopped on this path.",
196 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
198 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
203 visitedState_ = nullptr;
205 /* Check for deadlocks */
206 if (mc_model_checker->checkDeadlock()) {
208 return SIMGRID_MC_EXIT_DEADLOCK;
211 /* Traverse the stack backwards until a state with a non empty interleave
212 set is found, deleting all the states that have it empty in the way.
213 For each deleted state, check if the request that has generated it
214 (from it's predecesor state), depends on any other previous request
215 executed before it. If it does then add it to the interleave set of the
216 state that executed that previous request. */
218 while (!stack_.empty()) {
219 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
221 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
222 smx_simcall_t req = MC_state_get_internal_request(state.get());
223 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
224 xbt_die("Mutex is currently not supported with DPOR, "
225 "use --cfg=model-check/reduction:none");
226 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
227 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
228 simgrid::mc::State* prev_state = i->get();
229 if (reductionMode_ != simgrid::mc::ReductionMode::none
230 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
231 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
232 XBT_DEBUG("Dependent Transitions:");
234 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
235 char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
236 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
238 prev_req = MC_state_get_executed_request(state.get(), &value);
239 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
240 XBT_DEBUG("%s (state=%d)", req_str, state->num);
244 if (!MC_state_process_is_done(prev_state, issuer))
245 MC_state_interleave_process(prev_state, issuer);
247 XBT_DEBUG("Process %p is in done set", req->issuer);
251 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
253 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
258 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
259 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
260 req->call, issuer->pid, state->num,
261 MC_state_get_internal_request(prev_state)->call,
262 previous_issuer->pid,
269 if (MC_state_interleave_size(state.get())
270 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
271 /* We found a back-tracking point, let's loop */
272 XBT_DEBUG("Back-tracking to state %d at depth %zi",
273 state->num, stack_.size() + 1);
274 stack_.push_back(std::move(state));
275 simgrid::mc::replay(stack_);
276 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
277 stack_.back()->num, stack_.size());
280 XBT_DEBUG("Delete state %d at depth %zi",
281 state->num, stack_.size() + 1);
284 return SIMGRID_MC_EXIT_SUCCESS;
287 void SafetyChecker::init()
289 reductionMode_ = simgrid::mc::reduction_mode;
290 if( _sg_mc_termination)
291 reductionMode_ = simgrid::mc::ReductionMode::none;
292 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
293 reductionMode_ = simgrid::mc::ReductionMode::dpor;
295 if (_sg_mc_termination)
296 XBT_INFO("Check non progressive cycles");
298 XBT_INFO("Check a safety property");
299 mc_model_checker->wait_for_requests();
301 XBT_DEBUG("Starting the safety algorithm");
303 std::unique_ptr<simgrid::mc::State> initial_state =
304 std::unique_ptr<simgrid::mc::State>(MC_state_new());
306 XBT_DEBUG("**************************************************");
307 XBT_DEBUG("Initial state");
309 /* Wait for requests (schedules processes) */
310 mc_model_checker->wait_for_requests();
312 /* Get an enabled process and insert it in the interleave set of the initial state */
313 for (auto& p : mc_model_checker->process().simix_processes())
314 if (simgrid::mc::process_is_enabled(&p.copy)) {
315 MC_state_interleave_process(initial_state.get(), &p.copy);
316 if (reductionMode_ != simgrid::mc::ReductionMode::none)
320 stack_.push_back(std::move(initial_state));
322 /* Save the initial state */
323 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
324 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
327 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
331 SafetyChecker::~SafetyChecker()
335 Checker* createSafetyChecker(Session& session)
337 return new SafetyChecker(session);