Logo AND Algorithmique Numérique Distribuée

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