Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
DPOR: improve debug messages
[simgrid.git] / src / mc / checker / SafetyChecker.cpp
1 /* Copyright (c) 2016-2019. The SimGrid Team. All rights reserved.          */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include <cassert>
7 #include <cstdio>
8
9 #include <memory>
10 #include <string>
11 #include <vector>
12
13 #include <xbt/log.h>
14 #include <xbt/sysdep.h>
15
16 #include "src/mc/Session.hpp"
17 #include "src/mc/Transition.hpp"
18 #include "src/mc/VisitedState.hpp"
19 #include "src/mc/checker/SafetyChecker.hpp"
20 #include "src/mc/mc_config.hpp"
21 #include "src/mc/mc_exit.hpp"
22 #include "src/mc/mc_private.hpp"
23 #include "src/mc/mc_record.hpp"
24 #include "src/mc/mc_request.hpp"
25 #include "src/mc/mc_smx.hpp"
26
27 #include "src/xbt/mmalloc/mmprivate.h"
28
29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
30                                 "Logging specific to MC safety verification ");
31 namespace simgrid {
32 namespace mc {
33
34 void SafetyChecker::check_non_termination(simgrid::mc::State* current_state)
35 {
36   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
37     if (snapshot_equal((*state)->system_state.get(), current_state->system_state.get())) {
38       XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
39       XBT_INFO("******************************************");
40       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
41       XBT_INFO("******************************************");
42       XBT_INFO("Counter-example execution trace:");
43       for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
44         XBT_INFO("  %s", s.c_str());
45       simgrid::mc::dumpRecordPath();
46       simgrid::mc::session->log_state();
47
48       throw simgrid::mc::TerminationError();
49     }
50 }
51
52 RecordTrace SafetyChecker::get_record_trace() // override
53 {
54   RecordTrace res;
55   for (auto const& state : stack_)
56     res.push_back(state->get_transition());
57   return res;
58 }
59
60 std::vector<std::string> SafetyChecker::get_textual_trace() // override
61 {
62   std::vector<std::string> trace;
63   for (auto const& state : stack_) {
64     int value         = state->transition_.argument_;
65     smx_simcall_t req = &state->executed_req_;
66     if (req)
67       trace.push_back(simgrid::mc::request_to_string(
68         req, value, simgrid::mc::RequestType::executed));
69   }
70   return trace;
71 }
72
73 void SafetyChecker::log_state() // override
74 {
75   XBT_INFO("Expanded states = %lu", expanded_states_count_);
76   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
77   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
78 }
79
80 void SafetyChecker::run()
81 {
82   /* This function runs the DFS algorithm the state space.
83    * We do so iteratively instead of recursively, dealing with the call stack manually.
84    * This allows to explore the call stack at wish. */
85
86   while (not stack_.empty()) {
87
88     /* Get current state */
89     simgrid::mc::State* state = stack_.back().get();
90
91     XBT_DEBUG("**************************************************");
92     XBT_VERB("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num_,
93              state->interleave_size());
94
95     mc_model_checker->visited_states++;
96
97     // Backtrack if we reached the maximum depth
98     if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
99       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
100       this->backtrack();
101       continue;
102     }
103
104     // Backtrack if we are revisiting a state we saw previously
105     if (visited_state_ != nullptr) {
106       XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
107                 visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num);
108
109       visited_state_ = nullptr;
110       this->backtrack();
111       continue;
112     }
113
114     // Search an enabled transition in the current state; backtrack if the interleave set is empty
115     // get_request also sets state.transition to be the one corresponding to the returned req
116     smx_simcall_t req = MC_state_get_request(state);
117     // req is now the transition of the process that was selected to be executed
118
119     if (req == nullptr) {
120       XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
121
122       this->backtrack();
123       continue;
124     }
125
126     // If there are processes to interleave and the maximum depth has not been
127     // reached then perform one step of the exploration algorithm.
128     XBT_DEBUG(
129         "Execute: %s",
130         simgrid::mc::request_to_string(req, state->transition_.argument_, simgrid::mc::RequestType::simix).c_str());
131
132     std::string req_str;
133     if (dot_output != nullptr)
134       req_str = simgrid::mc::request_get_dot_output(req, state->transition_.argument_);
135
136     mc_model_checker->executed_transitions++;
137
138     /* Actually answer the request: let execute the selected request (MCed does one step) */
139     this->get_session().execute(state->transition_);
140
141     /* Create the new expanded state (copy the state of MCed into our MCer data) */
142     std::unique_ptr<simgrid::mc::State> next_state =
143         std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
144
145     if (_sg_mc_termination)
146       this->check_non_termination(next_state.get());
147
148     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
149     if (_sg_mc_max_visited_states > 0)
150       visited_state_ = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), true);
151
152     /* If this is a new state (or if we don't care about state-equality reduction) */
153     if (visited_state_ == nullptr) {
154
155       /* Get an enabled process and insert it in the interleave set of the next state */
156       for (auto& remoteActor : mc_model_checker->process().actors()) {
157         auto actor = remoteActor.copy.get_buffer();
158         if (simgrid::mc::actor_is_enabled(actor)) {
159           next_state->add_interleaving_set(actor);
160           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
161             break; // With DPOR, we take the first enabled transition
162         }
163       }
164
165       if (dot_output != nullptr)
166         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num_, next_state->num_, req_str.c_str());
167
168     } else if (dot_output != nullptr)
169       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num_,
170                    visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
171                    req_str.c_str());
172
173     stack_.push_back(std::move(next_state));
174   }
175
176   XBT_INFO("No property violation found.");
177   simgrid::mc::session->log_state();
178 }
179
180 void SafetyChecker::backtrack()
181 {
182   stack_.pop_back();
183
184   /* Check for deadlocks */
185   if (mc_model_checker->checkDeadlock()) {
186     MC_show_deadlock();
187     throw simgrid::mc::DeadlockError();
188   }
189
190   /* Traverse the stack backwards until a state with a non empty interleave
191      set is found, deleting all the states that have it empty in the way.
192      For each deleted state, check if the request that has generated it
193      (from it's predecessor state), depends on any other previous request
194      executed before it. If it does then add it to the interleave set of the
195      state that executed that previous request. */
196
197   while (not stack_.empty()) {
198     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
199     stack_.pop_back();
200     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
201       smx_simcall_t req = &state->internal_req;
202       if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK)
203         xbt_die("Mutex is currently not supported with DPOR,  use --cfg=model-check/reduction:none");
204
205       const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
206       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
207         simgrid::mc::State* prev_state = i->get();
208         if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
209           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
210             XBT_DEBUG("Dependent Transitions:");
211             int value              = prev_state->transition_.argument_;
212             smx_simcall_t prev_req = &prev_state->executed_req_;
213             XBT_DEBUG("%s (state=%d)",
214                       simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal).c_str(),
215                       prev_state->num_);
216             value    = state->transition_.argument_;
217             prev_req = &state->executed_req_;
218             XBT_DEBUG("%s (state=%d)",
219                       simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed).c_str(),
220                       state->num_);
221           }
222
223           if (not prev_state->actor_states_[issuer->get_pid()].is_done())
224             prev_state->add_interleaving_set(issuer);
225           else
226             XBT_DEBUG("Process %p is in done set", req->issuer_);
227
228           break;
229
230         } else if (req->issuer_ == prev_state->internal_req.issuer_) {
231
232           XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(req->call_),
233                     SIMIX_simcall_name(prev_state->internal_req.call_));
234           break;
235
236         } else {
237
238           const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
239           XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
240                     SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_,
241                     SIMIX_simcall_name(prev_state->internal_req.call_), previous_issuer->get_pid(), prev_state->num_);
242         }
243       }
244     }
245
246     if (state->interleave_size() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
247       /* We found a back-tracking point, let's loop */
248       XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
249       stack_.push_back(std::move(state));
250       this->restore_state();
251       XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num_, stack_.size());
252       break;
253     } else {
254       XBT_DEBUG("Delete state %d at depth %zu", state->num_, stack_.size() + 1);
255     }
256   }
257 }
258
259 void SafetyChecker::restore_state()
260 {
261   /* Intermediate backtracking */
262   simgrid::mc::State* last_state = stack_.back().get();
263   if (last_state->system_state) {
264     last_state->system_state->restore(&mc_model_checker->process());
265     return;
266   }
267
268   /* Restore the initial state */
269   simgrid::mc::session->restore_initial_state();
270
271   /* Traverse the stack from the state at position start and re-execute the transitions */
272   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
273     if (state == stack_.back())
274       break;
275     session->execute(state->transition_);
276     /* Update statistics */
277     mc_model_checker->visited_states++;
278     mc_model_checker->executed_transitions++;
279   }
280 }
281
282 SafetyChecker::SafetyChecker(Session& s) : Checker(s)
283 {
284   reductionMode_ = simgrid::mc::reduction_mode;
285   if (_sg_mc_termination)
286     reductionMode_ = simgrid::mc::ReductionMode::none;
287   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
288     reductionMode_ = simgrid::mc::ReductionMode::dpor;
289
290   if (_sg_mc_termination)
291     XBT_INFO("Check non progressive cycles");
292   else
293     XBT_INFO("Check a safety property. Reduction is: %s.",
294         (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
295             (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
296   simgrid::mc::session->initialize();
297
298   XBT_DEBUG("Starting the safety algorithm");
299
300   std::unique_ptr<simgrid::mc::State> initial_state =
301       std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
302
303   XBT_DEBUG("**************************************************");
304   XBT_DEBUG("Initial state");
305
306   /* Get an enabled actor and insert it in the interleave set of the initial state */
307   for (auto& actor : mc_model_checker->process().actors())
308     if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
309       initial_state->add_interleaving_set(actor.copy.get_buffer());
310       if (reductionMode_ != simgrid::mc::ReductionMode::none)
311         break;
312     }
313
314   stack_.push_back(std::move(initial_state));
315 }
316
317 Checker* createSafetyChecker(Session& s)
318 {
319   return new SafetyChecker(s);
320 }
321
322 }
323 }