From: thiery Date: Thu, 2 Dec 2010 17:18:59 +0000 (+0000) Subject: Cleaner detection of using model-checking. X-Git-Tag: v3.6_beta2~1002 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/a6c262a93734a964f6aaaddf59d933398db660ff Cleaner detection of using model-checking. libgras no longer needs to define _surf_do_model_check. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@8912 48e7efb5-ca39-0410-a469-dd3cf9ba447f --- diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index bdc16bd2c2..0a08e993da 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -16,6 +16,13 @@ #include "mc/datatypes.h" #include "simix/datatypes.h" +#ifdef HAVE_MC +extern int _surf_do_model_check; +#define MC_IS_ENABLED _surf_do_model_check +#else +#define MC_IS_ENABLED 0 +#endif + SG_BEGIN_DECL() /********************************* Global *************************************/ @@ -29,11 +36,6 @@ XBT_PUBLIC(int) MC_random(int, int); XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */ XBT_PUBLIC(void) MC_memory_exit(void); -/* - * Boolean indicating whether we want to activate the model-checker - */ -extern int _surf_do_model_check; - - SG_END_DECL() + #endif /* _MC_MC_H */ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index c29198cf41..acd09ed2a8 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -260,7 +260,7 @@ void MC_print_statistics(mc_stats_t stats) /************************* Assertion Checking *********************************/ void MC_assert(int prop) { - if (_surf_do_model_check && !prop) { + if (MC_IS_ENABLED && !prop) { INFO0("**************************"); INFO0("*** PROPERTY NOT VALID ***"); INFO0("**************************"); diff --git a/src/msg/global.c b/src/msg/global.c index 84894f7207..ef50ebe572 100644 --- a/src/msg/global.c +++ b/src/msg/global.c @@ -143,12 +143,10 @@ MSG_error_t MSG_main(void) fflush(stdout); fflush(stderr); -#ifdef HAVE_MC - if (_surf_do_model_check){ + if (MC_IS_ENABLED) { MC_modelcheck(); - }else -#endif - { + } + else { SIMIX_run(); } return MSG_OK; diff --git a/src/simix/private.h b/src/simix/private.h index f6bafe02fc..3ac7fd1ed8 100644 --- a/src/simix/private.h +++ b/src/simix/private.h @@ -22,8 +22,6 @@ #include "smurf_private.h" #include "synchro_private.h" -extern int _surf_do_model_check; - /********************************** Simix Global ******************************/ typedef struct s_smx_context_factory *smx_context_factory_t; diff --git a/src/simix/smx_host.c b/src/simix/smx_host.c index fec6e6990b..744bfc8327 100644 --- a/src/simix/smx_host.c +++ b/src/simix/smx_host.c @@ -8,6 +8,7 @@ #include "xbt/sysdep.h" #include "xbt/log.h" #include "xbt/dict.h" +#include "mc/mc.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_host, simix, "Logging specific to SIMIX (hosts)"); @@ -191,15 +192,12 @@ smx_action_t SIMIX_host_execute(const char *name, smx_host_t host, action->category = NULL; #endif -#ifdef HAVE_MC /* set surf's action */ - if (!_surf_do_model_check) -#endif - { - action->execution.surf_exec = - surf_workstation_model->extension.workstation.execute(host->host, - computation_amount); - surf_workstation_model->action_data_set(action->execution.surf_exec, action); + if (!MC_IS_ENABLED) { + action->execution.surf_exec = + surf_workstation_model->extension.workstation.execute(host->host, + computation_amount); + surf_workstation_model->action_data_set(action->execution.surf_exec, action); } #ifdef HAVE_TRACING @@ -237,17 +235,14 @@ smx_action_t SIMIX_host_parallel_execute( const char *name, for (i = 0; i < host_nb; i++) workstation_list[i] = host_list[i]->host; -#ifdef HAVE_MC /* set surf's action */ - if (!_surf_do_model_check) -#endif - { + if (!MC_IS_ENABLED) { action->execution.surf_exec = surf_workstation_model->extension.workstation. execute_parallel_task(host_nb, workstation_list, computation_amount, communication_amount, amount, rate); - surf_workstation_model->action_data_set(action->execution.surf_exec, action); + surf_workstation_model->action_data_set(action->execution.surf_exec, action); } DEBUG1("Create parallel execute action %p", action); @@ -278,7 +273,7 @@ void SIMIX_host_execution_cancel(smx_action_t action) { DEBUG1("Cancel action %p", action); - if (action->execution.surf_exec) + if (action->execution.surf_exec) surf_workstation_model->action_cancel(action->execution.surf_exec); } @@ -312,13 +307,11 @@ void SIMIX_pre_host_execution_wait(smx_req_t req) xbt_fifo_push(action->request_list, req); req->issuer->waiting_action = action; -#ifdef HAVE_MC /* set surf's action */ - if (_surf_do_model_check){ + if (MC_IS_ENABLED){ action->state = SIMIX_DONE; SIMIX_execution_finish(action); } -#endif /* If the action is already finished then perform the error handling */ if (action->state != SIMIX_RUNNING) diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c index f456aeb22a..7a457464d7 100644 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@ -255,12 +255,12 @@ smx_action_t SIMIX_comm_isend(smx_process_t src_proc, smx_rdv_t rdv, action->comm.src_buff = src_buff; action->comm.src_buff_size = src_buff_size; action->comm.data = data; -#ifdef HAVE_MC - if (_surf_do_model_check){ + + if (MC_IS_ENABLED) { action->state = SIMIX_RUNNING; return action; } -#endif + SIMIX_comm_start(action); return action; } @@ -288,12 +288,10 @@ smx_action_t SIMIX_comm_irecv(smx_process_t dst_proc, smx_rdv_t rdv, action->comm.dst_buff = dst_buff; action->comm.dst_buff_size = dst_buff_size; -#ifdef HAVE_MC - if (_surf_do_model_check){ + if (MC_IS_ENABLED) { action->state = SIMIX_RUNNING; return action; } -#endif SIMIX_comm_start(action); return action; @@ -309,12 +307,10 @@ void SIMIX_pre_comm_wait(smx_req_t req) xbt_fifo_push(action->request_list, req); req->issuer->waiting_action = action; -#ifdef HAVE_MC - if (_surf_do_model_check){ + if (MC_IS_ENABLED){ action->state = SIMIX_DONE; SIMIX_comm_finish(action); } -#endif /* If the action has already finish perform the error handling, */ /* otherwise set up a waiting timeout on the right side */ diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c index c1f19e169a..f6bc39dc2f 100644 --- a/src/simix/smx_process.c +++ b/src/simix/smx_process.c @@ -9,6 +9,7 @@ #include "xbt/log.h" #include "xbt/dict.h" #include "msg/mailbox.h" +#include "mc/mc.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix, "Logging specific to SIMIX (process)"); @@ -413,12 +414,10 @@ xbt_dict_t SIMIX_process_get_properties(smx_process_t process) void SIMIX_pre_process_sleep(smx_req_t req) { -#ifdef HAVE_MC - if(_surf_do_model_check){ + if (MC_IS_ENABLED) { req->process_sleep.result = SIMIX_DONE; SIMIX_request_answer(req); } -#endif smx_action_t action = SIMIX_process_sleep(req->issuer, req->process_sleep.duration); xbt_fifo_push(action->request_list, req); req->issuer->waiting_action = action; diff --git a/src/smpi/smpi_global.c b/src/smpi/smpi_global.c index 71362f6f31..2b736c5a9e 100644 --- a/src/smpi/smpi_global.c +++ b/src/smpi/smpi_global.c @@ -319,11 +319,9 @@ int MAIN__(void) fflush(stdout); fflush(stderr); -#ifdef HAVE_MC - if (_surf_do_model_check) + if (MC_IS_ENABLED) MC_modelcheck(); else -#endif SIMIX_run(); if (xbt_cfg_get_int(_surf_cfg_set, "smpi/display_timing")) diff --git a/src/surf/surf.c b/src/surf/surf.c index ad9b625186..f4d1895b3e 100644 --- a/src/surf/surf.c +++ b/src/surf/surf.c @@ -308,10 +308,8 @@ void surf_init(int *argc, char **argv) history = tmgr_history_new(); surf_config_init(argc, argv); -#ifdef HAVE_MC - if (_surf_do_model_check) + if (MC_IS_ENABLED) MC_memory_init(); -#endif } #ifdef _XBT_WIN32 diff --git a/src/xbt/mallocator.c b/src/xbt/mallocator.c index 51c9b75aea..60473a584c 100644 --- a/src/xbt/mallocator.c +++ b/src/xbt/mallocator.c @@ -9,10 +9,10 @@ #include "xbt/mallocator.h" #include "xbt/asserts.h" #include "xbt/sysdep.h" +#include "mc/mc.h" /* kill mallocators when model-checking is enabled */ #include "mallocator_private.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(xbt_mallocator, xbt, "Mallocators"); -extern int _surf_do_model_check; /* kill mallocators when this is true */ /** * \brief Constructor @@ -50,7 +50,7 @@ xbt_mallocator_t xbt_mallocator_new(int size, * The mallocator will give standard memory when we are using raw memory (so these blocks are killed on restore) * and the contrary (so these blocks will leak accross restores) */ - if (_surf_do_model_check) + if (MC_IS_ENABLED) size = 0; m = xbt_new0(s_xbt_mallocator_t, 1); @@ -58,7 +58,7 @@ xbt_mallocator_t xbt_mallocator_new(int size, if (XBT_LOG_ISENABLED(xbt_mallocator, xbt_log_priority_verbose)) xbt_backtrace_display_current(); - m->objects = xbt_new0(void *, _surf_do_model_check ? 1 : size); + m->objects = xbt_new0(void *, MC_IS_ENABLED ? 1 : size); m->max_size = size; m->current_size = 0; m->new_f = new_f; diff --git a/src/xbt/xbt_rl_time.c b/src/xbt/xbt_rl_time.c index 7d6618ee87..1fbf9eb7e5 100644 --- a/src/xbt/xbt_rl_time.c +++ b/src/xbt/xbt_rl_time.c @@ -26,7 +26,3 @@ void xbt_sleep(double sec) xbt_os_sleep(sec); } -/* This horribly badly placed. I just need to get that symbol with that value into libgras so that the mallocators are happy. - * EPR will save us all. One day. - */ -int _surf_do_model_check = 0;