From 0656c27cac6242675aba1df0f3c1ef6a79275e0c Mon Sep 17 00:00:00 2001 From: Frederic Suter Date: Mon, 23 Mar 2020 18:54:31 +0100 Subject: [PATCH] convert bugged1-liveness + Didn't check for leaks + Do not know whether the C stack cleaner is still relevant with C++ --- MANIFEST.in | 12 +- examples/deprecated/msg/mc/CMakeLists.txt | 43 +---- examples/deprecated/msg/mc/bugged1_liveness.c | 166 ------------------ .../deprecated/msg/mc/centralized_mutex.tesh | 2 +- .../msg/mc/deploy_bugged1_liveness.xml | 11 -- .../mc/deploy_bugged1_liveness_visited.xml | 11 -- examples/s4u/CMakeLists.txt | 45 ++++- .../promela_bugged1_liveness | 0 .../s4u-mc-bugged1-liveness-stack-cleaner} | 0 .../s4u-mc-bugged1-liveness-visited.tesh} | 2 +- .../s4u-mc-bugged1-liveness.cpp | 161 +++++++++++++++++ .../s4u-mc-bugged1-liveness.tesh} | 2 +- 12 files changed, 215 insertions(+), 240 deletions(-) delete mode 100644 examples/deprecated/msg/mc/bugged1_liveness.c delete mode 100644 examples/deprecated/msg/mc/deploy_bugged1_liveness.xml delete mode 100644 examples/deprecated/msg/mc/deploy_bugged1_liveness_visited.xml rename examples/{deprecated/msg/mc => s4u/mc-bugged1-liveness}/promela_bugged1_liveness (100%) rename examples/{deprecated/msg/mc/bugged1_liveness_stack_cleaner => s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner} (100%) rename examples/{deprecated/msg/mc/bugged1_liveness_visited.tesh => s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh} (96%) create mode 100644 examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp rename examples/{deprecated/msg/mc/bugged1_liveness.tesh => s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh} (91%) diff --git a/MANIFEST.in b/MANIFEST.in index fa48ede9a6..5038c32cb5 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -253,20 +253,13 @@ 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_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_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_liveness.xml -include examples/deprecated/msg/mc/deploy_bugged1_liveness_visited.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/promela_bugged1_liveness include examples/deprecated/msg/mc/promela_bugged2_liveness include examples/deprecated/msg/trace-categories/trace-categories.c include examples/deprecated/msg/trace-categories/trace-categories.tesh @@ -461,6 +454,11 @@ 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-liveness/promela_bugged1_liveness +include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner +include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh +include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp +include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.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 diff --git a/examples/deprecated/msg/mc/CMakeLists.txt b/examples/deprecated/msg/mc/CMakeLists.txt index 311923fda3..f020b32120 100644 --- a/examples/deprecated/msg/mc/CMakeLists.txt +++ b/examples/deprecated/msg/mc/CMakeLists.txt @@ -1,4 +1,4 @@ -foreach (x bugged3 centralized_mutex bugged1_liveness bugged2_liveness) +foreach (x bugged3 centralized_mutex bugged2_liveness) if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG) add_executable (${x} EXCLUDE_FROM_ALL ${x}.c) target_link_libraries(${x} simgrid) @@ -8,42 +8,7 @@ foreach (x bugged3 centralized_mutex bugged1_liveness bugged2_liveness) set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/deploy_${x}.xml) endforeach() -if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG) - if(HAVE_C_STACK_CLEANER) - add_executable (bugged1_liveness_cleaner_on EXCLUDE_FROM_ALL bugged1_liveness.c) - target_link_libraries(bugged1_liveness_cleaner_on simgrid) - set_target_properties(bugged1_liveness_cleaner_on PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fstack-cleaner") - add_dependencies(tests bugged1_liveness_cleaner_on) - - add_executable (bugged1_liveness_cleaner_off EXCLUDE_FROM_ALL bugged1_liveness.c) - target_link_libraries(bugged1_liveness_cleaner_off simgrid) - set_target_properties(bugged1_liveness_cleaner_off PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fno-stack-cleaner") - add_dependencies(tests bugged1_liveness_cleaner_off) - endif() - - 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 - --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/) - ENDIF() - ENDIF() - - if (enable_coverage) - SET_TESTS_PROPERTIES(mc-bugged1-liveness-visited-ucontext PROPERTIES RUN_SERIAL "TRUE") - endif() -endif() - -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) +set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.tesh PARENT_SCOPE) +set(xml_files ${xml_files} 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 - ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness_stack_cleaner PARENT_SCOPE) +set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness PARENT_SCOPE) diff --git a/examples/deprecated/msg/mc/bugged1_liveness.c b/examples/deprecated/msg/mc/bugged1_liveness.c deleted file mode 100644 index f0b9fdd52b..0000000000 --- a/examples/deprecated/msg/mc/bugged1_liveness.c +++ /dev/null @@ -1,166 +0,0 @@ -/* Copyright (c) 2012-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. */ - -/***************** Centralized Mutual Exclusion Algorithm *******************/ -/* This example implements a centralized mutual exclusion algorithm. */ -/* Bug : CS requests of client 1 not satisfied */ -/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */ -/****************************************************************************/ - -#ifdef GARBAGE_STACK -#include -#include -#include -#endif - -#include -#include -#include - -XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages"); - -int r=0; -int cs=0; - -#ifdef GARBAGE_STACK -/** Do not use a clean stack */ -static void garbage_stack(void) { - const size_t size = 256; - int fd = open("/dev/urandom", O_RDONLY); - char foo[size]; - read(fd, foo, size); - close(fd); -} -#endif - -static int coordinator(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[]) -{ - int CS_used = 0; - msg_task_t task = NULL; - msg_task_t answer = NULL; - xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); - char *req; - - while(1){ - MSG_task_receive(&task, "coordinator"); - const char *kind = MSG_task_get_name(task); - if (!strcmp(kind, "request")) { - req = MSG_task_get_data(task); - if (CS_used) { - XBT_INFO("CS already used. Queue the request."); - xbt_dynar_push(requests, &req); - } else { - if(strcmp(req, "1") != 0){ - XBT_INFO("CS idle. Grant immediatly"); - answer = MSG_task_create("grant", 0, 1000, NULL); - MSG_task_send(answer, req); - CS_used = 1; - answer = NULL; - } - } - } else { - if (!xbt_dynar_is_empty(requests)) { - XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests)); - xbt_dynar_shift(requests, &req); - if(strcmp(req, "1") != 0){ - MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); - }else{ - xbt_dynar_push(requests, &req); - CS_used = 0; - } - }else{ - XBT_INFO("CS release. resource now idle"); - CS_used = 0; - } - } - MSG_task_destroy(task); - task = NULL; - kind = NULL; - req = NULL; - } - return 0; -} - -static int client(int argc, char *argv[]) -{ - xbt_assert(argc == 2); - int my_pid = MSG_process_get_PID(MSG_process_self()); - - char *my_mailbox = xbt_strdup(argv[1]); - msg_task_t grant = NULL; - msg_task_t release = NULL; - - while(1){ - XBT_INFO("Ask the request"); - MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); - - if(strcmp(my_mailbox, "1") == 0){ - r = 1; - cs = 0; - XBT_INFO("Propositions changed : r=1, cs=0"); - } - - MSG_task_receive(&grant, my_mailbox); - const char *kind = MSG_task_get_name(grant); - - if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){ - cs = 1; - r = 0; - XBT_INFO("Propositions changed : r=0, cs=1"); - } - - MSG_task_destroy(grant); - grant = NULL; - kind = NULL; - - XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]); - - MSG_process_sleep(1); - - release = MSG_task_create("release", 0, 1000, NULL); - MSG_task_send(release, "coordinator"); - - release = NULL; - - MSG_process_sleep(my_pid); - - if(strcmp(my_mailbox, "1") == 0){ - cs=0; - r=0; - XBT_INFO("Propositions changed : r=0, cs=0"); - } - - } - return 0; -} - -static int raw_client(int argc, char *argv[]) -{ -#ifdef GARBAGE_STACK - // At this point the stack of the callee (client) is probably filled with - // zeros and uninitialized variables will contain 0. This call will place - // random byes in the stack of the callee: - garbage_stack(); -#endif - return client(argc, argv); -} - -int main(int argc, char *argv[]) -{ - MSG_init(&argc, argv); - - MC_automaton_new_propositional_symbol_pointer("r", &r); - MC_automaton_new_propositional_symbol_pointer("cs", &cs); - - MSG_create_environment(argv[1]); - - MSG_function_register("coordinator", coordinator); - MSG_function_register("client", raw_client); - MSG_launch_application(argv[2]); - - MSG_main(); - - return 0; -} diff --git a/examples/deprecated/msg/mc/centralized_mutex.tesh b/examples/deprecated/msg/mc/centralized_mutex.tesh index c4cf2a34df..f2202c4508 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 ${platfdir:=.}/model_checker_platform.xml +$ ${bindir:=.}/centralized_mutex ${platfdir:=.}/small_platform.xml diff --git a/examples/deprecated/msg/mc/deploy_bugged1_liveness.xml b/examples/deprecated/msg/mc/deploy_bugged1_liveness.xml deleted file mode 100644 index e47601c512..0000000000 --- a/examples/deprecated/msg/mc/deploy_bugged1_liveness.xml +++ /dev/null @@ -1,11 +0,0 @@ - - - - - - - - - - - diff --git a/examples/deprecated/msg/mc/deploy_bugged1_liveness_visited.xml b/examples/deprecated/msg/mc/deploy_bugged1_liveness_visited.xml deleted file mode 100644 index b8e29cdde3..0000000000 --- a/examples/deprecated/msg/mc/deploy_bugged1_liveness_visited.xml +++ /dev/null @@ -1,11 +0,0 @@ - - - - - - - - - - - diff --git a/examples/s4u/CMakeLists.txt b/examples/s4u/CMakeLists.txt index 623de0a9fc..32c18fe811 100644 --- a/examples/s4u/CMakeLists.txt +++ b/examples/s4u/CMakeLists.txt @@ -27,6 +27,22 @@ foreach (example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence) set(_${example}_factories "ucontext;raw;boost") endforeach() +if(SIMGRID_HAVE_MC) + set(_mc-bugged1-liveness_disable 1) + if(HAVE_C_STACK_CLEANER) + add_executable (s4u-mc-bugged1-liveness-cleaner-on EXCLUDE_FROM_ALL s4u-mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp) + target_link_libraries(s4u-mc-bugged1-liveness-cleaner-on simgrid) + set_target_properties(s4u-mc-bugged1-liveness-cleaner-on PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fstack-cleaner") + add_dependencies(tests s4u-mc-bugged1-liveness-cleaner-on) + + add_executable (s4u-mc-bugged1-liveness-cleaner-off EXCLUDE_FROM_ALL s4u-mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp) + target_link_libraries(s4u-mc-bugged1-liveness-cleaner-off simgrid) + set_target_properties(s4u-mc-bugged1-liveness-cleaner-off PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fno-stack-cleaner") + add_dependencies(tests s4u-mc-bugged1-liveness-cleaner-off) + endif() + +endif() + 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 +63,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-bugged1 mc-bugged2 mc-electric-fence mc-failing-assert + mc-bugged1 mc-bugged1-liveness 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 @@ -106,7 +122,27 @@ foreach(variant fun class) endforeach() set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/app-masterworkers/s4u-app-masterworkers.tesh) - +# Model-checking liveness +if(SIMGRID_HAVE_MC) + IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...) + ADD_TESH(s4u-mc-bugged1-liveness-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/s4u/mc-bugged1-liveness + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/ s4u-mc-bugged1-liveness.tesh) + ADD_TESH(s4u-mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/s4u/mc-bugged1-liveness + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --cd ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/ s4u-mc-bugged1-liveness-visited.tesh) + IF(HAVE_C_STACK_CLEANER) + # This test checks if the stack cleaner is making a difference: + ADD_TEST(s4u-mc-bugged1-liveness-stack-cleaner ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner + ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/ + ${CMAKE_BINARY_DIR}/examples/s4u/mc-bugged1-liveness/) + ENDIF() + ENDIF() + + if (enable_coverage) + SET_TESTS_PROPERTIES(mc-bugged1-liveness-visited-ucontext PROPERTIES RUN_SERIAL "TRUE") + endif() +ENDIF() # The tests the parallel variant of of DHTs @@ -164,6 +200,7 @@ endif() set(examples_src ${examples_src} ${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/s4u-network-ns3.cpp PARENT_SCOPE) set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/app-pingpong/simix-breakpoint.tesh + ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh ${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/s4u-network-ns3.tesh PARENT_SCOPE) set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/actor-create/s4u-actor-create_d.xml ${CMAKE_CURRENT_SOURCE_DIR}/actor-lifetime/s4u-actor-lifetime_d.xml @@ -191,7 +228,9 @@ set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/actor-create/s4u-a ${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/dogbone_d.xml ${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/onelink_d.xml ${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/one_cluster_d.xml PARENT_SCOPE) -set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/dht-kademlia/generate.py PARENT_SCOPE) +set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/dht-kademlia/generate.py + ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner + ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness/promela_bugged1_liveness PARENT_SCOPE) set(txt_files ${txt_files} ${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm-split-p0.txt ${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm-split-p1.txt ${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm.txt diff --git a/examples/deprecated/msg/mc/promela_bugged1_liveness b/examples/s4u/mc-bugged1-liveness/promela_bugged1_liveness similarity index 100% rename from examples/deprecated/msg/mc/promela_bugged1_liveness rename to examples/s4u/mc-bugged1-liveness/promela_bugged1_liveness diff --git a/examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner b/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner similarity index 100% rename from examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner rename to examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner diff --git a/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh b/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh similarity index 96% rename from examples/deprecated/msg/mc/bugged1_liveness_visited.tesh rename to examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh index 2cd54ab1c9..e88cc7e895 100644 --- a/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh +++ b/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh @@ -3,7 +3,7 @@ ! expect return 2 ! timeout 30 ! output ignore -$ ${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 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 1 --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/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp b/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp new file mode 100644 index 0000000000..9df987210f --- /dev/null +++ b/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp @@ -0,0 +1,161 @@ +/* Copyright (c) 2012-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. */ + +/***************** Centralized Mutual Exclusion Algorithm *******************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* Bug : CS requests of client 1 not satisfied */ +/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */ +/****************************************************************************/ + +#ifdef GARBAGE_STACK +#include +#include +#include +#endif + +#include +#include +#include + +XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages"); + +class Message { +public: + enum class Kind { GRANT, REQUEST, RELEASE }; + Kind kind = Kind::GRANT; + simgrid::s4u::Mailbox* return_mailbox = nullptr; + explicit Message(Message::Kind kind, simgrid::s4u::Mailbox* mbox) : kind(kind), return_mailbox(mbox) {} +}; + +int r = 0; +int cs = 0; + +#ifdef GARBAGE_STACK +/** Do not use a clean stack */ +static void garbage_stack(void) +{ + const size_t size = 256; + int fd = open("/dev/urandom", O_RDONLY); + char foo[size]; + read(fd, foo, size); + close(fd); +} +#endif + +static void coordinator() +{ + int CS_used = 0; + Message* m = nullptr; + std::queue requests; + + simgrid::s4u::Mailbox* mbox = simgrid::s4u::Mailbox::by_name("coordinator"); + + while (1) { + m = static_cast(mbox->get()); + if (m->kind == Message::Kind::REQUEST) { + if (CS_used) { + XBT_INFO("CS already used. Queue the request."); + requests.push(m->return_mailbox); + } else { + if (m->return_mailbox->get_name() != "1") { + XBT_INFO("CS idle. Grant immediatly"); + m->return_mailbox->put(new Message(Message::Kind::GRANT, mbox), 1000); + CS_used = 1; + } + } + } else { + if (not requests.empty()) { + XBT_INFO("CS release. Grant to queued requests (queue size: %zu)", requests.size()); + simgrid::s4u::Mailbox* req = requests.front(); + requests.pop(); + if (req->get_name() != "1") { + req->put(new Message(Message::Kind::GRANT, mbox), 1000); + } else { + requests.push(req); + CS_used = 0; + } + } else { + XBT_INFO("CS release. resource now idle"); + CS_used = 0; + } + } + delete m; + } +} + +static void client(int id) +{ + int my_pid = simgrid::s4u::this_actor::get_pid(); + + simgrid::s4u::Mailbox* my_mailbox = simgrid::s4u::Mailbox::by_name(std::to_string(id)); + + while (1) { + XBT_INFO("Ask the request"); + simgrid::s4u::Mailbox::by_name("coordinator")->put(new Message(Message::Kind::REQUEST, my_mailbox), 1000); + + if (id == 1) { + r = 1; + cs = 0; + XBT_INFO("Propositions changed : r=1, cs=0"); + } + + Message* grant = static_cast(my_mailbox->get()); + + if ((id == 1) && (grant->kind == Message::Kind::GRANT)) { + cs = 1; + r = 0; + XBT_INFO("Propositions changed : r=0, cs=1"); + } + + delete grant; + + XBT_INFO("%d got the answer. Sleep a bit and release it", id); + + simgrid::s4u::this_actor::sleep_for(1); + + simgrid::s4u::Mailbox::by_name("coordinator")->put(new Message(Message::Kind::RELEASE, my_mailbox), 1000); + + simgrid::s4u::this_actor::sleep_for(my_pid); + + if (id == 1) { + cs = 0; + r = 0; + XBT_INFO("Propositions changed : r=0, cs=0"); + } + } +} + +static void raw_client(int id) +{ +#ifdef GARBAGE_STACK + // At this point the stack of the callee (client) is probably filled with + // zeros and uninitialized variables will contain 0. This call will place + // random byes in the stack of the callee: + garbage_stack(); +#endif + client(id); +} + +int main(int argc, char* argv[]) +{ + simgrid::s4u::Engine e(&argc, argv); + + MC_automaton_new_propositional_symbol_pointer("r", &r); + MC_automaton_new_propositional_symbol_pointer("cs", &cs); + + e.load_platform(argv[1]); + + simgrid::s4u::Actor::create("coordinator", simgrid::s4u::Host::by_name("Tremblay"), coordinator); + if (std::stod(argv[2]) == 0) { + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Boivin"), raw_client, 1); + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Fafard"), raw_client, 2); + } else { // "Visited" case + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Boivin"), raw_client, 2); + simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Fafard"), raw_client, 1); + } + e.run(); + + return 0; +} diff --git a/examples/deprecated/msg/mc/bugged1_liveness.tesh b/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh similarity index 91% rename from examples/deprecated/msg/mc/bugged1_liveness.tesh rename to examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh index eb7572657c..e11847d40e 100644 --- a/examples/deprecated/msg/mc/bugged1_liveness.tesh +++ b/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh @@ -3,7 +3,7 @@ ! expect return 2 ! timeout 20 ! output ignore -$ ${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 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 0 --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 -- 2.20.1