src/mc/mc_global.c

   1 #include "../surf/surf_private.h"
   2 #include "../simix/private.h"
   3 #include "xbt/fifo.h"
   4 #include "private.h"
   5
   6 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
   7                                 "Logging specific to MC (global)");
   8
   9 /* MC global data structures */
  10 mc_snapshot_t initial_snapshot = NULL;
  11 xbt_fifo_t mc_stack = NULL;
  12 xbt_setset_t mc_setset = NULL;
  13 mc_stats_t mc_stats = NULL;
  14 char mc_replay_mode = FALSE;
  15
  16 /**
  17  *  \brief Initialize the model-checker data structures
  18  */
  19 void MC_init(int method)
  20 {
  21   /* Check if MC is already initialized */
  22   if(initial_snapshot)
  23     return;
  24
  25   /* Initialize the data structures that must be persistent across every
  26      iteration of the model-checker (in RAW memory) */
  27   MC_SET_RAW_MEM;
  28
  29   /* Initialize statistics */
  30   mc_stats = xbt_new0(s_mc_stats_t, 1);
  31   mc_stats->state_size = 1;
  32
  33   /* Create exploration stack */
  34   mc_stack = xbt_fifo_new();
  35
  36   /* Create the container for the sets */
  37   mc_setset = xbt_setset_new(20);
  38
  39   switch(method){
  40     case 0:
  41       MC_dfs_init();
  42       break;
  43     case 1:
  44       MC_dpor_init();
  45       break;
  46     default:
  47       break;
  48   }
  49
  50   /* Save the initial state */
  51   MC_SET_RAW_MEM;
  52   initial_snapshot = xbt_new(s_mc_snapshot_t,1);
  53   MC_take_snapshot(initial_snapshot);
  54   MC_UNSET_RAW_MEM;
  55 }
  56
  57 void MC_modelcheck(int method){
  58
  59   MC_init(method);
  60
  61   switch(method){
  62     case 0:
  63       MC_dfs();
  64       break;
  65     case 1:
  66       MC_dpor();
  67       break;
  68     default:
  69       break;
  70   }
  71 }
  72
  73
  74 /**
  75  * \brief Re-executes from the initial state all the transitions indicated by
  76  *        a given model-checker stack.
  77  * \param stack The stack with the transitions to execute.
  78 */
  79 void MC_replay(xbt_fifo_t stack)
  80 {
  81   xbt_fifo_item_t item;
  82   mc_state_t state;
  83   mc_transition_t trans;
  84
  85   DEBUG0("**** Begin Replay ****");
  86
  87   /* Restore the initial state */
  88   MC_restore_snapshot(initial_snapshot);
  89
  90   mc_replay_mode = TRUE;
  91
  92   MC_UNSET_RAW_MEM;
  93
  94   /* Traverse the stack from the initial state and re-execute the transitions */
  95   for(item = xbt_fifo_get_last_item(stack);
  96       item != xbt_fifo_get_first_item(stack);
  97       item = xbt_fifo_get_prev_item(item)){
  98
  99     state = (mc_state_t) xbt_fifo_get_item_content(item);
 100     trans = state->executed_transition;
 101
 102     /* Update statistics */
 103     mc_stats->visited_states++;
 104     mc_stats->executed_transitions++;
 105
 106     DEBUG1("Executing transition %s", trans->name);
 107     SIMIX_process_schedule(trans->process);
 108
 109     /* Do all surf's related black magic tricks to keep all working */
 110     MC_execute_surf_actions();
 111
 112     /* Schedule every process that got enabled due to the executed transition */
 113     MC_schedule_enabled_processes();
 114   }
 115   mc_replay_mode = FALSE;
 116   DEBUG0("**** End Replay ****");
 117 }
 118
 119 /**
 120  * \brief Dumps the contents of a model-checker's stack and shows the actual
 121  *        execution trace
 122  * \param stack The stack to dump
 123 */
 124 void MC_dump_stack(xbt_fifo_t stack)
 125 {
 126   mc_state_t state;
 127   mc_transition_t trans;
 128
 129   MC_SET_RAW_MEM;
 130   while( (state = (mc_state_t)xbt_fifo_pop(stack)) != NULL ){
 131     trans = state->executed_transition;
 132     if(trans)
 133       INFO1("%s", trans->name);
 134
 135     MC_state_delete(state);
 136   }
 137   MC_UNSET_RAW_MEM;
 138 }
 139
 140 void MC_show_stack(xbt_fifo_t stack)
 141 {
 142   mc_state_t state;
 143   mc_transition_t trans;
 144   xbt_fifo_item_t item;
 145
 146   INFO0("===========================");
 147   for(item=xbt_fifo_get_last_item(stack);
 148      (item?(state=(mc_state_t)(xbt_fifo_get_item_content(item))):(NULL));             \
 149       item=xbt_fifo_get_prev_item(item)){
 150     trans = state->executed_transition;
 151     if(trans){
 152       INFO1("%s", trans->name);
 153     }
 154   }
 155 }
 156
 157
 158 /**
 159  * \brief Schedules all the process that are ready to run
 160  *        As a side effect it performs some clean-up required by SIMIX
 161  */
 162 void MC_schedule_enabled_processes(void)
 163 {
 164   smx_process_t process;
 165
 166   //SIMIX_process_empty_trash();
 167
 168   /* Schedule every process that is ready to run due to an finished action */
 169   while ((process = xbt_swag_extract(simix_global->process_to_run))) {
 170     DEBUG2("Scheduling %s on %s", process->name, process->smx_host->name);
 171     SIMIX_process_schedule(process);
 172   }
 173 }
 174
 175 /******************************** States **************************************/
 176
 177 /**
 178  * \brief Creates a state data structure used by the exploration algorithm
 179  */
 180 mc_state_t MC_state_new(void)
 181 {
 182   mc_state_t state = NULL;
 183
 184   state = xbt_new0(s_mc_state_t, 1);
 185   state->transitions = xbt_setset_new_set(mc_setset);
 186   state->enabled_transitions = xbt_setset_new_set(mc_setset);
 187   state->interleave = xbt_setset_new_set(mc_setset);
 188   state->done = xbt_setset_new_set(mc_setset);
 189   state->executed_transition = NULL;
 190
 191   mc_stats->expanded_states++;
 192
 193   return state;
 194 }
 195 /**
 196  * \brief Deletes a state data structure
 197  * \param trans The state to be deleted
 198  */
 199 void MC_state_delete(mc_state_t state)
 200 {
 201   /*if(state->executed_transition)
 202     MC_transition_delete(state->executed_transition);*/
 203   xbt_setset_destroy_set(state->transitions);
 204   xbt_setset_destroy_set(state->enabled_transitions);
 205   xbt_setset_destroy_set(state->interleave);
 206   xbt_setset_destroy_set(state->done);
 207
 208   xbt_free(state);
 209 }
 210
 211 /************************** SURF Emulation ************************************/
 212
 213 /* Dirty hack, we manipulate surf's clock to simplify the integration of the
 214    model-checker */
 215 extern double NOW;
 216
 217 /**
 218  * \brief Executes all the actions at every model
 219  */
 220 void MC_execute_surf_actions(void)
 221 {
 222   unsigned int iter;
 223   surf_action_t action = NULL;
 224   surf_model_t model = NULL;
 225   smx_action_t smx_action = NULL;
 226
 227   /* Execute all the actions in every model */
 228   xbt_dynar_foreach(model_list, iter, model){
 229     while ((action = xbt_swag_extract(model->states.running_action_set))){
 230       /* FIXME: timeouts are not calculated correctly */
 231       if(NOW >= action->max_duration){
 232         surf_action_state_set(action, SURF_ACTION_DONE);
 233         smx_action = action->data;
 234         DEBUG5("Resource [%s] (%d): Executing RUNNING action \"%s\" (%p) MaxDuration %lf",
 235           model->name, xbt_swag_size(model->states.running_action_set),
 236           smx_action->name, smx_action, action->max_duration);
 237
 238         /* Copy the transfered data of the completed network actions */
 239         /* FIXME: be carefull it might not be an action of the network model */
 240         if(smx_action && smx_action->data != NULL)
 241           SIMIX_network_copy_data((smx_comm_t)smx_action->data);
 242
 243         if(smx_action)
 244           SIMIX_action_signal_all(smx_action);
 245       }
 246     }
 247     /*FIXME: check if this is always empty or not */
 248     while ((action = xbt_swag_extract(model->states.failed_action_set))) {
 249       smx_action = action->data;
 250       DEBUG4("Resource [%s] (%d): Executing FAILED action \"%s\" (%p)",
 251         model->name, xbt_swag_size(model->states.running_action_set),
 252         smx_action->name, smx_action);
 253       if (smx_action)
 254        SIMIX_action_signal_all(smx_action);
 255     }
 256   }
 257   /* That's it, now go one step deeper into the model-checking process! */
 258   NOW += 0.5;  /* FIXME: Check time increases*/
 259 }
 260
 261 /****************************** Statistics ************************************/
 262 void MC_print_statistics(mc_stats_t stats)
 263 {
 264   INFO1("State space size ~= %lu", stats->state_size);
 265   INFO1("Expanded states = %lu", stats->expanded_states);
 266   INFO1("Visited states = %lu", stats->visited_states);
 267   INFO1("Executed transitions = %lu", stats->executed_transitions);
 268   INFO1("Expanded / Visited = %lf",
 269     (double)stats->visited_states / stats->expanded_states);
 270   /*INFO1("Exploration coverage = %lf",
 271     (double)stats->expanded_states / stats->state_size);*/
 272 }
 273
 274 /************************* Assertion Checking *********************************/
 275 void MC_assert(int prop)
 276 {
 277   if(!prop){
 278     INFO0("**************************");
 279     INFO0("*** PROPERTY NOT VALID ***");
 280     INFO0("**************************");
 281     INFO0("Counter-example execution trace:");
 282     MC_dump_stack(mc_stack);
 283     MC_print_statistics(mc_stats);
 284     xbt_abort();
 285   }
 286 }
 287