From: Frederic Suter Date: Mon, 23 Mar 2020 15:43:06 +0000 (+0100) Subject: convert mc-bugged1 and mc-bugged2 X-Git-Tag: v3.26~711 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/100b572b5cdf8a4762953413ddb28be5a66b8af5?hp=895fe7fcdb5b1cf9661fcfbc3bcbe7b5518ed302 convert mc-bugged1 and mc-bugged2 --- diff --git a/MANIFEST.in b/MANIFEST.in index f5507733eb..fa48ede9a6 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -253,22 +253,16 @@ include examples/deprecated/java/trace/pingpong/Receiver.java include examples/deprecated/java/trace/pingpong/Sender.java include examples/deprecated/java/trace/pingpong/trace-pingpong.tesh include examples/deprecated/msg/README.doc -include examples/deprecated/msg/mc/bugged1.c -include examples/deprecated/msg/mc/bugged1.tesh include examples/deprecated/msg/mc/bugged1_liveness.c include examples/deprecated/msg/mc/bugged1_liveness.tesh include examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner include examples/deprecated/msg/mc/bugged1_liveness_visited.tesh -include examples/deprecated/msg/mc/bugged2.c -include examples/deprecated/msg/mc/bugged2.tesh include examples/deprecated/msg/mc/bugged2_liveness.c include examples/deprecated/msg/mc/bugged3.c include examples/deprecated/msg/mc/centralized_mutex.c include examples/deprecated/msg/mc/centralized_mutex.tesh -include examples/deprecated/msg/mc/deploy_bugged1.xml include examples/deprecated/msg/mc/deploy_bugged1_liveness.xml include examples/deprecated/msg/mc/deploy_bugged1_liveness_visited.xml -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 @@ -467,6 +461,10 @@ 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-bugged1/s4u-mc-bugged1.cpp +include examples/s4u/mc-bugged1/s4u-mc-bugged1.tesh +include examples/s4u/mc-bugged2/s4u-mc-bugged2.cpp +include examples/s4u/mc-bugged2/s4u-mc-bugged2.tesh 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 diff --git a/examples/deprecated/msg/mc/CMakeLists.txt b/examples/deprecated/msg/mc/CMakeLists.txt index 31a9c38596..311923fda3 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 bugged1_liveness bugged2_liveness) +foreach (x 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) @@ -21,12 +21,6 @@ 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 - --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 --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms @@ -45,9 +39,7 @@ if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG) endif() endif() -set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/bugged1.tesh - ${CMAKE_CURRENT_SOURCE_DIR}/bugged2.tesh - ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.tesh +set(tesh_files ${tesh_files} ${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 PARENT_SCOPE) diff --git a/examples/deprecated/msg/mc/bugged1.c b/examples/deprecated/msg/mc/bugged1.c deleted file mode 100644 index 66c0238ff1..0000000000 --- a/examples/deprecated/msg/mc/bugged1.c +++ /dev/null @@ -1,60 +0,0 @@ -/* Copyright (c) 2010-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 *********************/ -/* Server assumes a fixed order in the reception of messages from its clients */ -/* which is incorrect because the message ordering is non-deterministic */ -/******************************************************************************/ - -#include -#include - -#define N 3 - -XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example"); - -static int server(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[]) -{ - msg_task_t task = NULL; - int count = 0; - while (count < N) { - if (task) { - MSG_task_destroy(task); - task = NULL; - } - MSG_task_receive(&task, "mymailbox"); - count++; - } - int value_got = xbt_str_parse_int(MSG_task_get_name(task), "Task names must be integers, not '%s'"); - MC_assert(value_got == 3); - - 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 /*comp cost */ , 10000 /*comm size */ , NULL /*arbitrary data */ ); - - MSG_task_send(task, "mymailbox"); - - XBT_INFO("Sent!"); - return 0; -} - -int main(int argc, char *argv[]) -{ - MSG_init(&argc, argv); - - MSG_create_environment(argv[1]); - - MSG_function_register("server", server); - MSG_function_register("client", client); - MSG_launch_application("deploy_bugged1.xml"); - - MSG_main(); - return 0; -} diff --git a/examples/deprecated/msg/mc/bugged2.c b/examples/deprecated/msg/mc/bugged2.c deleted file mode 100644 index e8932b8cd7..0000000000 --- a/examples/deprecated/msg/mc/bugged2.c +++ /dev/null @@ -1,77 +0,0 @@ -/* Copyright (c) 2010-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 *********************/ -/* Server assumes a fixed order in the reception of messages from its clients */ -/* which is incorrect because the message ordering is non-deterministic */ -/******************************************************************************/ - -#include -#include -#define N 3 - -XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example"); - -static int server(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[]) -{ - msg_task_t task1 = NULL; - msg_task_t task2 = NULL; - - MSG_task_receive(&task1, "mymailbox"); - long val1 = xbt_str_parse_int(MSG_task_get_name(task1), "Task name is not a numerical ID: %s"); - MSG_task_destroy(task1); - task1 = NULL; - XBT_INFO("Received %ld", val1); - - MSG_task_receive(&task2, "mymailbox"); - long val2 = xbt_str_parse_int(MSG_task_get_name(task2), "Task name is not a numerical ID: %s"); - MSG_task_destroy(task2); - task2 = NULL; - XBT_INFO("Received %ld", val2); - - MC_assert(MIN(val1, val2) == 1); - - MSG_task_receive(&task1, "mymailbox"); - val1 = xbt_str_parse_int(MSG_task_get_name(task1), "Task name is not a numerical ID: %s"); - MSG_task_destroy(task1); - XBT_INFO("Received %ld", val1); - - MSG_task_receive(&task2, "mymailbox"); - val2 = xbt_str_parse_int(MSG_task_get_name(task2), "Task name is not a numerical ID: %s"); - MSG_task_destroy(task2); - XBT_INFO("Received %ld", val2); - - XBT_INFO("OK"); - return 0; -} - -static int client(int argc, char *argv[]) -{ - xbt_assert(argc == 2); - msg_task_t task1 = MSG_task_create(argv[1], 0, 10000, NULL); - msg_task_t task2 = MSG_task_create(argv[1], 0, 10000, NULL); - - XBT_INFO("Send %s", argv[1]); - MSG_task_send(task1, "mymailbox"); - - XBT_INFO("Send %s", argv[1]); - MSG_task_send(task2, "mymailbox"); - - return 0; -} - -int main(int argc, char *argv[]) -{ - MSG_init(&argc, argv); - - MSG_create_environment(argv[1]); - - MSG_function_register("server", server); - MSG_function_register("client", client); - MSG_launch_application("deploy_bugged2.xml"); - - MSG_main(); - return 0; -} diff --git a/examples/deprecated/msg/mc/deploy_bugged1.xml b/examples/deprecated/msg/mc/deploy_bugged1.xml deleted file mode 100644 index 1cbc7ab83a..0000000000 --- a/examples/deprecated/msg/mc/deploy_bugged1.xml +++ /dev/null @@ -1,16 +0,0 @@ - - - - - - - - - - - - - - - - diff --git a/examples/deprecated/msg/mc/deploy_bugged2.xml b/examples/deprecated/msg/mc/deploy_bugged2.xml deleted file mode 100644 index 08653275c2..0000000000 --- a/examples/deprecated/msg/mc/deploy_bugged2.xml +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - - - - diff --git a/examples/s4u/CMakeLists.txt b/examples/s4u/CMakeLists.txt index 6111467469..623de0a9fc 100644 --- a/examples/s4u/CMakeLists.txt +++ b/examples/s4u/CMakeLists.txt @@ -20,7 +20,7 @@ if(WIN32) set(_maestro-set_disable 1) endif() -foreach (example mc-failing-assert mc-electric-fence) +foreach (example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence) if(NOT SIMGRID_HAVE_MC) set(_${example}_disable 1) endif() @@ -31,7 +31,7 @@ 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) set_target_properties(s4u-network-ns3 PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/network-ns3) - add_dependencies(tests s4u-network-ns3) + add_dependencies(tests s4u-network-ns3) endif() # Deal with each example @@ -47,7 +47,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-electric-fence mc-failing-assert + mc-bugged1 mc-bugged2 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 diff --git a/examples/s4u/mc-bugged1/s4u-mc-bugged1.cpp b/examples/s4u/mc-bugged1/s4u-mc-bugged1.cpp new file mode 100644 index 0000000000..802403d2e0 --- /dev/null +++ b/examples/s4u/mc-bugged1/s4u-mc-bugged1.cpp @@ -0,0 +1,58 @@ +/* Copyright (c) 2010-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 *********************/ +/* Server assumes a fixed order in the reception of messages from its clients */ +/* which is incorrect because the message ordering is non-deterministic */ +/******************************************************************************/ + +#include +#include + +#define N 3 + +XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example"); + +static void server() +{ + void* received = nullptr; + int count = 0; + while (count < N) { + if (received) { + delete static_cast(received); + received = nullptr; + } + received = simgrid::s4u::Mailbox::by_name("mymailbox")->get(); + count++; + } + int value_got = *(static_cast(received)); + MC_assert(value_got == 3); + + XBT_INFO("OK"); +} + +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(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); + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostC"), client, 2); + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostD"), client, 3); + + e.run(); + return 0; +} diff --git a/examples/deprecated/msg/mc/bugged1.tesh b/examples/s4u/mc-bugged1/s4u-mc-bugged1.tesh similarity index 91% rename from examples/deprecated/msg/mc/bugged1.tesh rename to examples/s4u/mc-bugged1/s4u-mc-bugged1.tesh index 186e9a245a..d004d06e26 100644 --- a/examples/deprecated/msg/mc/bugged1.tesh +++ b/examples/s4u/mc-bugged1/s4u-mc-bugged1.tesh @@ -2,7 +2,7 @@ ! expect return 1 ! timeout 20 -$ ${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 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-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/s4u/mc-bugged2/s4u-mc-bugged2.cpp b/examples/s4u/mc-bugged2/s4u-mc-bugged2.cpp new file mode 100644 index 0000000000..6a89f02619 --- /dev/null +++ b/examples/s4u/mc-bugged2/s4u-mc-bugged2.cpp @@ -0,0 +1,71 @@ +/* Copyright (c) 2010-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 *********************/ +/* Server assumes a fixed order in the reception of messages from its clients */ +/* which is incorrect because the message ordering is non-deterministic */ +/******************************************************************************/ + +#include +#include +#define N 3 + +XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example"); + +static void server() +{ + void* received1 = nullptr; + void* received2 = nullptr; + + received1 = simgrid::s4u::Mailbox::by_name("mymailbox")->get(); + long val1 = *(static_cast(received1)); + received1 = nullptr; + XBT_INFO("Received %ld", val1); + + received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get(); + long val2 = *(static_cast(received2)); + received2 = nullptr; + XBT_INFO("Received %ld", val2); + + MC_assert(std::min(val1, val2) == 1); + + received1 = simgrid::s4u::Mailbox::by_name("mymailbox")->get(); + val1 = *(static_cast(received1)); + XBT_INFO("Received %ld", val1); + + received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get(); + val2 = *(static_cast(received2)); + XBT_INFO("Received %ld", val2); + + XBT_INFO("OK"); +} + +static void client(int id) +{ + int* payload1 = new int(); + *payload1 = id; + int* payload2 = new int(); + *payload2 = id; + + XBT_INFO("Send %d", id); + simgrid::s4u::Mailbox::by_name("mymailbox")->put(payload1, 10000); + + XBT_INFO("Send %d", id); + simgrid::s4u::Mailbox::by_name("mymailbox")->put(payload2, 10000); +} + +int main(int argc, char* argv[]) +{ + simgrid::s4u::Engine e(&argc, argv); + + 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); + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostC"), client, 2); + + e.run(); + return 0; +} diff --git a/examples/deprecated/msg/mc/bugged2.tesh b/examples/s4u/mc-bugged2/s4u-mc-bugged2.tesh similarity index 99% rename from examples/deprecated/msg/mc/bugged2.tesh rename to examples/s4u/mc-bugged2/s4u-mc-bugged2.tesh index d59df82d81..c6b3708211 100644 --- a/examples/deprecated/msg/mc/bugged2.tesh +++ b/examples/s4u/mc-bugged2/s4u-mc-bugged2.tesh @@ -2,7 +2,7 @@ ! expect return 1 ! timeout 20 -$ ${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 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-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