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
  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::checkNonDeterminism(simgrid::mc::State* current_state)
  57 {
  58   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  59     if(snapshot_compare(*i, 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 (simgrid::mc::State* state : stack_) {
  71     int value = 0;
  72     smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
  73     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
  74     const int pid = issuer->pid;
  75     res.push_back(RecordTraceElement(pid, value));
  76   }
  77   return res;
  78 }
  79
  80 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  81 {
  82   std::vector<std::string> trace;
  83   for (simgrid::mc::State* state : stack_) {
  84     int value;
  85     smx_simcall_t req = MC_state_get_executed_request(state, &value);
  86     if (req) {
  87       char* req_str = simgrid::mc::request_to_string(
  88         req, value, simgrid::mc::RequestType::executed);
  89       trace.push_back(req_str);
  90       xbt_free(req_str);
  91     }
  92   }
  93   return trace;
  94 }
  95
  96 int SafetyChecker::run()
  97 {
  98   this->init();
  99
 100   char *req_str = nullptr;
 101   int value;
 102   smx_simcall_t req = nullptr;
 103   simgrid::mc::State* prev_state = nullptr;
 104   simgrid::mc::State* next_state = nullptr;
 105   xbt_fifo_item_t item = nullptr;
 106   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 107
 108   while (!stack_.empty()) {
 109
 110     /* Get current state */
 111     simgrid::mc::State* state = stack_.back();
 112
 113     XBT_DEBUG("**************************************************");
 114     XBT_DEBUG(
 115       "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
 116       stack_.size(), state, state->num,
 117       MC_state_interleave_size(state), user_max_depth_reached);
 118
 119     /* Update statistics */
 120     mc_stats->visited_states++;
 121
 122     /* If there are processes to interleave and the maximum depth has not been reached
 123        then perform one step of the exploration algorithm */
 124     if (stack_.size() <= _sg_mc_max_depth && !user_max_depth_reached
 125         && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
 126
 127       req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 128       XBT_DEBUG("Execute: %s", req_str);
 129       xbt_free(req_str);
 130
 131       if (dot_output != nullptr)
 132         req_str = simgrid::mc::request_get_dot_output(req, value);
 133
 134       MC_state_set_executed_request(state, req, value);
 135       mc_stats->executed_transitions++;
 136
 137       // TODO, bundle both operations in a single message
 138       //   MC_execute_transition(req, value)
 139
 140       /* Answer the request */
 141       simgrid::mc::handle_simcall(req, value);
 142       mc_model_checker->wait_for_requests();
 143
 144       /* Create the new expanded state */
 145       next_state = MC_state_new();
 146
 147       if (_sg_mc_termination && this->checkNonDeterminism(next_state)){
 148           MC_show_non_termination();
 149           return SIMGRID_MC_EXIT_NON_TERMINATION;
 150       }
 151
 152       if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
 153
 154         /* Get an enabled process and insert it in the interleave set of the next state */
 155         for (auto& p : mc_model_checker->process().simix_processes())
 156           if (simgrid::mc::process_is_enabled(&p.copy)) {
 157             MC_state_interleave_process(next_state, &p.copy);
 158             if (reductionMode_ != simgrid::mc::ReductionMode::none)
 159               break;
 160           }
 161
 162         if (dot_output != nullptr)
 163           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 164
 165       } else if (dot_output != nullptr)
 166         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 167
 168       stack_.push_back(next_state);
 169
 170       if (dot_output != nullptr)
 171         xbt_free(req_str);
 172
 173       /* Let's loop again */
 174
 175       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 176     } else {
 177
 178       if (stack_.size() > _sg_mc_max_depth || user_max_depth_reached
 179           || visited_state != nullptr) {
 180
 181         if (user_max_depth_reached && visited_state == nullptr)
 182           XBT_DEBUG("User max depth reached !");
 183         else if (visited_state == nullptr)
 184           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 185         else
 186           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);
 187
 188       } else
 189         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 190           stack_.size() + 1);
 191
 192       /* Trash the current state, no longer needed */
 193       stack_.pop_back();
 194       XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1);
 195       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 196
 197       visited_state = nullptr;
 198
 199       /* Check for deadlocks */
 200       if (mc_model_checker->checkDeadlock()) {
 201         MC_show_deadlock();
 202         return SIMGRID_MC_EXIT_DEADLOCK;
 203       }
 204
 205       /* Traverse the stack backwards until a state with a non empty interleave
 206          set is found, deleting all the states that have it empty in the way.
 207          For each deleted state, check if the request that has generated it
 208          (from it's predecesor state), depends on any other previous request
 209          executed before it. If it does then add it to the interleave set of the
 210          state that executed that previous request. */
 211
 212       while (!stack_.empty()) {
 213         state = stack_.back();
 214         stack_.pop_back();
 215         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 216           req = MC_state_get_internal_request(state);
 217           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 218             xbt_die("Mutex is currently not supported with DPOR, "
 219               "use --cfg=model-check/reduction:none");
 220           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 221           for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 222             simgrid::mc::State* prev_state = *i;
 223             if (reductionMode_ != simgrid::mc::ReductionMode::none
 224                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
 225               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 226                 XBT_DEBUG("Dependent Transitions:");
 227                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 228                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
 229                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 230                 xbt_free(req_str);
 231                 prev_req = MC_state_get_executed_request(state, &value);
 232                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
 233                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 234                 xbt_free(req_str);
 235               }
 236
 237               if (!MC_state_process_is_done(prev_state, issuer))
 238                 MC_state_interleave_process(prev_state, issuer);
 239               else
 240                 XBT_DEBUG("Process %p is in done set", req->issuer);
 241
 242               break;
 243
 244             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 245
 246               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 247               break;
 248
 249             } else {
 250
 251               const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 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                         MC_state_get_internal_request(prev_state)->call,
 255                         previous_issuer->pid,
 256                         prev_state->num);
 257
 258             }
 259           }
 260         }
 261
 262         if (MC_state_interleave_size(state)
 263             && stack_.size() < _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(state);
 268           simgrid::mc::replay(stack_);
 269           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 270             state->num, stack_.size());
 271           break;
 272         } else {
 273           XBT_DEBUG("Delete state %d at depth %zi",
 274             state->num, stack_.size() + 1);
 275           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 276         }
 277       }
 278     }
 279   }
 280
 281   XBT_INFO("No property violation found.");
 282   MC_print_statistics(mc_stats);
 283   initial_global_state = nullptr;
 284   return SIMGRID_MC_EXIT_SUCCESS;
 285 }
 286
 287 void SafetyChecker::init()
 288 {
 289   reductionMode_ = simgrid::mc::reduction_mode;
 290   if( _sg_mc_termination)
 291     reductionMode_ = simgrid::mc::ReductionMode::none;
 292   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 293     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 294
 295   if (_sg_mc_termination)
 296     XBT_INFO("Check non progressive cycles");
 297   else
 298     XBT_INFO("Check a safety property");
 299   mc_model_checker->wait_for_requests();
 300
 301   XBT_DEBUG("Starting the safety algorithm");
 302
 303   simgrid::mc::visited_states.clear();
 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 }