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