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   int new_pair = 0;
 641
 642   mc_pair_t next_pair = NULL;
 643   xbt_dynar_t prop_values = NULL;
 644
 645   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 646
 647     if(current_pair->requests > 0){
 648
 649       if(current_pair->search_cycle){
 650
 651         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 652
 653           if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
 654
 655             XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
 656
 657             MC_SET_RAW_MEM;
 658             xbt_fifo_shift(mc_stack_liveness);
 659             if(dot_output != NULL)
 660               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, reached_num, initial_state_liveness->prev_req);
 661             MC_UNSET_RAW_MEM;
 662
 663             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 664             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 665             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 666             XBT_INFO("Counter-example that violates formula :");
 667             MC_show_stack_liveness(mc_stack_liveness);
 668             MC_dump_stack_liveness(mc_stack_liveness);
 669             MC_print_statistics(mc_stats);
 670             xbt_abort();
 671
 672           }
 673         }
 674       }
 675
 676       if((visited_num = is_visited_pair(current_pair)) != -1){
 677
 678         MC_SET_RAW_MEM;
 679         if(dot_output != NULL)
 680           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
 681         MC_UNSET_RAW_MEM;
 682
 683
 684       }else{
 685
 686         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 687
 688           MC_SET_RAW_MEM;
 689           if(dot_output != NULL){
 690             if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
 691               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
 692               xbt_free(initial_state_liveness->prev_req);
 693             }
 694             initial_state_liveness->prev_pair = current_pair->num;
 695           }
 696           MC_UNSET_RAW_MEM;
 697
 698           /* Debug information */
 699           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 700             req_str = MC_request_to_string(req, value);
 701             XBT_DEBUG("Execute: %s", req_str);
 702             xbt_free(req_str);
 703           }
 704
 705           MC_SET_RAW_MEM;
 706           if(dot_output != NULL){
 707             initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
 708             if(current_pair->search_cycle)
 709               fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 710           }
 711           MC_UNSET_RAW_MEM;
 712
 713           MC_state_set_executed_request(current_pair->graph_state, req, value);
 714           mc_stats->executed_transitions++;
 715
 716           /* Answer the request */
 717           SIMIX_simcall_pre(req, value);
 718
 719           /* Wait for requests (schedules processes) */
 720           MC_wait_for_requests();
 721
 722           MC_SET_RAW_MEM;
 723           prop_values = get_atomic_propositions_values();
 724           MC_UNSET_RAW_MEM;
 725
 726           /* Evaluate enabled transition according to atomic propositions values */
 727           cursor= 0;
 728           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 729
 730             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 731
 732             if(res == 1){ // enabled transition in automaton
 733
 734               if(new_pair)
 735                MC_replay_liveness(mc_stack_liveness, 1);
 736
 737               MC_SET_RAW_MEM;
 738
 739               next_pair = MC_pair_new();
 740               next_pair->graph_state = MC_state_new();
 741               next_pair->automaton_state = transition_succ->dst;
 742               next_pair->atomic_propositions = get_atomic_propositions_values();
 743
 744               /* Get enabled process and insert it in the interleave set of the next graph_state */
 745               xbt_swag_foreach(process, simix_global->process_list){
 746                 if(MC_process_is_enabled(process)){
 747                   MC_state_interleave_process(next_pair->graph_state, process);
 748                 }
 749               }
 750
 751               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 752
 753               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 754                 next_pair->search_cycle = 1;
 755
 756               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 757
 758               if(mc_stats->expanded_pairs%1000000 == 0)
 759                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 760
 761               MC_UNSET_RAW_MEM;
 762
 763               new_pair = 1;
 764
 765               MC_ddfs();
 766
 767             }
 768
 769           }
 770
 771           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 772           cursor = 0;
 773           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 774
 775             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 776
 777             if(res == 2){ // true transition in automaton
 778
 779               if(new_pair)
 780                 MC_replay_liveness(mc_stack_liveness, 1);
 781
 782               MC_SET_RAW_MEM;
 783
 784               next_pair = MC_pair_new();
 785               next_pair->graph_state = MC_state_new();
 786               next_pair->automaton_state = transition_succ->dst;
 787               next_pair->atomic_propositions = get_atomic_propositions_values();
 788
 789               /* Get enabled process and insert it in the interleave set of the next graph_state */
 790               xbt_swag_foreach(process, simix_global->process_list){
 791                 if(MC_process_is_enabled(process)){
 792                   MC_state_interleave_process(next_pair->graph_state, process);
 793                 }
 794               }
 795
 796               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 797
 798               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 799                 next_pair->search_cycle = 1;
 800
 801               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 802
 803               if(mc_stats->expanded_pairs%1000000 == 0)
 804                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 805
 806               MC_UNSET_RAW_MEM;
 807
 808               new_pair = 1;
 809
 810               MC_ddfs();
 811
 812             }
 813
 814           }
 815
 816           if(MC_state_interleave_size(current_pair->graph_state) > 0){
 817             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 818             MC_replay_liveness(mc_stack_liveness, 0);
 819           }
 820
 821         }
 822
 823       }
 824
 825     }else{
 826
 827       mc_stats->executed_transitions++;
 828
 829       XBT_DEBUG("No request to execute in this state, search evolution in Büchi Automaton.");
 830
 831       if(current_pair->search_cycle){
 832
 833         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 834
 835           if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
 836
 837             XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
 838
 839             MC_SET_RAW_MEM;
 840             xbt_fifo_shift(mc_stack_liveness);
 841             MC_UNSET_RAW_MEM;
 842
 843             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 844             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 845             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 846             XBT_INFO("Counter-example that violates formula :");
 847             MC_show_stack_liveness(mc_stack_liveness);
 848             MC_dump_stack_liveness(mc_stack_liveness);
 849             MC_print_statistics(mc_stats);
 850             xbt_abort();
 851
 852           }
 853         }
 854       }
 855
 856       if((visited_num = is_visited_pair(current_pair)) != -1){
 857
 858         XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
 859
 860       }else{
 861
 862         MC_SET_RAW_MEM;
 863         prop_values = get_atomic_propositions_values();
 864         MC_UNSET_RAW_MEM;
 865
 866         /* Evaluate enabled transition according to atomic propositions values */
 867         cursor= 0;
 868         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 869
 870           res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 871
 872           if(res == 1){ // enabled transition in automaton
 873
 874             if(new_pair)
 875               MC_replay_liveness(mc_stack_liveness, 1);
 876
 877             MC_SET_RAW_MEM;
 878
 879             next_pair = MC_pair_new();
 880             next_pair->graph_state = MC_state_new();
 881             next_pair->automaton_state = transition_succ->dst;
 882             next_pair->atomic_propositions = get_atomic_propositions_values();
 883             next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 884
 885             if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 886               next_pair->search_cycle = 1;
 887
 888             xbt_fifo_unshift(mc_stack_liveness, next_pair);
 889
 890             if(mc_stats->expanded_pairs%1000 == 0)
 891               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 892
 893             if(dot_output != NULL)
 894               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
 895
 896             MC_UNSET_RAW_MEM;
 897
 898             new_pair = 1;
 899
 900             MC_ddfs();
 901
 902           }
 903
 904         }
 905
 906         /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 907         cursor = 0;
 908         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 909
 910           res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 911
 912           if(res == 2){ // true transition in automaton
 913
 914             if(new_pair)
 915               MC_replay_liveness(mc_stack_liveness, 1);
 916
 917             MC_SET_RAW_MEM;
 918
 919             next_pair = MC_pair_new();
 920             next_pair->graph_state = MC_state_new();
 921             next_pair->automaton_state = transition_succ->dst;
 922             next_pair->atomic_propositions = get_atomic_propositions_values();
 923             next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 924
 925             if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 926               next_pair->search_cycle = 1;
 927
 928             xbt_fifo_unshift(mc_stack_liveness, next_pair);
 929
 930             if(mc_stats->expanded_pairs%1000 == 0)
 931               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 932
 933             if(dot_output != NULL)
 934               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
 935
 936             MC_UNSET_RAW_MEM;
 937
 938             new_pair = 1;
 939
 940             MC_ddfs();
 941
 942           }
 943
 944         }
 945       }
 946     }
 947
 948   }else{
 949
 950     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 951     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 952       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 953       if(_sg_mc_max_depth == 1000)
 954         XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 955     }
 956
 957   }
 958
 959   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 960     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 961   }else{
 962     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 963   }
 964
 965
 966   MC_SET_RAW_MEM;
 967   xbt_dynar_free(&prop_values);
 968   current_pair = xbt_fifo_shift(mc_stack_liveness);
 969   current_pair->stack_removed = 1;
 970   if(current_pair->search_cycle){
 971     remove_acceptance_pair(current_pair);
 972   }else{
 973     if(_sg_mc_visited == 0)
 974       MC_pair_delete(current_pair);
 975     else if(current_pair->visited_removed)
 976       MC_pair_delete(current_pair);
 977   }
 978   MC_UNSET_RAW_MEM;
 979
 980 }