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