src/mc/mc_dpor.c

   1 /* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved.           */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "mc_private.h"
   7
   8 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
   9                                 "Logging specific to MC DPOR exploration");
  10
  11 xbt_dynar_t visited_states;
  12
  13 static int is_visited_state(void);
  14
  15 static int is_visited_state(){
  16
  17   if(_surf_mc_stateful == 0)
  18     return 0;
  19
  20   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  21
  22   MC_SET_RAW_MEM;
  23
  24   mc_snapshot_t new_state = NULL;
  25   new_state = MC_take_snapshot();
  26
  27   MC_UNSET_RAW_MEM;
  28
  29   if(xbt_dynar_is_empty(visited_states)){
  30
  31     MC_SET_RAW_MEM;
  32     xbt_dynar_push(visited_states, &new_state);
  33     MC_UNSET_RAW_MEM;
  34
  35     if(raw_mem_set)
  36       MC_SET_RAW_MEM;
  37
  38     return 0;
  39
  40   }else{
  41
  42     MC_SET_RAW_MEM;
  43
  44     unsigned int cursor = 0;
  45     mc_snapshot_t state_test = NULL;
  46
  47     xbt_dynar_foreach(visited_states, cursor, state_test){
  48       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
  49         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
  50       if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
  51         if(raw_mem_set)
  52           MC_SET_RAW_MEM;
  53         else
  54           MC_UNSET_RAW_MEM;
  55
  56         return 1;
  57       }
  58     }
  59
  60     if(xbt_dynar_length(visited_states) == _surf_mc_stateful){
  61       mc_snapshot_t state_to_remove = NULL;
  62       xbt_dynar_shift(visited_states, &state_to_remove);
  63       MC_free_snapshot(state_to_remove);
  64     }
  65
  66     xbt_dynar_push(visited_states, &new_state);
  67
  68     MC_UNSET_RAW_MEM;
  69
  70     if(raw_mem_set)
  71       MC_SET_RAW_MEM;
  72
  73     return 0;
  74
  75   }
  76 }
  77
  78 /**
  79  *  \brief Initialize the DPOR exploration algorithm
  80  */
  81 void MC_dpor_init()
  82 {
  83
  84   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  85
  86   mc_state_t initial_state = NULL;
  87   smx_process_t process;
  88
  89   /* Create the initial state and push it into the exploration stack */
  90   MC_SET_RAW_MEM;
  91
  92   initial_state = MC_state_new();
  93   visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL);
  94
  95   MC_UNSET_RAW_MEM;
  96
  97   XBT_DEBUG("**************************************************");
  98   XBT_DEBUG("Initial state");
  99
 100   /* Wait for requests (schedules processes) */
 101   MC_wait_for_requests();
 102
 103   MC_SET_RAW_MEM;
 104
 105   xbt_swag_foreach(process, simix_global->process_list){
 106     if(MC_process_is_enabled(process)){
 107       XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 108     }
 109   }
 110
 111   /* Get an enabled process and insert it in the interleave set of the initial state */
 112   xbt_swag_foreach(process, simix_global->process_list){
 113     if(MC_process_is_enabled(process)){
 114       MC_state_interleave_process(initial_state, process);
 115       break;
 116     }
 117   }
 118
 119   xbt_fifo_unshift(mc_stack_safety, initial_state);
 120
 121   MC_UNSET_RAW_MEM;
 122
 123   if(raw_mem_set)
 124     MC_SET_RAW_MEM;
 125   else
 126     MC_UNSET_RAW_MEM;
 127
 128
 129   /* FIXME: Update Statistics
 130      mc_stats->state_size +=
 131      xbt_setset_set_size(initial_state->enabled_transitions); */
 132 }
 133
 134
 135 /**
 136  *   \brief Perform the model-checking operation using a depth-first search exploration
 137  *         with Dynamic Partial Order Reductions
 138  */
 139 void MC_dpor(void)
 140 {
 141
 142   char *req_str;
 143   int value;
 144   smx_simcall_t req = NULL, prev_req = NULL;
 145   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
 146   smx_process_t process = NULL;
 147   xbt_fifo_item_t item = NULL;
 148   int pos;
 149
 150   while (xbt_fifo_size(mc_stack_safety) > 0) {
 151
 152     /* Get current state */
 153     state = (mc_state_t)
 154       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 155
 156     XBT_DEBUG("**************************************************");
 157     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
 158               xbt_fifo_size(mc_stack_safety), state,
 159               MC_state_interleave_size(state));
 160
 161     /* Update statistics */
 162     mc_stats->visited_states++;
 163
 164     /* If there are processes to interleave and the maximum depth has not been reached
 165        then perform one step of the exploration algorithm */
 166     if (xbt_fifo_size(mc_stack_safety) < _surf_mc_max_depth &&
 167         (req = MC_state_get_request(state, &value))) {
 168
 169       /* Debug information */
 170       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 171         req_str = MC_request_to_string(req, value);
 172         XBT_DEBUG("Execute: %s", req_str);
 173         xbt_free(req_str);
 174       }
 175
 176       MC_state_set_executed_request(state, req, value);
 177       mc_stats->executed_transitions++;
 178
 179       /* Answer the request */
 180       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 181
 182       /* Wait for requests (schedules processes) */
 183       MC_wait_for_requests();
 184
 185       /* Create the new expanded state */
 186       MC_SET_RAW_MEM;
 187
 188       next_state = MC_state_new();
 189
 190       if(!is_visited_state()){
 191
 192         /* Get an enabled process and insert it in the interleave set of the next state */
 193         xbt_swag_foreach(process, simix_global->process_list){
 194           if(MC_process_is_enabled(process)){
 195             MC_state_interleave_process(next_state, process);
 196             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 197             //break;
 198           }
 199         }
 200
 201         if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
 202           next_state->system_state = MC_take_snapshot();
 203         }
 204
 205       }else{
 206
 207         XBT_DEBUG("State already visited !");
 208
 209       }
 210
 211       xbt_fifo_unshift(mc_stack_safety, next_state);
 212       MC_UNSET_RAW_MEM;
 213
 214       /* FIXME: Update Statistics
 215          mc_stats->state_size +=
 216          xbt_setset_set_size(next_state->enabled_transitions);*/
 217
 218       /* Let's loop again */
 219
 220       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 221     } else {
 222
 223       if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth){
 224
 225         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 226         if(req != NULL){
 227           XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 228           XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 229         }
 230
 231       }else{
 232
 233         XBT_DEBUG("There are no more processes to interleave.");
 234
 235       }
 236
 237       /* Trash the current state, no longer needed */
 238       MC_SET_RAW_MEM;
 239       xbt_fifo_shift(mc_stack_safety);
 240       MC_state_delete(state);
 241       MC_UNSET_RAW_MEM;
 242
 243       /* Check for deadlocks */
 244       if(MC_deadlock_check()){
 245         MC_show_deadlock(NULL);
 246         return;
 247       }
 248
 249       MC_SET_RAW_MEM;
 250       /* Traverse the stack backwards until a state with a non empty interleave
 251          set is found, deleting all the states that have it empty in the way.
 252          For each deleted state, check if the request that has generated it
 253          (from it's predecesor state), depends on any other previous request
 254          executed before it. If it does then add it to the interleave set of the
 255          state that executed that previous request. */
 256
 257       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 258         if(MC_state_interleave_size(state) == 0){
 259           req = MC_state_get_internal_request(state);
 260           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 261             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 262               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 263                 XBT_DEBUG("Dependent Transitions:");
 264                 prev_req = MC_state_get_executed_request(prev_state, &value);
 265                 req_str = MC_request_to_string(prev_req, value);
 266                 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 267                 xbt_free(req_str);
 268                 prev_req = MC_state_get_executed_request(state, &value);
 269                 req_str = MC_request_to_string(prev_req, value);
 270                 XBT_DEBUG("%s (state=%p)", req_str, state);
 271                 xbt_free(req_str);
 272               }
 273
 274               /*if(!MC_state_process_is_done(prev_state, req->issuer))
 275                 MC_state_interleave_process(prev_state, req->issuer);
 276               else
 277               XBT_DEBUG("Process %p is in done set", req->issuer);*/
 278
 279
 280               break;
 281
 282             }else{
 283
 284               //XBT_DEBUG("Independant transitions : (%lu) %d - (%lu) %d", req->issuer->pid, req->call, MC_state_get_internal_request(prev_state)->issuer->pid, MC_state_get_internal_request(prev_state)->call);
 285               MC_state_remove_interleave_process(prev_state, req->issuer);
 286
 287             }
 288           }
 289         }
 290         if (MC_state_interleave_size(state)) {
 291           /* We found a back-tracking point, let's loop */
 292           if(_surf_mc_checkpoint){
 293             if(state->system_state != NULL){
 294               MC_restore_snapshot(state->system_state);
 295               xbt_fifo_unshift(mc_stack_safety, state);
 296               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 297               MC_UNSET_RAW_MEM;
 298             }else{
 299               pos = xbt_fifo_size(mc_stack_safety);
 300               item = xbt_fifo_get_first_item(mc_stack_safety);
 301               while(pos>0){
 302                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 303                 if(restore_state->system_state != NULL){
 304                   break;
 305                 }else{
 306                   item = xbt_fifo_get_next_item(item);
 307                   pos--;
 308                 }
 309               }
 310               MC_restore_snapshot(restore_state->system_state);
 311               xbt_fifo_unshift(mc_stack_safety, state);
 312               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 313               MC_UNSET_RAW_MEM;
 314               MC_replay(mc_stack_safety, pos);
 315             }
 316           }else{
 317             xbt_fifo_unshift(mc_stack_safety, state);
 318             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 319             MC_UNSET_RAW_MEM;
 320             MC_replay(mc_stack_safety, -1);
 321           }
 322           break;
 323         } else {
 324           MC_state_delete(state);
 325         }
 326       }
 327       MC_UNSET_RAW_MEM;
 328     }
 329   }
 330   MC_print_statistics(mc_stats);
 331   MC_UNSET_RAW_MEM;
 332
 333   return;
 334 }
 335
 336
 337
 338