From eaf8316769037f78a4b9d475d9c81a182da655dc Mon Sep 17 00:00:00 2001 From: Frederic Suter Date: Tue, 10 Mar 2020 14:24:09 +0100 Subject: [PATCH] convert, simplify, and disable mc-electric-fence --- MANIFEST.in | 6 +- examples/deprecated/msg/mc/CMakeLists.txt | 5 +- .../msg/mc/deploy_electric_fence.xml | 13 ----- examples/deprecated/msg/mc/electric_fence.c | 58 ------------------- examples/s4u/CMakeLists.txt | 5 +- .../mc => s4u/mc-electric-fence}/platform.xml | 5 -- .../s4u-mc-electric-fence.cpp | 55 ++++++++++++++++++ 7 files changed, 64 insertions(+), 83 deletions(-) delete mode 100644 examples/deprecated/msg/mc/deploy_electric_fence.xml delete mode 100644 examples/deprecated/msg/mc/electric_fence.c rename examples/{deprecated/msg/mc => s4u/mc-electric-fence}/platform.xml (75%) create mode 100644 examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp diff --git a/MANIFEST.in b/MANIFEST.in index ae4bdc32bf..031b3693a6 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -262,9 +262,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/deploy_electric_fence.xml -include examples/deprecated/msg/mc/electric_fence.c -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/synchro-semaphore/synchro-semaphore.c @@ -464,6 +461,9 @@ 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 include examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh include examples/s4u/network-ns3/3hosts_2links_d.xml diff --git a/examples/deprecated/msg/mc/CMakeLists.txt b/examples/deprecated/msg/mc/CMakeLists.txt index e22c4a0943..f02d55eea9 100644 --- a/examples/deprecated/msg/mc/CMakeLists.txt +++ b/examples/deprecated/msg/mc/CMakeLists.txt @@ -1,4 +1,4 @@ -foreach (x bugged1 bugged2 bugged3 centralized_mutex electric_fence bugged1_liveness bugged2_liveness) +foreach (x bugged1 bugged2 bugged3 centralized_mutex bugged1_liveness bugged2_liveness) if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG) add_executable (${x} EXCLUDE_FROM_ALL ${x}.c) target_link_libraries(${x} simgrid) @@ -42,8 +42,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/deploy_electric_fence.xml b/examples/deprecated/msg/mc/deploy_electric_fence.xml deleted file mode 100644 index 75f6396303..0000000000 --- a/examples/deprecated/msg/mc/deploy_electric_fence.xml +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - - - - diff --git a/examples/deprecated/msg/mc/electric_fence.c b/examples/deprecated/msg/mc/electric_fence.c deleted file mode 100644 index edc2233005..0000000000 --- a/examples/deprecated/msg/mc/electric_fence.c +++ /dev/null @@ -1,58 +0,0 @@ -/* Copyright (c) 2013-2020. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -/******************** Non-deterministic message ordering *********************/ -/* This example implements one process which receives messages from two other */ -/* processes. There is no bug on it, it is just provided to test the soundness*/ -/* of the state space reduction with DPOR, if the maximum depth (defined with */ -/* --cfg=model-check/max-depth:) is reached. */ -/******************************************************************************/ - -#include -#include - -#define N 2 - -XBT_LOG_NEW_DEFAULT_CATEGORY(electric_fence, "Example to check the soundness of DPOR"); - -static int server(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[]) -{ - msg_task_t task1 = NULL; - msg_task_t task2 = NULL; - - msg_comm_t comm_received1 = MSG_task_irecv(&task1, "mymailbox"); - msg_comm_t comm_received2 = MSG_task_irecv(&task2, "mymailbox"); - - MSG_comm_wait(comm_received1, -1); - MSG_comm_wait(comm_received2, -1); - - XBT_INFO("OK"); - return 0; -} - -static int client(int argc, char *argv[]) -{ - xbt_assert(argc == 2); - msg_task_t task = MSG_task_create(argv[1], 0, 10000, NULL); - - MSG_task_send(task, "mymailbox"); - - XBT_INFO("Sent!"); - return 0; -} - -int main(int argc, char *argv[]) -{ - MSG_init(&argc, argv); - - MSG_create_environment("platform.xml"); - - MSG_function_register("server", server); - MSG_function_register("client", client); - MSG_launch_application("deploy_electric_fence.xml"); - - MSG_main(); - return 0; -} diff --git a/examples/s4u/CMakeLists.txt b/examples/s4u/CMakeLists.txt index 1fd55f57be..dd8c4e2e76 100644 --- a/examples/s4u/CMakeLists.txt +++ b/examples/s4u/CMakeLists.txt @@ -27,6 +27,8 @@ foreach (example mc-failing-assert) set(_${example}_factories "ucontext;raw;boost") endforeach() +set(_mc-electric-fence_disable 1) + if(SIMGRID_HAVE_NS3) add_executable (s4u-network-ns3 EXCLUDE_FROM_ALL network-ns3/s4u-network-ns3.cpp) target_link_libraries(s4u-network-ns3 simgrid) @@ -47,7 +49,7 @@ foreach (example actor-create actor-daemon actor-exiting actor-join actor-kill engine-filtering exec-async exec-basic exec-dvfs exec-ptask exec-remote exec-waitany exec-waitfor exec-dependent maestro-set - mc-failing-assert + mc-electric-fence mc-failing-assert io-async io-file-system io-file-remote io-disk-raw io-dependent platform-failures platform-profile platform-properties plugin-hostload @@ -179,6 +181,7 @@ 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/deprecated/msg/mc/platform.xml b/examples/s4u/mc-electric-fence/platform.xml similarity index 75% rename from examples/deprecated/msg/mc/platform.xml rename to examples/s4u/mc-electric-fence/platform.xml index 246d72b54f..fd7894d640 100644 --- a/examples/deprecated/msg/mc/platform.xml +++ b/examples/s4u/mc-electric-fence/platform.xml @@ -5,18 +5,13 @@ - - - - - diff --git a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp new file mode 100644 index 0000000000..dbeeaa1cf9 --- /dev/null +++ b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp @@ -0,0 +1,55 @@ +/* Copyright (c) 2013-2020. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +/******************** Non-deterministic message ordering *********************/ +/* This example implements one process which receives messages from two other */ +/* processes. There is no bug on it, it is just provided to test the soundness*/ +/* of the state space reduction with DPOR, if the maximum depth (defined with */ +/* --cfg=model-check/max-depth:) is reached. */ +/******************************************************************************/ + +#include +#include + +#define N 2 + +XBT_LOG_NEW_DEFAULT_CATEGORY(electric_fence, "Example to check the soundness of DPOR"); + +static void server() +{ + void* data1 = nullptr; + void* data2 = nullptr; + simgrid::s4u::CommPtr comm_received1 = simgrid::s4u::Mailbox::by_name("mymailbox")->get_async(&data1); + simgrid::s4u::CommPtr comm_received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get_async(&data2); + + comm_received1->wait(); + comm_received2->wait(); + + XBT_INFO("OK"); + delete static_cast(data1); + delete static_cast(data2); +} + +static void client(int id) +{ + int* payload = new int(); + *payload = id; + simgrid::s4u::Mailbox::by_name("mymailbox")->put(payload, 10000); + XBT_INFO("Sent!"); +} + +int main(int argc, char* argv[]) +{ + simgrid::s4u::Engine e(&argc, argv); + + e.load_platform("platform.xml"); + + 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); + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostC"), client, 2); + + e.run(); + return 0; +} -- 2.20.1