Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Remove user_max_depth which back up MC_cut() for now
[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 <list>
11
12 #include <xbt/log.h>
13 #include <xbt/sysdep.h>
14
15 #include "src/mc/mc_state.h"
16 #include "src/mc/mc_request.h"
17 #include "src/mc/mc_safety.h"
18 #include "src/mc/mc_private.h"
19 #include "src/mc/mc_record.h"
20 #include "src/mc/mc_smx.h"
21 #include "src/mc/Client.hpp"
22 #include "src/mc/mc_exit.h"
23 #include "src/mc/Checker.hpp"
24 #include "src/mc/SafetyChecker.hpp"
25 #include "src/mc/VisitedState.hpp"
26
27 #include "src/xbt/mmalloc/mmprivate.h"
28
29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
30                                 "Logging specific to MC safety verification ");
31 namespace simgrid {
32 namespace mc {
33
34 static void MC_show_non_termination(void)
35 {
36   XBT_INFO("******************************************");
37   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
38   XBT_INFO("******************************************");
39   XBT_INFO("Counter-example execution trace:");
40   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
41     XBT_INFO("%s", s.c_str());
42   MC_print_statistics(mc_stats);
43 }
44
45 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
46 {
47   simgrid::mc::Snapshot* s1 = state1->system_state.get();
48   simgrid::mc::Snapshot* s2 = state2->system_state.get();
49   int num1 = state1->num;
50   int num2 = state2->num;
51   return snapshot_compare(num1, s1, num2, s2);
52 }
53
54 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
55 {
56   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
57     if (snapshot_compare(i->get(), current_state) == 0){
58       XBT_INFO("Non-progressive cycle : state %d -> state %d",
59         (*i)->num, current_state->num);
60       return true;
61     }
62   return false;
63 }
64
65 RecordTrace SafetyChecker::getRecordTrace() // override
66 {
67   RecordTrace res;
68   for (auto const& state : stack_) {
69     int value = 0;
70     smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
71     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
72     const int pid = issuer->pid;
73     res.push_back(RecordTraceElement(pid, value));
74   }
75   return res;
76 }
77
78 std::vector<std::string> SafetyChecker::getTextualTrace() // override
79 {
80   std::vector<std::string> trace;
81   for (auto const& state : stack_) {
82     int value;
83     smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
84     if (req) {
85       char* req_str = simgrid::mc::request_to_string(
86         req, value, simgrid::mc::RequestType::executed);
87       trace.push_back(req_str);
88       xbt_free(req_str);
89     }
90   }
91   return trace;
92 }
93
94 int SafetyChecker::run()
95 {
96   this->init();
97
98   int value;
99   smx_simcall_t req = nullptr;
100   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
101
102   while (!stack_.empty()) {
103
104     /* Get current state */
105     simgrid::mc::State* state = stack_.back().get();
106
107     XBT_DEBUG("**************************************************");
108     XBT_DEBUG(
109       "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
110       stack_.size(), state, state->num,
111       MC_state_interleave_size(state));
112
113     /* Update statistics */
114     mc_stats->visited_states++;
115
116     /* If there are processes to interleave and the maximum depth has not been reached
117        then perform one step of the exploration algorithm */
118     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
119         && (req = MC_state_get_request(state, &value))
120         && visited_state == nullptr) {
121
122       char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
123       XBT_DEBUG("Execute: %s", req_str);
124       xbt_free(req_str);
125
126       if (dot_output != nullptr)
127         req_str = simgrid::mc::request_get_dot_output(req, value);
128
129       MC_state_set_executed_request(state, req, value);
130       mc_stats->executed_transitions++;
131
132       // TODO, bundle both operations in a single message
133       //   MC_execute_transition(req, value)
134
135       /* Answer the request */
136       simgrid::mc::handle_simcall(req, value);
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           || (visited_state = 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             MC_state_interleave_process(next_state.get(), &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", state->num, next_state->num, req_str);
161
162       } else if (dot_output != nullptr)
163         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
164
165       stack_.push_back(std::move(next_state));
166
167       if (dot_output != nullptr)
168         xbt_free(req_str);
169
170       /* Let's loop again */
171
172       /* The interleave set is empty or the maximum depth is reached, let's back-track */
173     } else {
174
175       if (stack_.size() > (std::size_t) _sg_mc_max_depth
176           || visited_state != nullptr) {
177
178         if (visited_state == nullptr)
179           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
180         else
181           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
182
183       } else
184         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
185           stack_.size() + 1);
186
187       /* Trash the current state, no longer needed */
188       XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
189       stack_.pop_back();
190
191       visited_state = nullptr;
192
193       /* Check for deadlocks */
194       if (mc_model_checker->checkDeadlock()) {
195         MC_show_deadlock();
196         return SIMGRID_MC_EXIT_DEADLOCK;
197       }
198
199       /* Traverse the stack backwards until a state with a non empty interleave
200          set is found, deleting all the states that have it empty in the way.
201          For each deleted state, check if the request that has generated it 
202          (from it's predecesor state), depends on any other previous request 
203          executed before it. If it does then add it to the interleave set of the
204          state that executed that previous request. */
205
206       while (!stack_.empty()) {
207         std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
208         stack_.pop_back();
209         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
210           req = MC_state_get_internal_request(state.get());
211           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
212             xbt_die("Mutex is currently not supported with DPOR, "
213               "use --cfg=model-check/reduction:none");
214           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
215           for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
216             simgrid::mc::State* prev_state = i->get();
217             if (reductionMode_ != simgrid::mc::ReductionMode::none
218                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
219               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
220                 XBT_DEBUG("Dependent Transitions:");
221                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
222                 char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
223                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
224                 xbt_free(req_str);
225                 prev_req = MC_state_get_executed_request(state.get(), &value);
226                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
227                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
228                 xbt_free(req_str);
229               }
230
231               if (!MC_state_process_is_done(prev_state, issuer))
232                 MC_state_interleave_process(prev_state, issuer);
233               else
234                 XBT_DEBUG("Process %p is in done set", req->issuer);
235
236               break;
237
238             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
239
240               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
241               break;
242
243             } else {
244
245               const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
246               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
247                         req->call, issuer->pid, state->num,
248                         MC_state_get_internal_request(prev_state)->call,
249                         previous_issuer->pid,
250                         prev_state->num);
251
252             }
253           }
254         }
255
256         if (MC_state_interleave_size(state.get())
257             && stack_.size() < (std::size_t) _sg_mc_max_depth) {
258           /* We found a back-tracking point, let's loop */
259           XBT_DEBUG("Back-tracking to state %d at depth %zi",
260             state->num, stack_.size() + 1);
261           stack_.push_back(std::move(state));
262           simgrid::mc::replay(stack_);
263           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
264             stack_.back()->num, stack_.size());
265           break;
266         } else {
267           XBT_DEBUG("Delete state %d at depth %zi",
268             state->num, stack_.size() + 1);
269         }
270       }
271     }
272   }
273
274   XBT_INFO("No property violation found.");
275   MC_print_statistics(mc_stats);
276   initial_global_state = nullptr;
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       MC_state_interleave_process(initial_state.get(), &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 }