#include "src/mc/Process.hpp"
#include "src/mc/ModelChecker.hpp"
#include "src/mc/mc_smx.h"
#endif
#include "src/mc/Process.hpp"
#include "src/mc/ModelChecker.hpp"
#include "src/mc/mc_smx.h"
#endif
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
int MC_random(int min, int max)
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
int MC_random(int min, int max)
SIMIX_simcall_handle(req, 0);
}
}
}
// Called from both MCer and MCed:
SIMIX_simcall_handle(req, 0);
}
}
}
// Called from both MCer and MCed:
case SIMCALL_COMM_WAIT:
/* FIXME: check also that src and dst processes are not suspended */
act = simcall_comm_wait__get__comm(req);
case SIMCALL_COMM_WAIT:
/* FIXME: check also that src and dst processes are not suspended */
act = simcall_comm_wait__get__comm(req);
// Fetch from MCed memory:
if (mc_mode == MC_MODE_SERVER) {
mc_model_checker->process().read(&temp_synchro, remote(act));
// Fetch from MCed memory:
if (mc_mode == MC_MODE_SERVER) {
mc_model_checker->process().read(&temp_synchro, remote(act));
/* If it has a timeout it will be always be enabled, because even if the
* communication is not ready, it can timeout and won't block. */
if (_sg_mc_timeout == 1)
/* If it has a timeout it will be always be enabled, because even if the
* communication is not ready, it can timeout and won't block. */
if (_sg_mc_timeout == 1)
}
/* On the other hand if it hasn't a timeout, check if the comm is ready.*/
else if (act->comm.detached && act->comm.src_proc == nullptr
}
/* On the other hand if it hasn't a timeout, check if the comm is ready.*/
else if (act->comm.detached && act->comm.src_proc == nullptr
// Fetch act from MCed memory:
if (mc_mode == MC_MODE_SERVER) {
memcpy(&act, buffer + comms->elmsize * index, sizeof(act));
// Fetch act from MCed memory:
if (mc_mode == MC_MODE_SERVER) {
memcpy(&act, buffer + comms->elmsize * index, sizeof(act));
#endif
act = xbt_dynar_get_as(comms, index, smx_synchro_t);
if (act->comm.src_proc && act->comm.dst_proc)
#endif
act = xbt_dynar_get_as(comms, index, smx_synchro_t);
if (act->comm.src_proc && act->comm.dst_proc)
s_smx_mutex_t temp_mutex;
if (mc_mode == MC_MODE_SERVER) {
mc_model_checker->process().read(&temp_mutex, remote(mutex));
s_smx_mutex_t temp_mutex;
if (mc_mode == MC_MODE_SERVER) {
mc_model_checker->process().read(&temp_mutex, remote(mutex));
// TODO, *(mutex->owner) :/
return MC_smx_resolve_process(mutex->owner)->pid ==
MC_smx_resolve_process(req->issuer)->pid;
// TODO, *(mutex->owner) :/
return MC_smx_resolve_process(mutex->owner)->pid ==
MC_smx_resolve_process(req->issuer)->pid;
|| req->call == SIMCALL_MC_RANDOM
|| req->call == SIMCALL_MUTEX_LOCK
|| req->call == SIMCALL_MUTEX_TRYLOCK
|| req->call == SIMCALL_MC_RANDOM
|| req->call == SIMCALL_MUTEX_LOCK
|| req->call == SIMCALL_MUTEX_TRYLOCK
static int prng_random(int min, int max)
{
unsigned long output_size = ((unsigned long) max - (unsigned long) min) + 1;
static int prng_random(int min, int max)
{
unsigned long output_size = ((unsigned long) max - (unsigned long) min) + 1;
SIMIX_simcall_handle(req, value);
#else
if (mc_mode == MC_MODE_CLIENT) {
SIMIX_simcall_handle(req, value);
#else
if (mc_mode == MC_MODE_CLIENT) {