Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Get rid of the ugly "value" out parameter in MC_state_get_request()
[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
29 #include "src/xbt/mmalloc/mmprivate.h"
30
31 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
32                                 "Logging specific to MC safety verification ");
33 namespace simgrid {
34 namespace mc {
35
36 static void MC_show_non_termination(void)
37 {
38   XBT_INFO("******************************************");
39   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
40   XBT_INFO("******************************************");
41   XBT_INFO("Counter-example execution trace:");
42   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
43     XBT_INFO("%s", s.c_str());
44   MC_print_statistics(mc_stats);
45 }
46
47 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
48 {
49   simgrid::mc::Snapshot* s1 = state1->system_state.get();
50   simgrid::mc::Snapshot* s2 = state2->system_state.get();
51   int num1 = state1->num;
52   int num2 = state2->num;
53   return snapshot_compare(num1, s1, num2, s2);
54 }
55
56 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
57 {
58   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
59     if (snapshot_compare(i->get(), current_state) == 0){
60       XBT_INFO("Non-progressive cycle : state %d -> state %d",
61         (*i)->num, current_state->num);
62       return true;
63     }
64   return false;
65 }
66
67 RecordTrace SafetyChecker::getRecordTrace() // override
68 {
69   RecordTrace res;
70   for (auto const& state : stack_)
71     res.push_back(state->getRecordElement());
72   return res;
73 }
74
75 std::vector<std::string> SafetyChecker::getTextualTrace() // override
76 {
77   std::vector<std::string> trace;
78   for (auto const& state : stack_) {
79     int value = state->req_num;
80     smx_simcall_t req = &state->executed_req;
81     if (req)
82       trace.push_back(simgrid::mc::request_to_string(
83         req, value, simgrid::mc::RequestType::executed));
84   }
85   return trace;
86 }
87
88 int SafetyChecker::run()
89 {
90   this->init();
91
92   while (!stack_.empty()) {
93
94     /* Get current state */
95     simgrid::mc::State* state = stack_.back().get();
96
97     XBT_DEBUG("**************************************************");
98     XBT_DEBUG(
99       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
100       stack_.size(), state, state->num,
101       state->interleaveSize());
102
103     mc_stats->visited_states++;
104
105     // The interleave set is empty or the maximum depth is reached,
106     // let's back-track.
107     smx_simcall_t req = nullptr;
108     if (stack_.size() > (std::size_t) _sg_mc_max_depth
109         || (req = MC_state_get_request(state)) == nullptr
110         || visitedState_ != nullptr) {
111       int res = this->backtrack();
112       if (res)
113         return res;
114       else
115         continue;
116     }
117
118     int req_num = state->req_num;
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, req_num, 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, req_num);
129
130     mc_stats->executed_transitions++;
131
132     // TODO, bundle both operations in a single message
133     //   MC_execute_transition(req, req_num)
134
135     /* Answer the request */
136     simgrid::mc::handle_simcall(req, req_num);
137     mc_model_checker->wait_for_requests();
138
139     /* Create the new expanded state */
140     std::unique_ptr<simgrid::mc::State> next_state =
141       std::unique_ptr<simgrid::mc::State>(MC_state_new());
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(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& p : mc_model_checker->process().simix_processes())
153         if (simgrid::mc::process_is_enabled(&p.copy)) {
154           next_state->interleave(&p.copy);
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   MC_print_statistics(mc_stats);
173   initial_global_state = nullptr;
174   return SIMGRID_MC_EXIT_SUCCESS;
175 }
176
177 int SafetyChecker::backtrack()
178 {
179   if (stack_.size() > (std::size_t) _sg_mc_max_depth
180       || visitedState_ != nullptr) {
181     if (visitedState_ == nullptr)
182       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
183     else
184       XBT_DEBUG("State already visited (equal to state %d),"
185         " exploration stopped on this path.",
186         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
187   } else
188     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
189       stack_.size() + 1);
190
191   stack_.pop_back();
192
193   visitedState_ = nullptr;
194
195   /* Check for deadlocks */
196   if (mc_model_checker->checkDeadlock()) {
197     MC_show_deadlock();
198     return SIMGRID_MC_EXIT_DEADLOCK;
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 predecesor 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, "
215           "use --cfg=model-check/reduction:none");
216       const smx_process_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 (reductionMode_ != simgrid::mc::ReductionMode::none
220             && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
221           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
222             XBT_DEBUG("Dependent Transitions:");
223             int value = prev_state->req_num;
224             smx_simcall_t prev_req = &prev_state->executed_req;
225             XBT_DEBUG("%s (state=%d)",
226               simgrid::mc::request_to_string(
227                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
228               prev_state->num);
229             value = state->req_num;
230             prev_req = &state->executed_req;
231             XBT_DEBUG("%s (state=%d)",
232               simgrid::mc::request_to_string(
233                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
234               state->num);
235           }
236
237           if (!prev_state->processStates[issuer->pid].isDone())
238             prev_state->interleave(issuer);
239           else
240             XBT_DEBUG("Process %p is in done set", req->issuer);
241
242           break;
243
244         } else if (req->issuer == prev_state->internal_req.issuer) {
245
246           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
247           break;
248
249         } else {
250
251           const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
252           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
253                     req->call, issuer->pid, state->num,
254                     prev_state->internal_req.call,
255                     previous_issuer->pid,
256                     prev_state->num);
257
258         }
259       }
260     }
261
262     if (state->interleaveSize()
263         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
264       /* We found a back-tracking point, let's loop */
265       XBT_DEBUG("Back-tracking to state %d at depth %zi",
266         state->num, stack_.size() + 1);
267       stack_.push_back(std::move(state));
268       simgrid::mc::replay(stack_);
269       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
270         stack_.back()->num, stack_.size());
271       break;
272     } else {
273       XBT_DEBUG("Delete state %d at depth %zi",
274         state->num, stack_.size() + 1);
275     }
276   }
277   return SIMGRID_MC_EXIT_SUCCESS;
278 }
279
280 void SafetyChecker::init()
281 {
282   reductionMode_ = simgrid::mc::reduction_mode;
283   if( _sg_mc_termination)
284     reductionMode_ = simgrid::mc::ReductionMode::none;
285   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
286     reductionMode_ = simgrid::mc::ReductionMode::dpor;
287
288   if (_sg_mc_termination)
289     XBT_INFO("Check non progressive cycles");
290   else
291     XBT_INFO("Check a safety property");
292   mc_model_checker->wait_for_requests();
293
294   XBT_DEBUG("Starting the safety algorithm");
295
296   std::unique_ptr<simgrid::mc::State> initial_state =
297     std::unique_ptr<simgrid::mc::State>(MC_state_new());
298
299   XBT_DEBUG("**************************************************");
300   XBT_DEBUG("Initial state");
301
302   /* Wait for requests (schedules processes) */
303   mc_model_checker->wait_for_requests();
304
305   /* Get an enabled process and insert it in the interleave set of the initial state */
306   for (auto& p : mc_model_checker->process().simix_processes())
307     if (simgrid::mc::process_is_enabled(&p.copy)) {
308       initial_state->interleave(&p.copy);
309       if (reductionMode_ != simgrid::mc::ReductionMode::none)
310         break;
311     }
312
313   stack_.push_back(std::move(initial_state));
314
315   /* Save the initial state */
316   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
317   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
318 }
319
320 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
321 {
322 }
323
324 SafetyChecker::~SafetyChecker()
325 {
326 }
327
328 Checker* createSafetyChecker(Session& session)
329 {
330   return new SafetyChecker(session);
331 }
332   
333 }
334 }