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/dynar.h>
14 #include <xbt/dynar.hpp>
16 #include <xbt/sysdep.h>
18 #include "src/mc/mc_state.h"
19 #include "src/mc/mc_request.h"
20 #include "src/mc/mc_safety.h"
21 #include "src/mc/mc_private.h"
22 #include "src/mc/mc_record.h"
23 #include "src/mc/mc_smx.h"
24 #include "src/mc/Client.hpp"
25 #include "src/mc/mc_exit.h"
26 #include "src/mc/Checker.hpp"
27 #include "src/mc/SafetyChecker.hpp"
28 #include "src/mc/VisitedState.hpp"
30 #include "src/xbt/mmalloc/mmprivate.h"
32 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
33 "Logging specific to MC safety verification ");
37 static void MC_show_non_termination(void)
39 XBT_INFO("******************************************");
40 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
41 XBT_INFO("******************************************");
42 XBT_INFO("Counter-example execution trace:");
43 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
44 XBT_INFO("%s", s.c_str());
45 MC_print_statistics(mc_stats);
48 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
50 simgrid::mc::Snapshot* s1 = state1->system_state.get();
51 simgrid::mc::Snapshot* s2 = state2->system_state.get();
52 int num1 = state1->num;
53 int num2 = state2->num;
54 return snapshot_compare(num1, s1, num2, s2);
57 bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
59 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
60 if(snapshot_compare(*i, current_state) == 0){
61 XBT_INFO("Non-progressive cycle : state %d -> state %d",
62 (*i)->num, current_state->num);
68 RecordTrace SafetyChecker::getRecordTrace() // override
71 for (simgrid::mc::State* state : stack_) {
73 smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
74 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
75 const int pid = issuer->pid;
76 res.push_back(RecordTraceElement(pid, value));
81 std::vector<std::string> SafetyChecker::getTextualTrace() // override
83 std::vector<std::string> trace;
84 for (simgrid::mc::State* state : stack_) {
86 smx_simcall_t req = MC_state_get_executed_request(state, &value);
88 char* req_str = simgrid::mc::request_to_string(
89 req, value, simgrid::mc::RequestType::executed);
90 trace.push_back(req_str);
97 int SafetyChecker::run()
101 char *req_str = nullptr;
103 smx_simcall_t req = nullptr;
104 simgrid::mc::State* prev_state = nullptr;
105 simgrid::mc::State* next_state = nullptr;
106 xbt_fifo_item_t item = nullptr;
107 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
109 while (!stack_.empty()) {
111 /* Get current state */
112 simgrid::mc::State* state = stack_.back();
114 XBT_DEBUG("**************************************************");
116 "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
117 stack_.size(), state, state->num,
118 MC_state_interleave_size(state), user_max_depth_reached);
120 /* Update statistics */
121 mc_stats->visited_states++;
123 /* If there are processes to interleave and the maximum depth has not been reached
124 then perform one step of the exploration algorithm */
125 if (stack_.size() <= _sg_mc_max_depth && !user_max_depth_reached
126 && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
128 req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
129 XBT_DEBUG("Execute: %s", req_str);
132 if (dot_output != nullptr)
133 req_str = simgrid::mc::request_get_dot_output(req, value);
135 MC_state_set_executed_request(state, req, value);
136 mc_stats->executed_transitions++;
138 // TODO, bundle both operations in a single message
139 // MC_execute_transition(req, value)
141 /* Answer the request */
142 simgrid::mc::handle_simcall(req, value);
143 mc_model_checker->wait_for_requests();
145 /* Create the new expanded state */
146 next_state = MC_state_new();
148 if (_sg_mc_termination && this->checkNonDeterminism(next_state)){
149 MC_show_non_termination();
150 return SIMGRID_MC_EXIT_NON_TERMINATION;
153 if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
155 /* Get an enabled process and insert it in the interleave set of the next state */
156 for (auto& p : mc_model_checker->process().simix_processes())
157 if (simgrid::mc::process_is_enabled(&p.copy)) {
158 MC_state_interleave_process(next_state, &p.copy);
159 if (reductionMode_ != simgrid::mc::ReductionMode::none)
163 if (dot_output != nullptr)
164 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
166 } else if (dot_output != nullptr)
167 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
169 stack_.push_back(next_state);
171 if (dot_output != nullptr)
174 /* Let's loop again */
176 /* The interleave set is empty or the maximum depth is reached, let's back-track */
179 if (stack_.size() > _sg_mc_max_depth || user_max_depth_reached
180 || visited_state != nullptr) {
182 if (user_max_depth_reached && visited_state == nullptr)
183 XBT_DEBUG("User max depth reached !");
184 else if (visited_state == nullptr)
185 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
187 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
190 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
193 /* Trash the current state, no longer needed */
195 XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1);
196 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
198 visited_state = 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 state = stack_.back();
216 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
217 req = MC_state_get_internal_request(state);
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;
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:");
228 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
229 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
230 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
232 prev_req = MC_state_get_executed_request(state, &value);
233 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
234 XBT_DEBUG("%s (state=%d)", req_str, state->num);
238 if (!MC_state_process_is_done(prev_state, issuer))
239 MC_state_interleave_process(prev_state, issuer);
241 XBT_DEBUG("Process %p is in done set", req->issuer);
245 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
247 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
252 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
253 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
254 req->call, issuer->pid, state->num,
255 MC_state_get_internal_request(prev_state)->call,
256 previous_issuer->pid,
263 if (MC_state_interleave_size(state)
264 && stack_.size() < _sg_mc_max_depth) {
265 /* We found a back-tracking point, let's loop */
266 XBT_DEBUG("Back-tracking to state %d at depth %zi",
267 state->num, stack_.size() + 1);
268 stack_.push_back(state);
269 simgrid::mc::replay(stack_);
270 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
271 state->num, stack_.size());
274 XBT_DEBUG("Delete state %d at depth %zi",
275 state->num, stack_.size() + 1);
276 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
282 XBT_INFO("No property violation found.");
283 MC_print_statistics(mc_stats);
284 initial_global_state = nullptr;
285 return SIMGRID_MC_EXIT_SUCCESS;
288 void SafetyChecker::init()
290 reductionMode_ = simgrid::mc::reduction_mode;
291 if( _sg_mc_termination)
292 reductionMode_ = simgrid::mc::ReductionMode::none;
293 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
294 reductionMode_ = simgrid::mc::ReductionMode::dpor;
296 if (_sg_mc_termination)
297 XBT_INFO("Check non progressive cycles");
299 XBT_INFO("Check a safety property");
300 mc_model_checker->wait_for_requests();
302 XBT_DEBUG("Starting the safety algorithm");
304 simgrid::mc::visited_states.clear();
306 simgrid::mc::State* initial_state = MC_state_new();
308 XBT_DEBUG("**************************************************");
309 XBT_DEBUG("Initial state");
311 /* Wait for requests (schedules processes) */
312 mc_model_checker->wait_for_requests();
314 /* Get an enabled process and insert it in the interleave set of the initial state */
315 for (auto& p : mc_model_checker->process().simix_processes())
316 if (simgrid::mc::process_is_enabled(&p.copy)) {
317 MC_state_interleave_process(initial_state, &p.copy);
318 if (reductionMode_ != simgrid::mc::ReductionMode::none)
322 stack_.push_back(initial_state);
324 /* Save the initial state */
325 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
326 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
329 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
333 SafetyChecker::~SafetyChecker()