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