Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
A first example with MC and S4U together
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Tue, 14 May 2019 10:15:50 +0000 (12:15 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Tue, 14 May 2019 10:16:28 +0000 (12:16 +0200)
examples/s4u/CMakeLists.txt
examples/s4u/README.rst
examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp [new file with mode: 0644]
examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh [new file with mode: 0644]

index 9596c01..18b19d1 100644 (file)
@@ -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
 ######################
 
index 1fab295..f751c6b 100644 (file)
@@ -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 <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/mc-failed-assert/s4u-mc-failed-assert.cpp>`_
+
 .. |br| raw:: html
 
    <br />
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 (file)
index 0000000..3a4a8a8
--- /dev/null
@@ -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 <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+
+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<int*>(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 (file)
index 0000000..f35e7b1
--- /dev/null
@@ -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