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. */
12 #include <xbt/dynar.h>
13 #include <xbt/dynar.hpp>
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"
28 #include "src/xbt/mmalloc/mmprivate.h"
30 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
31 "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 MC_dump_stack_safety(mc_stack);
43 MC_print_statistics(mc_stats);
46 static int is_exploration_stack_state(mc_state_t current_state){
49 mc_state_t stack_state;
50 for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
51 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
52 if(snapshot_compare(stack_state, current_state) == 0){
53 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
60 int SafetyChecker::run()
64 char *req_str = nullptr;
66 smx_simcall_t req = nullptr;
67 mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
68 xbt_fifo_item_t item = nullptr;
69 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
71 while (xbt_fifo_size(mc_stack) > 0) {
73 /* Get current state */
74 state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
76 XBT_DEBUG("**************************************************");
78 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
79 xbt_fifo_size(mc_stack), state, state->num,
80 MC_state_interleave_size(state), user_max_depth_reached);
82 /* Update statistics */
83 mc_stats->visited_states++;
85 /* If there are processes to interleave and the maximum depth has not been reached
86 then perform one step of the exploration algorithm */
87 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
88 && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
90 req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
91 XBT_DEBUG("Execute: %s", req_str);
94 if (dot_output != nullptr)
95 req_str = simgrid::mc::request_get_dot_output(req, value);
97 MC_state_set_executed_request(state, req, value);
98 mc_stats->executed_transitions++;
100 // TODO, bundle both operations in a single message
101 // MC_execute_transition(req, value)
103 /* Answer the request */
104 simgrid::mc::handle_simcall(req, value);
105 mc_model_checker->wait_for_requests();
107 /* Create the new expanded state */
108 next_state = MC_state_new();
110 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
111 MC_show_non_termination();
112 return SIMGRID_MC_EXIT_NON_TERMINATION;
115 if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
117 /* Get an enabled process and insert it in the interleave set of the next state */
118 for (auto& p : mc_model_checker->process().simix_processes())
119 if (simgrid::mc::process_is_enabled(&p.copy)) {
120 MC_state_interleave_process(next_state, &p.copy);
121 if (reductionMode_ != simgrid::mc::ReductionMode::none)
125 if (dot_output != nullptr)
126 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
128 } else if (dot_output != nullptr)
129 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
132 xbt_fifo_unshift(mc_stack, next_state);
134 if (dot_output != nullptr)
137 /* Let's loop again */
139 /* The interleave set is empty or the maximum depth is reached, let's back-track */
142 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
144 if (user_max_depth_reached && visited_state == nullptr)
145 XBT_DEBUG("User max depth reached !");
146 else if (visited_state == nullptr)
147 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
149 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);
152 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
154 /* Trash the current state, no longer needed */
155 xbt_fifo_shift(mc_stack);
156 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
157 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
159 visited_state = nullptr;
161 /* Check for deadlocks */
162 if (mc_model_checker->checkDeadlock()) {
164 return SIMGRID_MC_EXIT_DEADLOCK;
167 /* Traverse the stack backwards until a state with a non empty interleave
168 set is found, deleting all the states that have it empty in the way.
169 For each deleted state, check if the request that has generated it
170 (from it's predecesor state), depends on any other previous request
171 executed before it. If it does then add it to the interleave set of the
172 state that executed that previous request. */
174 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
175 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
176 req = MC_state_get_internal_request(state);
177 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
178 xbt_die("Mutex is currently not supported with DPOR, "
179 "use --cfg=model-check/reduction:none");
180 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
181 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
182 if (reductionMode_ != simgrid::mc::ReductionMode::none
183 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
184 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
185 XBT_DEBUG("Dependent Transitions:");
186 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
187 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
188 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
190 prev_req = MC_state_get_executed_request(state, &value);
191 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
192 XBT_DEBUG("%s (state=%d)", req_str, state->num);
196 if (!MC_state_process_is_done(prev_state, issuer))
197 MC_state_interleave_process(prev_state, issuer);
199 XBT_DEBUG("Process %p is in done set", req->issuer);
203 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
205 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
210 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
211 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
212 req->call, issuer->pid, state->num,
213 MC_state_get_internal_request(prev_state)->call,
214 previous_issuer->pid,
221 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
222 /* We found a back-tracking point, let's loop */
223 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
224 xbt_fifo_unshift(mc_stack, state);
226 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
229 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
230 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
236 XBT_INFO("No property violation found.");
237 MC_print_statistics(mc_stats);
238 return SIMGRID_MC_EXIT_SUCCESS;
241 void SafetyChecker::init()
243 reductionMode_ = simgrid::mc::reduction_mode;
244 if( _sg_mc_termination)
245 reductionMode_ = simgrid::mc::ReductionMode::none;
246 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
247 reductionMode_ = simgrid::mc::ReductionMode::dpor;
249 if (_sg_mc_termination)
250 XBT_INFO("Check non progressive cycles");
252 XBT_INFO("Check a safety property");
253 mc_model_checker->wait_for_requests();
255 XBT_DEBUG("Starting the safety algorithm");
257 /* Create exploration stack */
258 mc_stack = xbt_fifo_new();
260 simgrid::mc::visited_states.clear();
262 mc_state_t initial_state = MC_state_new();
264 XBT_DEBUG("**************************************************");
265 XBT_DEBUG("Initial state");
267 /* Wait for requests (schedules processes) */
268 mc_model_checker->wait_for_requests();
270 /* Get an enabled process and insert it in the interleave set of the initial state */
271 for (auto& p : mc_model_checker->process().simix_processes())
272 if (simgrid::mc::process_is_enabled(&p.copy)) {
273 MC_state_interleave_process(initial_state, &p.copy);
274 if (reductionMode_ != simgrid::mc::ReductionMode::none)
278 xbt_fifo_unshift(mc_stack, initial_state);
280 /* Save the initial state */
281 initial_global_state = xbt_new0(s_mc_global_t, 1);
282 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
285 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
289 SafetyChecker::~SafetyChecker()