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/dynar.h>
  14 #include <xbt/dynar.hpp>
  15 #include <xbt/fifo.h>
  16 #include <xbt/sysdep.h>
  17
  18 #include "src/mc/mc_state.h"
  19 #include "src/mc/mc_request.h"
  20 #include "src/mc/mc_safety.h"
  21 #include "src/mc/mc_private.h"
  22 #include "src/mc/mc_record.h"
  23 #include "src/mc/mc_smx.h"
  24 #include "src/mc/Client.hpp"
  25 #include "src/mc/mc_exit.h"
  26 #include "src/mc/Checker.hpp"
  27 #include "src/mc/SafetyChecker.hpp"
  28 #include "src/mc/VisitedState.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 void MC_show_non_termination(void)
  38 {
  39   XBT_INFO("******************************************");
  40   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  41   XBT_INFO("******************************************");
  42   XBT_INFO("Counter-example execution trace:");
  43   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  44     XBT_INFO("%s", s.c_str());
  45   MC_print_statistics(mc_stats);
  46 }
  47
  48 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  49 {
  50   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  51   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  52   int num1 = state1->num;
  53   int num2 = state2->num;
  54   return snapshot_compare(num1, s1, num2, s2);
  55 }
  56
  57 bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
  58 {
  59   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  60     if(snapshot_compare(*i, current_state) == 0){
  61       XBT_INFO("Non-progressive cycle : state %d -> state %d",
  62         (*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 (simgrid::mc::State* state : stack_) {
  72     int value = 0;
  73     smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
  74     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
  75     const int pid = issuer->pid;
  76     res.push_back(RecordTraceElement(pid, value));
  77   }
  78   return res;
  79 }
  80
  81 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  82 {
  83   std::vector<std::string> trace;
  84   for (simgrid::mc::State* state : stack_) {
  85     int value;
  86     smx_simcall_t req = MC_state_get_executed_request(state, &value);
  87     if (req) {
  88       char* req_str = simgrid::mc::request_to_string(
  89         req, value, simgrid::mc::RequestType::executed);
  90       trace.push_back(req_str);
  91       xbt_free(req_str);
  92     }
  93   }
  94   return trace;
  95 }
  96
  97 int SafetyChecker::run()
  98 {
  99   this->init();
 100
 101   char *req_str = nullptr;
 102   int value;
 103   smx_simcall_t req = nullptr;
 104   simgrid::mc::State* prev_state = nullptr;
 105   simgrid::mc::State* next_state = nullptr;
 106   xbt_fifo_item_t item = nullptr;
 107   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 108
 109   while (!stack_.empty()) {
 110
 111     /* Get current state */
 112     simgrid::mc::State* state = stack_.back();
 113
 114     XBT_DEBUG("**************************************************");
 115     XBT_DEBUG(
 116       "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
 117       stack_.size(), state, state->num,
 118       MC_state_interleave_size(state), user_max_depth_reached);
 119
 120     /* Update statistics */
 121     mc_stats->visited_states++;
 122
 123     /* If there are processes to interleave and the maximum depth has not been reached
 124        then perform one step of the exploration algorithm */
 125     if (stack_.size() <= _sg_mc_max_depth && !user_max_depth_reached
 126         && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
 127
 128       req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 129       XBT_DEBUG("Execute: %s", req_str);
 130       xbt_free(req_str);
 131
 132       if (dot_output != nullptr)
 133         req_str = simgrid::mc::request_get_dot_output(req, value);
 134
 135       MC_state_set_executed_request(state, req, value);
 136       mc_stats->executed_transitions++;
 137
 138       // TODO, bundle both operations in a single message
 139       //   MC_execute_transition(req, value)
 140
 141       /* Answer the request */
 142       simgrid::mc::handle_simcall(req, value);
 143       mc_model_checker->wait_for_requests();
 144
 145       /* Create the new expanded state */
 146       next_state = MC_state_new();
 147
 148       if (_sg_mc_termination && this->checkNonDeterminism(next_state)){
 149           MC_show_non_termination();
 150           return SIMGRID_MC_EXIT_NON_TERMINATION;
 151       }
 152
 153       if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
 154
 155         /* Get an enabled process and insert it in the interleave set of the next state */
 156         for (auto& p : mc_model_checker->process().simix_processes())
 157           if (simgrid::mc::process_is_enabled(&p.copy)) {
 158             MC_state_interleave_process(next_state, &p.copy);
 159             if (reductionMode_ != simgrid::mc::ReductionMode::none)
 160               break;
 161           }
 162
 163         if (dot_output != nullptr)
 164           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 165
 166       } else if (dot_output != nullptr)
 167         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 168
 169       stack_.push_back(next_state);
 170
 171       if (dot_output != nullptr)
 172         xbt_free(req_str);
 173
 174       /* Let's loop again */
 175
 176       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 177     } else {
 178
 179       if (stack_.size() > _sg_mc_max_depth || user_max_depth_reached
 180           || visited_state != nullptr) {
 181
 182         if (user_max_depth_reached && visited_state == nullptr)
 183           XBT_DEBUG("User max depth reached !");
 184         else if (visited_state == nullptr)
 185           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 186         else
 187           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);
 188
 189       } else
 190         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 191           stack_.size() + 1);
 192
 193       /* Trash the current state, no longer needed */
 194       stack_.pop_back();
 195       XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1);
 196       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 197
 198       visited_state = nullptr;
 199
 200       /* Check for deadlocks */
 201       if (mc_model_checker->checkDeadlock()) {
 202         MC_show_deadlock();
 203         return SIMGRID_MC_EXIT_DEADLOCK;
 204       }
 205
 206       /* Traverse the stack backwards until a state with a non empty interleave
 207          set is found, deleting all the states that have it empty in the way.
 208          For each deleted state, check if the request that has generated it
 209          (from it's predecesor state), depends on any other previous request
 210          executed before it. If it does then add it to the interleave set of the
 211          state that executed that previous request. */
 212
 213       while (!stack_.empty()) {
 214         state = stack_.back();
 215         stack_.pop_back();
 216         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 217           req = MC_state_get_internal_request(state);
 218           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 219             xbt_die("Mutex is currently not supported with DPOR, "
 220               "use --cfg=model-check/reduction:none");
 221           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 222           for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 223             simgrid::mc::State* prev_state = *i;
 224             if (reductionMode_ != simgrid::mc::ReductionMode::none
 225                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
 226               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 227                 XBT_DEBUG("Dependent Transitions:");
 228                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 229                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
 230                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 231                 xbt_free(req_str);
 232                 prev_req = MC_state_get_executed_request(state, &value);
 233                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
 234                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 235                 xbt_free(req_str);
 236               }
 237
 238               if (!MC_state_process_is_done(prev_state, issuer))
 239                 MC_state_interleave_process(prev_state, issuer);
 240               else
 241                 XBT_DEBUG("Process %p is in done set", req->issuer);
 242
 243               break;
 244
 245             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 246
 247               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 248               break;
 249
 250             } else {
 251
 252               const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 253               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 254                         req->call, issuer->pid, state->num,
 255                         MC_state_get_internal_request(prev_state)->call,
 256                         previous_issuer->pid,
 257                         prev_state->num);
 258
 259             }
 260           }
 261         }
 262
 263         if (MC_state_interleave_size(state)
 264             && stack_.size() < _sg_mc_max_depth) {
 265           /* We found a back-tracking point, let's loop */
 266           XBT_DEBUG("Back-tracking to state %d at depth %zi",
 267             state->num, stack_.size() + 1);
 268           stack_.push_back(state);
 269           simgrid::mc::replay(stack_);
 270           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 271             state->num, stack_.size());
 272           break;
 273         } else {
 274           XBT_DEBUG("Delete state %d at depth %zi",
 275             state->num, stack_.size() + 1);
 276           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 277         }
 278       }
 279     }
 280   }
 281
 282   XBT_INFO("No property violation found.");
 283   MC_print_statistics(mc_stats);
 284   initial_global_state = nullptr;
 285   return SIMGRID_MC_EXIT_SUCCESS;
 286 }
 287
 288 void SafetyChecker::init()
 289 {
 290   reductionMode_ = simgrid::mc::reduction_mode;
 291   if( _sg_mc_termination)
 292     reductionMode_ = simgrid::mc::ReductionMode::none;
 293   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 294     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 295
 296   if (_sg_mc_termination)
 297     XBT_INFO("Check non progressive cycles");
 298   else
 299     XBT_INFO("Check a safety property");
 300   mc_model_checker->wait_for_requests();
 301
 302   XBT_DEBUG("Starting the safety algorithm");
 303
 304   simgrid::mc::visited_states.clear();
 305
 306   simgrid::mc::State* initial_state = MC_state_new();
 307
 308   XBT_DEBUG("**************************************************");
 309   XBT_DEBUG("Initial state");
 310
 311   /* Wait for requests (schedules processes) */
 312   mc_model_checker->wait_for_requests();
 313
 314   /* Get an enabled process and insert it in the interleave set of the initial state */
 315   for (auto& p : mc_model_checker->process().simix_processes())
 316     if (simgrid::mc::process_is_enabled(&p.copy)) {
 317       MC_state_interleave_process(initial_state, &p.copy);
 318       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 319         break;
 320     }
 321
 322   stack_.push_back(initial_state);
 323
 324   /* Save the initial state */
 325   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 326   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 327 }
 328
 329 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 330 {
 331 }
 332
 333 SafetyChecker::~SafetyChecker()
 334 {
 335 }
 336
 337 }
 338 }