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 }