Logo AND Algorithmique Numérique Distribuée

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