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
 154           || (visited_state = visitedStates_.addVisitedState(next_state, true)) == nullptr) {
 155
 156         /* Get an enabled process and insert it in the interleave set of the next state */
 157         for (auto& p : mc_model_checker->process().simix_processes())
 158           if (simgrid::mc::process_is_enabled(&p.copy)) {
 159             MC_state_interleave_process(next_state, &p.copy);
 160             if (reductionMode_ != simgrid::mc::ReductionMode::none)
 161               break;
 162           }
 163
 164         if (dot_output != nullptr)
 165           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 166
 167       } else if (dot_output != nullptr)
 168         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 169
 170       stack_.push_back(next_state);
 171
 172       if (dot_output != nullptr)
 173         xbt_free(req_str);
 174
 175       /* Let's loop again */
 176
 177       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 178     } else {
 179
 180       if (stack_.size() > _sg_mc_max_depth || user_max_depth_reached
 181           || visited_state != nullptr) {
 182
 183         if (user_max_depth_reached && visited_state == nullptr)
 184           XBT_DEBUG("User max depth reached !");
 185         else if (visited_state == nullptr)
 186           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 187         else
 188           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);
 189
 190       } else
 191         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 192           stack_.size() + 1);
 193
 194       /* Trash the current state, no longer needed */
 195       stack_.pop_back();
 196       XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1);
 197       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 198
 199       visited_state = nullptr;
 200
 201       /* Check for deadlocks */
 202       if (mc_model_checker->checkDeadlock()) {
 203         MC_show_deadlock();
 204         return SIMGRID_MC_EXIT_DEADLOCK;
 205       }
 206
 207       /* Traverse the stack backwards until a state with a non empty interleave
 208          set is found, deleting all the states that have it empty in the way.
 209          For each deleted state, check if the request that has generated it
 210          (from it's predecesor state), depends on any other previous request
 211          executed before it. If it does then add it to the interleave set of the
 212          state that executed that previous request. */
 213
 214       while (!stack_.empty()) {
 215         state = stack_.back();
 216         stack_.pop_back();
 217         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 218           req = MC_state_get_internal_request(state);
 219           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 220             xbt_die("Mutex is currently not supported with DPOR, "
 221               "use --cfg=model-check/reduction:none");
 222           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 223           for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 224             simgrid::mc::State* prev_state = *i;
 225             if (reductionMode_ != simgrid::mc::ReductionMode::none
 226                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
 227               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 228                 XBT_DEBUG("Dependent Transitions:");
 229                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 230                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
 231                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 232                 xbt_free(req_str);
 233                 prev_req = MC_state_get_executed_request(state, &value);
 234                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
 235                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 236                 xbt_free(req_str);
 237               }
 238
 239               if (!MC_state_process_is_done(prev_state, issuer))
 240                 MC_state_interleave_process(prev_state, issuer);
 241               else
 242                 XBT_DEBUG("Process %p is in done set", req->issuer);
 243
 244               break;
 245
 246             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 247
 248               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 249               break;
 250
 251             } else {
 252
 253               const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 254               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 255                         req->call, issuer->pid, state->num,
 256                         MC_state_get_internal_request(prev_state)->call,
 257                         previous_issuer->pid,
 258                         prev_state->num);
 259
 260             }
 261           }
 262         }
 263
 264         if (MC_state_interleave_size(state)
 265             && stack_.size() < _sg_mc_max_depth) {
 266           /* We found a back-tracking point, let's loop */
 267           XBT_DEBUG("Back-tracking to state %d at depth %zi",
 268             state->num, stack_.size() + 1);
 269           stack_.push_back(state);
 270           simgrid::mc::replay(stack_);
 271           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 272             state->num, stack_.size());
 273           break;
 274         } else {
 275           XBT_DEBUG("Delete state %d at depth %zi",
 276             state->num, stack_.size() + 1);
 277           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 278         }
 279       }
 280     }
 281   }
 282
 283   XBT_INFO("No property violation found.");
 284   MC_print_statistics(mc_stats);
 285   initial_global_state = nullptr;
 286   return SIMGRID_MC_EXIT_SUCCESS;
 287 }
 288
 289 void SafetyChecker::init()
 290 {
 291   reductionMode_ = simgrid::mc::reduction_mode;
 292   if( _sg_mc_termination)
 293     reductionMode_ = simgrid::mc::ReductionMode::none;
 294   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 295     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 296
 297   if (_sg_mc_termination)
 298     XBT_INFO("Check non progressive cycles");
 299   else
 300     XBT_INFO("Check a safety property");
 301   mc_model_checker->wait_for_requests();
 302
 303   XBT_DEBUG("Starting the safety algorithm");
 304
 305   simgrid::mc::State* initial_state = MC_state_new();
 306
 307   XBT_DEBUG("**************************************************");
 308   XBT_DEBUG("Initial state");
 309
 310   /* Wait for requests (schedules processes) */
 311   mc_model_checker->wait_for_requests();
 312
 313   /* Get an enabled process and insert it in the interleave set of the initial state */
 314   for (auto& p : mc_model_checker->process().simix_processes())
 315     if (simgrid::mc::process_is_enabled(&p.copy)) {
 316       MC_state_interleave_process(initial_state, &p.copy);
 317       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 318         break;
 319     }
 320
 321   stack_.push_back(initial_state);
 322
 323   /* Save the initial state */
 324   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 325   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 326 }
 327
 328 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 329 {
 330 }
 331
 332 SafetyChecker::~SafetyChecker()
 333 {
 334 }
 335
 336 }
 337 }