src/mc/mc_global.c

   1 #include <unistd.h>
   2 #include <sys/types.h>
   3 #include <sys/wait.h>
   4
   5 #include "../surf/surf_private.h"
   6 #include "../simix/private.h"
   7 #include "xbt/fifo.h"
   8 #include "private.h"
   9
  10
  11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  12                                 "Logging specific to MC (global)");
  13
  14 /* MC global data structures */
  15 mc_snapshot_t initial_snapshot = NULL;
  16 xbt_fifo_t mc_stack = NULL;
  17 xbt_setset_t mc_setset = NULL;
  18 mc_stats_t mc_stats = NULL;
  19 mc_state_t mc_current_state = NULL;
  20 char mc_replay_mode = FALSE;
  21
  22 /**
  23  *  \brief Initialize the model-checker data structures
  24  */
  25 void MC_init(void)
  26 {
  27   smx_process_t process;
  28
  29   /* Check if MC is already initialized */
  30   if (initial_snapshot)
  31     return;
  32
  33   /* Initialize the data structures that must be persistent across every
  34      iteration of the model-checker (in RAW memory) */
  35   MC_SET_RAW_MEM;
  36
  37   /* Initialize statistics */
  38   mc_stats = xbt_new0(s_mc_stats_t, 1);
  39   mc_stats->state_size = 1;
  40
  41   /* Create exploration stack */
  42   mc_stack = xbt_fifo_new();
  43
  44   /* Create the container for the sets */
  45   mc_setset = xbt_setset_new(20);
  46
  47   /* Add the existing processes to mc's setset so they have an ID designated */
  48   xbt_swag_foreach(process, simix_global->process_list){
  49     xbt_setset_elm_add(mc_setset, process);
  50   }
  51
  52   /* Initialize the control variable */
  53   mc_exp_ctl = xbt_new0(e_mc_exp_ctl_t, 1);
  54   *mc_exp_ctl = MC_EXPLORE;
  55
  56   MC_UNSET_RAW_MEM;
  57
  58
  59
  60   /* Save the initial state */
  61 /*  MC_SET_RAW_MEM;
  62   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
  63   MC_take_snapshot(initial_snapshot);
  64   MC_UNSET_RAW_MEM;*/
  65 }
  66
  67 void MC_modelcheck(void)
  68 {
  69   int status;
  70   pid_t pid;
  71
  72   /* Compute initial state */
  73   MC_init();
  74
  75   /* Fork an mc's slave exploration process and wait for it. */
  76   /* The forked process will explore a trace until:
  77        - a back-tracking point is found (it sets mc_expl_ctl to MC_explore)
  78        - there are no more states to explore (it sets mc_expl_ctl to MC_STOP)
  79        - a property is invalid (or dead-lock)
  80    */
  81   while(*mc_exp_ctl == MC_EXPLORE){
  82     if((pid = fork())){
  83       waitpid(pid, &status, 0);
  84       mmalloc_detach(raw_heap);
  85       raw_heap = mmalloc_attach(raw_heap_fd, (char*)(std_heap) + STD_HEAP_SIZE + getpagesize());
  86
  87     if (WIFSIGNALED(status)) {
  88       INFO1("killed by signal %d\n", WTERMSIG(status));
  89       break;
  90     }else if (WIFSTOPPED(status)) {
  91       INFO1("stopped by signal %d\n", WSTOPSIG(status));
  92       break;
  93     }else if (WIFCONTINUED(status)) {
  94       INFO0("continued\n");
  95       break;
  96     }
  97
  98     if(*mc_exp_ctl == MC_DEADLOCK){
  99       INFO0("**************************");
 100       INFO0("*** DEAD-LOCK DETECTED ***");
 101       INFO0("**************************");
 102       MC_dump_stack(mc_stack);
 103       MC_print_statistics(mc_stats);
 104       break;
 105     }
 106
 107     }else{
 108       /* if mc_stack is empty then create first state, otherwise replay */
 109       if(xbt_fifo_size(mc_stack) == 0)
 110         MC_dpor_init();
 111       else
 112         MC_replay(mc_stack);
 113
 114       MC_dpor();
 115       MC_memory_exit();
 116       break;
 117     }
 118   }
 119
 120   /* If we are the mc's master process then exit */
 121   if(pid)
 122     MC_exit();
 123 }
 124
 125 void MC_exit(void)
 126 {
 127   mmalloc_detach(raw_heap);
 128   shm_unlink("raw_heap");
 129 }
 130
 131 int MC_random(int min, int max)
 132 {
 133   /*FIXME: return mc_current_state->executed_transition->random.value;*/
 134   return 0;
 135 }
 136
 137 /**
 138  * \brief Re-executes from the initial state all the transitions indicated by
 139  *        a given model-checker stack.
 140  * \param stack The stack with the transitions to execute.
 141 */
 142 void MC_replay(xbt_fifo_t stack)
 143 {
 144   char *req_str;
 145   smx_req_t req = NULL, saved_req = NULL;
 146   xbt_fifo_item_t item;
 147   mc_state_t state;
 148
 149   DEBUG0("**** Begin Replay ****");
 150
 151   /* Restore the initial state */
 152   /*MC_restore_snapshot(initial_snapshot);*/
 153
 154   MC_wait_for_requests();
 155
 156   /* Traverse the stack from the initial state and re-execute the transitions */
 157   for (item = xbt_fifo_get_last_item(stack);
 158        item != xbt_fifo_get_first_item(stack);
 159        item = xbt_fifo_get_prev_item(item)) {
 160
 161     state = (mc_state_t) xbt_fifo_get_item_content(item);
 162     saved_req = MC_state_get_executed_request(state);
 163
 164     if(saved_req){
 165       /* because we got a copy of the executed request, we have to fetch the
 166          real one, pointed by the request field of the issuer process */
 167       req = &saved_req->issuer->request;
 168
 169       /* Debug information */
 170       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 171         req_str = MC_request_to_string(req);
 172         DEBUG1("Replay: %s", req_str);
 173         xbt_free(req_str);
 174       }
 175     }
 176
 177     SIMIX_request_pre(req);
 178     MC_wait_for_requests();
 179
 180     /* Update statistics */
 181     mc_stats->visited_states++;
 182     mc_stats->executed_transitions++;
 183   }
 184   DEBUG0("**** End Replay ****");
 185 }
 186
 187 /**
 188  * \brief Dumps the contents of a model-checker's stack and shows the actual
 189  *        execution trace
 190  * \param stack The stack to dump
 191 */
 192 void MC_dump_stack(xbt_fifo_t stack)
 193 {
 194   mc_state_t state;
 195
 196   MC_show_stack(stack);
 197
 198   MC_SET_RAW_MEM;
 199   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 200     MC_state_delete(state);
 201   MC_UNSET_RAW_MEM;
 202 }
 203
 204 void MC_show_stack(xbt_fifo_t stack)
 205 {
 206   mc_state_t state;
 207   xbt_fifo_item_t item;
 208   smx_req_t req;
 209   char *req_str = NULL;
 210
 211   for (item = xbt_fifo_get_last_item(stack);
 212        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
 213         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 214     req = MC_state_get_executed_request(state);
 215     if(req){
 216       req_str = MC_request_to_string(req);
 217       INFO1("%s", req_str);
 218       xbt_free(req_str);
 219     }
 220   }
 221 }
 222
 223 /**
 224  * \brief Schedules all the process that are ready to run
 225  */
 226 void MC_wait_for_requests(void)
 227 {
 228   char *req_str = NULL;
 229   smx_req_t req = NULL;
 230
 231   do {
 232     SIMIX_context_runall(simix_global->process_to_run);
 233     while((req = SIMIX_request_pop())){
 234       if(!SIMIX_request_is_visible(req))
 235         SIMIX_request_pre(req);
 236       else if(req->call == REQ_COMM_WAITANY)
 237         THROW_UNIMPLEMENTED;
 238       else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 239         req_str = MC_request_to_string(req);
 240         DEBUG1("Got: %s", req_str);
 241         xbt_free(req_str);
 242       }
 243     }
 244   } while (xbt_swag_size(simix_global->process_to_run));
 245 }
 246
 247 /****************************** Statistics ************************************/
 248 void MC_print_statistics(mc_stats_t stats)
 249 {
 250   INFO1("State space size ~= %lu", stats->state_size);
 251   INFO1("Expanded states = %lu", stats->expanded_states);
 252   INFO1("Visited states = %lu", stats->visited_states);
 253   INFO1("Executed transitions = %lu", stats->executed_transitions);
 254   INFO1("Expanded / Visited = %lf",
 255         (double) stats->visited_states / stats->expanded_states);
 256   /*INFO1("Exploration coverage = %lf",
 257      (double)stats->expanded_states / stats->state_size); */
 258 }
 259
 260 /************************* Assertion Checking *********************************/
 261 void MC_assert(int prop)
 262 {
 263   if (MC_IS_ENABLED && !prop) {
 264     INFO0("**************************");
 265     INFO0("*** PROPERTY NOT VALID ***");
 266     INFO0("**************************");
 267     INFO0("Counter-example execution trace:");
 268     MC_dump_stack(mc_stack);
 269     MC_print_statistics(mc_stats);
 270     xbt_abort();
 271   }
 272 }
 273
 274 void MC_show_deadlock(smx_req_t req)
 275 {
 276   char *req_str = NULL;
 277   INFO0("**************************");
 278   INFO0("*** DEAD-LOCK DETECTED ***");
 279   INFO0("**************************");
 280   INFO0("Locked request:");
 281   req_str = MC_request_to_string(req);
 282   INFO1("%s", req_str);
 283   xbt_free(req_str);
 284   INFO0("Counter-example execution trace:");
 285   MC_dump_stack(mc_stack);
 286 }