Logo AND Algorithmique Numérique Distribuée

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