src/mc/mc_liveness.c

   1 /* Copyright (c) 2011-2014. The SimGrid Team.
   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 <unistd.h>
   8 #include <sys/wait.h>
   9
  10 #include <xbt/dynar.h>
  11 #include <xbt/automaton.h>
  12
  13 #include "mc_request.h"
  14 #include "mc_liveness.h"
  15 #include "mc_private.h"
  16 #include "mc_record.h"
  17 #include "mc_smx.h"
  18
  19 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  20                                 "Logging specific to algorithms for liveness properties verification");
  21
  22 /********* Global variables *********/
  23
  24 xbt_dynar_t acceptance_pairs;
  25 xbt_parmap_t parmap;
  26
  27 /********* Static functions *********/
  28
  29 static xbt_dynar_t get_atomic_propositions_values()
  30 {
  31   unsigned int cursor = 0;
  32   xbt_automaton_propositional_symbol_t ps = NULL;
  33   xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
  34   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) {
  35     int res = xbt_automaton_propositional_symbol_evaluate(ps);
  36     xbt_dynar_push_as(values, int, res);
  37   }
  38
  39   return values;
  40 }
  41
  42 static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
  43   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
  44
  45   mc_visited_pair_t new_pair = NULL;
  46   new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
  47   new_pair->acceptance_pair = 1;
  48
  49   if (xbt_dynar_is_empty(acceptance_pairs)) {
  50
  51     xbt_dynar_push(acceptance_pairs, &new_pair);
  52
  53   } else {
  54
  55     int min = -1, max = -1, index;
  56     //int res;
  57     mc_visited_pair_t pair_test;
  58     int cursor;
  59
  60     index = get_search_interval(acceptance_pairs, new_pair, &min, &max);
  61
  62     if (min != -1 && max != -1) {       // Acceptance pair with same number of processes and same heap bytes used exists
  63
  64       // Parallell implementation
  65       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
  66          if(res != -1){
  67          if(!raw_mem_set)
  68          MC_SET_STD_HEAP;
  69          return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
  70          } */
  71
  72       cursor = min;
  73       if(pair->search_cycle == 1){
  74         while (cursor <= max) {
  75           pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
  76           if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
  77             if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0) {
  78               if (snapshot_compare(pair_test, new_pair) == 0) {
  79                 XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
  80                 xbt_fifo_shift(mc_stack);
  81                 if (dot_output != NULL)
  82                   fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
  83                 mmalloc_set_current_heap(heap);
  84                 return NULL;
  85               }
  86             }
  87           }
  88           cursor++;
  89         }
  90       }
  91       xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
  92     } else {
  93       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
  94       if (pair_test->nb_processes < new_pair->nb_processes) {
  95         xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
  96       } else {
  97         if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
  98           xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
  99         else
 100           xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
 101       }
 102     }
 103
 104   }
 105   mmalloc_set_current_heap(heap);
 106   return new_pair;
 107 }
 108
 109 static void remove_acceptance_pair(int pair_num)
 110 {
 111   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 112
 113   unsigned int cursor = 0;
 114   mc_visited_pair_t pair_test = NULL;
 115   int pair_found = 0;
 116
 117   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) {
 118     if (pair_test->num == pair_num) {
 119        pair_found = 1;
 120       break;
 121     }
 122   }
 123
 124   if(pair_found == 1) {
 125     xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
 126
 127     pair_test->acceptance_removed = 1;
 128
 129     if (_sg_mc_visited == 0 || pair_test->visited_removed == 1)
 130       MC_visited_pair_delete(pair_test);
 131
 132   }
 133
 134   mmalloc_set_current_heap(heap);
 135 }
 136
 137
 138 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
 139                                        xbt_dynar_t atomic_propositions_values)
 140 {
 141
 142   switch (l->type) {
 143   case 0:{
 144       int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
 145       int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 146       return (left_res || right_res);
 147     }
 148   case 1:{
 149       int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
 150       int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 151       return (left_res && right_res);
 152     }
 153   case 2:{
 154       int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
 155       return (!res);
 156     }
 157   case 3:{
 158       unsigned int cursor = 0;
 159       xbt_automaton_propositional_symbol_t p = NULL;
 160       xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p) {
 161         if (strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
 162           return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int);
 163       }
 164       return -1;
 165     }
 166   case 4:{
 167       return 2;
 168     }
 169   default:
 170     return -1;
 171   }
 172 }
 173
 174 void MC_pre_modelcheck_liveness(void) {
 175
 176   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 177
 178   mc_pair_t initial_pair = NULL;
 179   smx_process_t process;
 180
 181   MC_wait_for_requests();
 182
 183   MC_SET_MC_HEAP;
 184
 185   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
 186   if(_sg_mc_visited > 0)
 187     visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
 188
 189   initial_global_state->snapshot = MC_take_snapshot(0);
 190   initial_global_state->prev_pair = 0;
 191
 192   unsigned int cursor = 0;
 193   xbt_automaton_state_t automaton_state;
 194
 195   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state) {
 196     if (automaton_state->type == -1) {  /* Initial automaton state */
 197
 198       initial_pair = MC_pair_new();
 199       initial_pair->automaton_state = automaton_state;
 200       initial_pair->graph_state = MC_state_new();
 201       initial_pair->atomic_propositions = get_atomic_propositions_values();
 202       initial_pair->depth = 1;
 203
 204       /* Get enabled processes and insert them in the interleave set of the graph_state */
 205       MC_EACH_SIMIX_PROCESS(process,
 206         if (MC_process_is_enabled(process)) {
 207           MC_state_interleave_process(initial_pair->graph_state, process);
 208         }
 209       );
 210
 211       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
 212       initial_pair->search_cycle = 0;
 213
 214       xbt_fifo_unshift(mc_stack, initial_pair);
 215     }
 216   }
 217
 218   MC_SET_STD_HEAP;
 219
 220   MC_modelcheck_liveness();
 221
 222   if (initial_global_state->raw_mem_set)
 223     MC_SET_MC_HEAP;
 224 }
 225
 226 void MC_modelcheck_liveness()
 227 {
 228   smx_process_t process = NULL;
 229   mc_pair_t current_pair = NULL;
 230   int value, res, visited_num = -1;
 231   smx_simcall_t req = NULL;
 232   xbt_automaton_transition_t transition_succ = NULL;
 233   int cursor = 0;
 234   mc_pair_t next_pair = NULL;
 235   xbt_dynar_t prop_values = NULL;
 236   mc_visited_pair_t reached_pair = NULL;
 237
 238   while(xbt_fifo_size(mc_stack) > 0){
 239
 240     /* Get current pair */
 241     current_pair = (mc_pair_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 242
 243     /* Update current state in buchi automaton */
 244     _mc_property_automaton->current_state = current_pair->automaton_state;
 245
 246     XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)",
 247        current_pair->depth, current_pair->search_cycle,
 248        MC_state_interleave_size(current_pair->graph_state), current_pair->num);
 249
 250     if (current_pair->requests > 0) {
 251
 252       if (current_pair->automaton_state->type == 1 && current_pair->exploration_started == 0) {
 253         /* If new acceptance pair, return new pair */
 254         if ((reached_pair = is_reached_acceptance_pair(current_pair)) == NULL) {
 255           int counter_example_depth = current_pair->depth;
 256           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 257           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 258           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 259           XBT_INFO("Counter-example that violates formula :");
 260           MC_show_stack_liveness(mc_stack);
 261           MC_dump_stack_liveness(mc_stack);
 262           MC_print_statistics(mc_stats);
 263           XBT_INFO("Counter-example depth : %d", counter_example_depth);
 264           xbt_abort();
 265         }
 266       }
 267
 268       /* Pair already visited ? stop the exploration on the current path */
 269       if ((current_pair->exploration_started == 0) && (visited_num = is_visited_pair(reached_pair, current_pair)) != -1) {
 270
 271         if (dot_output != NULL){
 272           MC_SET_MC_HEAP;
 273           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, visited_num, initial_global_state->prev_req);
 274           fflush(dot_output);
 275           MC_SET_STD_HEAP;
 276         }
 277
 278         XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
 279         MC_SET_MC_HEAP;
 280         current_pair->requests = 0;
 281         MC_SET_STD_HEAP;
 282         goto backtracking;
 283
 284       }else{
 285
 286         req = MC_state_get_request(current_pair->graph_state, &value);
 287
 288          if (dot_output != NULL) {
 289            MC_SET_MC_HEAP;
 290            if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
 291              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req);
 292              xbt_free(initial_global_state->prev_req);
 293            }
 294            initial_global_state->prev_pair = current_pair->num;
 295            initial_global_state->prev_req = MC_request_get_dot_output(req, value);
 296            if (current_pair->search_cycle)
 297              fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 298            fflush(dot_output);
 299            MC_SET_STD_HEAP;
 300          }
 301
 302          char* req_str = MC_request_to_string(req, value);
 303          XBT_DEBUG("Execute: %s", req_str);
 304          xbt_free(req_str);
 305
 306          /* Set request as executed */
 307          MC_state_set_executed_request(current_pair->graph_state, req, value);
 308
 309          /* Update mc_stats */
 310          mc_stats->executed_transitions++;
 311          if(current_pair->exploration_started == 0)
 312            mc_stats->visited_pairs++;
 313
 314          /* Answer the request */
 315          MC_simcall_handle(req, value);
 316
 317          /* Wait for requests (schedules processes) */
 318          MC_wait_for_requests();
 319
 320          MC_SET_MC_HEAP;
 321
 322          current_pair->requests--;
 323          current_pair->exploration_started = 1;
 324
 325          /* Get values of atomic propositions (variables used in the property formula) */
 326          prop_values = get_atomic_propositions_values();
 327
 328          /* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */
 329          cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
 330          while (cursor >= 0) {
 331            transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
 332            res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 333            if (res == 1 || res == 2) { /* 1 = True transition (always enabled), 2 = enabled transition according to atomic prop values */
 334               next_pair = MC_pair_new();
 335               next_pair->graph_state = MC_state_new();
 336               next_pair->automaton_state = transition_succ->dst;
 337               next_pair->atomic_propositions = get_atomic_propositions_values();
 338               next_pair->depth = current_pair->depth + 1;
 339               /* Get enabled processes and insert them in the interleave set of the next graph_state */
 340               MC_EACH_SIMIX_PROCESS(process,
 341                 if (MC_process_is_enabled(process)) {
 342                   MC_state_interleave_process(next_pair->graph_state, process);
 343                 }
 344               );
 345
 346               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 347
 348               /* FIXME : get search_cycle value for each acceptant state */
 349               if (next_pair->automaton_state->type == 1 || current_pair->search_cycle)
 350                 next_pair->search_cycle = 1;
 351
 352               /* Add new pair to the exploration stack */
 353               xbt_fifo_unshift(mc_stack, next_pair);
 354
 355            }
 356            cursor--;
 357          }
 358
 359          MC_SET_STD_HEAP;
 360
 361       } /* End of visited_pair test */
 362
 363     } else {
 364
 365     backtracking:
 366       if(visited_num == -1)
 367         XBT_DEBUG("No more request to execute. Looking for backtracking point.");
 368
 369       MC_SET_MC_HEAP;
 370
 371       xbt_dynar_free(&prop_values);
 372
 373       /* Traverse the stack backwards until a pair with a non empty interleave
 374          set is found, deleting all the pairs that have it empty in the way. */
 375       while ((current_pair = xbt_fifo_shift(mc_stack)) != NULL) {
 376         if (current_pair->requests > 0) {
 377           /* We found a backtracking point */
 378           XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
 379           xbt_fifo_unshift(mc_stack, current_pair);
 380           MC_SET_STD_HEAP;
 381           MC_replay_liveness(mc_stack);
 382           XBT_DEBUG("Backtracking done");
 383           break;
 384         }else{
 385           /* Delete pair */
 386           XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
 387           if (current_pair->automaton_state->type == 1)
 388             remove_acceptance_pair(current_pair->num);
 389           MC_pair_delete(current_pair);
 390         }
 391       }
 392
 393       MC_SET_STD_HEAP;
 394     } /* End of if (current_pair->requests > 0) else ... */
 395
 396   } /* End of while(xbt_fifo_size(mc_stack) > 0) */
 397
 398 }