Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Remove useless model-checker/model-checked round trip
[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   MC_print_statistics(mc_stats);
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",
63         (*i)->num, current_state->num);
64       return true;
65     }
66   return false;
67 }
68
69 RecordTrace SafetyChecker::getRecordTrace() // override
70 {
71   RecordTrace res;
72   for (auto const& state : stack_)
73     res.push_back(state->getTransition());
74   return res;
75 }
76
77 std::vector<std::string> SafetyChecker::getTextualTrace() // override
78 {
79   std::vector<std::string> trace;
80   for (auto const& state : stack_) {
81     int value = state->transition.argument;
82     smx_simcall_t req = &state->executed_req;
83     if (req)
84       trace.push_back(simgrid::mc::request_to_string(
85         req, value, simgrid::mc::RequestType::executed));
86   }
87   return trace;
88 }
89
90 int SafetyChecker::run()
91 {
92   this->init();
93
94   while (!stack_.empty()) {
95
96     /* Get current state */
97     simgrid::mc::State* state = stack_.back().get();
98
99     XBT_DEBUG("**************************************************");
100     XBT_DEBUG(
101       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
102       stack_.size(), state, state->num,
103       state->interleaveSize());
104
105     mc_stats->visited_states++;
106
107     // The interleave set is empty or the maximum depth is reached,
108     // let's back-track.
109     smx_simcall_t req = nullptr;
110     if (stack_.size() > (std::size_t) _sg_mc_max_depth
111         || (req = MC_state_get_request(state)) == nullptr
112         || visitedState_ != nullptr) {
113       int res = this->backtrack();
114       if (res)
115         return res;
116       else
117         continue;
118     }
119
120     // If there are processes to interleave and the maximum depth has not been
121     // reached then perform one step of the exploration algorithm.
122     XBT_DEBUG("Execute: %s",
123       simgrid::mc::request_to_string(
124         req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
125
126     std::string req_str;
127     if (dot_output != nullptr)
128       req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
129
130     mc_stats->executed_transitions++;
131
132     /* Answer the request */
133     this->getSession().execute(state->transition);
134
135     /* Create the new expanded state */
136     std::unique_ptr<simgrid::mc::State> next_state =
137       std::unique_ptr<simgrid::mc::State>(MC_state_new());
138
139     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
140         MC_show_non_termination();
141         return SIMGRID_MC_EXIT_NON_TERMINATION;
142     }
143
144     if (_sg_mc_visited == 0
145         || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
146
147       /* Get an enabled process and insert it in the interleave set of the next state */
148       for (auto& p : mc_model_checker->process().simix_processes())
149         if (simgrid::mc::process_is_enabled(&p.copy)) {
150           next_state->interleave(&p.copy);
151           if (reductionMode_ != simgrid::mc::ReductionMode::none)
152             break;
153         }
154
155       if (dot_output != nullptr)
156         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
157           state->num, next_state->num, req_str.c_str());
158
159     } else if (dot_output != nullptr)
160       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
161         state->num,
162         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
163
164     stack_.push_back(std::move(next_state));
165   }
166
167   XBT_INFO("No property violation found.");
168   MC_print_statistics(mc_stats);
169   initial_global_state = nullptr;
170   return SIMGRID_MC_EXIT_SUCCESS;
171 }
172
173 int SafetyChecker::backtrack()
174 {
175   if (stack_.size() > (std::size_t) _sg_mc_max_depth
176       || visitedState_ != nullptr) {
177     if (visitedState_ == nullptr)
178       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
179     else
180       XBT_DEBUG("State already visited (equal to state %d),"
181         " exploration stopped on this path.",
182         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
183   } else
184     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
185       stack_.size() + 1);
186
187   stack_.pop_back();
188
189   visitedState_ = nullptr;
190
191   /* Check for deadlocks */
192   if (mc_model_checker->checkDeadlock()) {
193     MC_show_deadlock();
194     return SIMGRID_MC_EXIT_DEADLOCK;
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 predecesor 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 (!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, "
211           "use --cfg=model-check/reduction:none");
212       const smx_process_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 (reductionMode_ != simgrid::mc::ReductionMode::none
216             && 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 (!prev_state->processStates[issuer->pid].isDone())
234             prev_state->interleave(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_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
248           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
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 %zi",
262         state->num, stack_.size() + 1);
263       stack_.push_back(std::move(state));
264       simgrid::mc::replay(stack_);
265       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
266         stack_.back()->num, stack_.size());
267       break;
268     } else {
269       XBT_DEBUG("Delete state %d at depth %zi",
270         state->num, stack_.size() + 1);
271     }
272   }
273   return SIMGRID_MC_EXIT_SUCCESS;
274 }
275
276 void SafetyChecker::init()
277 {
278   reductionMode_ = simgrid::mc::reduction_mode;
279   if( _sg_mc_termination)
280     reductionMode_ = simgrid::mc::ReductionMode::none;
281   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
282     reductionMode_ = simgrid::mc::ReductionMode::dpor;
283
284   if (_sg_mc_termination)
285     XBT_INFO("Check non progressive cycles");
286   else
287     XBT_INFO("Check a safety property");
288   mc_model_checker->wait_for_requests();
289
290   XBT_DEBUG("Starting the safety algorithm");
291
292   std::unique_ptr<simgrid::mc::State> initial_state =
293     std::unique_ptr<simgrid::mc::State>(MC_state_new());
294
295   XBT_DEBUG("**************************************************");
296   XBT_DEBUG("Initial state");
297
298   /* Get an enabled process and insert it in the interleave set of the initial state */
299   for (auto& p : mc_model_checker->process().simix_processes())
300     if (simgrid::mc::process_is_enabled(&p.copy)) {
301       initial_state->interleave(&p.copy);
302       if (reductionMode_ != simgrid::mc::ReductionMode::none)
303         break;
304     }
305
306   stack_.push_back(std::move(initial_state));
307
308   /* Save the initial state */
309   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
310   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
311 }
312
313 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
314 {
315 }
316
317 SafetyChecker::~SafetyChecker()
318 {
319 }
320
321 Checker* createSafetyChecker(Session& session)
322 {
323   return new SafetyChecker(session);
324 }
325   
326 }
327 }