src/mc/mc_safety.cpp

   1 /* Copyright (c) 2008-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 <assert.h>
   8
   9 #include "mc_state.h"
  10 #include "mc_request.h"
  11 #include "mc_safety.h"
  12 #include "mc_private.h"
  13 #include "mc_record.h"
  14 #include "mc_smx.h"
  15 #include "mc_client.h"
  16 #include "mc_exit.h"
  17
  18 #include "xbt/mmalloc/mmprivate.h"
  19
  20 extern "C" {
  21
  22 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  23                                 "Logging specific to MC safety verification ");
  24
  25 }
  26
  27 static int is_exploration_stack_state(mc_state_t current_state){
  28
  29   xbt_fifo_item_t item;
  30   mc_state_t stack_state;
  31   for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
  32     stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
  33     if(snapshot_compare(stack_state, current_state) == 0){
  34       XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
  35       return 1;
  36     }
  37   }
  38   return 0;
  39 }
  40
  41 static void MC_modelcheck_safety_init(void);
  42
  43 /**
  44  *  \brief Initialize the DPOR exploration algorithm
  45  */
  46 static void MC_pre_modelcheck_safety()
  47 {
  48   if (_sg_mc_visited > 0)
  49     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
  50
  51   mc_state_t initial_state = MC_state_new();
  52
  53   XBT_DEBUG("**************************************************");
  54   XBT_DEBUG("Initial state");
  55
  56   /* Wait for requests (schedules processes) */
  57   MC_wait_for_requests();
  58
  59   /* Get an enabled process and insert it in the interleave set of the initial state */
  60   smx_process_t process;
  61   MC_EACH_SIMIX_PROCESS(process,
  62     if (MC_process_is_enabled(process)) {
  63       MC_state_interleave_process(initial_state, process);
  64       if (mc_reduce_kind != e_mc_reduce_none)
  65         break;
  66     }
  67   );
  68
  69   xbt_fifo_unshift(mc_stack, initial_state);
  70 }
  71
  72
  73 /** \brief Model-check the application using a DFS exploration
  74  *         with DPOR (Dynamic Partial Order Reductions)
  75  */
  76 void MC_modelcheck_safety(void)
  77 {
  78   MC_modelcheck_safety_init();
  79
  80   char *req_str = NULL;
  81   int value;
  82   smx_simcall_t req = NULL;
  83   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  84   xbt_fifo_item_t item = NULL;
  85   mc_visited_state_t visited_state = NULL;
  86
  87   while (xbt_fifo_size(mc_stack) > 0) {
  88
  89     /* Get current state */
  90     state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  91
  92     XBT_DEBUG("**************************************************");
  93     XBT_DEBUG
  94         ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
  95          xbt_fifo_size(mc_stack), state, state->num,
  96          MC_state_interleave_size(state), user_max_depth_reached);
  97
  98     /* Update statistics */
  99     mc_stats->visited_states++;
 100
 101     /* If there are processes to interleave and the maximum depth has not been reached
 102        then perform one step of the exploration algorithm */
 103     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
 104         && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
 105
 106       req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
 107       XBT_DEBUG("Execute: %s", req_str);
 108       xbt_free(req_str);
 109
 110       if (dot_output != NULL) {
 111         req_str = MC_request_get_dot_output(req, value);
 112       }
 113
 114       MC_state_set_executed_request(state, req, value);
 115       mc_stats->executed_transitions++;
 116
 117       // TODO, bundle both operations in a single message
 118       //   MC_execute_transition(req, value)
 119
 120       /* Answer the request */
 121       MC_simcall_handle(req, value);
 122       MC_wait_for_requests();
 123
 124       /* Create the new expanded state */
 125       next_state = MC_state_new();
 126
 127       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
 128           MC_show_non_termination();
 129           exit(SIMGRID_EXIT_NON_TERMINATION);
 130       }
 131
 132       if ((visited_state = is_visited_state(next_state)) == NULL) {
 133
 134         /* Get an enabled process and insert it in the interleave set of the next state */
 135         smx_process_t process = NULL;
 136         MC_EACH_SIMIX_PROCESS(process,
 137           if (MC_process_is_enabled(process)) {
 138             MC_state_interleave_process(next_state, process);
 139             if (mc_reduce_kind != e_mc_reduce_none)
 140               break;
 141           }
 142         );
 143
 144         if (dot_output != NULL)
 145           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 146
 147       } else {
 148
 149         if (dot_output != NULL)
 150           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 151
 152       }
 153
 154       xbt_fifo_unshift(mc_stack, next_state);
 155
 156       if (dot_output != NULL)
 157         xbt_free(req_str);
 158
 159       /* Let's loop again */
 160
 161       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 162     } else {
 163
 164       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
 165
 166         if (user_max_depth_reached && visited_state == NULL)
 167           XBT_DEBUG("User max depth reached !");
 168         else if (visited_state == NULL)
 169           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 170         else
 171           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 172
 173       } else {
 174
 175         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 176
 177       }
 178
 179       /* Trash the current state, no longer needed */
 180       xbt_fifo_shift(mc_stack);
 181       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 182       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 183
 184       visited_state = NULL;
 185
 186       /* Check for deadlocks */
 187       if (MC_deadlock_check()) {
 188         MC_show_deadlock(NULL);
 189         exit(SIMGRID_EXIT_DEADLOCK);
 190       }
 191
 192       /* Traverse the stack backwards until a state with a non empty interleave
 193          set is found, deleting all the states that have it empty in the way.
 194          For each deleted state, check if the request that has generated it
 195          (from it's predecesor state), depends on any other previous request
 196          executed before it. If it does then add it to the interleave set of the
 197          state that executed that previous request. */
 198
 199       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
 200         if (mc_reduce_kind == e_mc_reduce_dpor) {
 201           req = MC_state_get_internal_request(state);
 202           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 203           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 204             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
 205               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 206                 XBT_DEBUG("Dependent Transitions:");
 207                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 208                 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
 209                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 210                 xbt_free(req_str);
 211                 prev_req = MC_state_get_executed_request(state, &value);
 212                 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
 213                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 214                 xbt_free(req_str);
 215               }
 216
 217               if (!MC_state_process_is_done(prev_state, issuer))
 218                 MC_state_interleave_process(prev_state, issuer);
 219               else
 220                 XBT_DEBUG("Process %p is in done set", req->issuer);
 221
 222               break;
 223
 224             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 225
 226               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 227               break;
 228
 229             } else {
 230
 231               const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 232               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 233                         req->call, issuer->pid, state->num,
 234                         MC_state_get_internal_request(prev_state)->call,
 235                         previous_issuer->pid,
 236                         prev_state->num);
 237
 238             }
 239           }
 240         }
 241
 242         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 243           /* We found a back-tracking point, let's loop */
 244           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 245           xbt_fifo_unshift(mc_stack, state);
 246           MC_replay(mc_stack);
 247           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
 248           break;
 249         } else {
 250           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 251           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 252         }
 253       }
 254     }
 255   }
 256
 257   XBT_INFO("No property violation found.");
 258   MC_print_statistics(mc_stats);
 259   exit(SIMGRID_EXIT_SUCCESS);
 260 }
 261
 262 static void MC_modelcheck_safety_init(void)
 263 {
 264   if(_sg_mc_termination)
 265     mc_reduce_kind = e_mc_reduce_none;
 266   else if (mc_reduce_kind == e_mc_reduce_unset)
 267     mc_reduce_kind = e_mc_reduce_dpor;
 268   _sg_mc_safety = 1;
 269   if (_sg_mc_termination)
 270     XBT_INFO("Check non progressive cycles");
 271   else
 272     XBT_INFO("Check a safety property");
 273   MC_wait_for_requests();
 274
 275   XBT_DEBUG("Starting the safety algorithm");
 276
 277   _sg_mc_safety = 1;
 278
 279   /* Create exploration stack */
 280   mc_stack = xbt_fifo_new();
 281
 282   MC_pre_modelcheck_safety();
 283
 284   /* Save the initial state */
 285   initial_global_state = xbt_new0(s_mc_global_t, 1);
 286   initial_global_state->snapshot = MC_take_snapshot(0);
 287 }