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