From: navarrop Date: Thu, 27 May 2010 14:32:18 +0000 (+0000) Subject: Add a variable HAVE_MC for enable model-checking. X-Git-Tag: v3_5~1006 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/c7f3c30ef936dacf568b44009d3948c8dc64228c Add a variable HAVE_MC for enable model-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@7802 48e7efb5-ca39-0410-a469-dd3cf9ba447f --- diff --git a/buildtools/Cmake/AddTests.cmake b/buildtools/Cmake/AddTests.cmake index 5436bb5f2f..f78cad5066 100644 --- a/buildtools/Cmake/AddTests.cmake +++ b/buildtools/Cmake/AddTests.cmake @@ -227,9 +227,11 @@ endif(HAVE_RUBY) # END TESH TESTS +if(HAVE_MC) ADD_TEST(mc-bugged1 ${CMAKE_BINARY_DIR}/bin/tesh --cd ${PROJECT_DIRECTORY}/examples/msg/mc bugged1.tesh) ADD_TEST(mc-bugged2 ${CMAKE_BINARY_DIR}/bin/tesh --cd ${PROJECT_DIRECTORY}/examples/msg/mc bugged2.tesh) ADD_TEST(mc-centralized ${CMAKE_BINARY_DIR}/bin/tesh --cd ${PROJECT_DIRECTORY}/examples/msg/mc centralized.tesh) +endif(HAVE_MC) if(HAVE_JAVA) # java examples diff --git a/buildtools/Cmake/CompleteInFiles.cmake b/buildtools/Cmake/CompleteInFiles.cmake index 549f91ad39..771754b9c1 100644 --- a/buildtools/Cmake/CompleteInFiles.cmake +++ b/buildtools/Cmake/CompleteInFiles.cmake @@ -60,9 +60,10 @@ if(enable_tracing) SET(HAVE_TRACING 1) endif(enable_tracing) -if(enable_model-checking) +if(enable_model-checking AND HAVE_MMAP) + SET(HAVE_MC 1) SET(MMALLOC_WANT_OVERIDE_LEGACY 1) -endif(enable_model-checking) +endif(enable_model-checking AND HAVE_MMAP) if(enable_lua) exec_program("lua -v" OUTPUT_VARIABLE LUA_VERSION) diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 9d116b71d2..82a0fec487 100755 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -195,9 +195,15 @@ set(XBT_SRC src/xbt/cunit.c src/xbt/graphxml_parse.c src/xbt/setset.c - src/xbt/mmalloc/mm.c ) +if(HAVE_MMAP) + set(XBT_SRC + ${XBT_SRC} + src/xbt/mmalloc/mm.c + ) +endif(HAVE_MMAP) + set(GTNETS_SRC src/surf/gtnets/gtnets_simulator.cc src/surf/gtnets/gtnets_topology.cc @@ -342,7 +348,6 @@ set(MC_SRC src/mc/private.h ) - set(install_HEADERS include/xbt/misc.h include/xbt/sysdep.h @@ -507,9 +512,15 @@ set(simgrid_sources ${GRAS_COMMON_SRC} ${GRAS_SG_SRC} ${AMOK_SRC} - ${MC_SRC} ) +if(enable_model-checking AND HAVE_MMAP) + set(simgrid_sources + ${simgrid_source} + ${MC_SRC} + ) +endif(enable_model-checking AND HAVE_MMAP) + ### Gras Lib sources set(gras_sources ${XBT_SRC} diff --git a/buildtools/Cmake/MakeExeLib.cmake b/buildtools/Cmake/MakeExeLib.cmake index 642e2c97f6..a19ad9d251 100644 --- a/buildtools/Cmake/MakeExeLib.cmake +++ b/buildtools/Cmake/MakeExeLib.cmake @@ -125,7 +125,11 @@ add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/priority) add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/masterslave) add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/trace) add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/tracing) -add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/mc) + +if(HAVE_MC) + add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/mc) +endif(HAVE_MC) + if(HAVE_GTNETS) add_definitions("-lgtnets -L${gtnets_path}/lib -I${gtnets_path}/include/gtnets") add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/gtnets) diff --git a/buildtools/Cmake/gras_config.h.in b/buildtools/Cmake/gras_config.h.in index ae34b1b94c..c0755edb5c 100644 --- a/buildtools/Cmake/gras_config.h.in +++ b/buildtools/Cmake/gras_config.h.in @@ -3,6 +3,7 @@ /* Set to true if enable_model-checking is true */ #cmakedefine MMALLOC_WANT_OVERIDE_LEGACY @MMALLOC_WANT_OVERIDE_LEGACY@ +#cmakedefine HAVE_MC @HAVE_MC@ /* Define if building universal (internal helper macro) */ #cmakedefine AC_APPLE_UNIVERSAL_BUILD @AC_APPLE_UNIVERSAL_BUILD@ diff --git a/src/msg/global.c b/src/msg/global.c index d711b6829f..72ea2f06c4 100644 --- a/src/msg/global.c +++ b/src/msg/global.c @@ -140,9 +140,11 @@ MSG_error_t MSG_main(void) fflush(stderr); SIMIX_init(); +#ifdef HAVE_MC if (_surf_do_model_check) MC_modelcheck(1); else +#endif while (SIMIX_solve(NULL, NULL) != -1.0); return MSG_OK; diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c index dd7b49a4f3..f1533a8019 100644 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@ -477,9 +477,10 @@ smx_comm_t SIMIX_network_isend(smx_rdv_t rdv, double task_size, double rate, smx_comm_t comm; /*If running in model-checking mode then intercept the communication action*/ - if (_surf_do_model_check) - MC_trans_intercept_isend(rdv); - + #ifdef HAVE_MC + if (_surf_do_model_check) + MC_trans_intercept_isend(rdv); + #endif /* Look for communication request matching our needs. If it is not found then create it and push it into the rendez-vous point */ comm = SIMIX_rdv_get_request(rdv, comm_recv); @@ -506,9 +507,10 @@ smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_s smx_comm_t comm; /*If running in model-checking mode then intercept the communication action*/ +#ifdef HAVE_MC if (_surf_do_model_check) MC_trans_intercept_irecv(rdv); - +#endif /* Look for communication request matching our needs. * If it is not found then create it and push it into the rendez-vous point */ @@ -532,9 +534,10 @@ smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_s XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout) { /*If running in model-checking mode then intercept the communication action*/ +#ifdef HAVE_MC if (_surf_do_model_check) MC_trans_intercept_wait(comm); - +#endif /* Wait for communication completion */ SIMIX_communication_wait_for_completion(comm, timeout); } @@ -543,8 +546,10 @@ XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout) XBT_INLINE int SIMIX_network_test(smx_comm_t comm) { /*If running in model-checking mode then intercept the communication action*/ +#ifdef HAVE_MC if (_surf_do_model_check) MC_trans_intercept_test(comm); +#endif /* Copy data if the communication is done */ if(comm->sem && !SIMIX_sem_would_block(comm->sem)){ @@ -566,9 +571,10 @@ unsigned int SIMIX_network_waitany(xbt_dynar_t comms) smx_comm_t comm,comm_finished=NULL; /*If running in model-checking mode then intercept the communication action*/ +#ifdef HAVE_MC if (_surf_do_model_check) MC_trans_intercept_waitany(comms); - +#endif xbt_dynar_foreach(comms,cursor,comm) xbt_dynar_push(sems,&(comm->sem)); @@ -582,4 +588,4 @@ unsigned int SIMIX_network_waitany(xbt_dynar_t comms) /* Check for errors and cleanup the comm */ SIMIX_communication_wait_for_completion(comm_finished,-1); return found_comm; -} \ No newline at end of file +} diff --git a/src/surf/surf.c b/src/surf/surf.c index 5b603282d2..5b31c8b398 100644 --- a/src/surf/surf.c +++ b/src/surf/surf.c @@ -278,9 +278,10 @@ void surf_init(int *argc, char **argv) history = tmgr_history_new(); surf_config_init(argc, argv); - +#ifdef HAVE_MC if (_surf_do_model_check) MC_memory_init(); +#endif } #ifdef WIN32