X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/6e1633c43c1a58d11116dff425e13abb49b2162c..756df47074b2d7b0721f234077f5ef8d75e13932:/src/mc/mc_base.cpp diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index c0f9ab9f14..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,18 +8,17 @@ #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 @@ -30,14 +29,18 @@ 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; @@ -133,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 @@ -170,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 @@ -220,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; } }