Logo AND Algorithmique Numérique Distribuée

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