src/mc/mc_global.c

   1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include <unistd.h>
   7 #include <sys/types.h>
   8 #include <sys/wait.h>
   9 #include <sys/time.h>
  10
  11 #include "../surf/surf_private.h"
  12 #include "../simix/smx_private.h"
  13 #include "xbt/fifo.h"
  14 #include "mc_private.h"
  15
  16 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
  17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  18                                 "Logging specific to MC (global)");
  19
  20 /* MC global data structures */
  21
  22 mc_state_t mc_current_state = NULL;
  23 char mc_replay_mode = FALSE;
  24 double *mc_time = NULL;
  25 mc_snapshot_t initial_snapshot = NULL;
  26
  27 /* Safety */
  28
  29 xbt_fifo_t mc_stack_safety_stateful = NULL;
  30 xbt_fifo_t mc_stack_safety_stateless = NULL;
  31 mc_stats_t mc_stats = NULL;
  32
  33 /* Liveness */
  34
  35 mc_stats_pair_t mc_stats_pair = NULL;
  36 xbt_fifo_t mc_stack_liveness = NULL;
  37 mc_snapshot_t initial_snapshot_liveness = NULL;
  38
  39 xbt_automaton_t automaton;
  40
  41 static void MC_init_liveness(xbt_automaton_t a);
  42 static void MC_assert_pair(int prop);
  43
  44
  45 /**
  46  *  \brief Initialize the model-checker data structures
  47  */
  48 void MC_init_safety_stateless(void)
  49 {
  50
  51   /* Check if MC is already initialized */
  52   if (initial_snapshot)
  53     return;
  54
  55   mc_time = xbt_new0(double, simix_process_maxpid);
  56
  57   /* Initialize the data structures that must be persistent across every
  58      iteration of the model-checker (in RAW memory) */
  59   MC_SET_RAW_MEM;
  60
  61   /* Initialize statistics */
  62   mc_stats = xbt_new0(s_mc_stats_t, 1);
  63   mc_stats->state_size = 1;
  64
  65   /* Create exploration stack */
  66   mc_stack_safety_stateless = xbt_fifo_new();
  67
  68   MC_UNSET_RAW_MEM;
  69
  70   MC_dpor_init();
  71
  72   MC_SET_RAW_MEM;
  73   /* Save the initial state */
  74   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
  75   MC_take_snapshot(initial_snapshot);
  76   MC_UNSET_RAW_MEM;
  77 }
  78
  79 void MC_init_safety_stateful(void){
  80
  81
  82    /* Check if MC is already initialized */
  83   if (initial_snapshot)
  84     return;
  85
  86   mc_time = xbt_new0(double, simix_process_maxpid);
  87
  88   /* Initialize the data structures that must be persistent across every
  89      iteration of the model-checker (in RAW memory) */
  90   MC_SET_RAW_MEM;
  91
  92   /* Initialize statistics */
  93   mc_stats = xbt_new0(s_mc_stats_t, 1);
  94   mc_stats->state_size = 1;
  95
  96   /* Create exploration stack */
  97   mc_stack_safety_stateful = xbt_fifo_new();
  98
  99   MC_UNSET_RAW_MEM;
 100
 101   MC_dpor_stateful_init();
 102
 103
 104 }
 105
 106 static void MC_init_liveness(xbt_automaton_t a){
 107
 108   XBT_DEBUG("Start init mc");
 109
 110   mc_time = xbt_new0(double, simix_process_maxpid);
 111
 112   /* Initialize the data structures that must be persistent across every
 113      iteration of the model-checker (in RAW memory) */
 114
 115   MC_SET_RAW_MEM;
 116
 117   /* Initialize statistics */
 118   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
 119
 120   XBT_DEBUG("Creating stack");
 121
 122  /* Create exploration stack */
 123   mc_stack_liveness = xbt_fifo_new();
 124
 125   MC_UNSET_RAW_MEM;
 126
 127   automaton = a;
 128
 129   MC_ddfs_init();
 130
 131
 132 }
 133
 134
 135 void MC_modelcheck(void)
 136 {
 137   MC_init_safety_stateless();
 138   MC_dpor();
 139   MC_exit();
 140 }
 141
 142 void MC_modelcheck_stateful(void)
 143 {
 144   MC_init_safety_stateful();
 145   MC_dpor_stateful();
 146   MC_exit();
 147 }
 148
 149
 150 void MC_modelcheck_liveness(xbt_automaton_t a){
 151   MC_init_liveness(a);
 152   MC_exit_liveness();
 153 }
 154
 155 void MC_exit_liveness(void)
 156 {
 157   MC_print_statistics_pairs(mc_stats_pair);
 158   //xbt_free(mc_time);
 159   //MC_memory_exit();
 160   exit(0);
 161 }
 162
 163
 164 void MC_exit(void)
 165 {
 166   MC_print_statistics(mc_stats);
 167   xbt_free(mc_time);
 168   MC_memory_exit();
 169 }
 170
 171
 172 int MC_random(int min, int max)
 173 {
 174   /*FIXME: return mc_current_state->executed_transition->random.value;*/
 175   return 0;
 176 }
 177
 178 /**
 179  * \brief Schedules all the process that are ready to run
 180  */
 181 void MC_wait_for_requests(void)
 182 {
 183   smx_process_t process;
 184   smx_simcall_t req;
 185   unsigned int iter;
 186
 187   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
 188     SIMIX_process_runall();
 189     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
 190       req = &process->simcall;
 191       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
 192           SIMIX_simcall_pre(req, 0);
 193     }
 194   }
 195 }
 196
 197 int MC_deadlock_check()
 198 {
 199   int deadlock = FALSE;
 200   smx_process_t process;
 201   if(xbt_swag_size(simix_global->process_list)){
 202     deadlock = TRUE;
 203     xbt_swag_foreach(process, simix_global->process_list){
 204       if(process->simcall.call != SIMCALL_NONE
 205          && MC_request_is_enabled(&process->simcall)){
 206         deadlock = FALSE;
 207         break;
 208       }
 209     }
 210   }
 211   return deadlock;
 212 }
 213
 214 /**
 215  * \brief Re-executes from the initial state all the transitions indicated by
 216  *        a given model-checker stack.
 217  * \param stack The stack with the transitions to execute.
 218 */
 219 void MC_replay(xbt_fifo_t stack)
 220 {
 221   int value;
 222   char *req_str;
 223   smx_simcall_t req = NULL, saved_req = NULL;
 224   xbt_fifo_item_t item;
 225   mc_state_t state;
 226
 227   XBT_DEBUG("**** Begin Replay ****");
 228
 229   /* Restore the initial state */
 230   MC_restore_snapshot(initial_snapshot);
 231   /* At the moment of taking the snapshot the raw heap was set, so restoring
 232    * it will set it back again, we have to unset it to continue  */
 233   MC_UNSET_RAW_MEM;
 234
 235   /* Traverse the stack from the initial state and re-execute the transitions */
 236   for (item = xbt_fifo_get_last_item(stack);
 237        item != xbt_fifo_get_first_item(stack);
 238        item = xbt_fifo_get_prev_item(item)) {
 239
 240     state = (mc_state_t) xbt_fifo_get_item_content(item);
 241     saved_req = MC_state_get_executed_request(state, &value);
 242
 243     if(saved_req){
 244       /* because we got a copy of the executed request, we have to fetch the
 245          real one, pointed by the request field of the issuer process */
 246       req = &saved_req->issuer->simcall;
 247
 248       /* Debug information */
 249       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 250         req_str = MC_request_to_string(req, value);
 251         XBT_DEBUG("Replay: %s (%p)", req_str, state);
 252         xbt_free(req_str);
 253       }
 254     }
 255
 256     SIMIX_simcall_pre(req, value);
 257     MC_wait_for_requests();
 258
 259     /* Update statistics */
 260     mc_stats->visited_states++;
 261     mc_stats->executed_transitions++;
 262   }
 263   XBT_DEBUG("**** End Replay ****");
 264 }
 265
 266 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 267 {
 268   int value;
 269   char *req_str;
 270   smx_simcall_t req = NULL, saved_req = NULL;
 271   xbt_fifo_item_t item;
 272   mc_state_t state;
 273   mc_pair_stateless_t pair;
 274   int depth = 1;
 275
 276   XBT_DEBUG("**** Begin Replay ****");
 277
 278   /* Restore the initial state */
 279   MC_restore_snapshot(initial_snapshot_liveness);
 280   /* At the moment of taking the snapshot the raw heap was set, so restoring
 281    * it will set it back again, we have to unset it to continue  */
 282   MC_UNSET_RAW_MEM;
 283
 284   if(all_stack){
 285
 286     item = xbt_fifo_get_last_item(stack);
 287
 288     while(depth <= xbt_fifo_size(stack)){
 289
 290       pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
 291       state = (mc_state_t) pair->graph_state;
 292
 293       if(pair->requests > 0){
 294
 295         saved_req = MC_state_get_executed_request(state, &value);
 296         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 297
 298         if(saved_req != NULL){
 299           /* because we got a copy of the executed request, we have to fetch the
 300              real one, pointed by the request field of the issuer process */
 301           req = &saved_req->issuer->simcall;
 302           //XBT_DEBUG("Req->call %u", req->call);
 303
 304           /* Debug information */
 305           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 306             req_str = MC_request_to_string(req, value);
 307             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 308             xbt_free(req_str);
 309           }
 310
 311         }
 312
 313         SIMIX_simcall_pre(req, value);
 314         MC_wait_for_requests();
 315       }
 316
 317       depth++;
 318
 319       /* Update statistics */
 320       mc_stats_pair->visited_pairs++;
 321
 322       item = xbt_fifo_get_prev_item(item);
 323     }
 324
 325   }else{
 326
 327     /* Traverse the stack from the initial state and re-execute the transitions */
 328     for (item = xbt_fifo_get_last_item(stack);
 329          item != xbt_fifo_get_first_item(stack);
 330          item = xbt_fifo_get_prev_item(item)) {
 331
 332       pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
 333       state = (mc_state_t) pair->graph_state;
 334
 335       if(pair->requests > 0){
 336
 337         saved_req = MC_state_get_executed_request(state, &value);
 338         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 339
 340         if(saved_req != NULL){
 341           /* because we got a copy of the executed request, we have to fetch the
 342              real one, pointed by the request field of the issuer process */
 343           req = &saved_req->issuer->simcall;
 344           //XBT_DEBUG("Req->call %u", req->call);
 345
 346           /* Debug information */
 347           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 348             req_str = MC_request_to_string(req, value);
 349             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 350             xbt_free(req_str);
 351           }
 352
 353         }
 354
 355         SIMIX_simcall_pre(req, value);
 356         MC_wait_for_requests();
 357       }
 358
 359       depth++;
 360
 361       /* Update statistics */
 362       mc_stats_pair->visited_pairs++;
 363     }
 364   }
 365
 366   XBT_DEBUG("**** End Replay ****");
 367 }
 368
 369
 370 /**
 371  * \brief Dumps the contents of a model-checker's stack and shows the actual
 372  *        execution trace
 373  * \param stack The stack to dump
 374 */
 375 void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
 376 {
 377   mc_state_t state;
 378
 379   MC_show_stack_safety_stateless(stack);
 380
 381   MC_SET_RAW_MEM;
 382   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 383     MC_state_delete(state);
 384   MC_UNSET_RAW_MEM;
 385 }
 386
 387
 388 void MC_show_stack_safety_stateless(xbt_fifo_t stack)
 389 {
 390   int value;
 391   mc_state_t state;
 392   xbt_fifo_item_t item;
 393   smx_simcall_t req;
 394   char *req_str = NULL;
 395
 396   for (item = xbt_fifo_get_last_item(stack);
 397        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
 398         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 399     req = MC_state_get_executed_request(state, &value);
 400     if(req){
 401       req_str = MC_request_to_string(req, value);
 402       XBT_INFO("%s", req_str);
 403       xbt_free(req_str);
 404     }
 405   }
 406 }
 407
 408 void MC_show_deadlock(smx_simcall_t req)
 409 {
 410   /*char *req_str = NULL;*/
 411   XBT_INFO("**************************");
 412   XBT_INFO("*** DEAD-LOCK DETECTED ***");
 413   XBT_INFO("**************************");
 414   XBT_INFO("Locked request:");
 415   /*req_str = MC_request_to_string(req);
 416   XBT_INFO("%s", req_str);
 417   xbt_free(req_str);*/
 418   XBT_INFO("Counter-example execution trace:");
 419   MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 420 }
 421
 422 void MC_show_deadlock_stateful(smx_simcall_t req)
 423 {
 424   /*char *req_str = NULL;*/
 425   XBT_INFO("**************************");
 426   XBT_INFO("*** DEAD-LOCK DETECTED ***");
 427   XBT_INFO("**************************");
 428   XBT_INFO("Locked request:");
 429   /*req_str = MC_request_to_string(req);
 430   XBT_INFO("%s", req_str);
 431   xbt_free(req_str);*/
 432   XBT_INFO("Counter-example execution trace:");
 433   MC_show_stack_safety_stateful(mc_stack_safety_stateful);
 434 }
 435
 436 void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
 437 {
 438   //mc_state_ws_t state;
 439
 440   MC_show_stack_safety_stateful(stack);
 441
 442   /*MC_SET_RAW_MEM;
 443   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 444     MC_state_delete(state);
 445     MC_UNSET_RAW_MEM;*/
 446 }
 447
 448
 449 void MC_show_stack_safety_stateful(xbt_fifo_t stack)
 450 {
 451   int value;
 452   mc_state_ws_t state;
 453   xbt_fifo_item_t item;
 454   smx_simcall_t req;
 455   char *req_str = NULL;
 456
 457   for (item = xbt_fifo_get_last_item(stack);
 458        (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
 459         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 460     req = MC_state_get_executed_request(state->graph_state, &value);
 461     if(req){
 462       req_str = MC_request_to_string(req, value);
 463       XBT_INFO("%s", req_str);
 464       xbt_free(req_str);
 465     }
 466   }
 467 }
 468
 469
 470 void MC_show_stack_liveness(xbt_fifo_t stack){
 471   int value;
 472   mc_pair_stateless_t pair;
 473   xbt_fifo_item_t item;
 474   smx_simcall_t req;
 475   char *req_str = NULL;
 476
 477   for (item = xbt_fifo_get_last_item(stack);
 478        (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
 479         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 480     req = MC_state_get_executed_request(pair->graph_state, &value);
 481     if(req){
 482       if(pair->requests>0){
 483         req_str = MC_request_to_string(req, value);
 484         XBT_INFO("%s", req_str);
 485         xbt_free(req_str);
 486       }else{
 487         XBT_INFO("End of system requests but evolution in Büchi automaton");
 488       }
 489     }
 490   }
 491 }
 492
 493 void MC_dump_stack_liveness(xbt_fifo_t stack){
 494   mc_pair_stateless_t pair;
 495
 496   MC_SET_RAW_MEM;
 497   while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
 498     MC_pair_stateless_delete(pair);
 499   MC_UNSET_RAW_MEM;
 500 }
 501
 502
 503 void MC_print_statistics(mc_stats_t stats)
 504 {
 505   //XBT_INFO("State space size ~= %lu", stats->state_size);
 506   XBT_INFO("Expanded states = %lu", stats->expanded_states);
 507   XBT_INFO("Visited states = %lu", stats->visited_states);
 508   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
 509   XBT_INFO("Expanded / Visited = %lf",
 510         (double) stats->visited_states / stats->expanded_states);
 511   /*XBT_INFO("Exploration coverage = %lf",
 512      (double)stats->expanded_states / stats->state_size); */
 513 }
 514
 515 void MC_print_statistics_pairs(mc_stats_pair_t stats)
 516 {
 517   XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
 518   XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
 519   //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
 520   XBT_INFO("Expanded / Visited = %lf",
 521         (double) stats->visited_pairs / stats->expanded_pairs);
 522   /*XBT_INFO("Exploration coverage = %lf",
 523      (double)stats->expanded_states / stats->state_size); */
 524 }
 525
 526 void MC_assert(int prop)
 527 {
 528   if (MC_IS_ENABLED ){
 529     if(!prop) {
 530       XBT_INFO("**************************");
 531       XBT_INFO("*** PROPERTY NOT VALID ***");
 532       XBT_INFO("**************************");
 533       XBT_INFO("Counter-example execution trace:");
 534       MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 535       MC_print_statistics(mc_stats);
 536       xbt_abort();
 537     }else{
 538       MC_print_statistics(mc_stats);
 539       xbt_abort();
 540     }
 541   }
 542 }
 543
 544 void MC_assert_stateful(int prop)
 545 {
 546   if (MC_IS_ENABLED && !prop) {
 547     XBT_INFO("**************************");
 548     XBT_INFO("*** PROPERTY NOT VALID ***");
 549     XBT_INFO("**************************");
 550     XBT_INFO("Counter-example execution trace:");
 551     MC_dump_stack_safety_stateful(mc_stack_safety_stateful);
 552     MC_print_statistics(mc_stats);
 553     xbt_abort();
 554   }
 555 }
 556
 557
 558 static void MC_assert_pair(int prop){
 559   if (MC_IS_ENABLED && !prop) {
 560     XBT_INFO("**************************");
 561     XBT_INFO("*** PROPERTY NOT VALID ***");
 562     XBT_INFO("**************************");
 563     //XBT_INFO("Counter-example execution trace:");
 564     MC_show_stack_liveness(mc_stack_liveness);
 565     //MC_dump_snapshot_stack(mc_snapshot_stack);
 566     MC_print_statistics_pairs(mc_stats_pair);
 567     xbt_abort();
 568   }
 569 }
 570
 571 void MC_process_clock_add(smx_process_t process, double amount)
 572 {
 573   mc_time[process->pid] += amount;
 574 }
 575
 576 double MC_process_clock_get(smx_process_t process)
 577 {
 578   if(mc_time)
 579     return mc_time[process->pid];
 580   else
 581     return 0;
 582 }
 583
 584 void MC_diff(void){
 585
 586   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 587   MC_take_snapshot_liveness(sn);
 588
 589   int i;
 590
 591   XBT_INFO("Number of regions : %u", sn->num_reg);
 592
 593   for(i=0; i<sn->num_reg; i++){
 594
 595     switch(sn->regions[i]->type){
 596     case 0: /* heap */
 597       XBT_INFO("Size of heap : %zu", sn->regions[i]->size);
 598       mmalloc_display_info_heap(sn->regions[i]->data);
 599       break;
 600     case 1 : /* libsimgrid */
 601       XBT_INFO("Size of libsimgrid : %zu", sn->regions[i]->size);
 602       break;
 603     case 2 : /* data program */
 604       XBT_INFO("Size of data program : %zu", sn->regions[i]->size);
 605       break;
 606     case 3 : /* stack */
 607       XBT_INFO("Size of stack : %zu", sn->regions[i]->size);
 608       XBT_INFO("Start addr of stack : %p", sn->regions[i]->start_addr);
 609       break;
 610     }
 611
 612   }
 613
 614 }