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 int is_exploration_stack_state(mc_state_t current_state){
39 mc_state_t stack_state;
40 for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
41 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
42 if(snapshot_compare(stack_state, current_state) == 0){
43 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
51 * \brief Initialize the DPOR exploration algorithm
53 void SafetyChecker::pre()
55 simgrid::mc::visited_states.clear();
57 mc_state_t initial_state = MC_state_new();
59 XBT_DEBUG("**************************************************");
60 XBT_DEBUG("Initial state");
62 /* Wait for requests (schedules processes) */
63 mc_model_checker->wait_for_requests();
65 /* Get an enabled process and insert it in the interleave set of the initial state */
66 for (auto& p : mc_model_checker->process().simix_processes())
67 if (simgrid::mc::process_is_enabled(&p.copy)) {
68 MC_state_interleave_process(initial_state, &p.copy);
69 if (reductionMode_ != simgrid::mc::ReductionMode::none)
73 xbt_fifo_unshift(mc_stack, initial_state);
76 int SafetyChecker::run()
80 char *req_str = nullptr;
82 smx_simcall_t req = nullptr;
83 mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
84 xbt_fifo_item_t item = nullptr;
85 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
87 while (xbt_fifo_size(mc_stack) > 0) {
89 /* Get current state */
90 state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
92 XBT_DEBUG("**************************************************");
94 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
95 xbt_fifo_size(mc_stack), state, state->num,
96 MC_state_interleave_size(state), user_max_depth_reached);
98 /* Update statistics */
99 mc_stats->visited_states++;
101 /* If there are processes to interleave and the maximum depth has not been reached
102 then perform one step of the exploration algorithm */
103 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
104 && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
106 req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
107 XBT_DEBUG("Execute: %s", req_str);
110 if (dot_output != nullptr)
111 req_str = simgrid::mc::request_get_dot_output(req, value);
113 MC_state_set_executed_request(state, req, value);
114 mc_stats->executed_transitions++;
116 // TODO, bundle both operations in a single message
117 // MC_execute_transition(req, value)
119 /* Answer the request */
120 simgrid::mc::handle_simcall(req, value);
121 mc_model_checker->wait_for_requests();
123 /* Create the new expanded state */
124 next_state = MC_state_new();
126 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
127 MC_show_non_termination();
128 return SIMGRID_MC_EXIT_NON_TERMINATION;
131 if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
133 /* Get an enabled process and insert it in the interleave set of the next state */
134 for (auto& p : mc_model_checker->process().simix_processes())
135 if (simgrid::mc::process_is_enabled(&p.copy)) {
136 MC_state_interleave_process(next_state, &p.copy);
137 if (reductionMode_ != simgrid::mc::ReductionMode::none)
141 if (dot_output != nullptr)
142 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
144 } else if (dot_output != nullptr)
145 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
148 xbt_fifo_unshift(mc_stack, next_state);
150 if (dot_output != nullptr)
153 /* Let's loop again */
155 /* The interleave set is empty or the maximum depth is reached, let's back-track */
158 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
160 if (user_max_depth_reached && visited_state == nullptr)
161 XBT_DEBUG("User max depth reached !");
162 else if (visited_state == nullptr)
163 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
165 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);
168 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
170 /* Trash the current state, no longer needed */
171 xbt_fifo_shift(mc_stack);
172 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
173 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
175 visited_state = nullptr;
177 /* Check for deadlocks */
178 if (mc_model_checker->checkDeadlock()) {
179 MC_show_deadlock(nullptr);
180 return SIMGRID_MC_EXIT_DEADLOCK;
183 /* Traverse the stack backwards until a state with a non empty interleave
184 set is found, deleting all the states that have it empty in the way.
185 For each deleted state, check if the request that has generated it
186 (from it's predecesor state), depends on any other previous request
187 executed before it. If it does then add it to the interleave set of the
188 state that executed that previous request. */
190 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
191 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
192 req = MC_state_get_internal_request(state);
193 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
194 xbt_die("Mutex is currently not supported with DPOR, "
195 "use --cfg=model-check/reduction:none");
196 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
197 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
198 if (reductionMode_ != simgrid::mc::ReductionMode::none
199 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
200 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
201 XBT_DEBUG("Dependent Transitions:");
202 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
203 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
204 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
206 prev_req = MC_state_get_executed_request(state, &value);
207 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
208 XBT_DEBUG("%s (state=%d)", req_str, state->num);
212 if (!MC_state_process_is_done(prev_state, issuer))
213 MC_state_interleave_process(prev_state, issuer);
215 XBT_DEBUG("Process %p is in done set", req->issuer);
219 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
221 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
226 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
227 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
228 req->call, issuer->pid, state->num,
229 MC_state_get_internal_request(prev_state)->call,
230 previous_issuer->pid,
237 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
238 /* We found a back-tracking point, let's loop */
239 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
240 xbt_fifo_unshift(mc_stack, state);
242 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
245 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
246 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
252 XBT_INFO("No property violation found.");
253 MC_print_statistics(mc_stats);
254 return SIMGRID_MC_EXIT_SUCCESS;
257 void SafetyChecker::init()
259 reductionMode_ = simgrid::mc::reduction_mode;
260 if( _sg_mc_termination)
261 reductionMode_ = simgrid::mc::ReductionMode::none;
262 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
263 reductionMode_ = simgrid::mc::ReductionMode::dpor;
265 if (_sg_mc_termination)
266 XBT_INFO("Check non progressive cycles");
268 XBT_INFO("Check a safety property");
269 mc_model_checker->wait_for_requests();
271 XBT_DEBUG("Starting the safety algorithm");
273 /* Create exploration stack */
274 mc_stack = xbt_fifo_new();
278 /* Save the initial state */
279 initial_global_state = xbt_new0(s_mc_global_t, 1);
280 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
283 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
287 SafetyChecker::~SafetyChecker()