Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
01c8f306c03f043fb921e302e90d489bd9a14e53
[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 i = stack_.rbegin(); i != stack_.rend(); ++i)
61     if (snapshot_compare(i->get(), current_state) == 0){
62       XBT_INFO("Non-progressive cycle: state %d -> state %d", (*i)->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   while (!stack_.empty()) {
100
101     /* Get current state */
102     simgrid::mc::State* state = stack_.back().get();
103
104     XBT_DEBUG("**************************************************");
105     XBT_DEBUG(
106       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
107       stack_.size(), state, state->num,
108       state->interleaveSize());
109
110     mc_model_checker->visited_states++;
111
112     // Backtrack if the interleave set is empty or the maximum depth is reached,
113     smx_simcall_t req = nullptr;
114     if (stack_.size() > (std::size_t) _sg_mc_max_depth
115         || (req = MC_state_get_request(state)) == nullptr
116         || visitedState_ != nullptr) {
117       int res = this->backtrack();
118       if (res)
119         return res;
120       else
121         continue;
122     }
123
124     // If there are processes to interleave and the maximum depth has not been
125     // reached then perform one step of the exploration algorithm.
126     XBT_DEBUG("Execute: %s",
127       simgrid::mc::request_to_string(
128         req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
129
130     std::string req_str;
131     if (dot_output != nullptr)
132       req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
133
134     mc_model_checker->executed_transitions++;
135
136     /* Answer the request */
137     this->getSession().execute(state->transition);
138
139     /* Create the new expanded state */
140     std::unique_ptr<simgrid::mc::State> next_state =
141         std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
142
143     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
144         MC_show_non_termination();
145         return SIMGRID_MC_EXIT_NON_TERMINATION;
146     }
147
148     if (_sg_mc_visited == 0
149         || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
150
151       /* Get an enabled process and insert it in the interleave set of the next state */
152       for (auto& actor : mc_model_checker->process().actors())
153         if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
154           next_state->interleave(actor.copy.getBuffer());
155           if (reductionMode_ != simgrid::mc::ReductionMode::none)
156             break;
157         }
158
159       if (dot_output != nullptr)
160         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
161           state->num, next_state->num, req_str.c_str());
162
163     } else if (dot_output != nullptr)
164       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
165         state->num,
166         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
167
168     stack_.push_back(std::move(next_state));
169   }
170
171   XBT_INFO("No property violation found.");
172   simgrid::mc::session->logState();
173   return SIMGRID_MC_EXIT_SUCCESS;
174 }
175
176 int SafetyChecker::backtrack()
177 {
178   if (stack_.size() > (std::size_t) _sg_mc_max_depth
179       || visitedState_ != nullptr) {
180     if (visitedState_ == nullptr)
181       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
182     else
183       XBT_DEBUG("State already visited (equal to state %d),"
184         " exploration stopped on this path.",
185         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
186   } else
187     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
188       stack_.size() + 1);
189
190   stack_.pop_back();
191
192   visitedState_ = nullptr;
193
194   /* Check for deadlocks */
195   if (mc_model_checker->checkDeadlock()) {
196     MC_show_deadlock();
197     return SIMGRID_MC_EXIT_DEADLOCK;
198   }
199
200   /* Traverse the stack backwards until a state with a non empty interleave
201      set is found, deleting all the states that have it empty in the way.
202      For each deleted state, check if the request that has generated it 
203      (from it's predecesor state), depends on any other previous request 
204      executed before it. If it does then add it to the interleave set of the
205      state that executed that previous request. */
206
207   while (!stack_.empty()) {
208     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
209     stack_.pop_back();
210     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
211       smx_simcall_t req = &state->internal_req;
212       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
213         xbt_die("Mutex is currently not supported with DPOR, "
214           "use --cfg=model-check/reduction:none");
215       const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
216       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
217         simgrid::mc::State* prev_state = i->get();
218         if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
219           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
220             XBT_DEBUG("Dependent Transitions:");
221             int value = prev_state->transition.argument;
222             smx_simcall_t prev_req = &prev_state->executed_req;
223             XBT_DEBUG("%s (state=%d)",
224               simgrid::mc::request_to_string(
225                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
226               prev_state->num);
227             value = state->transition.argument;
228             prev_req = &state->executed_req;
229             XBT_DEBUG("%s (state=%d)",
230               simgrid::mc::request_to_string(
231                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
232               state->num);
233           }
234
235           if (!prev_state->processStates[issuer->pid].isDone())
236             prev_state->interleave(issuer);
237           else
238             XBT_DEBUG("Process %p is in done set", req->issuer);
239
240           break;
241
242         } else if (req->issuer == prev_state->internal_req.issuer) {
243
244           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
245           break;
246
247         } else {
248
249           const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
250           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
251                     req->call, issuer->pid, state->num,
252                     prev_state->internal_req.call,
253                     previous_issuer->pid,
254                     prev_state->num);
255
256         }
257       }
258     }
259
260     if (state->interleaveSize()
261         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
262       /* We found a back-tracking point, let's loop */
263       XBT_DEBUG("Back-tracking to state %d at depth %zi",
264         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   return SIMGRID_MC_EXIT_SUCCESS;
276 }
277
278 void SafetyChecker::restoreState()
279 {
280   /* Intermediate backtracking */
281   simgrid::mc::State* state = stack_.back().get();
282   if (state->system_state) {
283     simgrid::mc::restore_snapshot(state->system_state);
284     return;
285   }
286
287   /* Restore the initial state */
288   simgrid::mc::session->restoreInitialState();
289
290   /* Traverse the stack from the state at position start and re-execute the transitions */
291   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
292     if (state == stack_.back())
293       break;
294     session->execute(state->transition);
295     /* Update statistics */
296     mc_model_checker->visited_states++;
297     mc_model_checker->executed_transitions++;
298   }
299 }
300
301 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
302 {
303   reductionMode_ = simgrid::mc::reduction_mode;
304   if (_sg_mc_termination)
305     reductionMode_ = simgrid::mc::ReductionMode::none;
306   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
307     reductionMode_ = simgrid::mc::ReductionMode::dpor;
308
309   if (_sg_mc_termination)
310     XBT_INFO("Check non progressive cycles");
311   else
312     XBT_INFO("Check a safety property");
313   simgrid::mc::session->initialize();
314
315   XBT_DEBUG("Starting the safety algorithm");
316
317   std::unique_ptr<simgrid::mc::State> initial_state =
318       std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
319
320   XBT_DEBUG("**************************************************");
321   XBT_DEBUG("Initial state");
322
323   /* Get an enabled actor and insert it in the interleave set of the initial state */
324   for (auto& actor : mc_model_checker->process().actors())
325     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
326       initial_state->interleave(actor.copy.getBuffer());
327       if (reductionMode_ != simgrid::mc::ReductionMode::none)
328         break;
329     }
330
331   stack_.push_back(std::move(initial_state));
332 }
333
334 SafetyChecker::~SafetyChecker()
335 {
336 }
337
338 Checker* createSafetyChecker(Session& session)
339 {
340   return new SafetyChecker(session);
341 }
342   
343 }
344 }