src/mc/mc_base.c

   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 <simgrid/simix.h>
  10
  11 #include "mc_base.h"
  12 #include "../simix/smx_private.h"
  13 #include "mc_record.h"
  14
  15 #ifdef HAVE_MC
  16 #include "mc_process.h"
  17 #include "mc_model_checker.h"
  18 #include "mc_protocol.h"
  19 #include "mc_smx.h"
  20 #include "mc_server.h"
  21 #endif
  22
  23 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
  24
  25 void MC_wait_for_requests(void)
  26 {
  27 #ifdef HAVE_MC
  28   if (mc_mode == MC_MODE_SERVER) {
  29     MC_server_wait_client(&mc_model_checker->process);
  30     return;
  31   }
  32 #endif
  33
  34   smx_process_t process;
  35   smx_simcall_t req;
  36   unsigned int iter;
  37
  38   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
  39     SIMIX_process_runall();
  40     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
  41       req = &process->simcall;
  42       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
  43         SIMIX_simcall_handle(req, 0);
  44     }
  45   }
  46 }
  47
  48 int MC_request_is_enabled(smx_simcall_t req)
  49 {
  50   unsigned int index = 0;
  51   smx_synchro_t act = 0;
  52 #ifdef HAVE_MC
  53   s_smx_synchro_t temp_synchro;
  54 #endif
  55
  56   switch (req->call) {
  57   case SIMCALL_NONE:
  58     return FALSE;
  59
  60   case SIMCALL_COMM_WAIT:
  61     /* FIXME: check also that src and dst processes are not suspended */
  62     act = simcall_comm_wait__get__comm(req);
  63
  64 #ifdef HAVE_MC
  65     // Fetch from MCed memory:
  66     if (!MC_process_is_self(&mc_model_checker->process)) {
  67       MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
  68         &temp_synchro, act, sizeof(temp_synchro),
  69         MC_PROCESS_INDEX_ANY);
  70       act = &temp_synchro;
  71     }
  72 #endif
  73
  74     if (simcall_comm_wait__get__timeout(req) >= 0) {
  75       /* If it has a timeout it will be always be enabled, because even if the
  76        * communication is not ready, it can timeout and won't block. */
  77       if (_sg_mc_timeout == 1)
  78         return TRUE;
  79     } else {
  80       /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
  81       if (act->comm.detached && act->comm.src_proc == NULL
  82           && act->comm.type == SIMIX_COMM_READY)
  83         return (act->comm.dst_proc != NULL);
  84     }
  85     return (act->comm.src_proc && act->comm.dst_proc);
  86
  87   case SIMCALL_COMM_WAITANY: {
  88 #ifdef HAVE_MC
  89     // Read dynar:
  90     s_xbt_dynar_t comms;
  91     MC_process_read_simple(&mc_model_checker->process,
  92       &comms, simcall_comm_waitany__get__comms(req), sizeof(comms));
  93     // Read dynar buffer:
  94     assert(comms.elmsize == sizeof(act));
  95     size_t buffer_size = comms.elmsize * comms.used;
  96     char buffer[buffer_size];
  97     MC_process_read_simple(&mc_model_checker->process,
  98       buffer, comms.data, sizeof(buffer));
  99 #endif
 100
 101 #ifdef HAVE_MC
 102     for (index = 0; index < comms.used; ++index) {
 103       memcpy(&act, buffer + comms.elmsize * index, sizeof(act));
 104 #else
 105     xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
 106 #endif
 107
 108 #ifdef HAVE_MC
 109       // Fetch from MCed memory:
 110       if (!MC_process_is_self(&mc_model_checker->process)) {
 111         MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
 112           &temp_synchro, act, sizeof(temp_synchro),
 113           MC_PROCESS_INDEX_ANY);
 114         act = &temp_synchro;
 115       }
 116 #endif
 117
 118       if (act->comm.src_proc && act->comm.dst_proc)
 119         return TRUE;
 120     }
 121     return FALSE;
 122   }
 123
 124   case SIMCALL_MUTEX_LOCK: {
 125     smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
 126 #ifdef HAVE_MC
 127     s_smx_mutex_t temp_mutex;
 128     if (!MC_process_is_self(&mc_model_checker->process)) {
 129       MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
 130         &temp_mutex, mutex, sizeof(temp_mutex),
 131         MC_PROCESS_INDEX_ANY);
 132       mutex = &temp_mutex;
 133     }
 134 #endif
 135     if(mutex->owner == NULL)
 136       return TRUE;
 137     else
 138 #ifdef HAVE_MC
 139       // TODO, *(mutex->owner) :/
 140       return MC_smx_resolve_process(mutex->owner)->pid ==
 141         MC_smx_resolve_process(req->issuer)->pid;
 142 #else
 143       return mutex->owner->pid == req->issuer->pid;
 144 #endif
 145     }
 146
 147   default:
 148     /* The rest of the requests are always enabled */
 149     return TRUE;
 150   }
 151 }
 152
 153 int MC_request_is_visible(smx_simcall_t req)
 154 {
 155   return req->call == SIMCALL_COMM_ISEND
 156       || req->call == SIMCALL_COMM_IRECV
 157       || req->call == SIMCALL_COMM_WAIT
 158       || req->call == SIMCALL_COMM_WAITANY
 159       || req->call == SIMCALL_COMM_TEST
 160       || req->call == SIMCALL_COMM_TESTANY
 161       || req->call == SIMCALL_MC_RANDOM
 162       || req->call == SIMCALL_MUTEX_LOCK
 163 #ifdef HAVE_MC
 164       || req->call == SIMCALL_MC_SNAPSHOT
 165       || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS
 166 #endif
 167       ;
 168 }
 169
 170 int MC_random(int min, int max)
 171 {
 172   /*FIXME: return mc_current_state->executed_transition->random.value; */
 173   return simcall_mc_random(min, max);
 174 }
 175
 176 static int prng_random(int min, int max)
 177 {
 178   unsigned long output_size = ((unsigned long) max - (unsigned long) min) + 1;
 179   unsigned long input_size = (unsigned long) RAND_MAX + 1;
 180   unsigned long reject_size = input_size % output_size;
 181   unsigned long accept_size = input_size - reject_size; // module*accept_size
 182
 183   // Use rejection in order to avoid skew
 184   long x;
 185   do {
 186 #ifndef _XBT_WIN32
 187     x = random();
 188 #else
 189     x = rand();
 190 #endif
 191   } while( x >= accept_size );
 192   return min + (x % output_size);
 193 }
 194
 195 int simcall_HANDLER_mc_random(smx_simcall_t simcall, int min, int max)
 196 {
 197   if (!MC_is_active() && !MC_record_path){
 198     return prng_random(min, max);
 199   }
 200
 201   return simcall->mc_value;
 202 }