src/mc/mc_dpor.c

   1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
   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 "private.h"
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  10                                 "Logging specific to MC DPOR exploration");
  11
  12 /**
  13  *  \brief Initialize the DPOR exploration algorithm
  14  */
  15 void MC_dpor_init()
  16 {
  17   mc_state_t initial_state = NULL;
  18   smx_process_t process;
  19
  20   /* Create the initial state and push it into the exploration stack */
  21   MC_SET_RAW_MEM;
  22   initial_state = MC_state_new();
  23   xbt_fifo_unshift(mc_stack_safety_stateless, initial_state);
  24   MC_UNSET_RAW_MEM;
  25
  26   XBT_DEBUG("**************************************************");
  27   XBT_DEBUG("Initial state");
  28
  29   /* Wait for requests (schedules processes) */
  30   MC_wait_for_requests();
  31
  32   MC_SET_RAW_MEM;
  33   /* Get an enabled process and insert it in the interleave set of the initial state */
  34   xbt_swag_foreach(process, simix_global->process_list){
  35     if(MC_process_is_enabled(process)){
  36       MC_state_interleave_process(initial_state, process);
  37       break;
  38     }
  39   }
  40   MC_UNSET_RAW_MEM;
  41
  42   /* FIXME: Update Statistics
  43   mc_stats->state_size +=
  44       xbt_setset_set_size(initial_state->enabled_transitions); */
  45 }
  46
  47
  48 /**
  49  *      \brief Perform the model-checking operation using a depth-first search exploration
  50  *         with Dynamic Partial Order Reductions
  51  */
  52 void MC_dpor(void)
  53 {
  54   char *req_str;
  55   int value;
  56   smx_req_t req = NULL, prev_req = NULL;
  57   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  58   smx_process_t process = NULL;
  59   xbt_fifo_item_t item = NULL;
  60
  61   while (xbt_fifo_size(mc_stack_safety_stateless) > 0) {
  62
  63     /* Get current state */
  64     state = (mc_state_t)
  65       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateless));
  66
  67     XBT_DEBUG("**************************************************");
  68     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
  69            xbt_fifo_size(mc_stack_safety_stateless), state,
  70            MC_state_interleave_size(state));
  71
  72     /* Update statistics */
  73     mc_stats->visited_states++;
  74
  75     /* If there are processes to interleave and the maximum depth has not been reached
  76        then perform one step of the exploration algorithm */
  77     if (xbt_fifo_size(mc_stack_safety_stateless) < MAX_DEPTH &&
  78         (req = MC_state_get_request(state, &value))) {
  79
  80       /* Debug information */
  81       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  82         req_str = MC_request_to_string(req, value);
  83         XBT_DEBUG("Execute: %s", req_str);
  84         xbt_free(req_str);
  85       }
  86
  87       MC_state_set_executed_request(state, req, value);
  88       mc_stats->executed_transitions++;
  89
  90       /* Answer the request */
  91       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
  92
  93       /* Wait for requests (schedules processes) */
  94       MC_wait_for_requests();
  95
  96       /* Create the new expanded state */
  97       MC_SET_RAW_MEM;
  98       next_state = MC_state_new();
  99       xbt_fifo_unshift(mc_stack_safety_stateless, next_state);
 100
 101       /* Get an enabled process and insert it in the interleave set of the next state */
 102       xbt_swag_foreach(process, simix_global->process_list){
 103         if(MC_process_is_enabled(process)){
 104           MC_state_interleave_process(next_state, process);
 105           break;
 106         }
 107       }
 108       MC_UNSET_RAW_MEM;
 109
 110       /* FIXME: Update Statistics
 111       mc_stats->state_size +=
 112           xbt_setset_set_size(next_state->enabled_transitions);*/
 113
 114       /* Let's loop again */
 115
 116       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 117     } else {
 118       XBT_DEBUG("There are no more processes to interleave.");
 119
 120       /* Trash the current state, no longer needed */
 121       MC_SET_RAW_MEM;
 122       xbt_fifo_shift(mc_stack_safety_stateless);
 123       MC_state_delete(state);
 124       MC_UNSET_RAW_MEM;
 125
 126       /* Check for deadlocks */
 127       if(MC_deadlock_check()){
 128         MC_show_deadlock(NULL);
 129         return;
 130       }
 131
 132       MC_SET_RAW_MEM;
 133       /* Traverse the stack backwards until a state with a non empty interleave
 134          set is found, deleting all the states that have it empty in the way.
 135          For each deleted state, check if the request that has generated it
 136          (from it's predecesor state), depends on any other previous request
 137          executed before it. If it does then add it to the interleave set of the
 138          state that executed that previous request. */
 139       while ((state = xbt_fifo_shift(mc_stack_safety_stateless)) != NULL) {
 140         req = MC_state_get_internal_request(state);
 141         xbt_fifo_foreach(mc_stack_safety_stateless, item, prev_state, mc_state_t) {
 142           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 143             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 144               XBT_DEBUG("Dependent Transitions:");
 145               prev_req = MC_state_get_executed_request(prev_state, &value);
 146               req_str = MC_request_to_string(prev_req, value);
 147               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 148               xbt_free(req_str);
 149               prev_req = MC_state_get_executed_request(state, &value);
 150               req_str = MC_request_to_string(prev_req, value);
 151               XBT_DEBUG("%s (state=%p)", req_str, state);
 152               xbt_free(req_str);
 153             }
 154
 155             if(!MC_state_process_is_done(prev_state, req->issuer))
 156               MC_state_interleave_process(prev_state, req->issuer);
 157             else
 158               XBT_DEBUG("Process %p is in done set", req->issuer);
 159
 160             break;
 161           }
 162         }
 163         if (MC_state_interleave_size(state)) {
 164           /* We found a back-tracking point, let's loop */
 165           xbt_fifo_unshift(mc_stack_safety_stateless, state);
 166           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateless));
 167           MC_UNSET_RAW_MEM;
 168           MC_replay(mc_stack_safety_stateless);
 169           break;
 170         } else {
 171           MC_state_delete(state);
 172         }
 173       }
 174       MC_UNSET_RAW_MEM;
 175     }
 176   }
 177   MC_UNSET_RAW_MEM;
 178   return;
 179 }
 180
 181
 182 /********************* DPOR stateful *********************/
 183
 184 mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
 185   mc_state_ws_t sws = NULL;
 186   sws = xbt_new0(s_mc_state_ws_t, 1);
 187   sws->system_state = s;
 188   sws->graph_state = gs;
 189   return sws;
 190 }
 191
 192 void MC_dpor_stateful_init(){
 193
 194   XBT_DEBUG("**************************************************");
 195   XBT_DEBUG("DPOR (stateful) init");
 196   XBT_DEBUG("**************************************************");
 197
 198   mc_state_t initial_graph_state;
 199   smx_process_t process;
 200   mc_snapshot_t initial_system_snapshot;
 201   mc_state_ws_t initial_state ;
 202
 203   MC_wait_for_requests();
 204
 205   MC_SET_RAW_MEM;
 206
 207   initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 208
 209   initial_graph_state = MC_state_new();
 210   xbt_swag_foreach(process, simix_global->process_list){
 211     if(MC_process_is_enabled(process)){
 212       MC_state_interleave_process(initial_graph_state, process);
 213       break;
 214     }
 215   }
 216
 217   MC_take_snapshot(initial_system_snapshot);
 218
 219   initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
 220   xbt_fifo_unshift(mc_stack_safety_stateful, initial_state);
 221
 222   MC_UNSET_RAW_MEM;
 223
 224 }
 225
 226 void MC_dpor_stateful(){
 227
 228   smx_process_t process = NULL;
 229
 230   if(xbt_fifo_size(mc_stack_safety_stateful) == 0)
 231     return;
 232
 233   int value;
 234   mc_state_t next_graph_state = NULL;
 235   smx_req_t req = NULL, prev_req = NULL;
 236   char *req_str;
 237   xbt_fifo_item_t item = NULL;
 238
 239   mc_snapshot_t next_snapshot;
 240   mc_state_ws_t current_state;
 241   mc_state_ws_t prev_state;
 242   mc_state_ws_t next_state;
 243
 244   while(xbt_fifo_size(mc_stack_safety_stateful) > 0){
 245
 246     current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateful));
 247
 248
 249     XBT_DEBUG("**************************************************");
 250     XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_stack_safety_stateful),current_state, MC_state_interleave_size(current_state->graph_state));
 251
 252     mc_stats->visited_states++;
 253     if(mc_stats->expanded_states>1100)
 254       exit(0);
 255     //sleep(1);
 256
 257     if((xbt_fifo_size(mc_stack_safety_stateful) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
 258
 259       /* Debug information */
 260       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 261         req_str = MC_request_to_string(req, value);
 262         //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
 263         XBT_DEBUG("Execute: %s",req_str);
 264         xbt_free(req_str);
 265       }
 266
 267       MC_state_set_executed_request(current_state->graph_state, req, value);
 268       mc_stats->executed_transitions++;
 269
 270       /* Answer the request */
 271       SIMIX_request_pre(req, value);
 272
 273       /* Wait for requests (schedules processes) */
 274       MC_wait_for_requests();
 275
 276       /* Create the new expanded graph_state */
 277       MC_SET_RAW_MEM;
 278
 279       next_graph_state = MC_state_new();
 280
 281       /* Get an enabled process and insert it in the interleave set of the next graph_state */
 282       xbt_swag_foreach(process, simix_global->process_list){
 283         if(MC_process_is_enabled(process)){
 284           MC_state_interleave_process(next_graph_state, process);
 285           break;
 286         }
 287       }
 288
 289       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 290       MC_take_snapshot(next_snapshot);
 291
 292       next_state = new_state_ws(next_snapshot, next_graph_state);
 293       xbt_fifo_unshift(mc_stack_safety_stateful, next_state);
 294
 295       MC_UNSET_RAW_MEM;
 296
 297     }else{
 298       XBT_DEBUG("There are no more processes to interleave.");
 299
 300       /* Trash the current state, no longer needed */
 301       MC_SET_RAW_MEM;
 302       xbt_fifo_shift(mc_stack_safety_stateful);
 303       MC_UNSET_RAW_MEM;
 304
 305       /* Check for deadlocks */
 306       if(MC_deadlock_check()){
 307         MC_show_deadlock_stateful(NULL);
 308         return;
 309       }
 310
 311       MC_SET_RAW_MEM;
 312       while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
 313         req = MC_state_get_internal_request(current_state->graph_state);
 314         xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
 315           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
 316             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 317               XBT_DEBUG("Dependent Transitions:");
 318               prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
 319               req_str = MC_request_to_string(prev_req, value);
 320               XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
 321               xbt_free(req_str);
 322               prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
 323               req_str = MC_request_to_string(prev_req, value);
 324               XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
 325               xbt_free(req_str);
 326             }
 327
 328             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
 329               MC_state_interleave_process(prev_state->graph_state, req->issuer);
 330
 331             } else {
 332               XBT_DEBUG("Process %p is in done set", req->issuer);
 333             }
 334
 335             break;
 336           }
 337         }
 338
 339         if(MC_state_interleave_size(current_state->graph_state)){
 340           MC_restore_snapshot(current_state->system_state);
 341           xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
 342           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
 343           MC_UNSET_RAW_MEM;
 344           break;
 345         }
 346       }
 347
 348       MC_UNSET_RAW_MEM;
 349
 350     }
 351   }
 352   MC_UNSET_RAW_MEM;
 353   return;
 354 }
 355
 356
 357
 358 /************ DPOR 2 (invisible and independant transitions) ************/
 359
 360 xbt_dynar_t reached_pairs_prop;
 361 xbt_dynar_t visible_transitions;
 362 xbt_dynar_t enabled_processes;
 363
 364 mc_prop_ato_t new_proposition(char* id, int value){
 365   mc_prop_ato_t prop = NULL;
 366   prop = xbt_new0(s_mc_prop_ato_t, 1);
 367   prop->id = strdup(id);
 368   prop->value = value;
 369   return prop;
 370 }
 371
 372 mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
 373   mc_pair_prop_t pair = NULL;
 374   pair = xbt_new0(s_mc_pair_prop_t, 1);
 375   pair->system_state = sn;
 376   pair->automaton_state = st;
 377   pair->graph_state = sg;
 378   pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
 379   pair->fully_expanded = 0;
 380   pair->interleave = 0;
 381   mc_stats_pair->expanded_pairs++;
 382   return pair;
 383 }
 384
 385 int reached_prop(mc_pair_prop_t pair){
 386
 387   char* hash_reached = malloc(sizeof(char)*160);
 388   unsigned int c= 0;
 389
 390   MC_SET_RAW_MEM;
 391   char *hash = malloc(sizeof(char)*160);
 392   xbt_sha((char *)&pair, hash);
 393   xbt_dynar_foreach(reached_pairs_prop, c, hash_reached){
 394     if(strcmp(hash, hash_reached) == 0){
 395       MC_UNSET_RAW_MEM;
 396       return 1;
 397     }
 398   }
 399
 400   MC_UNSET_RAW_MEM;
 401   return 0;
 402 }
 403
 404 void set_pair_prop_reached(mc_pair_prop_t pair){
 405
 406   if(reached_prop(pair) == 0){
 407     MC_SET_RAW_MEM;
 408     char *hash = malloc(sizeof(char)*160) ;
 409     xbt_sha((char *)&pair, hash);
 410     xbt_dynar_push(reached_pairs_prop, &hash);
 411     MC_UNSET_RAW_MEM;
 412   }
 413
 414 }
 415
 416 int invisible(mc_pair_prop_t p, mc_pair_prop_t np){
 417   mc_prop_ato_t prop1;
 418   mc_prop_ato_t prop2;
 419   int i;
 420   for(i=0;i<xbt_dynar_length(p->propositions); i++){
 421     prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t);
 422     prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t);
 423     //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value);
 424     if(prop1->value != prop2->value)
 425           return 0;
 426   }
 427   return 1;
 428
 429 }
 430
 431 void set_fully_expanded(mc_pair_prop_t pair){
 432   pair->fully_expanded = 1;
 433 }
 434
 435 void MC_dpor2_init(xbt_automaton_t a)
 436 {
 437   mc_pair_prop_t initial_pair = NULL;
 438   mc_state_t initial_graph_state = NULL;
 439   mc_snapshot_t initial_system_state = NULL;
 440   xbt_state_t initial_automaton_state = NULL;
 441
 442
 443   MC_SET_RAW_MEM;
 444   initial_graph_state = MC_state_new();
 445   MC_UNSET_RAW_MEM;
 446
 447   /* Wait for requests (schedules processes) */
 448   MC_wait_for_requests();
 449
 450   unsigned int cursor = 0;
 451   unsigned int cursor2 = 0;
 452   xbt_state_t automaton_state = NULL;
 453   int res;
 454   xbt_transition_t transition_succ;
 455
 456   xbt_dynar_foreach(a->states, cursor, automaton_state){
 457     if(automaton_state->type == -1){
 458       xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
 459         res = MC_automaton_evaluate_label(a, transition_succ->label);
 460         if((res == 1) || (res == 2)){
 461           initial_automaton_state = transition_succ->dst;
 462           break;
 463         }
 464       }
 465     }
 466
 467     if(initial_automaton_state != NULL)
 468       break;
 469   }
 470
 471   if(initial_automaton_state == NULL){
 472     cursor = 0;
 473     xbt_dynar_foreach(a->states, cursor, automaton_state){
 474       if(automaton_state->type == -1){
 475         initial_automaton_state = automaton_state;
 476         break;
 477       }
 478     }
 479   }
 480
 481   reached_pairs_prop = xbt_dynar_new(sizeof(char *), NULL);
 482   visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL);
 483   enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL);
 484
 485   MC_SET_RAW_MEM;
 486   initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
 487   MC_take_snapshot(initial_system_state);
 488   initial_pair = new_pair_prop(initial_system_state, initial_graph_state, initial_automaton_state);
 489   cursor = 0;
 490   xbt_propositional_symbol_t ps;
 491   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 492     int (*f)() = ps->function;
 493     int val = (*f)();
 494     mc_prop_ato_t pa = new_proposition(ps->pred, val);
 495     xbt_dynar_push(initial_pair->propositions, &pa);
 496   }
 497   xbt_fifo_unshift(mc_stack_liveness_stateful, initial_pair);
 498   MC_UNSET_RAW_MEM;
 499
 500
 501   XBT_DEBUG("**************************************************");
 502   XBT_DEBUG("Initial pair");
 503
 504   MC_dpor2(a, 0);
 505
 506 }
 507
 508
 509 void MC_dpor2(xbt_automaton_t a, int search_cycle)
 510 {
 511   char *req_str;
 512   int value;
 513   smx_req_t req = NULL, prev_req = NULL;
 514   mc_state_t next_graph_state = NULL;
 515   mc_snapshot_t next_system_state = NULL;
 516   xbt_state_t next_automaton_state = NULL;
 517   xbt_transition_t transition_succ;
 518   unsigned int cursor;
 519   int res;
 520   mc_pair_prop_t pair = NULL, next_pair = NULL, prev_pair = NULL;
 521   smx_process_t process = NULL;
 522   xbt_fifo_item_t item = NULL;
 523   int d;
 524
 525
 526   while (xbt_fifo_size(mc_stack_liveness_stateful) > 0) {
 527
 528     /* Get current pair */
 529     pair = (mc_pair_prop_t)
 530       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 531
 532     XBT_DEBUG("**************************************************");
 533     XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
 534               xbt_fifo_size(mc_stack_liveness_stateful), pair, MC_state_interleave_size(pair->graph_state));
 535
 536     if(MC_state_interleave_size(pair->graph_state) == 0){
 537
 538       xbt_dynar_reset(enabled_processes);
 539
 540       MC_SET_RAW_MEM;
 541
 542       xbt_swag_foreach(process, simix_global->process_list){
 543         if(MC_process_is_enabled(process)){
 544           xbt_dynar_push(enabled_processes, &process);
 545           //XBT_DEBUG("Process : pid=%lu",process->pid);
 546         }
 547       }
 548
 549       //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
 550
 551       //XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
 552
 553       if(xbt_dynar_length(enabled_processes) > 0){
 554         for(d=0;d<pair->interleave;d++){
 555           xbt_dynar_shift(enabled_processes, NULL);
 556         }
 557       }
 558
 559       //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
 560
 561       if(pair->fully_expanded == 0){
 562         if(xbt_dynar_length(enabled_processes) > 0){
 563           MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t));
 564           //XBT_DEBUG("Interleave process");
 565         }
 566       }
 567
 568       MC_UNSET_RAW_MEM;
 569
 570     }
 571
 572
 573     /* Update statistics */
 574     mc_stats_pair->visited_pairs++;
 575     //sleep(1);
 576
 577     /*cursor = 0;
 578     mc_prop_ato_t pato;
 579     xbt_dynar_foreach(pair->propositions, cursor, pato){
 580       XBT_DEBUG("%s : %d", pato->id, pato->value);
 581       }*/
 582
 583     /* Test acceptance pair and acceptance cycle*/
 584
 585     if(pair->automaton_state->type == 1){
 586       if(search_cycle == 0){
 587         set_pair_prop_reached(pair);
 588         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
 589       }else{
 590         if(reached_prop(pair) == 1){
 591           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 592           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 593           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 594           XBT_INFO("Counter-example that violates formula :");
 595           MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 596           MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 597           MC_print_statistics_pairs(mc_stats_pair);
 598           exit(0);
 599         }
 600       }
 601     }
 602
 603     /* If there are processes to interleave and the maximum depth has not been reached
 604        then perform one step of the exploration algorithm */
 605     if (xbt_fifo_size(mc_stack_liveness_stateful) < MAX_DEPTH &&
 606         (req = MC_state_get_request(pair->graph_state, &value))) {
 607
 608       /* Debug information */
 609       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 610         req_str = MC_request_to_string(req, value);
 611         XBT_DEBUG("Execute: %s", req_str);
 612         xbt_free(req_str);
 613       }
 614
 615       MC_state_set_executed_request(pair->graph_state, req, value);
 616       //mc_stats_pairs->executed_transitions++;
 617
 618       /* Answer the request */
 619       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
 620
 621       /* Wait for requests (schedules processes) */
 622       MC_wait_for_requests();
 623
 624       /* Create the new expanded state */
 625       MC_SET_RAW_MEM;
 626
 627       pair->interleave++;
 628       //XBT_DEBUG("Process interleaved in pair %p : %u", pair, MC_state_interleave_size(pair->graph_state));
 629       //xbt_dynar_pop(enabled_processes, NULL);
 630
 631       next_graph_state = MC_state_new();
 632
 633       next_system_state = xbt_new0(s_mc_snapshot_t, 1);
 634       MC_take_snapshot(next_system_state);
 635       MC_UNSET_RAW_MEM;
 636
 637       cursor = 0;
 638       xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
 639         res = MC_automaton_evaluate_label(a, transition_succ->label);
 640         if((res == 1) || (res == 2)){ // enabled transition in automaton
 641           next_automaton_state = transition_succ->dst;
 642           break;
 643         }
 644       }
 645
 646       if(next_automaton_state == NULL){
 647         next_automaton_state = pair->automaton_state;
 648       }
 649
 650       MC_SET_RAW_MEM;
 651
 652       next_pair = new_pair_prop(next_system_state, next_graph_state, next_automaton_state);
 653       cursor = 0;
 654       xbt_propositional_symbol_t ps;
 655       xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 656         int (*f)() = ps->function;
 657         int val = (*f)();
 658         mc_prop_ato_t pa = new_proposition(ps->pred, val);
 659         xbt_dynar_push(next_pair->propositions, &pa);
 660         //XBT_DEBUG("%s : %d", pa->id, pa->value);
 661       }
 662       xbt_fifo_unshift(mc_stack_liveness_stateful, next_pair);
 663
 664       cursor = 0;
 665       if((invisible(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
 666         set_fully_expanded(pair);
 667         if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié
 668           xbt_dynar_foreach(enabled_processes, cursor, process){
 669             MC_state_interleave_process(pair->graph_state, process);
 670           }
 671         }
 672         XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state));
 673       }
 674
 675       MC_UNSET_RAW_MEM;
 676
 677
 678       /* Let's loop again */
 679
 680       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 681     } else {
 682       XBT_DEBUG("There are no more processes to interleave.");
 683
 684       /* Trash the current state, no longer needed */
 685       MC_SET_RAW_MEM;
 686       xbt_fifo_shift(mc_stack_liveness_stateful);
 687       //MC_state_delete(state);
 688       MC_UNSET_RAW_MEM;
 689
 690       /* Check for deadlocks */
 691       if(MC_deadlock_check()){
 692         MC_show_deadlock(NULL);
 693         return;
 694       }
 695
 696       MC_SET_RAW_MEM;
 697       /* Traverse the stack backwards until a state with a non empty interleave
 698          set is found, deleting all the states that have it empty in the way.
 699          For each deleted state, check if the request that has generated it
 700          (from it's predecesor state), depends on any other previous request
 701          executed before it. If it does then add it to the interleave set of the
 702          state that executed that previous request. */
 703       while ((pair = xbt_fifo_shift(mc_stack_liveness_stateful)) != NULL) {
 704         req = MC_state_get_internal_request(pair->graph_state);
 705         xbt_fifo_foreach(mc_stack_liveness_stateful, item, prev_pair, mc_pair_prop_t) {
 706           if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
 707             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 708               XBT_DEBUG("Dependent Transitions:");
 709               prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
 710               req_str = MC_request_to_string(prev_req, value);
 711               XBT_DEBUG("%s (pair=%p)", req_str, prev_pair);
 712               xbt_free(req_str);
 713               prev_req = MC_state_get_executed_request(pair->graph_state, &value);
 714               req_str = MC_request_to_string(prev_req, value);
 715               XBT_DEBUG("%s (pair=%p)", req_str, pair);
 716               xbt_free(req_str);
 717             }
 718
 719             if(prev_pair->fully_expanded == 0){
 720               if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
 721                 MC_state_interleave_process(prev_pair->graph_state, req->issuer);
 722                 XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair);
 723               }else{
 724                 XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid);
 725               }
 726             }
 727
 728             break;
 729           }
 730         }
 731
 732
 733         if (MC_state_interleave_size(pair->graph_state) > 0) {
 734           /* We found a back-tracking point, let's loop */
 735           MC_restore_snapshot(pair->system_state);
 736           xbt_fifo_unshift(mc_stack_liveness_stateful, pair);
 737           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_liveness_stateful));
 738           MC_UNSET_RAW_MEM;
 739           break;
 740         } else {
 741           //MC_state_delete(state);
 742         }
 743       }
 744       MC_UNSET_RAW_MEM;
 745     }
 746   }
 747   MC_UNSET_RAW_MEM;
 748   return;
 749 }
 750
 751 /************ DPOR 3 (invisible and independant transitions with coloration of pairs) ************/
 752
 753 int expanded;
 754 xbt_dynar_t reached_pairs_prop_col;
 755 xbt_dynar_t visited_pairs_prop_col;
 756
 757
 758
 759 mc_pair_prop_col_t new_pair_prop_col(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
 760
 761   mc_pair_prop_col_t pair = NULL;
 762   pair = xbt_new0(s_mc_pair_prop_col_t, 1);
 763   pair->system_state = sn;
 764   pair->automaton_state = st;
 765   pair->graph_state = sg;
 766   pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
 767   pair->fully_expanded = 0;
 768   pair->interleave = 0;
 769   pair->color=ORANGE;
 770   mc_stats_pair->expanded_pairs++;
 771   //XBT_DEBUG("New pair %p : automaton=%p", pair, st);
 772   return pair;
 773 }
 774
 775 void set_expanded(mc_pair_prop_col_t pair){
 776   pair->expanded = expanded;
 777 }
 778
 779 int reached_prop_col(mc_pair_prop_col_t pair){
 780
 781   char* hash_reached = malloc(sizeof(char)*160);
 782   unsigned int c= 0;
 783
 784   MC_SET_RAW_MEM;
 785   char *hash = malloc(sizeof(char)*160);
 786   xbt_sha((char *)&pair, hash);
 787   xbt_dynar_foreach(reached_pairs_prop_col, c, hash_reached){
 788     if(strcmp(hash, hash_reached) == 0){
 789       MC_UNSET_RAW_MEM;
 790       return 1;
 791     }
 792   }
 793
 794   MC_UNSET_RAW_MEM;
 795   return 0;
 796 }
 797
 798 void set_pair_prop_col_reached(mc_pair_prop_col_t pair){
 799
 800   if(reached_prop_col(pair) == 0){
 801     MC_SET_RAW_MEM;
 802     char *hash = malloc(sizeof(char)*160) ;
 803     xbt_sha((char *)&pair, hash);
 804     xbt_dynar_push(reached_pairs_prop_col, &hash);
 805     MC_UNSET_RAW_MEM;
 806   }
 807
 808 }
 809
 810 int invisible_col(mc_pair_prop_col_t p, mc_pair_prop_col_t np){
 811   mc_prop_ato_t prop1;
 812   mc_prop_ato_t prop2;
 813   int i;
 814   for(i=0;i<xbt_dynar_length(p->propositions); i++){
 815     prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t);
 816     prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t);
 817     //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value);
 818     if(prop1->value != prop2->value)
 819           return 0;
 820   }
 821   return 1;
 822
 823 }
 824
 825 void set_fully_expanded_col(mc_pair_prop_col_t pair){
 826   pair->fully_expanded = 1;
 827   pair->color = GREEN;
 828 }
 829
 830 void set_pair_prop_col_visited(mc_pair_prop_col_t pair, int sc){
 831
 832   MC_SET_RAW_MEM;
 833   mc_visited_pair_prop_col_t p = NULL;
 834   p = xbt_new0(s_mc_visited_pair_prop_col_t, 1);
 835   p->pair = pair;
 836   p->search_cycle = sc;
 837   char *hash = malloc(sizeof(char)*160);
 838   xbt_sha((char *)&p, hash);
 839   xbt_dynar_push(visited_pairs_prop_col, &hash);
 840   MC_UNSET_RAW_MEM;
 841
 842 }
 843
 844 int visited_pair_prop_col(mc_pair_prop_col_t pair, int sc){
 845
 846   char* hash_visited = malloc(sizeof(char)*160);
 847   unsigned int c= 0;
 848
 849   MC_SET_RAW_MEM;
 850   mc_visited_pair_prop_col_t p = NULL;
 851   p = xbt_new0(s_mc_visited_pair_prop_col_t, 1);
 852   p->pair = pair;
 853   p->search_cycle = sc;
 854   char *hash = malloc(sizeof(char)*160);
 855   xbt_sha((char *)&p, hash);
 856   xbt_dynar_foreach(visited_pairs_prop_col, c, hash_visited){
 857     if(strcmp(hash, hash_visited) == 0){
 858       MC_UNSET_RAW_MEM;
 859       return 1;
 860     }
 861   }
 862
 863   MC_UNSET_RAW_MEM;
 864   return 0;
 865
 866 }
 867
 868 void MC_dpor3_init(xbt_automaton_t a)
 869 {
 870   mc_pair_prop_col_t initial_pair = NULL;
 871   mc_state_t initial_graph_state = NULL;
 872   mc_snapshot_t initial_system_state = NULL;
 873   xbt_state_t initial_automaton_state = NULL;
 874
 875
 876   MC_SET_RAW_MEM;
 877   initial_graph_state = MC_state_new();
 878   MC_UNSET_RAW_MEM;
 879
 880   /* Wait for requests (schedules processes) */
 881   MC_wait_for_requests();
 882
 883   unsigned int cursor = 0;
 884   unsigned int cursor2 = 0;
 885   xbt_state_t automaton_state = NULL;
 886   int res;
 887   xbt_transition_t transition_succ;
 888
 889   xbt_dynar_foreach(a->states, cursor, automaton_state){
 890     if(automaton_state->type == -1){
 891       xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
 892         res = MC_automaton_evaluate_label(a, transition_succ->label);
 893         if((res == 1) || (res == 2)){
 894           initial_automaton_state = transition_succ->dst;
 895           break;
 896         }
 897       }
 898     }
 899
 900     if(initial_automaton_state != NULL)
 901       break;
 902   }
 903
 904   if(initial_automaton_state == NULL){
 905     cursor = 0;
 906     xbt_dynar_foreach(a->states, cursor, automaton_state){
 907       if(automaton_state->type == -1){
 908         initial_automaton_state = automaton_state;
 909         break;
 910       }
 911     }
 912   }
 913
 914   reached_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL);
 915   visited_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL);
 916   visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL);
 917   enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL);
 918   expanded = 0;
 919
 920   MC_SET_RAW_MEM;
 921   initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
 922   MC_take_snapshot(initial_system_state);
 923   initial_pair = new_pair_prop_col(initial_system_state, initial_graph_state, initial_automaton_state);
 924   cursor = 0;
 925   xbt_propositional_symbol_t ps;
 926   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 927     int (*f)() = ps->function;
 928     int val = (*f)();
 929     mc_prop_ato_t pa = new_proposition(ps->pred, val);
 930     xbt_dynar_push(initial_pair->propositions, &pa);
 931   }
 932   xbt_fifo_unshift(mc_stack_liveness_stateful, initial_pair);
 933   MC_UNSET_RAW_MEM;
 934
 935
 936   XBT_DEBUG("**************************************************");
 937   XBT_DEBUG("Initial pair");
 938
 939   MC_dpor3(a, 0);
 940
 941 }
 942
 943
 944 void MC_dpor3(xbt_automaton_t a, int search_cycle)
 945 {
 946   char *req_str;
 947   int value;
 948   smx_req_t req = NULL, prev_req = NULL;
 949   mc_state_t next_graph_state = NULL;
 950   mc_snapshot_t next_system_state = NULL;
 951   xbt_state_t next_automaton_state = NULL;
 952   xbt_transition_t transition_succ;
 953   unsigned int cursor;
 954   int res;
 955   mc_pair_prop_col_t pair = NULL, next_pair = NULL, prev_pair = NULL;
 956   smx_process_t process = NULL;
 957   xbt_fifo_item_t item = NULL;
 958   int d;
 959
 960
 961   while (xbt_fifo_size(mc_stack_liveness_stateful) > 0) {
 962
 963     /* Get current pair */
 964     pair = (mc_pair_prop_col_t)
 965       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 966
 967     XBT_DEBUG("**************************************************");
 968     XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
 969               xbt_fifo_size(mc_stack_liveness_stateful), pair, MC_state_interleave_size(pair->graph_state));
 970
 971     if(MC_state_interleave_size(pair->graph_state) == 0){
 972
 973       xbt_dynar_reset(enabled_processes);
 974
 975       MC_SET_RAW_MEM;
 976
 977       xbt_swag_foreach(process, simix_global->process_list){
 978         if(MC_process_is_enabled(process)){
 979           xbt_dynar_push(enabled_processes, &process);
 980           //XBT_DEBUG("Process : pid=%lu",process->pid);
 981         }
 982       }
 983
 984       //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
 985
 986       //XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
 987
 988       if(xbt_dynar_length(enabled_processes) > 0){
 989         for(d=0;d<pair->interleave;d++){
 990           xbt_dynar_shift(enabled_processes, NULL);
 991         }
 992       }
 993
 994       //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
 995
 996       if(pair->fully_expanded == 0){
 997         if(xbt_dynar_length(enabled_processes) > 0){
 998           MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t));
 999           //XBT_DEBUG("Interleave process");
1000         }
1001       }
1002
1003       MC_UNSET_RAW_MEM;
1004
1005     }
1006
1007
1008     /* Update statistics */
1009     mc_stats_pair->visited_pairs++;
1010     //sleep(1);
1011
1012     /* Test acceptance pair and acceptance cycle*/
1013
1014     if(pair->automaton_state->type == 1){
1015       if(search_cycle == 0){
1016         set_pair_prop_col_reached(pair);
1017         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
1018       }else{
1019         if(reached_prop_col(pair) == 1){
1020           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1021           XBT_INFO("|             ACCEPTANCE CYCLE            |");
1022           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1023           XBT_INFO("Counter-example that violates formula :");
1024           MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
1025           MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
1026           MC_print_statistics_pairs(mc_stats_pair);
1027           exit(0);
1028         }
1029       }
1030     }
1031
1032     /* If there are processes to interleave and the maximum depth has not been reached
1033        then perform one step of the exploration algorithm */
1034     if (xbt_fifo_size(mc_stack_liveness_stateful) < MAX_DEPTH &&
1035         (req = MC_state_get_request(pair->graph_state, &value))) {
1036
1037       set_pair_prop_col_visited(pair, search_cycle);
1038
1039       /* Debug information */
1040       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
1041         req_str = MC_request_to_string(req, value);
1042         XBT_DEBUG("Execute: %s", req_str);
1043         xbt_free(req_str);
1044       }
1045
1046       MC_state_set_executed_request(pair->graph_state, req, value);
1047
1048       /* Answer the request */
1049       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
1050
1051       /* Wait for requests (schedules processes) */
1052       MC_wait_for_requests();
1053
1054       /* Create the new expanded state */
1055       MC_SET_RAW_MEM;
1056
1057       pair->interleave++;
1058
1059       next_graph_state = MC_state_new();
1060
1061       next_system_state = xbt_new0(s_mc_snapshot_t, 1);
1062       MC_take_snapshot(next_system_state);
1063       MC_UNSET_RAW_MEM;
1064
1065       cursor = 0;
1066       xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
1067         res = MC_automaton_evaluate_label(a, transition_succ->label);
1068         if((res == 1) || (res == 2)){ // enabled transition in automaton
1069           next_automaton_state = transition_succ->dst;
1070           break;
1071         }
1072       }
1073
1074       if(next_automaton_state == NULL)
1075         next_automaton_state = pair->automaton_state;
1076
1077       MC_SET_RAW_MEM;
1078
1079       next_pair = new_pair_prop_col(next_system_state, next_graph_state, next_automaton_state);
1080       cursor = 0;
1081       xbt_propositional_symbol_t ps;
1082       xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
1083         int (*f)() = ps->function;
1084         int val = (*f)();
1085         mc_prop_ato_t pa = new_proposition(ps->pred, val);
1086         xbt_dynar_push(next_pair->propositions, &pa);
1087       }
1088       xbt_fifo_unshift(mc_stack_liveness_stateful, next_pair);
1089
1090       cursor = 0;
1091       if((invisible_col(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
1092         set_fully_expanded_col(pair);
1093         if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié
1094           xbt_dynar_foreach(enabled_processes, cursor, process){
1095             MC_state_interleave_process(pair->graph_state, process);
1096           }
1097         }
1098         XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state));
1099       }
1100
1101       MC_UNSET_RAW_MEM;
1102
1103
1104       /* Let's loop again */
1105
1106       /* The interleave set is empty or the maximum depth is reached, let's back-track */
1107     } else {
1108       XBT_DEBUG("There are no more processes to interleave.");
1109
1110       /* Trash the current state, no longer needed */
1111       MC_SET_RAW_MEM;
1112       xbt_fifo_shift(mc_stack_liveness_stateful);
1113       //MC_state_delete(state);
1114       MC_UNSET_RAW_MEM;
1115
1116       /* Check for deadlocks */
1117       if(MC_deadlock_check()){
1118         MC_show_deadlock(NULL);
1119         return;
1120       }
1121
1122       MC_SET_RAW_MEM;
1123       /* Traverse the stack backwards until a state with a non empty interleave
1124          set is found, deleting all the states that have it empty in the way.
1125          For each deleted state, check if the request that has generated it
1126          (from it's predecesor state), depends on any other previous request
1127          executed before it. If it does then add it to the interleave set of the
1128          state that executed that previous request. */
1129       while ((pair = xbt_fifo_shift(mc_stack_liveness_stateful)) != NULL) {
1130         req = MC_state_get_internal_request(pair->graph_state);
1131         xbt_fifo_foreach(mc_stack_liveness_stateful, item, prev_pair, mc_pair_prop_col_t) {
1132           if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
1133             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
1134               XBT_DEBUG("Dependent Transitions:");
1135               prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
1136               req_str = MC_request_to_string(prev_req, value);
1137               XBT_DEBUG("%s (pair=%p)", req_str, prev_pair);
1138               xbt_free(req_str);
1139               prev_req = MC_state_get_executed_request(pair->graph_state, &value);
1140               req_str = MC_request_to_string(prev_req, value);
1141               XBT_DEBUG("%s (pair=%p)", req_str, pair);
1142               xbt_free(req_str);
1143             }
1144
1145             if(prev_pair->fully_expanded == 0){
1146               if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
1147                 MC_state_interleave_process(prev_pair->graph_state, req->issuer);
1148                 XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair);
1149               }else{
1150                 XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid);
1151               }
1152             }
1153
1154             break;
1155           }
1156         }
1157
1158
1159         if (MC_state_interleave_size(pair->graph_state) > 0) {
1160           /* We found a back-tracking point, let's loop */
1161           MC_restore_snapshot(pair->system_state);
1162           xbt_fifo_unshift(mc_stack_liveness_stateful, pair);
1163           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_liveness_stateful));
1164           MC_UNSET_RAW_MEM;
1165           break;
1166         } else {
1167           //MC_state_delete(state);
1168         }
1169       }
1170       MC_UNSET_RAW_MEM;
1171     }
1172   }
1173   MC_UNSET_RAW_MEM;
1174   return;
1175 }