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 5436bb5..f78cad5 100644 (file)
--- a/buildtools/Cmake/AddTests.cmake
+++ b/buildtools/Cmake/AddTests.cmake
@@ -227,9 +227,11 @@ endif(HAVE_RUBY)
 
 # END TESH TESTS
 
 
 # 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)
 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
 
 if(HAVE_JAVA)
 # java examples

diff --git a/buildtools/Cmake/CompleteInFiles.cmake b/buildtools/Cmake/CompleteInFiles.cmake
index 549f91a..771754b 100644 (file)
--- a/buildtools/Cmake/CompleteInFiles.cmake
+++ b/buildtools/Cmake/CompleteInFiles.cmake
@@ -60,9 +60,10 @@ if(enable_tracing)
        SET(HAVE_TRACING 1)
 endif(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)
        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)
 
 if(enable_lua)
        exec_program("lua -v" OUTPUT_VARIABLE LUA_VERSION)

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 9d116b7..82a0fec 100755 (executable)
--- 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/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
 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
 )
 
        src/mc/private.h
 )
 

-

 set(install_HEADERS
 include/xbt/misc.h
 include/xbt/sysdep.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}
        ${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}
 ### Gras Lib sources
 set(gras_sources
        ${XBT_SRC}

diff --git a/buildtools/Cmake/MakeExeLib.cmake b/buildtools/Cmake/MakeExeLib.cmake
index 642e2c9..a19ad9d 100644 (file)
--- 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/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)
 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 ae34b1b..c0755ed 100644 (file)
--- 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@
 
 /* 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@
 
 /* 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 d711b68..72ea2f0 100644 (file)
--- a/src/msg/global.c
+++ b/src/msg/global.c
@@ -140,9 +140,11 @@ MSG_error_t MSG_main(void)
   fflush(stderr);
   SIMIX_init();
 
   fflush(stderr);
   SIMIX_init();
 

+#ifdef HAVE_MC

   if (_surf_do_model_check)
     MC_modelcheck(1);
   else
   if (_surf_do_model_check)
     MC_modelcheck(1);
   else

+#endif

     while (SIMIX_solve(NULL, NULL) != -1.0);
   
   return MSG_OK;
     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 dd7b49a..f1533a8 100644 (file)
--- 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*/
   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);
   /* 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*/
   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);
   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
    */
   /* 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*/
 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);
   if (_surf_do_model_check)
     MC_trans_intercept_wait(comm);

-  
+#endif

   /* Wait for communication completion */
   SIMIX_communication_wait_for_completion(comm, timeout);
 }
   /* 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*/
 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);
   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)){
 
   /* 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*/
   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);
   if (_surf_do_model_check)
     MC_trans_intercept_waitany(comms);

-    
+#endif

   xbt_dynar_foreach(comms,cursor,comm)
     xbt_dynar_push(sems,&(comm->sem));
 
   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;
   /* 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 5b60328..5b31c8b 100644 (file)
--- 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);
     history = tmgr_history_new();
 
   surf_config_init(argc, argv);

-
+#ifdef HAVE_MC

   if (_surf_do_model_check)
     MC_memory_init();
   if (_surf_do_model_check)
     MC_memory_init();

+#endif

 }
 
 #ifdef WIN32
 }
 
 #ifdef WIN32