src/mc/LivenessChecker.cpp

   1 /* Copyright (c) 2011-2015. 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 <cstring>
   8
   9 #include <algorithm>
  10 #include <memory>
  11 #include <list>
  12
  13 #include <unistd.h>
  14 #include <sys/wait.h>
  15
  16 #include <xbt/automaton.h>
  17 #include <xbt/dynar.h>
  18 #include <xbt/dynar.hpp>
  19 #include <xbt/log.h>
  20 #include <xbt/sysdep.h>
  21
  22 #include "src/mc/mc_request.h"
  23 #include "src/mc/LivenessChecker.hpp"
  24 #include "src/mc/mc_private.h"
  25 #include "src/mc/mc_record.h"
  26 #include "src/mc/mc_smx.h"
  27 #include "src/mc/Client.hpp"
  28 #include "src/mc/mc_private.h"
  29 #include "src/mc/mc_replay.h"
  30 #include "src/mc/mc_safety.h"
  31 #include "src/mc/mc_exit.h"
  32 #include "src/mc/Transition.hpp"
  33
  34 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  35                                 "Logging specific to algorithms for liveness properties verification");
  36
  37 /********* Static functions *********/
  38
  39 namespace simgrid {
  40 namespace mc {
  41
  42 VisitedPair::VisitedPair(
  43   int pair_num, xbt_automaton_state_t automaton_state,
  44   std::shared_ptr<const std::vector<int>> atomic_propositions,
  45   std::shared_ptr<simgrid::mc::State> graph_state)
  46 {
  47   simgrid::mc::Process* process = &(mc_model_checker->process());
  48
  49   this->graph_state = std::move(graph_state);
  50   if(this->graph_state->system_state == nullptr)
  51     this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
  52   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
  53     process->get_heap()->heaplimit,
  54     process->get_malloc_info());
  55
  56   this->nb_processes = mc_model_checker->process().simix_processes().size();
  57
  58   this->automaton_state = automaton_state;
  59   this->num = pair_num;
  60   this->other_num = -1;
  61   this->atomic_propositions = std::move(atomic_propositions);
  62 }
  63
  64 VisitedPair::~VisitedPair()
  65 {
  66 }
  67
  68 static bool evaluate_label(
  69   xbt_automaton_exp_label_t l, std::vector<int> const& values)
  70 {
  71   switch (l->type) {
  72   case xbt_automaton_exp_label::AUT_OR:
  73     return evaluate_label(l->u.or_and.left_exp, values)
  74       || evaluate_label(l->u.or_and.right_exp, values);
  75   case xbt_automaton_exp_label::AUT_AND:
  76     return evaluate_label(l->u.or_and.left_exp, values)
  77       && evaluate_label(l->u.or_and.right_exp, values);
  78   case xbt_automaton_exp_label::AUT_NOT:
  79     return !evaluate_label(l->u.exp_not, values);
  80   case xbt_automaton_exp_label::AUT_PREDICAT:{
  81       unsigned int cursor = 0;
  82       xbt_automaton_propositional_symbol_t p = nullptr;
  83       xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
  84         if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
  85           return values[cursor] != 0;
  86       }
  87       xbt_die("Missing predicate");
  88     }
  89   case xbt_automaton_exp_label::AUT_ONE:
  90     return true;
  91   default:
  92     xbt_die("Unexpected vaue for automaton");
  93   }
  94 }
  95
  96 Pair::Pair() : num(++mc_stats->expanded_pairs)
  97 {}
  98
  99 Pair::~Pair() {}
 100
 101 std::shared_ptr<const std::vector<int>> LivenessChecker::getPropositionValues()
 102 {
 103   std::vector<int> values;
 104   unsigned int cursor = 0;
 105   xbt_automaton_propositional_symbol_t ps = nullptr;
 106   xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, ps)
 107     values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
 108   return std::make_shared<const std::vector<int>>(std::move(values));
 109 }
 110
 111 int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
 112 {
 113   simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get();
 114   simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get();
 115   int num1 = state1->num;
 116   int num2 = state2->num;
 117   return simgrid::mc::snapshot_compare(num1, s1, num2, s2);
 118 }
 119
 120 std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
 121 {
 122   std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
 123     pair->num, pair->automaton_state, pair->atomic_propositions,
 124     pair->graph_state);
 125
 126   auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(),
 127     new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 128
 129   if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
 130     std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
 131     if (xbt_automaton_state_compare(
 132           pair_test->automaton_state, new_pair->automaton_state) != 0
 133         || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions)
 134         || this->compare(pair_test.get(), new_pair.get()) != 0)
 135       continue;
 136     XBT_INFO("Pair %d already reached (equal to pair %d) !",
 137       new_pair->num, pair_test->num);
 138     explorationStack_.pop_back();
 139     if (dot_output != nullptr)
 140       fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 141         initial_global_state->prev_pair, pair_test->num,
 142         initial_global_state->prev_req.c_str());
 143     return nullptr;
 144   }
 145
 146   acceptancePairs_.insert(res.first, new_pair);
 147   return new_pair;
 148 }
 149
 150 void LivenessChecker::removeAcceptancePair(int pair_num)
 151 {
 152   for (auto i = acceptancePairs_.begin(); i != acceptancePairs_.end(); ++i)
 153     if ((*i)->num == pair_num) {
 154       acceptancePairs_.erase(i);
 155       break;
 156     }
 157 }
 158
 159 void LivenessChecker::prepare(void)
 160 {
 161   mc_model_checker->wait_for_requests();
 162   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 163   initial_global_state->prev_pair = 0;
 164
 165   std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
 166
 167   // For each initial state of the property automaton, push a
 168   // (application_state, automaton_state) pair to the exploration stack:
 169   unsigned int cursor = 0;
 170   xbt_automaton_state_t automaton_state;
 171   xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state)
 172     if (automaton_state->type == -1)
 173       explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos));
 174 }
 175
 176
 177 void LivenessChecker::replay()
 178 {
 179   XBT_DEBUG("**** Begin Replay ****");
 180
 181   /* Intermediate backtracking */
 182   if(_sg_mc_checkpoint > 0) {
 183     simgrid::mc::Pair* pair = explorationStack_.back().get();
 184     if(pair->graph_state->system_state){
 185       simgrid::mc::restore_snapshot(pair->graph_state->system_state);
 186       return;
 187     }
 188   }
 189
 190   /* Restore the initial state */
 191   simgrid::mc::restore_snapshot(initial_global_state->snapshot);
 192
 193   /* Traverse the stack from the initial state and re-execute the transitions */
 194   int depth = 1;
 195   for (std::shared_ptr<Pair> const& pair : explorationStack_) {
 196     if (pair == explorationStack_.back())
 197       break;
 198
 199     std::shared_ptr<State> state = pair->graph_state;
 200
 201     if (pair->exploration_started) {
 202
 203       int req_num = state->transition.argument;
 204       smx_simcall_t saved_req = &state->executed_req;
 205
 206       smx_simcall_t req = nullptr;
 207
 208       if (saved_req != nullptr) {
 209         /* because we got a copy of the executed request, we have to fetch the
 210              real one, pointed by the request field of the issuer process */
 211         const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
 212         req = &issuer->simcall;
 213
 214         /* Debug information */
 215         XBT_DEBUG("Replay (depth = %d) : %s (%p)",
 216           depth,
 217           simgrid::mc::request_to_string(
 218             req, req_num, simgrid::mc::RequestType::simix).c_str(),
 219           state.get());
 220       }
 221
 222       mc_model_checker->handle_simcall(state->transition);
 223       mc_model_checker->wait_for_requests();
 224     }
 225
 226     /* Update statistics */
 227     mc_stats->visited_pairs++;
 228     mc_stats->executed_transitions++;
 229
 230     depth++;
 231
 232   }
 233
 234   XBT_DEBUG("**** End Replay ****");
 235 }
 236
 237 /**
 238  * \brief Checks whether a given pair has already been visited by the algorithm.
 239  */
 240 int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair)
 241 {
 242   if (_sg_mc_visited == 0)
 243     return -1;
 244
 245   if (visited_pair == nullptr)
 246     visited_pair = std::make_shared<VisitedPair>(
 247       pair->num, pair->automaton_state, pair->atomic_propositions,
 248       pair->graph_state);
 249
 250   auto range = std::equal_range(visitedPairs_.begin(), visitedPairs_.end(),
 251     visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 252
 253   for (auto i = range.first; i != range.second; ++i) {
 254     VisitedPair* pair_test = i->get();
 255     if (xbt_automaton_state_compare(
 256           pair_test->automaton_state, visited_pair->automaton_state) != 0
 257         || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions)
 258         || this->compare(pair_test, visited_pair.get()) != 0)
 259         continue;
 260     if (pair_test->other_num == -1)
 261       visited_pair->other_num = pair_test->num;
 262     else
 263       visited_pair->other_num = pair_test->other_num;
 264     if (dot_output == nullptr)
 265       XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", visited_pair->num, pair_test->num);
 266     else
 267       XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
 268         visited_pair->num, pair_test->num, visited_pair->other_num);
 269     (*i) = std::move(visited_pair);
 270     return (*i)->other_num;
 271   }
 272
 273   visitedPairs_.insert(range.first, std::move(visited_pair));
 274   this->purgeVisitedPairs();
 275   return -1;
 276 }
 277
 278 void LivenessChecker::purgeVisitedPairs()
 279 {
 280   if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
 281     // Remove the oldest entry with a linear search:
 282     visitedPairs_.erase(std::min_element(
 283       visitedPairs_.begin(), visitedPairs_.end(),
 284       [](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {
 285         return a->num < b->num; } ));
 286   }
 287 }
 288
 289 LivenessChecker::LivenessChecker(Session& session) : Checker(session)
 290 {
 291 }
 292
 293 LivenessChecker::~LivenessChecker()
 294 {
 295 }
 296
 297 RecordTrace LivenessChecker::getRecordTrace() // override
 298 {
 299   RecordTrace res;
 300   for (std::shared_ptr<Pair> const& pair : explorationStack_)
 301     res.push_back(pair->graph_state->getTransition());
 302   return res;
 303 }
 304
 305 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 306 {
 307   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 308   XBT_INFO("|             ACCEPTANCE CYCLE            |");
 309   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 310   XBT_INFO("Counter-example that violates formula :");
 311   simgrid::mc::dumpRecordPath();
 312   for (auto& s : this->getTextualTrace())
 313     XBT_INFO("%s", s.c_str());
 314   MC_print_statistics(mc_stats);
 315   XBT_INFO("Counter-example depth : %zd", depth);
 316 }
 317
 318 std::vector<std::string> LivenessChecker::getTextualTrace() // override
 319 {
 320   std::vector<std::string> trace;
 321   for (std::shared_ptr<Pair> const& pair : explorationStack_) {
 322     int req_num = pair->graph_state->transition.argument;
 323     smx_simcall_t req = &pair->graph_state->executed_req;
 324     if (req && req->call != SIMCALL_NONE)
 325       trace.push_back(simgrid::mc::request_to_string(
 326         req, req_num, simgrid::mc::RequestType::executed));
 327   }
 328   return trace;
 329 }
 330
 331 int LivenessChecker::main(void)
 332 {
 333   while (!explorationStack_.empty()){
 334     std::shared_ptr<Pair> current_pair = explorationStack_.back();
 335
 336     /* Update current state in buchi automaton */
 337     simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
 338
 339     XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %zd, pair_num = %d, requests = %d)",
 340        current_pair->depth, current_pair->search_cycle,
 341        current_pair->graph_state->interleaveSize(),
 342        current_pair->num,
 343        current_pair->requests);
 344
 345     if (current_pair->requests == 0) {
 346       this->backtrack();
 347       continue;
 348     }
 349
 350     std::shared_ptr<VisitedPair> reached_pair;
 351     if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started
 352         && (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) {
 353       this->showAcceptanceCycle(current_pair->depth);
 354       return SIMGRID_MC_EXIT_LIVENESS;
 355     }
 356
 357     /* Pair already visited ? stop the exploration on the current path */
 358     int visited_num = -1;
 359     if ((!current_pair->exploration_started)
 360       && (visited_num = this->insertVisitedPair(
 361         reached_pair, current_pair.get())) != -1) {
 362       if (dot_output != nullptr){
 363         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 364           initial_global_state->prev_pair, visited_num,
 365           initial_global_state->prev_req.c_str());
 366         fflush(dot_output);
 367       }
 368       XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
 369       current_pair->requests = 0;
 370       this->backtrack();
 371       continue;
 372     }
 373
 374     smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
 375     int req_num = current_pair->graph_state->transition.argument;
 376
 377     if (dot_output != nullptr) {
 378       if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
 379         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 380           initial_global_state->prev_pair, current_pair->num,
 381           initial_global_state->prev_req.c_str());
 382         initial_global_state->prev_req.clear();
 383       }
 384       initial_global_state->prev_pair = current_pair->num;
 385       initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, req_num);
 386       if (current_pair->search_cycle)
 387         fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 388       fflush(dot_output);
 389     }
 390
 391     XBT_DEBUG("Execute: %s",
 392       simgrid::mc::request_to_string(
 393         req, req_num, simgrid::mc::RequestType::simix).c_str());
 394
 395     /* Update mc_stats */
 396     mc_stats->executed_transitions++;
 397     if (!current_pair->exploration_started)
 398       mc_stats->visited_pairs++;
 399
 400     /* Answer the request */
 401     mc_model_checker->handle_simcall(current_pair->graph_state->transition);
 402
 403     /* Wait for requests (schedules processes) */
 404     mc_model_checker->wait_for_requests();
 405
 406     current_pair->requests--;
 407     current_pair->exploration_started = true;
 408
 409     /* Get values of atomic propositions (variables used in the property formula) */
 410     std::shared_ptr<const std::vector<int>> prop_values = this->getPropositionValues();
 411
 412     // For each enabled transition in the property automaton, push a
 413     // (application_state, automaton_state) pair to the exploration stack:
 414     int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
 415     while (cursor >= 0) {
 416       xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
 417       if (evaluate_label(transition_succ->label, *prop_values))
 418           explorationStack_.push_back(this->newPair(
 419             current_pair.get(), transition_succ->dst, prop_values));
 420        cursor--;
 421      }
 422
 423   }
 424
 425   XBT_INFO("No property violation found.");
 426   MC_print_statistics(mc_stats);
 427   return SIMGRID_MC_EXIT_SUCCESS;
 428 }
 429
 430 std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
 431 {
 432   std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
 433   next_pair->automaton_state = state;
 434   next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
 435   next_pair->atomic_propositions = std::move(propositions);
 436   if (current_pair)
 437     next_pair->depth = current_pair->depth + 1;
 438   else
 439     next_pair->depth = 1;
 440   /* Get enabled processes and insert them in the interleave set of the next graph_state */
 441   for (auto& p : mc_model_checker->process().simix_processes())
 442     if (simgrid::mc::process_is_enabled(&p.copy))
 443       next_pair->graph_state->interleave(&p.copy);
 444   next_pair->requests = next_pair->graph_state->interleaveSize();
 445   /* FIXME : get search_cycle value for each acceptant state */
 446   if (next_pair->automaton_state->type == 1 ||
 447       (current_pair && current_pair->search_cycle))
 448     next_pair->search_cycle = true;
 449   else
 450     next_pair->search_cycle = false;
 451   return std::move(next_pair);
 452 }
 453
 454 void LivenessChecker::backtrack()
 455 {
 456   /* Traverse the stack backwards until a pair with a non empty interleave
 457      set is found, deleting all the pairs that have it empty in the way. */
 458   while (!explorationStack_.empty()) {
 459     std::shared_ptr<simgrid::mc::Pair> current_pair = explorationStack_.back();
 460     explorationStack_.pop_back();
 461     if (current_pair->requests > 0) {
 462       /* We found a backtracking point */
 463       XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
 464       explorationStack_.push_back(std::move(current_pair));
 465       this->replay();
 466       XBT_DEBUG("Backtracking done");
 467       break;
 468     } else {
 469       XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
 470       if (current_pair->automaton_state->type == 1)
 471         this->removeAcceptancePair(current_pair->num);
 472     }
 473   }
 474 }
 475
 476 int LivenessChecker::run()
 477 {
 478   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
 479   MC_automaton_load(_sg_mc_property_file);
 480   mc_model_checker->wait_for_requests();
 481
 482   XBT_DEBUG("Starting the liveness algorithm");
 483
 484   /* Create the initial state */
 485   simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 486
 487   this->prepare();
 488   int res = this->main();
 489   simgrid::mc::initial_global_state = nullptr;
 490
 491   return res;
 492 }
 493
 494 Checker* createLivenessChecker(Session& session)
 495 {
 496   return new LivenessChecker(session);
 497 }
 498
 499 }
 500 }