X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/54dc4437fa893572ced42c3e9174f4a9888b0258..756df47074b2d7b0721f234077f5ef8d75e13932:/src/mc/mc_base.cpp diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 008f129bd8..d7cf4ebc5e 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2014. The SimGrid Team. +/* Copyright (c) 2008-2015. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it @@ -8,34 +8,39 @@ #include -#include "mc_base.h" -#include "../simix/smx_private.h" -#include "mc/mc_record.h" -#include "mc/mc_replay.h" +#include "src/mc/mc_base.h" +#include "src/simix/smx_private.h" +#include "src/mc/mc_record.h" +#include "src/mc/mc_replay.h" #include "mc/mc.h" +#include "src/mc/mc_protocol.h" #ifdef HAVE_MC -#include "mc_process.h" -#include "ModelChecker.hpp" -#include "mc_protocol.h" -#include "mc_smx.h" -#include "mc_server.h" +#include "src/mc/Process.hpp" +#include "src/mc/ModelChecker.hpp" +#include "src/mc/mc_smx.h" #endif +#ifdef HAVE_MC using simgrid::mc::remote; +#endif extern "C" { XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); +int MC_random(int min, int max) +{ + xbt_assert(mc_mode != MC_MODE_SERVER); + /* TODO, if the MC is disabled we do not really need to make a simcall for + * this :) */ + /* FIXME: return mc_current_state->executed_transition->random.value; */ + return simcall_mc_random(min, max); +} + void MC_wait_for_requests(void) { -#ifdef HAVE_MC - if (mc_mode == MC_MODE_SERVER) { - MC_server_wait_client(&mc_model_checker->process()); - return; - } -#endif + assert(mc_mode != MC_MODE_SERVER); smx_process_t process; smx_simcall_t req; @@ -131,6 +136,9 @@ int MC_request_is_enabled(smx_simcall_t req) return FALSE; } + case SIMCALL_MUTEX_TRYLOCK: + return TRUE; + case SIMCALL_MUTEX_LOCK: { smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req); #ifdef HAVE_MC @@ -168,6 +176,7 @@ int MC_request_is_visible(smx_simcall_t req) || req->call == SIMCALL_COMM_TESTANY || req->call == SIMCALL_MC_RANDOM || req->call == SIMCALL_MUTEX_LOCK + || req->call == SIMCALL_MUTEX_TRYLOCK #ifdef HAVE_MC || req->call == SIMCALL_MC_SNAPSHOT || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS @@ -175,12 +184,6 @@ int MC_request_is_visible(smx_simcall_t req) ; } -int MC_random(int min, int max) -{ - /*FIXME: return mc_current_state->executed_transition->random.value; */ - return simcall_mc_random(min, max); -} - static int prng_random(int min, int max) { unsigned long output_size = ((unsigned long) max - (unsigned long) min) + 1; @@ -224,7 +227,8 @@ void MC_simcall_handle(smx_simcall_t req, int value) xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, i, pi) { if (req == &pi->copy.simcall) { - MC_server_simcall_handle(&mc_model_checker->process(), pi->copy.pid, value); + mc_model_checker->simcall_handle( + mc_model_checker->process(), pi->copy.pid, value); return; } }