From 895fe7fcdb5b1cf9661fcfbc3bcbe7b5518ed302 Mon Sep 17 00:00:00 2001 From: Frederic Suter Date: Mon, 23 Mar 2020 15:49:10 +0100 Subject: [PATCH] mess with mc examples platform (prepare the transition to s4u) --- MANIFEST.in | 3 +-- examples/deprecated/msg/mc/CMakeLists.txt | 19 +++++++++++++------ examples/deprecated/msg/mc/bugged1.c | 2 +- examples/deprecated/msg/mc/bugged1.tesh | 2 +- .../deprecated/msg/mc/bugged1_liveness.tesh | 2 +- .../msg/mc/bugged1_liveness_visited.tesh | 2 +- examples/deprecated/msg/mc/bugged2.c | 2 +- examples/deprecated/msg/mc/bugged2.tesh | 2 +- examples/deprecated/msg/mc/bugged3.c | 2 +- .../deprecated/msg/mc/centralized_mutex.c | 2 +- .../deprecated/msg/mc/centralized_mutex.tesh | 2 +- .../model_checker_platform.xml} | 0 examples/s4u/CMakeLists.txt | 15 +++++++-------- examples/s4u/mc-electric-fence/platform.xml | 17 ----------------- .../s4u-mc-electric-fence.cpp | 2 +- .../s4u-mc-electric-fence.tesh | 2 +- tools/cmake/DefinePackages.cmake | 1 + 17 files changed, 33 insertions(+), 44 deletions(-) rename examples/{deprecated/msg/mc/platform.xml => platforms/model_checker_platform.xml} (100%) delete mode 100644 examples/s4u/mc-electric-fence/platform.xml diff --git a/MANIFEST.in b/MANIFEST.in index 9adbfd3954..f5507733eb 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -272,7 +272,6 @@ include examples/deprecated/msg/mc/deploy_bugged2.xml include examples/deprecated/msg/mc/deploy_bugged2_liveness.xml include examples/deprecated/msg/mc/deploy_bugged3.xml include examples/deprecated/msg/mc/deploy_centralized_mutex.xml -include examples/deprecated/msg/mc/platform.xml include examples/deprecated/msg/mc/promela_bugged1_liveness include examples/deprecated/msg/mc/promela_bugged2_liveness include examples/deprecated/msg/trace-categories/trace-categories.c @@ -468,7 +467,6 @@ include examples/s4u/io-file-system/s4u-io-file-system.cpp include examples/s4u/io-file-system/s4u-io-file-system.tesh include examples/s4u/maestro-set/s4u-maestro-set.cpp include examples/s4u/maestro-set/s4u-maestro-set.tesh -include examples/s4u/mc-electric-fence/platform.xml include examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp include examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh include examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp @@ -1897,6 +1895,7 @@ include examples/platforms/g5k.xml include examples/platforms/griffon.xml include examples/platforms/hosts_with_disks.xml include examples/platforms/meta_cluster.xml +include examples/platforms/model_checker_platform.xml include examples/platforms/multicore_machine.xml include examples/platforms/ns3-big-cluster.xml include examples/platforms/onelink.xml diff --git a/examples/deprecated/msg/mc/CMakeLists.txt b/examples/deprecated/msg/mc/CMakeLists.txt index e83a129bc0..31a9c38596 100644 --- a/examples/deprecated/msg/mc/CMakeLists.txt +++ b/examples/deprecated/msg/mc/CMakeLists.txt @@ -21,11 +21,19 @@ if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG) add_dependencies(tests bugged1_liveness_cleaner_off) endif() - ADD_TESH_FACTORIES(mc-bugged1 "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1.tesh) - ADD_TESH_FACTORIES(mc-bugged2 "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged2.tesh) + ADD_TESH_FACTORIES(mc-bugged1 "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1.tesh) + ADD_TESH_FACTORIES(mc-bugged2 "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged2.tesh) IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...) - ADD_TESH(mc-bugged1-liveness-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness.tesh) - ADD_TESH(mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_visited.tesh) + ADD_TESH(mc-bugged1-liveness-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness.tesh) + ADD_TESH(mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_visited.tesh) IF(HAVE_C_STACK_CLEANER) # This test checks if the stack cleaner is making a difference: ADD_TEST(mc-bugged1-liveness-stack-cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/ ${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc/) @@ -42,8 +50,7 @@ set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/bugged1.tesh ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.tesh ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness_visited.tesh ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.tesh PARENT_SCOPE) -set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged1_liveness_visited.xml - ${CMAKE_CURRENT_SOURCE_DIR}/platform.xml PARENT_SCOPE) +set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged1_liveness_visited.xml PARENT_SCOPE) set(examples_src ${examples_src} PARENT_SCOPE) set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged1_liveness ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness diff --git a/examples/deprecated/msg/mc/bugged1.c b/examples/deprecated/msg/mc/bugged1.c index efc27d6400..66c0238ff1 100644 --- a/examples/deprecated/msg/mc/bugged1.c +++ b/examples/deprecated/msg/mc/bugged1.c @@ -49,7 +49,7 @@ int main(int argc, char *argv[]) { MSG_init(&argc, argv); - MSG_create_environment("platform.xml"); + MSG_create_environment(argv[1]); MSG_function_register("server", server); MSG_function_register("client", client); diff --git a/examples/deprecated/msg/mc/bugged1.tesh b/examples/deprecated/msg/mc/bugged1.tesh index 2aea4788db..186e9a245a 100644 --- a/examples/deprecated/msg/mc/bugged1.tesh +++ b/examples/deprecated/msg/mc/bugged1.tesh @@ -2,7 +2,7 @@ ! expect return 1 ! timeout 20 -$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256 +$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1 ${platfdir:=.}/model_checker_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256 > [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. > [ 0.000000] (2:client@HostB) Sent! > [ 0.000000] (3:client@HostC) Sent! diff --git a/examples/deprecated/msg/mc/bugged1_liveness.tesh b/examples/deprecated/msg/mc/bugged1_liveness.tesh index c835b729aa..eb7572657c 100644 --- a/examples/deprecated/msg/mc/bugged1_liveness.tesh +++ b/examples/deprecated/msg/mc/bugged1_liveness.tesh @@ -3,7 +3,7 @@ ! expect return 2 ! timeout 20 ! output ignore -$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../../platforms/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness +$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness > [ 0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (3:client@Fafard) Ask the request diff --git a/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh b/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh index f8c45844da..2cd54ab1c9 100644 --- a/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh +++ b/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh @@ -3,7 +3,7 @@ ! expect return 2 ! timeout 30 ! output ignore -$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../../platforms/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness +$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness > [ 0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (3:client@Fafard) Ask the request diff --git a/examples/deprecated/msg/mc/bugged2.c b/examples/deprecated/msg/mc/bugged2.c index 448c054262..e8932b8cd7 100644 --- a/examples/deprecated/msg/mc/bugged2.c +++ b/examples/deprecated/msg/mc/bugged2.c @@ -66,7 +66,7 @@ int main(int argc, char *argv[]) { MSG_init(&argc, argv); - MSG_create_environment("platform.xml"); + MSG_create_environment(argv[1]); MSG_function_register("server", server); MSG_function_register("client", client); diff --git a/examples/deprecated/msg/mc/bugged2.tesh b/examples/deprecated/msg/mc/bugged2.tesh index 719ffe2016..d59df82d81 100644 --- a/examples/deprecated/msg/mc/bugged2.tesh +++ b/examples/deprecated/msg/mc/bugged2.tesh @@ -2,7 +2,7 @@ ! expect return 1 ! timeout 20 -$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged2 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256 +$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged2 ${platfdir:=.}/model_checker_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256 > [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. > [ 0.000000] (2:client@HostB) Send 1 > [ 0.000000] (3:client@HostC) Send 2 diff --git a/examples/deprecated/msg/mc/bugged3.c b/examples/deprecated/msg/mc/bugged3.c index 57cd689c2d..3e326e3ac5 100644 --- a/examples/deprecated/msg/mc/bugged3.c +++ b/examples/deprecated/msg/mc/bugged3.c @@ -56,7 +56,7 @@ int main(int argc, char *argv[]) { MSG_init(&argc, argv); - MSG_create_environment("platform.xml"); + MSG_create_environment(argv[1]); MSG_function_register("server", server); MSG_function_register("client", client); diff --git a/examples/deprecated/msg/mc/centralized_mutex.c b/examples/deprecated/msg/mc/centralized_mutex.c index 38f9d3ba37..34cc4909e8 100644 --- a/examples/deprecated/msg/mc/centralized_mutex.c +++ b/examples/deprecated/msg/mc/centralized_mutex.c @@ -81,7 +81,7 @@ static int client(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[]) int main(int argc, char *argv[]) { MSG_init(&argc, argv); - MSG_create_environment("../../platforms/small_platform.xml"); + MSG_create_environment(argv[1]); MSG_function_register("coordinator", coordinator); MSG_function_register("client", client); MSG_launch_application("deploy_centralized_mutex.xml"); diff --git a/examples/deprecated/msg/mc/centralized_mutex.tesh b/examples/deprecated/msg/mc/centralized_mutex.tesh index 52986c45f0..c4cf2a34df 100644 --- a/examples/deprecated/msg/mc/centralized_mutex.tesh +++ b/examples/deprecated/msg/mc/centralized_mutex.tesh @@ -1,3 +1,3 @@ #!/usr/bin/env tesh -$ ${bindir:=.}/centralized_mutex +$ ${bindir:=.}/centralized_mutex ${platfdir:=.}/model_checker_platform.xml diff --git a/examples/deprecated/msg/mc/platform.xml b/examples/platforms/model_checker_platform.xml similarity index 100% rename from examples/deprecated/msg/mc/platform.xml rename to examples/platforms/model_checker_platform.xml diff --git a/examples/s4u/CMakeLists.txt b/examples/s4u/CMakeLists.txt index ee5fd7b8ba..6111467469 100644 --- a/examples/s4u/CMakeLists.txt +++ b/examples/s4u/CMakeLists.txt @@ -73,10 +73,10 @@ foreach (example actor-create actor-daemon actor-exiting actor-join actor-kill # message("Factories of ${example}: ${_${example}_factories}") ADD_TESH_FACTORIES(s4u-${example} "${_${example}_factories}" - --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} - --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms - --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} - ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh) + --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} + ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh) else() message(STATUS "Example ${example} disabled, thus not compiled.") unset(_${example}_disabled) @@ -123,9 +123,9 @@ foreach(example app-bittorrent app-masterworkers ) ADD_TESH_FACTORIES(s4u-${example}-parallel "${parallel-factories}" --cfg contexts/nthreads:4 ${CONTEXTS_SYNCHRO} --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} - --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms - --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} - ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh) + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} + ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh) endforeach() # ns3-tests @@ -179,7 +179,6 @@ set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/actor-create/s4u-a ${CMAKE_CURRENT_SOURCE_DIR}/dht-kademlia/s4u-dht-kademlia_d.xml ${CMAKE_CURRENT_SOURCE_DIR}/energy-boot/platform_boot.xml ${CMAKE_CURRENT_SOURCE_DIR}/io-file-remote/s4u-io-file-remote_d.xml - ${CMAKE_CURRENT_SOURCE_DIR}/mc-electric-fence/platform.xml ${CMAKE_CURRENT_SOURCE_DIR}/platform-properties/s4u-platform-properties_d.xml ${CMAKE_CURRENT_SOURCE_DIR}/platform-failures/s4u-platform-failures_d.xml ${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm-split_d.xml diff --git a/examples/s4u/mc-electric-fence/platform.xml b/examples/s4u/mc-electric-fence/platform.xml deleted file mode 100644 index fd7894d640..0000000000 --- a/examples/s4u/mc-electric-fence/platform.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - - - - - - - - diff --git a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp index 0dbced1356..66c250d73e 100644 --- a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp +++ b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp @@ -42,7 +42,7 @@ int main(int argc, char* argv[]) { simgrid::s4u::Engine e(&argc, argv); - e.load_platform("platform.xml"); + e.load_platform(argv[1]); simgrid::s4u::Actor::create("server", simgrid::s4u::Host::by_name("HostA"), server); simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostB"), client, 1); diff --git a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh index 35b9790e5a..f86c4a992d 100644 --- a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh +++ b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh @@ -1,6 +1,6 @@ #!/usr/bin/env tesh -$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence platform.xml +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${platfdir}/model_checker_platform.xml > [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor. > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent! > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index d957410401..97f04c6481 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -1139,6 +1139,7 @@ set(PLATFORMS_EXAMPLES examples/platforms/optorsim/transform_optorsim_platform.pl examples/platforms/config.xml examples/platforms/config_tracing.xml + examples/platforms/model_checker_platform.xml examples/platforms/profiles/bourassa_state.profile examples/platforms/profiles/fafard_state.profile examples/platforms/profiles/faulty_host.profile -- 2.20.1