src/mc/mc_liveness.c

   1 /* Copyright (c) 2011-2013 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 "mc_private.h"
   7 #include <unistd.h>
   8 #include <sys/wait.h>
   9
  10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  11                                 "Logging specific to algorithms for liveness properties verification");
  12
  13 /********* Global variables *********/
  14
  15 xbt_dynar_t acceptance_pairs;
  16 xbt_dynar_t visited_pairs;
  17 xbt_dynar_t successors;
  18
  19
  20 /********* Static functions *********/
  21
  22 static xbt_dynar_t get_atomic_propositions_values(){
  23   int res;
  24   int_f_void_t f;
  25   unsigned int cursor = 0;
  26   xbt_automaton_propositional_symbol_t ps = NULL;
  27   xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
  28
  29   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
  30     f = (int_f_void_t)ps->function;
  31     res = f();
  32     xbt_dynar_push_as(values, int, res);
  33   }
  34
  35   return values;
  36 }
  37
  38 static int is_reached_acceptance_pair(mc_pair_t pair){
  39
  40   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  41
  42   if(xbt_dynar_is_empty(acceptance_pairs)){
  43
  44     MC_SET_RAW_MEM;
  45     if(pair->graph_state->system_state == NULL){
  46       pair->graph_state->system_state = MC_take_snapshot();
  47       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
  48     }
  49     xbt_dynar_push(acceptance_pairs, &pair);
  50     MC_UNSET_RAW_MEM;
  51
  52     if(raw_mem_set)
  53       MC_SET_RAW_MEM;
  54
  55     return -1;
  56
  57   }else{
  58
  59     MC_SET_RAW_MEM;
  60
  61     if(pair->graph_state->system_state == NULL){
  62       pair->graph_state->system_state = MC_take_snapshot();
  63       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
  64     }
  65
  66     size_t current_bytes_used = pair->heap_bytes_used;
  67     int current_nb_processes = pair->nb_processes;
  68
  69     unsigned int cursor = 0;
  70     int previous_cursor = 0, next_cursor = 0;
  71     int start = 0;
  72     int end = xbt_dynar_length(acceptance_pairs) - 1;
  73
  74     mc_pair_t pair_test = NULL;
  75     size_t bytes_used_test;
  76     int nb_processes_test;
  77     int same_processes_and_bytes_not_found = 1;
  78
  79     while(start <= end && same_processes_and_bytes_not_found){
  80       cursor = (start + end) / 2;
  81       pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
  82       bytes_used_test = pair_test->heap_bytes_used;
  83       nb_processes_test = pair_test->nb_processes;
  84       if(nb_processes_test < current_nb_processes)
  85         start = cursor + 1;
  86       else if(nb_processes_test > current_nb_processes)
  87         end = cursor - 1;
  88       else if(nb_processes_test == current_nb_processes){
  89         if(bytes_used_test < current_bytes_used)
  90           start = cursor + 1;
  91         else if(bytes_used_test > current_bytes_used)
  92           end = cursor - 1;
  93         else if(bytes_used_test == current_bytes_used){
  94           same_processes_and_bytes_not_found = 0;
  95           if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
  96             if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
  97               XBT_DEBUG("Compare with state %d", pair_test->num);
  98               if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
  99                 if(raw_mem_set)
 100                   MC_SET_RAW_MEM;
 101                 else
 102                   MC_UNSET_RAW_MEM;
 103                 return pair_test->num;
 104               }
 105             }
 106           }
 107           /* Search another pair with same number of bytes used in std_heap */
 108           previous_cursor = cursor - 1;
 109           while(previous_cursor >= 0){
 110             pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_pair_t);
 111             bytes_used_test = pair_test->heap_bytes_used;
 112             if(bytes_used_test != current_bytes_used)
 113               break;
 114             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
 115               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
 116                 XBT_DEBUG("Compare with state %d", pair_test->num);
 117                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
 118                   if(raw_mem_set)
 119                     MC_SET_RAW_MEM;
 120                   else
 121                     MC_UNSET_RAW_MEM;
 122                   return pair_test->num;
 123                 }
 124               }
 125             }
 126             previous_cursor--;
 127           }
 128           next_cursor = cursor + 1;
 129           while(next_cursor < xbt_dynar_length(acceptance_pairs)){
 130             pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_pair_t);
 131             bytes_used_test = pair_test->heap_bytes_used;
 132             if(bytes_used_test != current_bytes_used)
 133               break;
 134             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
 135               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
 136                 XBT_DEBUG("Compare with state %d", pair_test->num);
 137                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
 138                   if(raw_mem_set)
 139                     MC_SET_RAW_MEM;
 140                   else
 141                     MC_UNSET_RAW_MEM;
 142                   return pair_test->num;
 143                 }
 144               }
 145             }
 146             next_cursor++;
 147           }
 148         }
 149       }
 150     }
 151
 152     pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
 153     bytes_used_test = pair_test->heap_bytes_used;
 154
 155     if(bytes_used_test < current_bytes_used)
 156       xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
 157     else
 158       xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
 159
 160
 161     MC_UNSET_RAW_MEM;
 162
 163     if(raw_mem_set)
 164       MC_SET_RAW_MEM;
 165
 166     return -1;
 167
 168   }
 169
 170 }
 171
 172
 173 static void set_acceptance_pair_reached(mc_pair_t pair){
 174
 175   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 176
 177   if(xbt_dynar_is_empty(acceptance_pairs)){
 178
 179      MC_SET_RAW_MEM;
 180      if(pair->graph_state->system_state == NULL){
 181        pair->graph_state->system_state = MC_take_snapshot();
 182        pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
 183      }
 184      xbt_dynar_push(acceptance_pairs, &pair);
 185      MC_UNSET_RAW_MEM;
 186
 187   }else{
 188
 189     MC_SET_RAW_MEM;
 190
 191     if(pair->graph_state->system_state == NULL){
 192       pair->graph_state->system_state = MC_take_snapshot();
 193       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
 194     }
 195
 196     size_t current_bytes_used = pair->heap_bytes_used;
 197     int current_nb_processes = pair->nb_processes;
 198
 199     unsigned int cursor = 0;
 200     int start = 0;
 201     int end = xbt_dynar_length(acceptance_pairs) - 1;
 202
 203     mc_pair_t pair_test = NULL;
 204     size_t bytes_used_test = 0;
 205     int nb_processes_test;
 206
 207     while(start <= end){
 208       cursor = (start + end) / 2;
 209       pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
 210       bytes_used_test = pair_test->heap_bytes_used;
 211       nb_processes_test = pair_test->nb_processes;
 212       if(nb_processes_test < current_nb_processes)
 213         start = cursor + 1;
 214       if(nb_processes_test > current_nb_processes)
 215         end = cursor - 1;
 216       if(nb_processes_test == current_nb_processes){
 217         if(bytes_used_test < current_bytes_used)
 218           start = cursor + 1;
 219         if(bytes_used_test > current_bytes_used)
 220           end = cursor - 1;
 221         if(bytes_used_test == current_bytes_used)
 222           break;
 223       }
 224     }
 225
 226     if(bytes_used_test < current_bytes_used)
 227       xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
 228     else
 229       xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
 230
 231     MC_UNSET_RAW_MEM;
 232
 233   }
 234
 235   if(raw_mem_set)
 236     MC_SET_RAW_MEM;
 237
 238 }
 239
 240 static void remove_acceptance_pair(mc_pair_t pair){
 241
 242   unsigned int cursor = 0;
 243   mc_pair_t pair_test;
 244   int pair_found = 0;
 245
 246   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
 247     if(pair_test->num == pair->num){
 248       pair_found = 1;
 249       break;
 250     }
 251   }
 252
 253   if(pair_found)
 254     xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
 255
 256   pair->acceptance_removed = 1;
 257
 258   if(pair->stack_removed && pair->acceptance_removed){
 259     if(_sg_mc_visited == 0){
 260       MC_pair_delete(pair);
 261     }else if(pair->visited_removed){
 262       MC_pair_delete(pair);
 263     }
 264   }
 265
 266 }
 267
 268 static int is_visited_pair(mc_pair_t pair){
 269
 270   if(_sg_mc_visited == 0)
 271     return -1;
 272
 273   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 274
 275   if(xbt_dynar_is_empty(visited_pairs)){
 276
 277     MC_SET_RAW_MEM;
 278     if(pair->graph_state->system_state == NULL)
 279       pair->graph_state->system_state = MC_take_snapshot();
 280     xbt_dynar_push(visited_pairs, &pair);
 281     MC_UNSET_RAW_MEM;
 282
 283     if(raw_mem_set)
 284       MC_SET_RAW_MEM;
 285
 286     return -1;
 287
 288   }else{
 289
 290     MC_SET_RAW_MEM;
 291
 292     if(pair->graph_state->system_state == NULL)
 293       pair->graph_state->system_state = MC_take_snapshot();
 294
 295     size_t current_bytes_used = pair->heap_bytes_used;
 296     int current_nb_processes = pair->nb_processes;
 297
 298     unsigned int cursor = 0;
 299     int previous_cursor = 0, next_cursor = 0;
 300     int start = 0;
 301     int end = xbt_dynar_length(visited_pairs) - 1;
 302
 303     mc_pair_t pair_test = NULL;
 304     size_t bytes_used_test;
 305     int nb_processes_test;
 306     int same_processes_and_bytes_not_found = 1;
 307
 308     while(start <= end && same_processes_and_bytes_not_found){
 309       cursor = (start + end) / 2;
 310       pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
 311       bytes_used_test = pair_test->heap_bytes_used;
 312       nb_processes_test = pair_test->nb_processes;
 313       if(nb_processes_test < current_nb_processes)
 314         start = cursor + 1;
 315       else if(nb_processes_test > current_nb_processes)
 316         end = cursor - 1;
 317       else if(nb_processes_test == current_nb_processes){
 318         if(bytes_used_test < current_bytes_used)
 319           start = cursor + 1;
 320         else if(bytes_used_test > current_bytes_used)
 321           end = cursor - 1;
 322         else if(bytes_used_test == current_bytes_used){
 323           same_processes_and_bytes_not_found = 0;
 324           if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
 325             if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
 326               if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
 327                 if(pair_test->other_num == -1)
 328                   pair->other_num = pair_test->num;
 329                 else
 330                   pair->other_num = pair_test->other_num;
 331                 if(dot_output == NULL)
 332                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 333                 else
 334                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 335                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 336                 xbt_dynar_insert_at(visited_pairs, cursor, &pair);
 337                 pair_test->visited_removed = 1;
 338                 if(pair_test->stack_removed && pair_test->visited_removed){
 339                   if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 340                     if(pair_test->acceptance_removed){
 341                       MC_pair_delete(pair_test);
 342                     }
 343                   }else{
 344                     MC_pair_delete(pair_test);
 345                   }
 346                 }
 347                 if(raw_mem_set)
 348                   MC_SET_RAW_MEM;
 349                 else
 350                   MC_UNSET_RAW_MEM;
 351                 return pair->other_num;
 352               }
 353             }
 354           }
 355           /* Search another pair with same number of bytes used in std_heap */
 356           previous_cursor = cursor - 1;
 357           while(previous_cursor >= 0){
 358             pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_pair_t);
 359             bytes_used_test = pair_test->heap_bytes_used;
 360             if(bytes_used_test != current_bytes_used)
 361               break;
 362             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
 363               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
 364                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
 365                   if(pair_test->other_num == -1)
 366                     pair->other_num = pair_test->num;
 367                   else
 368                     pair->other_num = pair_test->other_num;
 369                   if(dot_output == NULL)
 370                     XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 371                   else
 372                     XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 373                   xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
 374                   xbt_dynar_insert_at(visited_pairs, previous_cursor, &pair);
 375                   pair_test->visited_removed = 1;
 376                   if(pair_test->stack_removed && pair_test->visited_removed){
 377                     if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 378                       if(pair_test->acceptance_removed){
 379                         MC_pair_delete(pair_test);
 380                       }
 381                     }else{
 382                       MC_pair_delete(pair_test);
 383                     }
 384                   }
 385                   if(raw_mem_set)
 386                     MC_SET_RAW_MEM;
 387                   else
 388                     MC_UNSET_RAW_MEM;
 389                   return pair->other_num;
 390                 }
 391               }
 392             }
 393             previous_cursor--;
 394           }
 395           next_cursor = cursor + 1;
 396           while(next_cursor < xbt_dynar_length(visited_pairs)){
 397             pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_pair_t);
 398             bytes_used_test = pair_test->heap_bytes_used;
 399             if(bytes_used_test != current_bytes_used)
 400               break;
 401             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
 402               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
 403                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
 404                   if(pair_test->other_num == -1)
 405                     pair->other_num = pair_test->num;
 406                   else
 407                     pair->other_num = pair_test->other_num;
 408                   if(dot_output == NULL)
 409                     XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 410                   else
 411                     XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 412                   xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
 413                   xbt_dynar_insert_at(visited_pairs, next_cursor, &pair);
 414                   pair_test->visited_removed = 1;
 415                   if(pair_test->stack_removed && pair_test->visited_removed){
 416                     if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 417                       if(pair_test->acceptance_removed){
 418                         MC_pair_delete(pair_test);
 419                       }
 420                     }else{
 421                       MC_pair_delete(pair_test);
 422                     }
 423                   }
 424                   if(raw_mem_set)
 425                     MC_SET_RAW_MEM;
 426                   else
 427                     MC_UNSET_RAW_MEM;
 428                   return pair->other_num;
 429                 }
 430               }
 431             }
 432             next_cursor++;
 433           }
 434         }
 435       }
 436     }
 437
 438     pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
 439     bytes_used_test = pair_test->heap_bytes_used;
 440
 441     if(bytes_used_test < current_bytes_used)
 442       xbt_dynar_insert_at(visited_pairs, cursor + 1, &pair);
 443     else
 444       xbt_dynar_insert_at(visited_pairs, cursor, &pair);
 445
 446     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
 447       int min = mc_stats->expanded_states;
 448       unsigned int cursor2 = 0;
 449       unsigned int index = 0;
 450       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
 451         if(pair_test->num < min){
 452           index = cursor2;
 453           min = pair_test->num;
 454         }
 455       }
 456       xbt_dynar_remove_at(visited_pairs, index, &pair_test);
 457       pair_test->visited_removed = 1;
 458       if(pair_test->stack_removed && pair_test->acceptance_removed && pair_test->visited_removed)
 459         MC_pair_delete(pair_test);
 460
 461     }
 462
 463     MC_UNSET_RAW_MEM;
 464
 465     if(raw_mem_set)
 466       MC_SET_RAW_MEM;
 467
 468     return -1;
 469
 470   }
 471
 472 }
 473
 474 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
 475
 476   switch(l->type){
 477   case 0 : {
 478     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
 479     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 480     return (left_res || right_res);
 481   }
 482   case 1 : {
 483     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
 484     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 485     return (left_res && right_res);
 486   }
 487   case 2 : {
 488     int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
 489     return (!res);
 490   }
 491   case 3 : {
 492     unsigned int cursor = 0;
 493     xbt_automaton_propositional_symbol_t p = NULL;
 494     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 495       if(strcmp(p->pred, l->u.predicat) == 0)
 496         return (int)xbt_dynar_get_as(atomic_propositions_values, cursor, int);
 497     }
 498     return -1;
 499   }
 500   case 4 : {
 501     return 2;
 502   }
 503   default :
 504     return -1;
 505   }
 506 }
 507
 508
 509 /********* DDFS Algorithm *********/
 510
 511
 512 void MC_ddfs_init(void){
 513
 514   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 515
 516   XBT_DEBUG("**************************************************");
 517   XBT_DEBUG("Double-DFS init");
 518   XBT_DEBUG("**************************************************");
 519
 520   mc_pair_t initial_pair = NULL;
 521   smx_process_t process;
 522
 523   MC_wait_for_requests();
 524
 525   MC_SET_RAW_MEM;
 526
 527   acceptance_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 528   visited_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 529   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 530
 531   initial_state_liveness->snapshot = MC_take_snapshot();
 532   initial_state_liveness->prev_pair = 0;
 533
 534   MC_UNSET_RAW_MEM;
 535
 536   unsigned int cursor = 0;
 537   xbt_automaton_state_t automaton_state;
 538
 539   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
 540     if(automaton_state->type == -1){ /* Initial automaton state */
 541
 542       MC_SET_RAW_MEM;
 543
 544       initial_pair = MC_pair_new();
 545       initial_pair->automaton_state = automaton_state;
 546       initial_pair->graph_state = MC_state_new();
 547       initial_pair->atomic_propositions = get_atomic_propositions_values();
 548
 549       /* Get enabled process and insert it in the interleave set of the graph_state */
 550       xbt_swag_foreach(process, simix_global->process_list){
 551         if(MC_process_is_enabled(process)){
 552           MC_state_interleave_process(initial_pair->graph_state, process);
 553         }
 554       }
 555
 556       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
 557       initial_pair->search_cycle = 0;
 558
 559       xbt_fifo_unshift(mc_stack_liveness, initial_pair);
 560
 561       MC_UNSET_RAW_MEM;
 562
 563       MC_ddfs();
 564
 565       if(cursor != 0){
 566         MC_restore_snapshot(initial_state_liveness->snapshot);
 567         MC_UNSET_RAW_MEM;
 568       }
 569
 570
 571     }else if(automaton_state->type == 2){ /* Acceptance automaton state */
 572
 573       MC_SET_RAW_MEM;
 574
 575       initial_pair = MC_pair_new();
 576       initial_pair->automaton_state = automaton_state;
 577       initial_pair->graph_state = MC_state_new();
 578       initial_pair->atomic_propositions = get_atomic_propositions_values();
 579
 580       /* Get enabled process and insert it in the interleave set of the graph_state */
 581       xbt_swag_foreach(process, simix_global->process_list){
 582         if(MC_process_is_enabled(process)){
 583           MC_state_interleave_process(initial_pair->graph_state, process);
 584         }
 585       }
 586
 587       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
 588       initial_pair->search_cycle = 1;
 589
 590       xbt_fifo_unshift(mc_stack_liveness, initial_pair);
 591
 592       MC_UNSET_RAW_MEM;
 593
 594       set_acceptance_pair_reached(initial_pair);
 595
 596       MC_ddfs();
 597
 598       if(cursor != 0){
 599         MC_restore_snapshot(initial_state_liveness->snapshot);
 600         MC_UNSET_RAW_MEM;
 601       }
 602     }
 603   }
 604
 605   if(initial_state_liveness->raw_mem_set)
 606     MC_SET_RAW_MEM;
 607   else
 608     MC_UNSET_RAW_MEM;
 609
 610
 611 }
 612
 613
 614 void MC_ddfs(){
 615
 616   smx_process_t process;
 617   mc_pair_t current_pair = NULL;
 618
 619   if(xbt_fifo_size(mc_stack_liveness) == 0)
 620     return;
 621
 622   /* Get current pair */
 623   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 624
 625   /* Update current state in buchi automaton */
 626   _mc_property_automaton->current_state = current_pair->automaton_state;
 627
 628   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle);
 629
 630   mc_stats->visited_pairs++;
 631
 632   int value;
 633   smx_simcall_t req = NULL;
 634   char *req_str;
 635
 636   xbt_automaton_transition_t transition_succ;
 637   unsigned int cursor = 0;
 638   int res;
 639   int reached_num, visited_num;
 640
 641   mc_pair_t next_pair = NULL;
 642   xbt_dynar_t prop_values = NULL;
 643
 644   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 645
 646     if(current_pair->requests > 0){
 647
 648       if(current_pair->search_cycle){
 649
 650         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 651
 652           if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
 653
 654             XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
 655
 656             MC_SET_RAW_MEM;
 657             xbt_fifo_shift(mc_stack_liveness);
 658             if(dot_output != NULL)
 659               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, reached_num, initial_state_liveness->prev_req);
 660             MC_UNSET_RAW_MEM;
 661
 662             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 663             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 664             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 665             XBT_INFO("Counter-example that violates formula :");
 666             MC_show_stack_liveness(mc_stack_liveness);
 667             MC_dump_stack_liveness(mc_stack_liveness);
 668             MC_print_statistics(mc_stats);
 669             xbt_abort();
 670
 671           }
 672         }
 673       }
 674
 675       if((visited_num = is_visited_pair(current_pair)) != -1){
 676
 677         MC_SET_RAW_MEM;
 678         if(dot_output != NULL)
 679           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
 680         MC_UNSET_RAW_MEM;
 681
 682
 683       }else{
 684
 685         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 686
 687           MC_SET_RAW_MEM;
 688           if(dot_output != NULL){
 689             if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
 690               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
 691               xbt_free(initial_state_liveness->prev_req);
 692             }
 693             initial_state_liveness->prev_pair = current_pair->num;
 694           }
 695           MC_UNSET_RAW_MEM;
 696
 697           /* Debug information */
 698           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 699             req_str = MC_request_to_string(req, value);
 700             XBT_DEBUG("Execute: %s", req_str);
 701             xbt_free(req_str);
 702           }
 703
 704           MC_SET_RAW_MEM;
 705           if(dot_output != NULL){
 706             initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
 707             if(current_pair->search_cycle)
 708               fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 709           }
 710           MC_UNSET_RAW_MEM;
 711
 712           MC_state_set_executed_request(current_pair->graph_state, req, value);
 713           mc_stats->executed_transitions++;
 714
 715           /* Answer the request */
 716           SIMIX_simcall_pre(req, value);
 717
 718           /* Wait for requests (schedules processes) */
 719           MC_wait_for_requests();
 720
 721           MC_SET_RAW_MEM;
 722           prop_values = get_atomic_propositions_values();
 723           MC_UNSET_RAW_MEM;
 724
 725           /* Evaluate enabled transition according to atomic propositions values */
 726           cursor= 0;
 727           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 728
 729             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 730
 731             if(res == 1){ // enabled transition in automaton
 732
 733               MC_SET_RAW_MEM;
 734
 735               next_pair = MC_pair_new();
 736               next_pair->graph_state = MC_state_new();
 737               next_pair->automaton_state = transition_succ->dst;
 738               next_pair->atomic_propositions = get_atomic_propositions_values();
 739
 740               /* Get enabled process and insert it in the interleave set of the next graph_state */
 741               xbt_swag_foreach(process, simix_global->process_list){
 742                 if(MC_process_is_enabled(process)){
 743                   MC_state_interleave_process(next_pair->graph_state, process);
 744                 }
 745               }
 746
 747               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 748
 749               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 750                 next_pair->search_cycle = 1;
 751
 752               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 753
 754               if(mc_stats->expanded_pairs%1000000 == 0)
 755                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 756
 757               MC_UNSET_RAW_MEM;
 758
 759               MC_ddfs();
 760
 761             }
 762
 763           }
 764
 765           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 766           cursor = 0;
 767           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 768
 769             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 770
 771             if(res == 2){ // true transition in automaton
 772
 773               MC_SET_RAW_MEM;
 774
 775               next_pair = MC_pair_new();
 776               next_pair->graph_state = MC_state_new();
 777               next_pair->automaton_state = transition_succ->dst;
 778               next_pair->atomic_propositions = get_atomic_propositions_values();
 779
 780               /* Get enabled process and insert it in the interleave set of the next graph_state */
 781               xbt_swag_foreach(process, simix_global->process_list){
 782                 if(MC_process_is_enabled(process)){
 783                   MC_state_interleave_process(next_pair->graph_state, process);
 784                 }
 785               }
 786
 787               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 788
 789               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 790                 next_pair->search_cycle = 1;
 791
 792               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 793
 794               if(mc_stats->expanded_pairs%1000000 == 0)
 795                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 796
 797               MC_UNSET_RAW_MEM;
 798
 799               MC_ddfs();
 800
 801             }
 802
 803           }
 804
 805           if(MC_state_interleave_size(current_pair->graph_state) > 0){
 806             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 807             MC_replay_liveness(mc_stack_liveness, 0);
 808           }
 809
 810         }
 811
 812       }
 813
 814     }else{
 815
 816       mc_stats->executed_transitions++;
 817
 818       XBT_DEBUG("No request to execute in this state, search evolution in Büchi Automaton.");
 819
 820       if(current_pair->search_cycle){
 821
 822         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 823
 824           if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
 825
 826             XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
 827
 828             MC_SET_RAW_MEM;
 829             xbt_fifo_shift(mc_stack_liveness);
 830             MC_UNSET_RAW_MEM;
 831
 832             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 833             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 834             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 835             XBT_INFO("Counter-example that violates formula :");
 836             MC_show_stack_liveness(mc_stack_liveness);
 837             MC_dump_stack_liveness(mc_stack_liveness);
 838             MC_print_statistics(mc_stats);
 839             xbt_abort();
 840
 841           }
 842         }
 843       }
 844
 845       if((visited_num = is_visited_pair(current_pair)) != -1){
 846
 847         XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
 848
 849       }else{
 850
 851         MC_SET_RAW_MEM;
 852         prop_values = get_atomic_propositions_values();
 853         MC_UNSET_RAW_MEM;
 854
 855         /* Evaluate enabled transition according to atomic propositions values */
 856         cursor= 0;
 857         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 858
 859           res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 860
 861           if(res == 1){ // enabled transition in automaton
 862
 863             MC_SET_RAW_MEM;
 864
 865             next_pair = MC_pair_new();
 866             next_pair->graph_state = MC_state_new();
 867             next_pair->automaton_state = transition_succ->dst;
 868             next_pair->atomic_propositions = get_atomic_propositions_values();
 869             next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 870
 871             if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 872               next_pair->search_cycle = 1;
 873
 874             xbt_fifo_unshift(mc_stack_liveness, next_pair);
 875
 876             if(mc_stats->expanded_pairs%1000 == 0)
 877               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 878
 879             if(dot_output != NULL)
 880               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
 881
 882             MC_UNSET_RAW_MEM;
 883
 884             MC_ddfs();
 885
 886           }
 887
 888         }
 889
 890         /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 891         cursor = 0;
 892         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 893
 894           res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 895
 896           if(res == 2){ // true transition in automaton
 897
 898             MC_SET_RAW_MEM;
 899
 900             next_pair = MC_pair_new();
 901             next_pair->graph_state = MC_state_new();
 902             next_pair->automaton_state = transition_succ->dst;
 903             next_pair->atomic_propositions = get_atomic_propositions_values();
 904             next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 905
 906             if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 907               next_pair->search_cycle = 1;
 908
 909             xbt_fifo_unshift(mc_stack_liveness, next_pair);
 910
 911             if(mc_stats->expanded_pairs%1000 == 0)
 912               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 913
 914             if(dot_output != NULL)
 915               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
 916
 917             MC_UNSET_RAW_MEM;
 918
 919             MC_ddfs();
 920
 921           }
 922
 923         }
 924       }
 925     }
 926
 927   }else{
 928
 929     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 930     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 931       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 932       if(_sg_mc_max_depth == 1000)
 933         XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 934     }
 935
 936   }
 937
 938   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 939     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 940   }else{
 941     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 942   }
 943
 944
 945   MC_SET_RAW_MEM;
 946   xbt_dynar_free(&prop_values);
 947   current_pair = xbt_fifo_shift(mc_stack_liveness);
 948   current_pair->stack_removed = 1;
 949   if(current_pair->search_cycle){
 950     remove_acceptance_pair(current_pair);
 951   }else{
 952     if(_sg_mc_visited == 0)
 953       MC_pair_delete(current_pair);
 954     else if(current_pair->visited_removed)
 955       MC_pair_delete(current_pair);
 956   }
 957
 958   MC_UNSET_RAW_MEM;
 959
 960 }