include examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh
include examples/cpp/mc-bugged1/s4u-mc-bugged1.cpp
include examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh
+include examples/cpp/mc-bugged2-liveness/promela_bugged2_liveness
+include examples/cpp/mc-bugged2-liveness/s4u-mc-bugged2-liveness.cpp
+include examples/cpp/mc-bugged2-liveness/s4u-mc-bugged2-liveness.tesh
include examples/cpp/mc-bugged2/s4u-mc-bugged2.cpp
include examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
include examples/cpp/mc-electric-fence/s4u-mc-electric-fence.cpp
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/mc/bugged2-liveness.tesh
-include examples/deprecated/msg/mc/bugged2_liveness.c
include examples/deprecated/msg/mc/centralized_mutex.c
include examples/deprecated/msg/mc/centralized_mutex.tesh
-include examples/deprecated/msg/mc/deploy_bugged2_liveness.xml
include examples/deprecated/msg/mc/deploy_centralized_mutex.xml
-include examples/deprecated/msg/mc/promela_bugged2_liveness
include examples/python/actor-create/actor-create.py
include examples/python/actor-create/actor-create.tesh
include examples/python/actor-daemon/actor-daemon.py
#foreach(example ) # no test to be build in any case
#endforeach()
-
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)
# liveness model-checking works only on 64bits (for now ...)
set(_mc-bugged1-liveness_factories "ucontext") # Timeout
add_dependencies(tests-mc s4u-mc-bugged1-liveness)
+ set(_mc-bugged2-liveness_factories "ucontext") # Timeout
else()
set(_mc-bugged1-liveness_disable 1)
endif()
+
+ # This example never ends, disable it for now
+ set(_mc-bugged2-liveness_disable 1)
# This example hit the 5' timeout on CI, disable it for now
# ADD_TESH(s4u-mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/mc-bugged1-liveness
else()
foreach (example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence
- mc-bugged1-liveness)
+ mc-bugged1-liveness mc-bugged2-liveness)
set(_${example}_disable 1)
endforeach()
endif()
exec-async exec-basic exec-dvfs exec-remote exec-waitany exec-waitfor exec-dependent exec-unassigned
exec-ptask-multicore exec-cpu-nonlinear exec-cpu-factors exec-failure
maestro-set
- mc-bugged1 mc-bugged1-liveness mc-bugged2 mc-electric-fence mc-failing-assert
+ mc-bugged1 mc-bugged1-liveness mc-bugged2 mc-bugged2-liveness mc-electric-fence mc-failing-assert
network-ns3 network-ns3-wifi network-wifi
io-async io-priority io-degradation io-file-system io-file-remote io-disk-raw io-dependent
platform-failures platform-profile platform-properties
${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
${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)
+ ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness/promela_bugged1_liveness
+ ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged2-liveness/promela_bugged2_liveness PARENT_SCOPE)
set(txt_files ${txt_files} ${CMAKE_CURRENT_SOURCE_DIR}/dag-from-dax/simple_dax_with_cycle.xml
${CMAKE_CURRENT_SOURCE_DIR}/dag-from-dax/smalldax.xml
${CMAKE_CURRENT_SOURCE_DIR}/dag-from-dot/dag.dot
--- /dev/null
+/* Copyright (c) 2012-2021. 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. */
+
+/***************************** Bugged2 ****************************************/
+/* This example implements a centralized mutual exclusion algorithm. */
+/* One client stay always in critical section */
+/* LTL property checked : !(GFcs) */
+/******************************************************************************/
+
+#include <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(bugged2_liveness, "my log messages");
+
+class Message {
+public:
+ enum class Kind { GRANT, NOT_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 cs = 0;
+
+static void coordinator()
+{
+ int CS_used = 0; // initially the CS is idle
+ std::queue<simgrid::s4u::Mailbox*> requests;
+
+ simgrid::s4u::Mailbox* mbox = simgrid::s4u::Mailbox::by_name("coordinator");
+
+ while (true) {
+ auto m = mbox->get_unique<Message>();
+ if (m->kind == Message::Kind::REQUEST) {
+ if (CS_used) {
+ XBT_INFO("CS already used.");
+ m->return_mailbox->put(new Message(Message::Kind::NOT_GRANT, mbox), 1000);
+ } else { // can serve it immediately
+ XBT_INFO("CS idle. Grant immediately");
+ m->return_mailbox->put(new Message(Message::Kind::GRANT, mbox), 1000);
+ CS_used = 1;
+ }
+ } else { // that's a release. Check if someone was waiting for the lock
+ XBT_INFO("CS release. resource now idle");
+ CS_used = 0;
+ }
+ }
+}
+
+static void client(int id)
+{
+ aid_t my_pid = simgrid::s4u::this_actor::get_pid();
+
+ simgrid::s4u::Mailbox* my_mailbox = simgrid::s4u::Mailbox::by_name(std::to_string(id));
+
+ while (true) {
+ XBT_INFO("Client (%d) asks the request", id);
+ simgrid::s4u::Mailbox::by_name("coordinator")->put(new Message(Message::Kind::REQUEST, my_mailbox), 1000);
+
+ auto grant = my_mailbox->get_unique<Message>();
+
+ if (grant->kind == Message::Kind::GRANT) {
+ XBT_INFO("Client (%d) got the answer (grant). Sleep a bit and release it", id);
+ if (id == 1)
+ cs = 1;
+ } else {
+ XBT_INFO("Client (%d) got the answer (not grant). Try again", id);
+ }
+
+ simgrid::s4u::this_actor::sleep_for(my_pid);
+ }
+}
+
+int main(int argc, char* argv[])
+{
+ simgrid::s4u::Engine e(&argc, argv);
+
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
+
+ e.load_platform(argv[1]);
+
+ simgrid::s4u::Actor::create("coordinator", e.host_by_name("Tremblay"), coordinator);
+ simgrid::s4u::Actor::create("client", e.host_by_name("Fafard"), client, 1);
+ simgrid::s4u::Actor::create("client", e.host_by_name("Boivin"), client, 2);
+
+ e.run();
+
+ return 0;
+}
--- /dev/null
+#!/usr/bin/env tesh
+
+! expect return 2
+! timeout 20
+! output ignore
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged2-liveness ${platfdir:=.}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged2_liveness
-foreach (x centralized_mutex bugged2_liveness)
+foreach (x centralized_mutex)
if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG)
add_executable (${x} EXCLUDE_FROM_ALL ${x}.c)
target_link_libraries(${x} simgrid)
set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/deploy_${x}.xml)
endforeach()
-set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/bugged2-liveness.tesh
- ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.tesh 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_bugged2_liveness PARENT_SCOPE)
-
-#if(SIMGRID_HAVE_MC)
-# IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...)
-# ADD_TESH(mc-bugged2-liveness-ucontext --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}
-# --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
-# --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc
-# bugged2-liveness.tesh)
-# ENDIF()
-#ENDIF()
\ No newline at end of file
+++ /dev/null
-#!/usr/bin/env tesh
-
-! expect return 2
-! timeout 20
-! output ignore
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged2_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged2_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged2_liveness
+++ /dev/null
-/* Copyright (c) 2012-2021. 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. */
-
-/***************************** Bugged2 ****************************************/
-/* This example implements a centralized mutual exclusion algorithm. */
-/* One client stay always in critical section */
-/* LTL property checked : !(GFcs) */
-/******************************************************************************/
-
-#include <simgrid/modelchecker.h>
-#include <simgrid/msg.h>
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "my log messages");
-
-int cs = 0;
-
-static int coordinator(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[])
-{
- int CS_used = 0; // initially the CS is idle
-
- while (1) {
- msg_task_t task = NULL;
- MSG_task_receive(&task, "coordinator");
- const char *kind = MSG_task_get_name(task); //is it a request or a release?
- if (!strcmp(kind, "request")) { // that's a request
- const char* req = MSG_task_get_data(task);
- if (CS_used) {
- XBT_INFO("CS already used.");
- msg_task_t answer = MSG_task_create("not grant", 0, 1000, NULL);
- MSG_task_send(answer, req);
- } else { // can serve it immediately
- XBT_INFO("CS idle. Grant immediately");
- msg_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
- MSG_task_send(answer, req);
- CS_used = 1;
- }
- } else { // that's a release. Check if someone was waiting for the lock
- XBT_INFO("CS release. resource now idle");
- CS_used = 0;
- }
- MSG_task_destroy(task);
- kind = 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]);
-
- while(1){
- XBT_INFO("Client (%s) asks the request", my_mailbox);
- MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
-
- msg_task_t answer = NULL;
- MSG_task_receive(&answer, my_mailbox);
-
- const char* kind = MSG_task_get_name(answer);
-
- if (!strcmp(kind, "grant")) {
- XBT_INFO("Client (%s) got the answer (grant). Sleep a bit and release it", my_mailbox);
- if(!strcmp(my_mailbox, "1"))
- cs = 1;
- }else{
- XBT_INFO("Client (%s) got the answer (not grant). Try again", my_mailbox);
- }
-
- MSG_task_destroy(answer);
- kind = NULL;
-
- MSG_process_sleep(my_pid);
- }
- return 0;
-}
-
-int main(int argc, char *argv[])
-{
- MSG_init(&argc, argv);
-
- MC_automaton_new_propositional_symbol_pointer("cs", &cs);
-
- MSG_create_environment(argv[1]);
- MSG_function_register("coordinator", coordinator);
- MSG_function_register("client", client);
- MSG_launch_application(argv[2]);
- MSG_main();
-
- return 0;
-
-}
+++ /dev/null
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
-<platform version="4.1">
- <actor host="Tremblay" function="coordinator" />
- <actor host="Fafard" function="client" >
- <argument value="1"/>
- </actor>
- <actor host="Boivin" function="client" >
- <argument value="2"/>
- </actor>
-</platform>
