src/mc/checker/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 <memory>
  10 #include <list>
  11
  12 #include <boost/range/algorithm.hpp>
  13
  14 #include <unistd.h>
  15 #include <sys/wait.h>
  16
  17 #include <xbt/automaton.h>
  18 #include <xbt/dynar.h>
  19 #include <xbt/dynar.hpp>
  20 #include <xbt/log.h>
  21 #include <xbt/sysdep.h>
  22
  23 #include "src/mc/Session.hpp"
  24 #include "src/mc/Transition.hpp"
  25 #include "src/mc/checker/LivenessChecker.hpp"
  26 #include "src/mc/mc_exit.h"
  27 #include "src/mc/mc_private.h"
  28 #include "src/mc/mc_private.h"
  29 #include "src/mc/mc_record.h"
  30 #include "src/mc/mc_replay.h"
  31 #include "src/mc/mc_request.h"
  32 #include "src/mc/mc_safety.h"
  33 #include "src/mc/mc_smx.h"
  34 #include "src/mc/remote/Client.hpp"
  35
  36 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  37                                 "Logging specific to algorithms for liveness properties verification");
  38
  39 /********* Static functions *********/
  40
  41 namespace simgrid {
  42 namespace mc {
  43
  44 VisitedPair::VisitedPair(
  45   int pair_num, xbt_automaton_state_t automaton_state,
  46   std::shared_ptr<const std::vector<int>> atomic_propositions,
  47   std::shared_ptr<simgrid::mc::State> graph_state)
  48 {
  49   simgrid::mc::Process* process = &(mc_model_checker->process());
  50
  51   this->graph_state = std::move(graph_state);
  52   if(this->graph_state->system_state == nullptr)
  53     this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
  54   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
  55     process->get_heap()->heaplimit,
  56     process->get_malloc_info());
  57
  58   this->actors_count = mc_model_checker->process().actors().size();
  59
  60   this->automaton_state = automaton_state;
  61   this->num = pair_num;
  62   this->other_num = -1;
  63   this->atomic_propositions = std::move(atomic_propositions);
  64 }
  65
  66 VisitedPair::~VisitedPair() = default;
  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(unsigned long expanded_pairs) : num(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 = boost::range::equal_range(acceptancePairs_, new_pair.get(),
 127                                        simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap());
 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         this->previousPair_, pair_test->num,
 142         this->previousRequest_.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::replay()
 160 {
 161   XBT_DEBUG("**** Begin Replay ****");
 162
 163   /* Intermediate backtracking */
 164   if(_sg_mc_checkpoint > 0) {
 165     simgrid::mc::Pair* pair = explorationStack_.back().get();
 166     if(pair->graph_state->system_state){
 167       simgrid::mc::restore_snapshot(pair->graph_state->system_state);
 168       return;
 169     }
 170   }
 171
 172   /* Restore the initial state */
 173   simgrid::mc::session->restoreInitialState();
 174
 175   /* Traverse the stack from the initial state and re-execute the transitions */
 176   int depth = 1;
 177   for (std::shared_ptr<Pair> const& pair : explorationStack_) {
 178     if (pair == explorationStack_.back())
 179       break;
 180
 181     std::shared_ptr<State> state = pair->graph_state;
 182
 183     if (pair->exploration_started) {
 184
 185       int req_num = state->transition.argument;
 186       smx_simcall_t saved_req = &state->executed_req;
 187
 188       smx_simcall_t req = nullptr;
 189
 190       if (saved_req != nullptr) {
 191         /* because we got a copy of the executed request, we have to fetch the
 192              real one, pointed by the request field of the issuer process */
 193         const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
 194         req = &issuer->simcall;
 195
 196         /* Debug information */
 197         XBT_DEBUG("Replay (depth = %d) : %s (%p)",
 198           depth,
 199           simgrid::mc::request_to_string(
 200             req, req_num, simgrid::mc::RequestType::simix).c_str(),
 201           state.get());
 202       }
 203
 204       this->getSession().execute(state->transition);
 205     }
 206
 207     /* Update statistics */
 208     visitedPairsCount_++;
 209     mc_model_checker->executed_transitions++;
 210
 211     depth++;
 212
 213   }
 214
 215   XBT_DEBUG("**** End Replay ****");
 216 }
 217
 218 /**
 219  * \brief Checks whether a given pair has already been visited by the algorithm.
 220  */
 221 int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair)
 222 {
 223   if (_sg_mc_max_visited_states == 0)
 224     return -1;
 225
 226   if (visited_pair == nullptr)
 227     visited_pair = std::make_shared<VisitedPair>(
 228       pair->num, pair->automaton_state, pair->atomic_propositions,
 229       pair->graph_state);
 230
 231   auto range = boost::range::equal_range(visitedPairs_, visited_pair.get(),
 232                                          simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap());
 233
 234   for (auto i = range.first; i != range.second; ++i) {
 235     VisitedPair* pair_test = i->get();
 236     if (xbt_automaton_state_compare(
 237           pair_test->automaton_state, visited_pair->automaton_state) != 0
 238         || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions)
 239         || this->compare(pair_test, visited_pair.get()) != 0)
 240         continue;
 241     if (pair_test->other_num == -1)
 242       visited_pair->other_num = pair_test->num;
 243     else
 244       visited_pair->other_num = pair_test->other_num;
 245     if (dot_output == nullptr)
 246       XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", visited_pair->num, pair_test->num);
 247     else
 248       XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
 249         visited_pair->num, pair_test->num, visited_pair->other_num);
 250     (*i) = std::move(visited_pair);
 251     return (*i)->other_num;
 252   }
 253
 254   visitedPairs_.insert(range.first, std::move(visited_pair));
 255   this->purgeVisitedPairs();
 256   return -1;
 257 }
 258
 259 void LivenessChecker::purgeVisitedPairs()
 260 {
 261   if (_sg_mc_max_visited_states != 0 && visitedPairs_.size() > (std::size_t)_sg_mc_max_visited_states) {
 262     // Remove the oldest entry with a linear search:
 263     visitedPairs_.erase(boost::min_element(visitedPairs_,
 264       [](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {
 265         return a->num < b->num; } ));
 266   }
 267 }
 268
 269 LivenessChecker::LivenessChecker(Session& session) : Checker(session)
 270 {
 271 }
 272
 273 LivenessChecker::~LivenessChecker()
 274 {
 275 }
 276
 277 RecordTrace LivenessChecker::getRecordTrace() // override
 278 {
 279   RecordTrace res;
 280   for (std::shared_ptr<Pair> const& pair : explorationStack_)
 281     res.push_back(pair->graph_state->getTransition());
 282   return res;
 283 }
 284
 285 void LivenessChecker::logState() // override
 286 {
 287   Checker::logState();
 288   XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
 289   XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
 290   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
 291 }
 292
 293 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 294 {
 295   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 296   XBT_INFO("|             ACCEPTANCE CYCLE            |");
 297   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 298   XBT_INFO("Counter-example that violates formula :");
 299   simgrid::mc::dumpRecordPath();
 300   for (auto& s : this->getTextualTrace())
 301     XBT_INFO("%s", s.c_str());
 302   simgrid::mc::session->logState();
 303   XBT_INFO("Counter-example depth : %zd", depth);
 304 }
 305
 306 std::vector<std::string> LivenessChecker::getTextualTrace() // override
 307 {
 308   std::vector<std::string> trace;
 309   for (std::shared_ptr<Pair> const& pair : explorationStack_) {
 310     int req_num = pair->graph_state->transition.argument;
 311     smx_simcall_t req = &pair->graph_state->executed_req;
 312     if (req && req->call != SIMCALL_NONE)
 313       trace.push_back(simgrid::mc::request_to_string(
 314         req, req_num, simgrid::mc::RequestType::executed));
 315   }
 316   return trace;
 317 }
 318
 319 std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state,
 320                                                std::shared_ptr<const std::vector<int>> propositions)
 321 {
 322   std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
 323   next_pair->automaton_state      = state;
 324   next_pair->graph_state          = std::shared_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 325   next_pair->atomic_propositions  = std::move(propositions);
 326   if (current_pair)
 327     next_pair->depth = current_pair->depth + 1;
 328   else
 329     next_pair->depth = 1;
 330   /* Get enabled actors and insert them in the interleave set of the next graph_state */
 331   for (auto& actor : mc_model_checker->process().actors())
 332     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
 333       next_pair->graph_state->interleave(actor.copy.getBuffer());
 334   next_pair->requests = next_pair->graph_state->interleaveSize();
 335   /* FIXME : get search_cycle value for each accepting state */
 336   if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
 337     next_pair->search_cycle = true;
 338   else
 339     next_pair->search_cycle = false;
 340   return next_pair;
 341 }
 342
 343 void LivenessChecker::backtrack()
 344 {
 345   /* Traverse the stack backwards until a pair with a non empty interleave
 346      set is found, deleting all the pairs that have it empty in the way. */
 347   while (!explorationStack_.empty()) {
 348     std::shared_ptr<simgrid::mc::Pair> current_pair = explorationStack_.back();
 349     explorationStack_.pop_back();
 350     if (current_pair->requests > 0) {
 351       /* We found a backtracking point */
 352       XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
 353       explorationStack_.push_back(std::move(current_pair));
 354       this->replay();
 355       XBT_DEBUG("Backtracking done");
 356       break;
 357     } else {
 358       XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
 359       if (current_pair->automaton_state->type == 1)
 360         this->removeAcceptancePair(current_pair->num);
 361     }
 362   }
 363 }
 364
 365 void LivenessChecker::run()
 366 {
 367   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
 368   MC_automaton_load(_sg_mc_property_file);
 369
 370   XBT_DEBUG("Starting the liveness algorithm");
 371   simgrid::mc::session->initialize();
 372
 373   /* Initialize */
 374   this->previousPair_ = 0;
 375
 376   std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
 377
 378   // For each initial state of the property automaton, push a
 379   // (application_state, automaton_state) pair to the exploration stack:
 380   unsigned int cursor = 0;
 381   xbt_automaton_state_t automaton_state;
 382   xbt_dynar_foreach (simgrid::mc::property_automaton->states, cursor, automaton_state)
 383     if (automaton_state->type == -1)
 384       explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos));
 385
 386   /* Actually run the double DFS search for counter-examples */
 387   while (!explorationStack_.empty()){
 388     std::shared_ptr<Pair> current_pair = explorationStack_.back();
 389
 390     /* Update current state in buchi automaton */
 391     simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
 392
 393     XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %zd, pair_num = %d, requests = %d)",
 394        current_pair->depth, current_pair->search_cycle,
 395        current_pair->graph_state->interleaveSize(),
 396        current_pair->num,
 397        current_pair->requests);
 398
 399     if (current_pair->requests == 0) {
 400       this->backtrack();
 401       continue;
 402     }
 403
 404     std::shared_ptr<VisitedPair> reached_pair;
 405     if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started
 406         && (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) {
 407       this->showAcceptanceCycle(current_pair->depth);
 408       throw simgrid::mc::LivenessError();
 409     }
 410
 411     /* Pair already visited ? stop the exploration on the current path */
 412     int visited_num = -1;
 413     if ((!current_pair->exploration_started)
 414       && (visited_num = this->insertVisitedPair(
 415         reached_pair, current_pair.get())) != -1) {
 416       if (dot_output != nullptr){
 417         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 418           this->previousPair_, visited_num,
 419           this->previousRequest_.c_str());
 420         fflush(dot_output);
 421       }
 422       XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
 423       current_pair->requests = 0;
 424       this->backtrack();
 425       continue;
 426     }
 427
 428     smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
 429     int req_num = current_pair->graph_state->transition.argument;
 430
 431     if (dot_output != nullptr) {
 432       if (this->previousPair_ != 0 && this->previousPair_ != current_pair->num) {
 433         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 434           this->previousPair_, current_pair->num,
 435           this->previousRequest_.c_str());
 436         this->previousRequest_.clear();
 437       }
 438       this->previousPair_ = current_pair->num;
 439       this->previousRequest_ = simgrid::mc::request_get_dot_output(req, req_num);
 440       if (current_pair->search_cycle)
 441         fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 442       fflush(dot_output);
 443     }
 444
 445     XBT_DEBUG("Execute: %s",
 446       simgrid::mc::request_to_string(
 447         req, req_num, simgrid::mc::RequestType::simix).c_str());
 448
 449     /* Update stats */
 450     mc_model_checker->executed_transitions++;
 451     if (!current_pair->exploration_started)
 452       visitedPairsCount_++;
 453
 454     /* Answer the request */
 455     mc_model_checker->handle_simcall(current_pair->graph_state->transition);
 456
 457     /* Wait for requests (schedules processes) */
 458     mc_model_checker->wait_for_requests();
 459
 460     current_pair->requests--;
 461     current_pair->exploration_started = true;
 462
 463     /* Get values of atomic propositions (variables used in the property formula) */
 464     std::shared_ptr<const std::vector<int>> prop_values = this->getPropositionValues();
 465
 466     // For each enabled transition in the property automaton, push a
 467     // (application_state, automaton_state) pair to the exploration stack:
 468     for (int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; cursor >= 0; cursor--) {
 469       xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
 470       if (evaluate_label(transition_succ->label, *prop_values))
 471           explorationStack_.push_back(this->newPair(
 472             current_pair.get(), transition_succ->dst, prop_values));
 473      }
 474
 475   }
 476
 477   XBT_INFO("No property violation found.");
 478   simgrid::mc::session->logState();
 479 }
 480
 481 Checker* createLivenessChecker(Session& session)
 482 {
 483   return new LivenessChecker(session);
 484 }
 485
 486 }
 487 }