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
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
-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)
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
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)
+++ /dev/null
-/* 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 <simgrid/msg.h>
-#include <simgrid/modelchecker.h>
-
-#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;
-}
+++ /dev/null
-/* 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 <simgrid/msg.h>
-#include <simgrid/modelchecker.h>
-#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;
-}
+++ /dev/null
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
-<platform version="4.1">
- <actor host="HostA" function="server">
- <argument value="0"/>
- </actor>
- <actor host="HostB" function="client">
- <argument value="1"/>
- </actor>
- <actor host="HostC" function="client">
- <argument value="2"/>
- </actor>
- <actor host="HostD" function="client">
- <argument value="3"/>
- </actor>
-</platform>
+++ /dev/null
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
-<platform version="4.1">
- <actor host="HostA" function="server">
- <argument value="0"/>
- </actor>
- <actor host="HostB" function="client">
- <argument value="1"/>
- </actor>
- <actor host="HostC" function="client">
- <argument value="2"/>
- </actor>
-</platform>
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()
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
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
--- /dev/null
+/* 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 <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+
+#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<int*>(received);
+ received = nullptr;
+ }
+ received = simgrid::s4u::Mailbox::by_name("mymailbox")->get();
+ count++;
+ }
+ int value_got = *(static_cast<int*>(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;
+}
! 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!
--- /dev/null
+/* 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 <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+#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<int*>(received1));
+ received1 = nullptr;
+ XBT_INFO("Received %ld", val1);
+
+ received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get();
+ long val2 = *(static_cast<int*>(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<int*>(received1));
+ XBT_INFO("Received %ld", val1);
+
+ received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get();
+ val2 = *(static_cast<int*>(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;
+}
! 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
