From 5cc0dbf7b395e9908158c91662cefececaeb5f19 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 14 May 2019 12:15:50 +0200 Subject: [PATCH] A first example with MC and S4U together --- examples/s4u/CMakeLists.txt | 24 +++++++ examples/s4u/README.rst | 17 +++++ .../s4u-mc-failing-assert.cpp | 62 +++++++++++++++++++ .../s4u-mc-failing-assert.tesh | 27 ++++++++ 4 files changed, 130 insertions(+) create mode 100644 examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp create mode 100644 examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh diff --git a/examples/s4u/CMakeLists.txt b/examples/s4u/CMakeLists.txt index 9596c01808..18b19d1f11 100644 --- a/examples/s4u/CMakeLists.txt +++ b/examples/s4u/CMakeLists.txt @@ -31,6 +31,30 @@ foreach (example actor-create actor-daemon actor-exiting actor-join actor-kill ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh) endforeach() + +# Model-checking examples: with only one source and tested with all factories but thread +###################################################################### + +foreach (example mc-failing-assert) + if(SIMGRID_HAVE_MC) + add_executable (s4u-${example} EXCLUDE_FROM_ALL ${example}/s4u-${example}.cpp) + add_dependencies (tests s4u-${example}) + target_link_libraries(s4u-${example} simgrid) + set_target_properties(s4u-${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${example}) + + + ADD_TESH_FACTORIES(s4u-${example} "ucontext;raw;boost" + --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) + endif() + + set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-${example}.tesh) + set(examples_src ${examples_src} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-${example}.cpp) +endforeach() + + # Multi-files examples ###################### diff --git a/examples/s4u/README.rst b/examples/s4u/README.rst index 1fab295d2f..f751c6bc14 100644 --- a/examples/s4u/README.rst +++ b/examples/s4u/README.rst @@ -408,6 +408,23 @@ Distributed Hash Tables (DHT) .. TODO:: document here the examples about plugins +======================= +Model-Checking Examples +======================= + +The model-checker can be used to exhaustively search for issues in the +tested application. It must be activated at compile time, but this +mode is rather experimental in SimGrid (as of v3.22). You should not +enable it unless you really want to formally verify your applications: +SimGrid is slower and maybe less robust when MC is enabled. + + - **Failed assert** + In this example, two actors send some data to a central server, + which asserts that the messages are always received in the same order. + This is obviously wrong, and the model-checker correctly finds a + counter-example to that assertion. + |br| `examples/s4u/mc-failed-assert/s4u-mc-failed-assert.cpp `_ + .. |br| raw:: html
diff --git a/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp b/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp new file mode 100644 index 0000000000..3a4a8a8cc3 --- /dev/null +++ b/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp @@ -0,0 +1,62 @@ +/* Copyright (c) 2010-2019. 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 + +XBT_LOG_NEW_DEFAULT_CATEGORY(mc_assert_example, "Logging channel used in this example"); + +static int server(int worker_amount) +{ + int value_got = -1; + simgrid::s4u::Mailbox* mb = simgrid::s4u::Mailbox::by_name("server"); + for (int count = 0; count < worker_amount; count++) { + int* msg = static_cast(mb->get()); + value_got = *msg; + free(msg); + } + /* + * We assert here that the last message we got (which overwrite any previously received message) is the one from the + * last worker This will obviously fail when the messages are received out of order. + */ + MC_assert(value_got == 2); + + XBT_INFO("OK"); + return 0; +} + +static int client(int rank) +{ + /* I just send my rank onto the mailbox. It must be passed as a stable memory block (thus the new) so that that + * memory survives even after the end of the client */ + + simgrid::s4u::Mailbox* mailbox = simgrid::s4u::Mailbox::by_name("server"); + mailbox->put(new int(rank), 1 /* communication cost is not really relevant in MC mode */); + + XBT_INFO("Sent!"); + return 0; +} + +int main(int argc, char* argv[]) +{ + simgrid::s4u::Engine e(&argc, argv); + xbt_assert(argc > 1, "Usage: %s platform_file\n", argv[0]); + + e.load_platform(argv[1]); + auto hosts = e.get_all_hosts(); + xbt_assert(hosts.size() >= 3, "This example requires at least 3 hosts"); + + simgrid::s4u::Actor::create("server", hosts[0], &server, 2); + simgrid::s4u::Actor::create("client1", hosts[1], &client, 1); + simgrid::s4u::Actor::create("client2", hosts[2], &client, 2); + + e.run(); + return 0; +} diff --git a/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh b/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh new file mode 100644 index 0000000000..f35e7b19fa --- /dev/null +++ b/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh @@ -0,0 +1,27 @@ +#!/usr/bin/env tesh + +! expect return 1 +! timeout 20 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning +> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (1:server@Boivin) OK +> [ 0.000000] (3:client2@Fafard) Sent! +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (1:server@Boivin) OK +> [ 0.000000] (3:client2@Fafard) Sent! +> [ 0.000000] (2:client1@Bourassa) Sent! +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) Counter-example execution trace: +> [ 0.000000] (0:maestro@) [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only)) +> [ 0.000000] (0:maestro@) [(3)Fafard (client2)] iSend(src=(3)Fafard (client2), buff=(verbose only), size=(verbose only)) +> [ 0.000000] (0:maestro@) [(1)Boivin (server)] Wait(comm=(verbose only) [(3)Fafard (client2)-> (1)Boivin (server)]) +> [ 0.000000] (0:maestro@) [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only)) +> [ 0.000000] (0:maestro@) [(2)Bourassa (client1)] iSend(src=(2)Bourassa (client1), buff=(verbose only), size=(verbose only)) +> [ 0.000000] (0:maestro@) [(1)Boivin (server)] Wait(comm=(verbose only) [(2)Bourassa (client1)-> (1)Boivin (server)]) +> [ 0.000000] (0:maestro@) Expanded states = 18 +> [ 0.000000] (0:maestro@) Visited states = 36 +> [ 0.000000] (0:maestro@) Executed transitions = 32 -- 2.20.1