From: Martin Quinson Date: Fri, 3 Nov 2023 16:55:49 +0000 (+0100) Subject: Merge branch 'master' into simgrid-fork-changelog-plugins X-Git-Tag: v3.35~89^2~22 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/cc96213b38543567f85c88be37be5c50c1f9e6e9?hp=32e1a75e59e8437be5a940e1aee5c0408893f2b4 Merge branch 'master' into simgrid-fork-changelog-plugins --- diff --git a/.gitignore b/.gitignore index c4b7ab787b..97d5571cbb 100644 --- a/.gitignore +++ b/.gitignore @@ -104,6 +104,10 @@ tags callgrind.out.* ### Examples and traces *.exe +examples/c/activityset-testany/c-activityset-testany +examples/c/activityset-waitall/c-activityset-waitall +examples/c/activityset-waitallfor/c-activityset-waitallfor +examples/c/activityset-waitany/c-activityset-waitany examples/c/actor-create/c-actor-create examples/c/actor-daemon/c-actor-daemon examples/c/actor-exiting/c-actor-exiting @@ -143,6 +147,10 @@ examples/c/platform-failures/c-platform-failures examples/c/platform-properties/c-platform-properties examples/c/plugin-host-load/c-plugin-host-load examples/c/synchro-semaphore/c-synchro-semaphore +examples/cpp/activityset-testany/s4u-activityset-testany +examples/cpp/activityset-waitall/s4u-activityset-waitall +examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor +examples/cpp/activityset-waitany/s4u-activityset-waitany examples/cpp/actor-create/s4u-actor-create examples/cpp/actor-daemon/s4u-actor-daemon examples/cpp/actor-exiting/s4u-actor-exiting @@ -175,8 +183,11 @@ examples/cpp/comm-waitall/s4u-comm-waitall examples/cpp/comm-waitany/s4u-comm-waitany examples/cpp/comm-waituntil/s4u-comm-waituntil examples/cpp/dag-comm/s4u-dag-comm +examples/cpp/dag-tuto/s4u-dag-tuto examples/cpp/dag-failure/s4u-dag-failure examples/cpp/dag-from-dax/s4u-dag-from-dax +examples/cpp/dag-from-dax-simple/s4u-dag-from-dax-simple +examples/cpp/dag-from-json-simple/s4u-dag-from-json-simple examples/cpp/dag-from-dot/s4u-dag-from-dot examples/cpp/dag-io/s4u-dag-io examples/cpp/dag-scheduling/s4u-dag-scheduling @@ -239,6 +250,13 @@ examples/cpp/synchro-condition-variable/s4u-synchro-condition-variable examples/cpp/synchro-condition-variable-waituntil/s4u-synchro-condition-variable-waituntil examples/cpp/synchro-mutex/s4u-synchro-mutex examples/cpp/synchro-semaphore/s4u-synchro-semaphore +examples/cpp/task-dispatch/s4u-task-dispatch +examples/cpp/task-io/s4u-task-io +examples/cpp/task-microservice/s4u-task-microservice +examples/cpp/task-parallelism/s4u-task-parallelism +examples/cpp/task-simple/s4u-task-simple +examples/cpp/task-storm/s4u-task-storm +examples/cpp/task-switch-host/s4u-task-switch-host examples/cpp/torus-multicpu/ examples/cpp/trace-categories/s4u-trace-categories examples/cpp/trace-host-user-variables/s4u-trace-host-user-variables diff --git a/ChangeLog b/ChangeLog index c3e7d414e3..0da01dda5d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -6,12 +6,16 @@ S4U: - New function NetZone::add_route(host1, host2, links) when you don't need gateways Also add a variant with s4u::Link, when you don't want to specify the directions on symmetric routes. - - Introduce a Mailbox::get_async() with no payload parameter. You can use the new + - Introduce a Mailbox::get_async() with no payload parameter. You can use the new Comm::get_payload() once the communication is over to retrieve the payload. - Implement recursive mutexes. Simply pass true to the constructor to get one. - Update of the Task model. Each Task now consists of a dispatcher, a collector and one or more instances. The parallelism degree of each of these can be set. Several examples have been added or modified accordingly. + - Introduce a new MessageQueue abstraction and associated Mess simulated object. + The behavior of a MessageQueue is similar to that of a Mailbox, but intended for + control messages that do not incur any simulated cost. Information is automagically + transported over thin air between producer and consumer. See examples/cpp/mess-wait SMPI: - New SMPI_app_instance_join(): wait for the completion of a started MPI instance @@ -37,9 +41,17 @@ Plugins: The examples were updated accordingly. The battery can now act as a simple connector. See battery-connector example. - Revamp of the Photovoltaic plugin: now called SolarPanel and complete rewrite of the API + - Revamp of the Photovoltaic plugin: now called SolarPanel and complete rewrite of the API - Add chiller plugin: enable the management of chillers consuming electrical energy to compensate heat generated by hosts. +Kernel: + - optimize an internal data structure (replace boost::circular_buffer_space_optimized by + std::deque to store pending and unmatched Comms in Mailboxes). It is actually a revert + to what was used a few years back. The boost structure had a lower memory footprint than + deques, but it appeared that their "space_optimized" character was generating a huge lot + of refcount changes on the stored Comms. + ---------------------------------------------------------------------------- SimGrid (3.34) June 26. 2023 diff --git a/MANIFEST.in b/MANIFEST.in index 3f03f8bb5a..0eec0465f0 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -676,6 +676,22 @@ include teshsuite/mc/dwarf-expression/dwarf-expression.cpp include teshsuite/mc/dwarf-expression/dwarf-expression.tesh include teshsuite/mc/dwarf/dwarf.cpp include teshsuite/mc/dwarf/dwarf.tesh +include teshsuite/mc/mcmini/barber_shop_deadlock.c +include teshsuite/mc/mcmini/barber_shop_deadlock.tesh +include teshsuite/mc/mcmini/barber_shop_ok.c +include teshsuite/mc/mcmini/barber_shop_ok.tesh +include teshsuite/mc/mcmini/philosophers_mutex_deadlock.c +include teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh +include teshsuite/mc/mcmini/philosophers_mutex_ok.c +include teshsuite/mc/mcmini/philosophers_mutex_ok.tesh +include teshsuite/mc/mcmini/philosophers_semaphores_deadlock.c +include teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh +include teshsuite/mc/mcmini/philosophers_semaphores_ok.c +include teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh +include teshsuite/mc/mcmini/producer_consumer_deadlock.c +include teshsuite/mc/mcmini/producer_consumer_deadlock.tesh +include teshsuite/mc/mcmini/producer_consumer_ok.c +include teshsuite/mc/mcmini/producer_consumer_ok.tesh include teshsuite/mc/mutex-handling/mutex-handling.cpp include teshsuite/mc/mutex-handling/mutex-handling.tesh include teshsuite/mc/mutex-handling/without-mutex-handling.tesh @@ -2320,8 +2336,8 @@ include src/mc/sosp/Snapshot.hpp include src/mc/sosp/Snapshot_test.cpp include src/mc/transition/Transition.cpp include src/mc/transition/Transition.hpp -include src/mc/transition/TransitionActorJoin.cpp -include src/mc/transition/TransitionActorJoin.hpp +include src/mc/transition/TransitionActor.cpp +include src/mc/transition/TransitionActor.hpp include src/mc/transition/TransitionAny.cpp include src/mc/transition/TransitionAny.hpp include src/mc/transition/TransitionComm.cpp diff --git a/docs/source/Release_Notes.rst b/docs/source/Release_Notes.rst index bd5f6a7b59..346f563697 100644 --- a/docs/source/Release_Notes.rst +++ b/docs/source/Release_Notes.rst @@ -668,7 +668,13 @@ This feature is not very usable yet, as you have to manually annotate your code, Version 3.35 (TBD) ------------------ - +**On the interface front**, we introduced a new MessageQueue abstraction and associated Mess simulated object. The behavior of a +MessageQueue is similar to that of a Mailbox, but intended for control messages that do not incur any simulated cost. +Information is automagically transported over thin air between producer and consumer. Internally, the implementation is very +similar to Mailboxes and Comms, only simpler. The motivation for this new abstraction came from a scalability issue observed in +the WRENCH framework, which is heavily based on control messages. When the simulated size of these messages is set to 0, it creates +very short lived network actions (i.e., lasting for only the route latency) that tend to overwhelm the LMM. Switching from Mailbox +to MessageQueue for such information exchange avoid this problem and greatly improves the scalability of WRENCH-based simulators. .. |br| raw:: html diff --git a/examples/cpp/activityset-waitall/s4u-activityset-waitall.cpp b/examples/cpp/activityset-waitall/s4u-activityset-waitall.cpp index efbc3a08ab..2c9cf1ad8b 100644 --- a/examples/cpp/activityset-waitall/s4u-activityset-waitall.cpp +++ b/examples/cpp/activityset-waitall/s4u-activityset-waitall.cpp @@ -9,28 +9,30 @@ #include namespace sg4 = simgrid::s4u; -XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_activity_waittany, "Messages specific for this s4u example"); +XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_activity_waitall, "Messages specific for this s4u example"); static void bob() { sg4::Mailbox* mbox = sg4::Mailbox::by_name("mbox"); + sg4::MessageQueue* mqueue = sg4::MessageQueue::by_name("mqueue"); const sg4::Disk* disk = sg4::Host::current()->get_disks().front(); std::string* payload; + std::string* message; XBT_INFO("Create my asynchronous activities"); auto exec = sg4::this_actor::exec_async(5e9); auto comm = mbox->get_async(&payload); auto io = disk->read_async(3e8); + auto mess = mqueue->get_async(&message); - sg4::ActivitySet pending_activities({boost::dynamic_pointer_cast(exec), - boost::dynamic_pointer_cast(comm), - boost::dynamic_pointer_cast(io)}); + sg4::ActivitySet pending_activities({exec, comm, io, mess}); XBT_INFO("Wait for asynchronous activities to complete, all in one shot."); pending_activities.wait_all(); XBT_INFO("All activities are completed."); delete payload; + delete message; } static void alice() @@ -40,6 +42,12 @@ static void alice() sg4::Mailbox::by_name("mbox")->put(payload, 6e8); } +static void carl() +{ + auto* payload = new std::string("Control Message"); + sg4::MessageQueue::by_name("mqueue")->put(payload); +} + int main(int argc, char* argv[]) { sg4::Engine e(&argc, argv); @@ -48,6 +56,7 @@ int main(int argc, char* argv[]) sg4::Actor::create("bob", e.host_by_name("bob"), bob); sg4::Actor::create("alice", e.host_by_name("alice"), alice); + sg4::Actor::create("carl", e.host_by_name("carl"), carl); e.run(); diff --git a/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.cpp b/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.cpp index 971d77441c..a322cc4f1b 100644 --- a/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.cpp +++ b/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.cpp @@ -9,20 +9,23 @@ #include namespace sg4 = simgrid::s4u; -XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_activity_waittany, "Messages specific for this s4u example"); +XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_activity_waitallfor, "Messages specific for this s4u example"); static void bob() { sg4::Mailbox* mbox = sg4::Mailbox::by_name("mbox"); + sg4::MessageQueue* mqueue = sg4::MessageQueue::by_name("mqueue"); const sg4::Disk* disk = sg4::Host::current()->get_disks().front(); std::string* payload; + std::string* message; XBT_INFO("Create my asynchronous activities"); auto exec = sg4::this_actor::exec_async(5e9); auto comm = mbox->get_async(&payload); auto io = disk->read_async(3e8); + auto mess = mqueue->get_async(&message); - sg4::ActivitySet pending_activities({exec, comm, io}); + sg4::ActivitySet pending_activities({exec, comm, io, mess}); XBT_INFO("Wait for asynchronous activities to complete"); while (not pending_activities.empty()) { @@ -34,6 +37,8 @@ static void bob() while (auto completed_one = pending_activities.test_any()) { if (boost::dynamic_pointer_cast(completed_one)) XBT_INFO("Completed a Comm"); + if (boost::dynamic_pointer_cast(completed_one)) + XBT_INFO("Completed a Mess"); if (boost::dynamic_pointer_cast(completed_one)) XBT_INFO("Completed an Exec"); if (boost::dynamic_pointer_cast(completed_one)) @@ -42,6 +47,7 @@ static void bob() } XBT_INFO("Last activity is complete"); delete payload; + delete message; } static void alice() @@ -51,6 +57,14 @@ static void alice() sg4::Mailbox::by_name("mbox")->put(payload, 6e8); } +static void carl() +{ + sg4::this_actor::sleep_for(1.99); + auto* payload = new std::string("Control Message"); + XBT_INFO("Send '%s'", payload->c_str()); + sg4::MessageQueue::by_name("mqueue")->put(payload); +} + int main(int argc, char* argv[]) { sg4::Engine e(&argc, argv); @@ -59,6 +73,7 @@ int main(int argc, char* argv[]) sg4::Actor::create("bob", e.host_by_name("bob"), bob); sg4::Actor::create("alice", e.host_by_name("alice"), alice); + sg4::Actor::create("carl", e.host_by_name("carl"), carl); e.run(); diff --git a/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.tesh b/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.tesh index 014c4f028e..ce8db4ac50 100644 --- a/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.tesh +++ b/examples/cpp/activityset-waitallfor/s4u-activityset-waitallfor.tesh @@ -5,7 +5,9 @@ $ ${bindir:=.}/s4u-activityset-waitallfor ${platfdir}/hosts_with_disks.xml "--lo > [0.000000] [ bob] Create my asynchronous activities > [0.000000] [ bob] Wait for asynchronous activities to complete > [1.000000] [ bob] Not all activities are terminated yet. +> [1.990000] [ carl] Send 'Control Message' > [2.000000] [ bob] Not all activities are terminated yet. +> [2.000000] [ bob] Completed a Mess > [3.000000] [ bob] Not all activities are terminated yet. > [3.000000] [ bob] Completed an I/O > [4.000000] [ bob] Not all activities are terminated yet. diff --git a/examples/cpp/activityset-waitany/s4u-activityset-waitany.cpp b/examples/cpp/activityset-waitany/s4u-activityset-waitany.cpp index 6f081b3ca6..6c8baef61e 100644 --- a/examples/cpp/activityset-waitany/s4u-activityset-waitany.cpp +++ b/examples/cpp/activityset-waitany/s4u-activityset-waitany.cpp @@ -9,22 +9,23 @@ #include namespace sg4 = simgrid::s4u; -XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_activity_waittany, "Messages specific for this s4u example"); +XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_activity_waitany, "Messages specific for this s4u example"); static void bob() { sg4::Mailbox* mbox = sg4::Mailbox::by_name("mbox"); + sg4::MessageQueue* mqueue = sg4::MessageQueue::by_name("mqueue"); const sg4::Disk* disk = sg4::Host::current()->get_disks().front(); std::string* payload; + std::string* message; XBT_INFO("Create my asynchronous activities"); auto exec = sg4::this_actor::exec_async(5e9); auto comm = mbox->get_async(&payload); auto io = disk->read_async(3e8); + auto mess = mqueue->get_async(&message); - sg4::ActivitySet pending_activities({boost::dynamic_pointer_cast(exec), - boost::dynamic_pointer_cast(comm), - boost::dynamic_pointer_cast(io)}); + sg4::ActivitySet pending_activities({exec, comm, io, mess}); XBT_INFO("Wait for asynchronous activities to complete"); while (not pending_activities.empty()) { @@ -32,6 +33,8 @@ static void bob() if (completed_one != nullptr) { if (boost::dynamic_pointer_cast(completed_one)) XBT_INFO("Completed a Comm"); + if (boost::dynamic_pointer_cast(completed_one)) + XBT_INFO("Completed a Mess"); if (boost::dynamic_pointer_cast(completed_one)) XBT_INFO("Completed an Exec"); if (boost::dynamic_pointer_cast(completed_one)) @@ -40,6 +43,7 @@ static void bob() } XBT_INFO("Last activity is complete"); delete payload; + delete message; } static void alice() @@ -49,6 +53,14 @@ static void alice() sg4::Mailbox::by_name("mbox")->put(payload, 6e8); } +static void carl() +{ + sg4::this_actor::sleep_for(2); + auto* payload = new std::string("Control Message"); + XBT_INFO("Send '%s'", payload->c_str()); + sg4::MessageQueue::by_name("mqueue")->put(payload); +} + int main(int argc, char* argv[]) { sg4::Engine e(&argc, argv); @@ -57,6 +69,7 @@ int main(int argc, char* argv[]) sg4::Actor::create("bob", e.host_by_name("bob"), bob); sg4::Actor::create("alice", e.host_by_name("alice"), alice); + sg4::Actor::create("carl", e.host_by_name("carl"), carl); e.run(); diff --git a/examples/cpp/activityset-waitany/s4u-activityset-waitany.tesh b/examples/cpp/activityset-waitany/s4u-activityset-waitany.tesh index b9ecf1eafa..e665de5b6c 100644 --- a/examples/cpp/activityset-waitany/s4u-activityset-waitany.tesh +++ b/examples/cpp/activityset-waitany/s4u-activityset-waitany.tesh @@ -4,6 +4,8 @@ $ ${bindir:=.}/s4u-activityset-waitany ${platfdir}/hosts_with_disks.xml "--log=r > [0.000000] [alice] Send 'Message' > [0.000000] [ bob] Create my asynchronous activities > [0.000000] [ bob] Wait for asynchronous activities to complete +> [2.000000] [ carl] Send 'Control Message' +> [2.000000] [ bob] Completed a Mess > [3.000000] [ bob] Completed an I/O > [5.000000] [ bob] Completed an Exec > [5.197828] [ bob] Completed a Comm diff --git a/examples/cpp/battery-degradation/s4u-battery-degradation.cpp b/examples/cpp/battery-degradation/s4u-battery-degradation.cpp index 13b149ef46..4973587089 100644 --- a/examples/cpp/battery-degradation/s4u-battery-degradation.cpp +++ b/examples/cpp/battery-degradation/s4u-battery-degradation.cpp @@ -10,14 +10,17 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(battery_degradation, "Messages specific for this s4u example"); -static void manager() +int main(int argc, char* argv[]) { + simgrid::s4u::Engine e(&argc, argv); + e.load_platform(argv[1]); + auto battery = simgrid::plugins::Battery::init("Battery", 0.8, -200, 200, 0.9, 0.9, 10, 100); battery->set_load("load", 100.0); auto handler1 = battery->schedule_handler( - 0.2, simgrid::plugins::Battery::DISCHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, [battery]() { + 0.2, simgrid::plugins::Battery::DISCHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, [&battery]() { XBT_INFO("%f,%f,SoC", simgrid::s4u::Engine::get_clock(), battery->get_state_of_charge()); XBT_INFO("%f,%f,SoH", simgrid::s4u::Engine::get_clock(), battery->get_state_of_health()); battery->set_load("load", -100.0); @@ -26,7 +29,7 @@ static void manager() std::shared_ptr handler2; handler2 = battery->schedule_handler( 0.8, simgrid::plugins::Battery::CHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, - [battery, handler1, handler2]() { + [&battery, &handler1, &handler2]() { XBT_INFO("%f,%f,SoC", simgrid::s4u::Engine::get_clock(), battery->get_state_of_charge()); XBT_INFO("%f,%f,SoH", simgrid::s4u::Engine::get_clock(), battery->get_state_of_health()); if (battery->get_state_of_health() < 0.1) { @@ -35,14 +38,6 @@ static void manager() } battery->set_load("load", 100.0); }); -} - -int main(int argc, char* argv[]) -{ - simgrid::s4u::Engine e(&argc, argv); - e.load_platform(argv[1]); - - simgrid::s4u::Actor::create("manager", e.host_by_name("MyHost1"), manager); e.run(); return 0; diff --git a/examples/cpp/battery-energy/s4u-battery-energy.cpp b/examples/cpp/battery-energy/s4u-battery-energy.cpp index c50ef02cae..6db88125a4 100644 --- a/examples/cpp/battery-energy/s4u-battery-energy.cpp +++ b/examples/cpp/battery-energy/s4u-battery-energy.cpp @@ -21,7 +21,7 @@ static void manager() battery->schedule_handler( 0.2, simgrid::plugins::Battery::DISCHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, - [battery, &host1, &host2, &host3]() { + [&battery, &host1, &host2, &host3]() { XBT_INFO("Handler -> Battery low: SoC: %f SoH: %f Energy stored: %fJ Energy provided: %fJ Energy consumed %fJ", battery->get_state_of_charge(), battery->get_state_of_health(), battery->get_energy_stored(), battery->get_energy_provided(), battery->get_energy_consumed()); diff --git a/examples/cpp/battery-simple/s4u-battery-simple.cpp b/examples/cpp/battery-simple/s4u-battery-simple.cpp index 04eb4f6d13..61a4186239 100644 --- a/examples/cpp/battery-simple/s4u-battery-simple.cpp +++ b/examples/cpp/battery-simple/s4u-battery-simple.cpp @@ -28,7 +28,7 @@ int main(int argc, char* argv[]) XBT_INFO("Set load to %fW", load_w); battery->schedule_handler( - 0.2, simgrid::plugins::Battery::DISCHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, [battery, &load_w]() { + 0.2, simgrid::plugins::Battery::DISCHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, [&battery, &load_w]() { XBT_INFO("Discharged state: SoC: %f SoH: %f Energy stored: %fJ Energy provided: %fJ Energy consumed %fJ", battery->get_state_of_charge(), battery->get_state_of_health(), battery->get_energy_stored(), battery->get_energy_provided(), battery->get_energy_consumed()); @@ -37,7 +37,7 @@ int main(int argc, char* argv[]) }); battery->schedule_handler( - 0.8, simgrid::plugins::Battery::CHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, [battery]() { + 0.8, simgrid::plugins::Battery::CHARGE, simgrid::plugins::Battery::Handler::PERSISTANT, [&battery]() { XBT_INFO("Charged state: SoC: %f SoH: %f Energy stored: %fJ Energy provided: %fJ Energy consumed %fJ", battery->get_state_of_charge(), battery->get_state_of_health(), battery->get_energy_stored(), battery->get_energy_provided(), battery->get_energy_consumed()); @@ -45,5 +45,6 @@ int main(int argc, char* argv[]) }); e.run(); + return 0; } \ No newline at end of file diff --git a/examples/cpp/io-dependent/s4u-io-dependent.cpp b/examples/cpp/io-dependent/s4u-io-dependent.cpp index 4772376fa3..f64c4c2e46 100644 --- a/examples/cpp/io-dependent/s4u-io-dependent.cpp +++ b/examples/cpp/io-dependent/s4u-io-dependent.cpp @@ -17,10 +17,7 @@ static void test() sg4::IoPtr carl_read = sg4::Host::by_name("carl")->get_disks().front()->io_init(4000000, sg4::Io::OpType::READ); sg4::ExecPtr carl_compute = sg4::Host::by_name("carl")->exec_init(1e9); - sg4::ActivitySet pending_activities ({boost::dynamic_pointer_cast(bob_compute), - boost::dynamic_pointer_cast(bob_write), - boost::dynamic_pointer_cast(carl_read), - boost::dynamic_pointer_cast(carl_compute)}); + sg4::ActivitySet pending_activities ({bob_compute, bob_write, carl_read, carl_compute}); // Name the activities (for logging purposes only) bob_compute->set_name("bob compute"); diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh index b17f900737..9ed6eb7f45 100644 --- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh +++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh @@ -18,21 +18,21 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] Sleep set actually containing: > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] Sleep set actually containing: > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) -> [Checker] BARRIER_WAIT(barrier: 0) (state=3) +> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=3) > [Checker] Sleep set actually containing: > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_WAIT(barrier: 0) (state=3) -> [Checker] BARRIER_WAIT(barrier: 0) (state=4) +> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=3) +> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=4) > [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_WAIT(barrier: 0) (state=4) +> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=4) > [Checker] 0 actors remain, but none of them need to be interleaved (depth 6). > [Checker] Execution came to an end at 1;2;1;2 (state: 5, depth: 5) > [Checker] Backtracking from 1;2;1;2 @@ -50,40 +50,40 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] Sleep set actually containing: > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] Sleep set actually containing: > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3) > [Checker] Sleep set actually containing: > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) -> [Checker] BARRIER_WAIT(barrier: 0) (state=4) +> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=4) > [Checker] Sleep set actually containing: > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_WAIT(barrier: 0) (state=4) -> [Checker] BARRIER_WAIT(barrier: 0) (state=5) +> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=4) +> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=5) > [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) -> [Checker] BARRIER_WAIT(barrier: 0) (state=5) +> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3) +> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=5) > [Checker] Sleep set actually containing: > [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_WAIT(barrier: 0) (state=5) -> [Checker] BARRIER_WAIT(barrier: 0) (state=6) +> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=5) +> [Checker] #3 BARRIER_WAIT(barrier: 0) (state=6) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_WAIT(barrier: 0) (state=4) -> [Checker] BARRIER_WAIT(barrier: 0) (state=6) +> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=4) +> [Checker] #3 BARRIER_WAIT(barrier: 0) (state=6) > [Checker] Dependent Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) -> [Checker] BARRIER_WAIT(barrier: 0) (state=6) +> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] #3 BARRIER_WAIT(barrier: 0) (state=6) > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8). > [Checker] Execution came to an end at 1;2;3;1;2;3 (state: 7, depth: 7) > [Checker] Backtracking from 1;2;3;1;2;3 @@ -91,8 +91,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] <2,BARRIER_ASYNC_LOCK(barrier: 0)> > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] 3 actors remain, but none of them need to be interleaved (depth 4). > [Checker] Backtracking from 1;3 > [Checker] DFS exploration ended. 8 unique states visited; 1 backtracks (1 transition replays, 10 states visited overall) \ No newline at end of file diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh index f7f1a551d8..5f726fec70 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -14,24 +14,24 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] Sleep set actually containing: > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) +> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) +> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=2) -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) +> [Checker] #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=2) +> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) > [Checker] Dependent Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1) -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) +> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1) +> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4) > [Checker] Sleep set actually containing: > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) -> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=5) +> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) +> [Checker] #2 MUTEX_WAIT(mutex: 0, owner: 2) (state=5) > [Checker] Sleep set actually containing: > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6) +> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3) +> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6) > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8). > [Checker] Execution came to an end at 1;1;1;2;2;2 (state: 7, depth: 7) > [Checker] Backtracking from 1;1;1;2;2;2 @@ -39,11 +39,11 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] <1,MUTEX_UNLOCK(mutex: 0, owner: -1)> > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=2) -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) +> [Checker] #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=2) +> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) > [Checker] Dependent Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1) -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) +> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1) +> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3) > [Checker] 2 actors remain, but none of them need to be interleaved (depth 5). > [Checker] Backtracking from 1;1;2 > [Checker] Sleep set actually containing: @@ -52,28 +52,28 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs. > [Checker] Sleep set actually containing: > [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 9, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1) -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9) +> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1) +> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9) > [Checker] Sleep set actually containing: > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 10, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9) -> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=10) +> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9) +> [Checker] #2 MUTEX_WAIT(mutex: 0, owner: 2) (state=10) > [Checker] Sleep set actually containing: > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 11, 0 interleaves) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11) +> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9) +> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11) > [Checker] Sleep set actually containing: > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 12, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11) -> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=12) +> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11) +> [Checker] #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=12) > [Checker] Sleep set actually containing: > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 13, 0 interleaves) > [Checker] Dependent Transitions: -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11) -> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=13) +> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11) +> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=13) > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8). > [Checker] Execution came to an end at 2;1;2;2;1;1 (state: 14, depth: 7) > [Checker] Backtracking from 2;1;2;2;1;1 diff --git a/examples/cpp/task-storm/s4u-task-storm.cpp b/examples/cpp/task-storm/s4u-task-storm.cpp index 0a0ab7143b..ca0f61ea5c 100644 --- a/examples/cpp/task-storm/s4u-task-storm.cpp +++ b/examples/cpp/task-storm/s4u-task-storm.cpp @@ -111,11 +111,13 @@ int main(int argc, char* argv[]) auto data = t->get_token_from(SA_to_B1)->get_data(); t->deque_token_from(SA_to_B1); t->set_amount(*data * 10); + delete data; }); B2->on_this_start_cb([&SA_to_B2](sg4::Task* t) { auto data = t->get_token_from(SA_to_B2)->get_data(); t->deque_token_from(SA_to_B2); t->set_amount(*data * 10); + delete data; }); // Enqueue firings for tasks without predecessors diff --git a/examples/sthread/pthread-mc-mutex-recursive.tesh b/examples/sthread/pthread-mc-mutex-recursive.tesh index 984a4b56d1..892ecc3de6 100644 --- a/examples/sthread/pthread-mc-mutex-recursive.tesh +++ b/examples/sthread/pthread-mc-mutex-recursive.tesh @@ -2,7 +2,6 @@ ! ignore .*LD_PRELOAD.* $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-mutex-recursive -> sthread is intercepting the execution of ./pthread-mutex-recursive > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. > Got the lock on the default mutex. > Failed to relock the default mutex. diff --git a/examples/sthread/pthread-mc-mutex-simple.tesh b/examples/sthread/pthread-mc-mutex-simple.tesh index 9e38ceadf3..d9b8daf514 100644 --- a/examples/sthread/pthread-mc-mutex-simple.tesh +++ b/examples/sthread/pthread-mc-mutex-simple.tesh @@ -3,7 +3,6 @@ ! ignore .*LD_PRELOAD.* $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-mutex-simple -> sthread is intercepting the execution of ./pthread-mutex-simple > All threads are started. > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. > The thread 0 is terminating. @@ -12,4 +11,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec > The thread 1 is terminating. > The thread 0 is terminating. > User's main is terminating. -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 18 unique states visited; 2 backtracks (2 transition replays, 22 states visited overall) \ No newline at end of file +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 18 unique states visited; 2 backtracks (2 transition replays, 22 states visited overall) diff --git a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh index e843a409b9..1f6e97dade 100644 --- a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh +++ b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh @@ -6,7 +6,6 @@ ! ignore .*LD_PRELOAD.* $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-mutex-simpledeadlock -> sthread is intercepting the execution of ./pthread-mutex-simpledeadlock > All threads are started. > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. > The thread 0 is terminating. diff --git a/examples/sthread/pthread-mc-producer-consumer.tesh b/examples/sthread/pthread-mc-producer-consumer.tesh index 584b7a5857..29f2c47fae 100644 --- a/examples/sthread/pthread-mc-producer-consumer.tesh +++ b/examples/sthread/pthread-mc-producer-consumer.tesh @@ -2,18 +2,15 @@ ! ignore .*LD_PRELOAD.* $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -C 1 -P 1 -> sthread is intercepting the execution of ./pthread-producer-consumer > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. > [0.000000] [mc_dfs/INFO] DFS exploration ended. 786 unique states visited; 97 backtracks (2049 transition replays, 2932 states visited overall) $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:sdpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -C 1 -P 1 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'sdpor' -> sthread is intercepting the execution of ./pthread-producer-consumer > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: sdpor. > [0.000000] [mc_dfs/INFO] DFS exploration ended. 1186 unique states visited; 157 backtracks (3403 transition replays, 4746 states visited overall) $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -C 1 -P 1 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' -> sthread is intercepting the execution of ./pthread-producer-consumer > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. > [0.000000] [mc_dfs/INFO] DFS exploration ended. 39 unique states visited; 0 backtracks (0 transition replays, 39 states visited overall) diff --git a/examples/sthread/pthread-mutex-recursive.tesh b/examples/sthread/pthread-mutex-recursive.tesh index ca535da834..0879b2c14e 100644 --- a/examples/sthread/pthread-mutex-recursive.tesh +++ b/examples/sthread/pthread-mutex-recursive.tesh @@ -1,5 +1,4 @@ $ env ASAN_OPTIONS=verify_asan_link_order=0:$ASAN_OPTIONS LD_PRELOAD=${libdir:=.}/libsthread.so ./pthread-mutex-recursive -> sthread is intercepting the execution of ./pthread-mutex-recursive > Got the lock on the default mutex. > Failed to relock the default mutex. > Got the lock on the recursive mutex. diff --git a/examples/sthread/pthread-mutex-simple.tesh b/examples/sthread/pthread-mutex-simple.tesh index 2e12ec1204..f4b3f3cd6b 100644 --- a/examples/sthread/pthread-mutex-simple.tesh +++ b/examples/sthread/pthread-mutex-simple.tesh @@ -1,5 +1,4 @@ $ env ASAN_OPTIONS=verify_asan_link_order=0:$ASAN_OPTIONS LD_PRELOAD=${libdir:=.}/libsthread.so ./pthread-mutex-simple -> sthread is intercepting the execution of ./pthread-mutex-simple > All threads are started. > The thread 0 is terminating. > The thread 1 is terminating. diff --git a/examples/sthread/pthread-producer-consumer.tesh b/examples/sthread/pthread-producer-consumer.tesh index d8bf22cf52..471fbe8102 100644 --- a/examples/sthread/pthread-producer-consumer.tesh +++ b/examples/sthread/pthread-producer-consumer.tesh @@ -1,5 +1,4 @@ $ env ASAN_OPTIONS=verify_asan_link_order=0:$ASAN_OPTIONS LD_PRELOAD=${libdir:=.}/libsthread.so ./pthread-producer-consumer -> sthread is intercepting the execution of ./pthread-producer-consumer > Producer 1: Insert Item 0 at 0 > Producer 2: Insert Item 0 at 1 > Consumer 1: Remove Item 0 from 0 @@ -15,7 +14,6 @@ $ env ASAN_OPTIONS=verify_asan_link_order=0:$ASAN_OPTIONS LD_PRELOAD=${libdir:=. > [0.000000] [sthread/INFO] All threads exited. Terminating the simulation. $ env ASAN_OPTIONS=verify_asan_link_order=0:$ASAN_OPTIONS LD_PRELOAD=${libdir:=.}/libsthread.so ./pthread-producer-consumer -c 2 -C 1 -p 2 -P 1 -> sthread is intercepting the execution of ./pthread-producer-consumer > Producer 1: Insert Item 0 at 0 > Consumer 1: Remove Item 0 from 0 > Producer 1: Insert Item 1 at 1 diff --git a/examples/sthread/stdobject/stdobject.tesh b/examples/sthread/stdobject/stdobject.tesh index bb8e1b7beb..602c3f4589 100644 --- a/examples/sthread/stdobject/stdobject.tesh +++ b/examples/sthread/stdobject/stdobject.tesh @@ -5,7 +5,6 @@ ! ignore .*LD_PRELOAD.* $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/stdobject "--log=root.fmt:[%11.6r]%e(%a@%h)%e%m%n" --log=no_loc -> sthread is intercepting the execution of ./stdobject > starting two helpers... > waiting for helpers to finish... > [ 0.000000] (maestro@) Start a DFS exploration. Reduction is: dpor. diff --git a/examples/sthread/sthread-mutex-simple.tesh b/examples/sthread/sthread-mutex-simple.tesh index c44bd9794c..67afd1a12b 100644 --- a/examples/sthread/sthread-mutex-simple.tesh +++ b/examples/sthread/sthread-mutex-simple.tesh @@ -1,5 +1,4 @@ $ ./sthread-mutex-simple -> sthread is intercepting the execution of ./sthread-mutex-simple > All threads are started. > The thread 0 is terminating. > The thread 1 is terminating. diff --git a/include/simgrid/plugins/solar_panel.hpp b/include/simgrid/plugins/solar_panel.hpp index 5fa424bd36..0ba319c059 100644 --- a/include/simgrid/plugins/solar_panel.hpp +++ b/include/simgrid/plugins/solar_panel.hpp @@ -42,7 +42,7 @@ class SolarPanel { friend void intrusive_ptr_add_ref(SolarPanel* o) { o->refcount_.fetch_add(1, std::memory_order_relaxed); } #endif - inline static xbt::signal on_power_change; + static xbt::signal on_power_change; xbt::signal on_this_power_change; public: diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index 2d2cf8827e..3bd6ab97f1 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -73,6 +73,15 @@ std::string ActorJoinSimcall::to_string() const { return "ActorJoin(pid:" + std::to_string(other_->get_pid()) + ")"; } +void ActorSleepSimcall::serialize(std::stringstream& stream) const +{ + stream << (short)mc::Transition::Type::ACTOR_SLEEP; +} + +std::string ActorSleepSimcall::to_string() const +{ + return "ActorSleep()"; +} void ObjectAccessSimcallObserver::serialize(std::stringstream& stream) const { diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp index 4cb7f22c3c..d43ac00ead 100644 --- a/src/kernel/actor/SimcallObserver.hpp +++ b/src/kernel/actor/SimcallObserver.hpp @@ -127,6 +127,14 @@ public: double get_timeout() const { return timeout_; } }; +class ActorSleepSimcall final : public SimcallObserver { + +public: + ActorSleepSimcall(ActorImpl* actor) : SimcallObserver(actor) {} + void serialize(std::stringstream& stream) const override; + std::string to_string() const override; +}; + class ObjectAccessSimcallObserver final : public SimcallObserver { ObjectAccessSimcallItem* const object_; diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index 49622dd275..a1217a6752 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -158,7 +158,8 @@ void RemoteApp::get_actors_status(std::map& whereto) const actor_transitions.emplace_back(deserialize_transition(actor.aid, times_considered, stream)); } - XBT_DEBUG("Received %zu transitions for actor %ld", actor_transitions.size(), actor.aid); + XBT_DEBUG("Received %zu transitions for actor %ld. The first one is %s", actor_transitions.size(), actor.aid, + (actor_transitions.size() > 0 ? actor_transitions[0]->to_string().c_str() : "null")); whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered, std::move(actor_transitions)); } } diff --git a/src/mc/api/strategy/BasicStrategy.hpp b/src/mc/api/strategy/BasicStrategy.hpp index fd28633977..de0fe65d9b 100644 --- a/src/mc/api/strategy/BasicStrategy.hpp +++ b/src/mc/api/strategy/BasicStrategy.hpp @@ -7,13 +7,17 @@ #define SIMGRID_MC_BASICSTRATEGY_HPP #include "Strategy.hpp" +#include "src/mc/explo/Exploration.hpp" + +XBT_LOG_EXTERNAL_CATEGORY(mc_dfs); namespace simgrid::mc { /** Basic MC guiding class which corresponds to no guide. When asked for different states * it will follow a depth first search politics to minize the number of opened states. */ class BasicStrategy : public Strategy { - int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer + int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positive value to work with + // threshold in DFSExplorer public: void copy_from(const Strategy* strategy) override @@ -21,7 +25,16 @@ public: const auto* cast_strategy = dynamic_cast(strategy); xbt_assert(cast_strategy != nullptr); depth_ = cast_strategy->depth_ - 1; - xbt_assert(depth_ > 0, "The exploration reached a depth greater than %d. We will stop here to prevent weird interaction with DFSExplorer. If you want to change that behaviour, you should augment the size of the search by using --cfg=model-check/max-depth:", _sg_mc_max_depth.get()); + if (depth_ <= 0) { + XBT_CERROR(mc_dfs, + "The exploration reached a depth greater than %d. Change the depth limit with " + "--cfg=model-check/max-depth. Here are the 100 first trace elements", + _sg_mc_max_depth.get()); + auto trace = Exploration::get_instance()->get_textual_trace(100); + for (auto elm : trace) + XBT_CERROR(mc_dfs, " %s", elm.c_str()); + xbt_die("Aborting now."); + } } BasicStrategy() = default; ~BasicStrategy() override = default; diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 451920da63..8af62121d3 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -253,8 +253,10 @@ void DFSExplorer::run() continue; } else if (prev_state->get_transition_out()->depends(state->get_transition_out().get())) { XBT_VERB("Dependent Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); - XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_, + prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_, + state->get_transition_out()->to_string().c_str(), state->get_num()); if (prev_state->is_actor_enabled(issuer_id)) { if (not prev_state->is_actor_done(issuer_id)) { @@ -273,8 +275,10 @@ void DFSExplorer::run() break; } else { XBT_VERB("INDEPENDENT Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); - XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_, + prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_, + state->get_transition_out()->to_string().c_str(), state->get_num()); } tmp_stack.pop_back(); } diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 3c8e6507bf..d219abd0d0 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -83,7 +83,7 @@ static const char* signal_name(int status) } } -std::vector Exploration::get_textual_trace() +std::vector Exploration::get_textual_trace(int max_elements) { std::vector trace; for (auto const& transition : get_record_trace()) { @@ -93,6 +93,9 @@ std::vector Exploration::get_textual_trace() transition->to_string().c_str())); else trace.push_back(xbt::string_printf("Actor %ld in simcall %s", transition->aid_, transition->to_string().c_str())); + max_elements--; + if (max_elements == 0) + break; } return trace; } diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index 64114d4bf2..571ed19e54 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -60,7 +60,7 @@ public: virtual RecordTrace get_record_trace() = 0; /** Generate a textual execution trace of the simulated application */ - std::vector get_textual_trace(); + std::vector get_textual_trace(int max_elements = -1); /** Log additional information about the state of the model-checker */ virtual void log_state(); diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp index 283b7c9dcc..88c6839bb0 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp @@ -9,7 +9,7 @@ #include "src/mc/explo/odpor/Execution.hpp" #include "src/mc/explo/odpor/odpor_forward.hpp" #include "src/mc/transition/Transition.hpp" -#include "src/mc/transition/TransitionActorJoin.hpp" +#include "src/mc/transition/TransitionActor.hpp" #include "src/mc/transition/TransitionAny.hpp" #include "src/mc/transition/TransitionComm.hpp" #include "src/mc/transition/TransitionObjectAccess.hpp" diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.hpp b/src/mc/explo/udpor/ExtensionSetCalculator.hpp index 60a4ac375b..cd68c9c7ff 100644 --- a/src/mc/explo/udpor/ExtensionSetCalculator.hpp +++ b/src/mc/explo/udpor/ExtensionSetCalculator.hpp @@ -9,7 +9,7 @@ #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" #include "src/mc/transition/Transition.hpp" -#include "src/mc/transition/TransitionActorJoin.hpp" +#include "src/mc/transition/TransitionActor.hpp" #include "src/mc/transition/TransitionAny.hpp" #include "src/mc/transition/TransitionComm.hpp" #include "src/mc/transition/TransitionObjectAccess.hpp" diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 5d00307aa9..a74b1260d9 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -225,6 +225,9 @@ void AppSide::handle_actors_status() const std::vector status; for (auto const& [aid, actor] : actor_list) { + xbt_assert(actor); + xbt_assert(actor->simcall_.observer_, "simcall %s in actor %s has no observer.", actor->simcall_.get_cname(), + actor->get_cname()); s_mc_message_actors_status_one_t one = {}; one.type = MessageType::ACTORS_STATUS_REPLY_TRANSITION; one.aid = aid; diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp index 84ad991fd5..fc3a5e2309 100644 --- a/src/mc/transition/Transition.cpp +++ b/src/mc/transition/Transition.cpp @@ -11,7 +11,7 @@ #if SIMGRID_HAVE_MC #include "src/mc/explo/Exploration.hpp" -#include "src/mc/transition/TransitionActorJoin.hpp" +#include "src/mc/transition/TransitionActor.hpp" #include "src/mc/transition/TransitionAny.hpp" #include "src/mc/transition/TransitionComm.hpp" #include "src/mc/transition/TransitionObjectAccess.hpp" @@ -95,6 +95,8 @@ Transition* deserialize_transition(aid_t issuer, int times_considered, std::stri case Transition::Type::ACTOR_JOIN: return new ActorJoinTransition(issuer, times_considered, stream); + case Transition::Type::ACTOR_SLEEP: + return new ActorSleepTransition(issuer, times_considered, stream); case Transition::Type::OBJECT_ACCESS: return new ObjectAccessTransition(issuer, times_considered, stream); diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp index 4bdf7d262b..9a840246c4 100644 --- a/src/mc/transition/Transition.hpp +++ b/src/mc/transition/Transition.hpp @@ -31,14 +31,23 @@ class Transition { public: /* Ordering is important here. depends() implementations only consider subsequent types in this ordering */ - XBT_DECLARE_ENUM_CLASS(Type, RANDOM, ACTOR_JOIN, /* First because indep with anybody including themselves */ - OBJECT_ACCESS, /* high priority because indep with almost everybody */ - TESTANY, WAITANY, /* high priority because they can rewrite themselves to *_WAIT */ - BARRIER_ASYNC_LOCK, BARRIER_WAIT, /* BARRIER transitions sorted alphabetically */ - COMM_ASYNC_RECV, COMM_ASYNC_SEND, COMM_TEST, COMM_WAIT, /* Alphabetical ordering of COMM_* */ - MUTEX_ASYNC_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, /* alphabetical */ - SEM_ASYNC_LOCK, SEM_UNLOCK, SEM_WAIT, /* alphabetical ordering of SEM transitions */ - /* UNKNOWN must be last */ UNKNOWN); + XBT_DECLARE_ENUM_CLASS(Type, + /* First because indep with anybody including themselves */ + RANDOM, ACTOR_JOIN, ACTOR_SLEEP, + /* high priority because indep with almost everybody */ + OBJECT_ACCESS, + /* high priority because they can rewrite themselves to *_WAIT */ + TESTANY, WAITANY, + /* BARRIER transitions sorted alphabetically */ + BARRIER_ASYNC_LOCK, BARRIER_WAIT, + /* Alphabetical ordering of COMM_* */ + COMM_ASYNC_RECV, COMM_ASYNC_SEND, COMM_TEST, COMM_WAIT, + /* alphabetical */ + MUTEX_ASYNC_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, + /* alphabetical ordering of SEM transitions */ + SEM_ASYNC_LOCK, SEM_UNLOCK, SEM_WAIT, + /* UNKNOWN must be last */ + UNKNOWN); Type type_ = Type::UNKNOWN; aid_t aid_ = 0; diff --git a/src/mc/transition/TransitionActorJoin.cpp b/src/mc/transition/TransitionActor.cpp similarity index 68% rename from src/mc/transition/TransitionActorJoin.cpp rename to src/mc/transition/TransitionActor.cpp index 463bfcbc6a..70608f14da 100644 --- a/src/mc/transition/TransitionActorJoin.cpp +++ b/src/mc/transition/TransitionActor.cpp @@ -3,7 +3,7 @@ /* 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. */ -#include "src/mc/transition/TransitionActorJoin.hpp" +#include "src/mc/transition/TransitionActor.hpp" #include "simgrid/config.h" #include "xbt/asserts.h" #include "xbt/string.hpp" @@ -27,6 +27,10 @@ std::string ActorJoinTransition::to_string(bool verbose) const } bool ActorJoinTransition::depends(const Transition* other) const { + // Actions executed by the same actor are always dependent + if (other->aid_ == aid_) + return true; + // Joining is dependent with any transition whose // actor is that of the `other` action. , Join i if (other->aid_ == target_) { @@ -43,4 +47,23 @@ bool ActorJoinTransition::depends(const Transition* other) const return false; } +ActorSleepTransition::ActorSleepTransition(aid_t issuer, int times_considered, std::stringstream& stream) + : Transition(Type::ACTOR_SLEEP, issuer, times_considered) +{ + XBT_DEBUG("ActorSleepTransition()"); +} +std::string ActorSleepTransition::to_string(bool verbose) const +{ + return xbt::string_printf("ActorSleep()"); +} +bool ActorSleepTransition::depends(const Transition* other) const +{ + // Actions executed by the same actor are always dependent + if (other->aid_ == aid_) + return true; + + // Sleeping is indep with any other transitions: always enabled, not impacted by any transition + return false; +} + } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionActorJoin.hpp b/src/mc/transition/TransitionActor.hpp similarity index 71% rename from src/mc/transition/TransitionActorJoin.hpp rename to src/mc/transition/TransitionActor.hpp index 78bc7659e5..34df4417eb 100644 --- a/src/mc/transition/TransitionActorJoin.hpp +++ b/src/mc/transition/TransitionActor.hpp @@ -3,8 +3,8 @@ /* 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. */ -#ifndef SIMGRID_MC_TRANSITION_ACTOR_JOIN_HPP -#define SIMGRID_MC_TRANSITION_ACTOR_JOIN_HPP +#ifndef SIMGRID_MC_TRANSITION_ACTOR_HPP +#define SIMGRID_MC_TRANSITION_ACTOR_HPP #include "src/kernel/actor/SimcallObserver.hpp" #include "src/mc/transition/Transition.hpp" @@ -29,6 +29,14 @@ public: aid_t get_target() const { return target_; } }; +class ActorSleepTransition : public Transition { + +public: + ActorSleepTransition(aid_t issuer, int times_considered, std::stringstream& stream); + std::string to_string(bool verbose) const override; + bool depends(const Transition* other) const override; +}; + } // namespace simgrid::mc #endif diff --git a/src/plugins/solar_panel.cpp b/src/plugins/solar_panel.cpp index abf999513d..c6f2581f80 100644 --- a/src/plugins/solar_panel.cpp +++ b/src/plugins/solar_panel.cpp @@ -43,6 +43,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(SolarPanel, kernel, "Logging specific to the sol namespace simgrid::plugins { +xbt::signal SolarPanel::on_power_change; + /* SolarPanel */ void SolarPanel::update() diff --git a/src/s4u/s4u_Actor.cpp b/src/s4u/s4u_Actor.cpp index e60f73d5fa..573d708555 100644 --- a/src/s4u/s4u_Actor.cpp +++ b/src/s4u/s4u_Actor.cpp @@ -328,18 +328,22 @@ void sleep_for(double duration) } kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self(); + kernel::actor::ActorSleepSimcall observer(issuer); + Actor::on_sleep(*issuer->get_ciface()); issuer->get_ciface()->on_this_sleep(*issuer->get_ciface()); - kernel::actor::simcall_blocking([issuer, duration]() { - if (MC_is_active() || MC_record_replay_is_active()) { - MC_process_clock_add(issuer, duration); - issuer->simcall_answer(); - return; - } - kernel::activity::ActivityImplPtr sync = issuer->sleep(duration); - sync->register_simcall(&issuer->simcall_); - }); + kernel::actor::simcall_blocking( + [issuer, duration]() { + if (MC_is_active() || MC_record_replay_is_active()) { + // MC_process_clock_add(issuer, duration); // BUG: Makes the exploration loop + issuer->simcall_answer(); + } else { + kernel::activity::ActivityImplPtr sync = issuer->sleep(duration); + sync->register_simcall(&issuer->simcall_); + } + }, + &observer); Actor::on_wake_up(*issuer->get_ciface()); issuer->get_ciface()->on_this_wake_up(*issuer->get_ciface()); diff --git a/src/s4u/s4u_Io.cpp b/src/s4u/s4u_Io.cpp index a0482b5ca7..e8aa898590 100644 --- a/src/s4u/s4u_Io.cpp +++ b/src/s4u/s4u_Io.cpp @@ -99,7 +99,7 @@ ssize_t Io::deprecated_wait_any_for(const std::vector& ios, double timeou { ActivitySet set; for (const auto& io : ios) - set.push(boost::dynamic_pointer_cast(io)); + set.push(io); auto* ret = set.wait_any_for(timeout).get(); for (size_t i = 0; i < ios.size(); i++) diff --git a/src/sthread/sthread_impl.cpp b/src/sthread/sthread_impl.cpp index de2667b0e1..9dbf78913e 100644 --- a/src/sthread/sthread_impl.cpp +++ b/src/sthread/sthread_impl.cpp @@ -275,6 +275,7 @@ int sthread_gettimeofday(struct timeval* tv) void sthread_sleep(double seconds) { + XBT_DEBUG("sleep(%lf)", seconds); simgrid::s4u::this_actor::sleep_for(seconds); } diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index 7addb33912..67fe6ab6ec 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -36,10 +36,6 @@ set_target_properties(without-mutex-handling PROPERTIES COMPILE_FLAGS -DDISABLE_ set_target_properties(without-mutex-handling PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/mutex-handling) add_dependencies(tests-mc without-mutex-handling) -set(teshsuite_src ${teshsuite_src} PARENT_SCOPE) -set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-replay.tesh - ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/without-mutex-handling.tesh PARENT_SCOPE) - ADD_TESH(mc-random-bug-replay --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh) IF(SIMGRID_HAVE_MC) ADD_TESH(tesh-mc-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:none) @@ -56,3 +52,52 @@ ENDIF() if(enable_coverage) ADD_TEST(cover-mc-mutex-handling ${CMAKE_CURRENT_BINARY_DIR}/mutex-handling/mutex-handling ${CMAKE_HOME_DIRECTORY}/examples/platforms/small_platform.xml) endif() + + +if("${CMAKE_SYSTEM}" MATCHES "Linux") + foreach(x +# +# simple_cond_broadcast_deadlock simple_semaphore_deadlock simple_barrier_deadlock simple_cond_deadlock +# simple_semaphores_deadlock +# +# +# philosophers_spurious_deadlock +# simple_barrier_with_threads_deadlock +# simple_semaphores_with_threads_deadlock +# simple_cond_broadcast_with_semaphore_deadlock1 simple_cond_broadcast_with_semaphore_deadlock2 +# simple_mutex_deadlock +# simple_mutex_with_threads_deadlock + + barber_shop_ok barber_shop_deadlock + philosophers_semaphores_ok philosophers_semaphores_deadlock + philosophers_mutex_ok philosophers_mutex_deadlock + producer_consumer_ok producer_consumer_deadlock + + + # producer_consumer_spurious_nok # infinite no-op loop + +# +# +# simple_barrier_ok simple_barrier_with_threads_ok simple_cond_broadcast_ok +# simple_cond_broadcast_with_semaphore_ok simple_cond_ok simple_mutex_ok +# simple_mutex_with_threads_ok simple_semaphores_ok simple_semaphores_with_threads_ok simple_threads_ok + ) + + set(teshsuite_src ${teshsuite_src} ${CMAKE_CURRENT_SOURCE_DIR}/mcmini/${x}.c) + set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/mcmini/${x}.tesh) + + add_executable (mcmini-${x} EXCLUDE_FROM_ALL mcmini/${x}.c) + set_target_properties(mcmini-${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/mcmini) + target_link_libraries(mcmini-${x} PRIVATE Threads::Threads) + add_dependencies(tests-mc mcmini-${x}) + if(SIMGRID_HAVE_STATEFUL_MC) # Only needed to introspect the binary + target_link_libraries(mcmini-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13 + endif() + + ADD_TESH(mc-mini-${x} --setenv libdir=${CMAKE_BINARY_DIR}/lib --setenv bindir=${CMAKE_CURRENT_BINARY_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/mcmini/${x}.tesh) + endforeach() +endif() + +set(teshsuite_src ${teshsuite_src} PARENT_SCOPE) +set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-replay.tesh + ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/without-mutex-handling.tesh PARENT_SCOPE) diff --git a/teshsuite/mc/mcmini/barber_shop_deadlock.c b/teshsuite/mc/mcmini/barber_shop_deadlock.c new file mode 100644 index 0000000000..c10c970bd5 --- /dev/null +++ b/teshsuite/mc/mcmini/barber_shop_deadlock.c @@ -0,0 +1,107 @@ +#define _REENTRANT + +#include +#include +#include +#include +#include + +// The maximum number of customer threads. +#define MAX_CUSTOMERS 10 + +// Define the semaphores. +sem_t waitingRoom; +sem_t barberChair; +sem_t barberPillow; +sem_t seatBelt; + +// Flag to stop the barber thread when all customers have been serviced. +int allDone = 0; +int DEBUG = 0; + +static void *customer(void *number) { + int num = *(int *)number; + + if(DEBUG) printf("Customer %d leaving for barber shop.\n", num); + if(DEBUG) printf("Customer %d arrived at barber shop.\n", num); + + sem_wait(&waitingRoom); + + if(DEBUG) printf("Customer %d entering waiting room.\n", num); + + sem_wait(&barberChair); + + if(DEBUG) printf("Customer %d waking the barber.\n", num); + sem_post(&barberPillow); + + sem_wait(&seatBelt); + + sem_post(&barberChair); + if(DEBUG) printf("Customer %d leaving barber shop.\n", num); + return NULL; +} + +static void *barber(void *junk) { + while (!allDone) { + if(DEBUG) printf("The barber is sleeping\n"); + sem_wait(&barberPillow); + + if (!allDone) { + if(DEBUG) printf("The barber is cutting hair\n"); + if(DEBUG) printf("The barber has finished cutting hair.\n"); + sem_post(&seatBelt); + } + else { + if(DEBUG) printf("The barber is going home for the day.\n"); + } + } + return NULL; +} + +int main(int argc, char *argv[]) { + if(argc != 5){ + printf("Usage: %s numCustomers numChairs RandSeed DEBUG\n", argv[0]); + return 1; + } + + pthread_t btid; + pthread_t tid[MAX_CUSTOMERS]; + int i, numCustomers, numChairs; + long RandSeed; + int Number[MAX_CUSTOMERS]; + + numCustomers = atoi(argv[1]); + numChairs = atoi(argv[2]); + RandSeed = atol(argv[3]); + DEBUG = atoi(argv[4]); + + if (numCustomers > MAX_CUSTOMERS) { + printf("The maximum number of Customers is %d.\n", MAX_CUSTOMERS); + exit(-1); + } + + srand48(RandSeed); + + for (i=0; i [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 4 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:6) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall SEM_WAIT(sem_id:2 not granted) +> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted) +> [0.000000] [ker_engine/INFO] Actor 7 (thread 6@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 1, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_UNLOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 3, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 3, no timeout) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 1, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_UNLOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 3, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 4, no timeout) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 1, granted: yes) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_UNLOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 3) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 3, granted: yes) +> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 5, no timeout) +> [0.000000] [mc_global/INFO] Actor 6 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 7 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;3;3;3;3;3;2;2;2;3;3;3;1;4;4;4;4;4;2;2;2;4;4;4;1;5;5;5;5;5;2;2;2;5;5;5;1;6;7' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 40 unique states visited; 0 backtracks (0 transition replays, 40 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/barber_shop_ok.c b/teshsuite/mc/mcmini/barber_shop_ok.c new file mode 100644 index 0000000000..b0f17ca859 --- /dev/null +++ b/teshsuite/mc/mcmini/barber_shop_ok.c @@ -0,0 +1,183 @@ +#ifdef _REENTRANT +#undef _REENTRANT +#endif +#define _REENTRANT + +#include +#include +#include +#include +#include + +// The maximum number of customer threads. +#define MAX_CUSTOMERS 25 + +// Define the semaphores. + +// waitingRoom Limits the # of customers allowed +// to enter the waiting room at one time. +sem_t waitingRoom; + +// barberChair ensures mutually exclusive access to +// the barber chair. +sem_t barberChair; + +// barberPillow is used to allow the barber to sleep +// until a customer arrives. +sem_t barberPillow; + +// seatBelt is used to make the customer to wait until +// the barber is done cutting his/her hair. +sem_t seatBelt; + +// Flag to stop the barber thread when all customers +// have been serviced. +int allDone = 0; +int DEBUG = 0; + +static void randwait(int secs) +{ + int len; + + // Generate a random number... + len = (int)((drand48() * secs) + 1); + sleep(len); +} + +static void* customer(void* number) +{ + int num = *(int*)number; + + // Leave for the shop and take some random amount of + // time to arrive. + if (DEBUG) + printf("Customer %d leaving for barber shop.\n", num); + randwait(5); + if (DEBUG) + printf("Customer %d arrived at barber shop.\n", num); + + // Wait for space to open up in the waiting room... + sem_wait(&waitingRoom); + if (DEBUG) + printf("Customer %d entering waiting room.\n", num); + + // Wait for the barber chair to become free. + sem_wait(&barberChair); + + // The chair is free so give up your spot in the + // waiting room. + sem_post(&waitingRoom); + + // Wake up the barber... + if (DEBUG) + printf("Customer %d waking the barber.\n", num); + sem_post(&barberPillow); + + // Wait for the barber to finish cutting your hair. + sem_wait(&seatBelt); + + // Give up the chair. + sem_post(&barberChair); + if (DEBUG) + printf("Customer %d leaving barber shop.\n", num); + return NULL; +} + +static void* barber(void* junk) +{ + // While there are still customers to be serviced... + // Our barber is omnicient and can tell if there are + // customers still on the way to his shop. + while (!allDone) { + + // Sleep until someone arrives and wakes you.. + if (DEBUG) + printf("The barber is sleeping\n"); + sem_wait(&barberPillow); + + // Skip this stuff at the end... + if (!allDone) { + + // Take a random amount of time to cut the + // customer's hair. + if (DEBUG) + printf("The barber is cutting hair\n"); + randwait(3); + if (DEBUG) + printf("The barber has finished cutting hair.\n"); + + // Release the customer when done cutting... + sem_post(&seatBelt); + } else { + if (DEBUG) + printf("The barber is going home for the day.\n"); + } + } + return NULL; +} + +int main(int argc, char* argv[]) +{ + pthread_t btid; + pthread_t tid[MAX_CUSTOMERS]; + long RandSeed; + int i, numCustomers, numChairs; + int Number[MAX_CUSTOMERS]; + + // Check to make sure there are the right number of + // command line arguments. + if (argc != 5) { + printf("Use: SleepBarber \n"); + exit(-1); + } + + // Get the command line arguments and convert them + // into integers. + numCustomers = atoi(argv[1]); + numChairs = atoi(argv[2]); + RandSeed = atol(argv[3]); + DEBUG = atoi(argv[4]); + + // Make sure the number of threads is less than the number of + // customers we can support. + if (numCustomers > MAX_CUSTOMERS) { + printf("The maximum number of Customers is %d.\n", MAX_CUSTOMERS); + exit(-1); + } + + printf("\nSleepBarber.c\n\n"); + printf("A solution to the sleeping barber problem using semaphores.\n"); + + // Initialize the random number generator with a new seed. + srand48(RandSeed); + + // Initialize the numbers array. + for (i = 0; i < MAX_CUSTOMERS; i++) { + Number[i] = i; + } + + // Initialize the semaphores with initial values... + sem_init(&waitingRoom, 0, numChairs); + sem_init(&barberChair, 0, 1); + sem_init(&barberPillow, 0, 0); + sem_init(&seatBelt, 0, 0); + + // Create the barber. + pthread_create(&btid, NULL, barber, NULL); + + // Create the customers. + for (i = 0; i < numCustomers; i++) { + pthread_create(&tid[i], NULL, customer, (void*)&Number[i]); + } + + // Join each of the threads to wait for them to finish. + for (i = 0; i < numCustomers; i++) { + pthread_join(tid[i], NULL); + } + + // When all of the customers are finished, kill the + // barber thread. + allDone = 1; + sem_post(&barberPillow); // Wake the barber so he will exit. + pthread_join(btid, NULL); +} diff --git a/teshsuite/mc/mcmini/barber_shop_ok.tesh b/teshsuite/mc/mcmini/barber_shop_ok.tesh new file mode 100644 index 0000000000..6fc22cd8e9 --- /dev/null +++ b/teshsuite/mc/mcmini/barber_shop_ok.tesh @@ -0,0 +1,10 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-barber_shop_ok 3 2 0 0 +> +> SleepBarber.c +> +> A solution to the sleeping barber problem using semaphores. +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 5169 unique states visited; 959 backtracks (21531 transition replays, 27659 states visited overall) diff --git a/teshsuite/mc/mcmini/philosophers_mutex_deadlock.c b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.c new file mode 100644 index 0000000000..4497df76cd --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.c @@ -0,0 +1,59 @@ +// Naive dining philosophers solution, which leads to deadlock. + +#include +#include +#include +#include + +int DEBUG = 0; + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; +} *forks; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + + if(DEBUG) printf("Philosopher %d just ate.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc != 3){ + printf("Usage: %s NUM_PHILOSOPHERS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + + forks = malloc(NUM_THREADS * sizeof(struct forks)); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], &mutex_resource[(i+1) % NUM_THREADS]}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + free(forks); + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh new file mode 100644 index 0000000000..6d31afa740 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh @@ -0,0 +1,35 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +! expect return 3 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_mutex_deadlock 5 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 6 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:2 owner:4) +> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:3 owner:5) +> [0.000000] [ker_engine/INFO] Actor 5 (thread 4@Lilibeth) simcall MUTEX_WAIT(mutex_id:4 owner:6) +> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_WAIT(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 3, owner: 5) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 3, owner: 5) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_WAIT(mutex: 3, owner: 5) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 4, owner: 6) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 4, owner: 6) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_WAIT(mutex: 4, owner: 6) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;4;3;4;5;4;5;6;5;6;6' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1298 unique states visited; 199 backtracks (3432 transition replays, 4929 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/philosophers_mutex_ok.c b/teshsuite/mc/mcmini/philosophers_mutex_ok.c new file mode 100644 index 0000000000..8c30821b31 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_ok.c @@ -0,0 +1,65 @@ +#include +#include +#include +#include + +int DEBUG = 0; + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; + pthread_mutex_t *dining_fork; +}; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + pthread_mutex_lock(forks->dining_fork); + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + pthread_mutex_unlock(forks->dining_fork); + + if(DEBUG) + printf("Philosopher %d is eating.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + return NULL; +} + +int main(int argc, char* argv[]) +{ + if(argc != 3){ + printf("Usage: %s NUM_THREADS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + struct forks forks[NUM_THREADS]; + + pthread_mutex_t dining_fork; + pthread_mutex_init(&dining_fork, NULL); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], + &mutex_resource[(i+1) % NUM_THREADS], + &dining_fork}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_mutex_ok.tesh b/teshsuite/mc/mcmini/philosophers_mutex_ok.tesh new file mode 100644 index 0000000000..d90ff92995 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_mutex_ok.tesh @@ -0,0 +1,6 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_mutex_ok 5 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 14170 unique states visited; 2087 backtracks (45202 transition replays, 61459 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.c b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.c new file mode 100644 index 0000000000..92e58b1b59 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.c @@ -0,0 +1,67 @@ +// Dining philosophers solution with semaphores + +#include +#include +#include +#include +#include + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; + sem_t* sem_dining; + int DEBUG; +} *forks; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + sem_wait(forks->sem_dining); + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + + if(forks->DEBUG) printf("Philosopher %d just ate.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + sem_post(forks->sem_dining); + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc != 3){ + printf("Usage: %s NUM_PHILOSOPHERS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + int DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + sem_t sem_dining; + sem_init(&sem_dining, 0, NUM_THREADS); + + forks = malloc(NUM_THREADS * sizeof(struct forks)); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], + &mutex_resource[(i+1) % NUM_THREADS], + &sem_dining, + DEBUG}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + free(forks); + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh new file mode 100644 index 0000000000..66020c9203 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh @@ -0,0 +1,33 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +! expect return 3 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_deadlock 3 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 4 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:2 owner:4) +> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_WAIT(mutex: 2, owner: 4) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;2;2;3;3;3;2;3;4;4;4;3;4;4' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 890 unique states visited; 90 backtracks (1415 transition replays, 2395 states visited overall) diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_ok.c b/teshsuite/mc/mcmini/philosophers_semaphores_ok.c new file mode 100644 index 0000000000..b11e49ffec --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_ok.c @@ -0,0 +1,66 @@ +#include +#include +#include +#include +#include + +int DEBUG = 0; + +struct forks { + int philosopher; + pthread_mutex_t *left_fork; + pthread_mutex_t *right_fork; + sem_t* sem_dining; +}; + +static void * philosopher_doit(void *forks_arg) { + struct forks *forks = forks_arg; + sem_wait(forks->sem_dining); + pthread_mutex_lock(forks->left_fork); + pthread_mutex_lock(forks->right_fork); + + if(DEBUG) + printf("Philosopher %d is eating.\n", forks->philosopher); + + pthread_mutex_unlock(forks->left_fork); + pthread_mutex_unlock(forks->right_fork); + sem_post(forks->sem_dining); + return NULL; +} + +int main(int argc, char* argv[]) +{ + if(argc != 3){ + printf("Usage: %s NUM_THREADS DEBUG\n", argv[0]); + return 1; + } + + int NUM_THREADS = atoi(argv[1]); + DEBUG = atoi(argv[2]); + + pthread_t thread[NUM_THREADS]; + pthread_mutex_t mutex_resource[NUM_THREADS]; + struct forks forks[NUM_THREADS]; + + sem_t sem_dining; + sem_init(&sem_dining, 0, NUM_THREADS - 1); + + int i; + for (i = 0; i < NUM_THREADS; i++) { + pthread_mutex_init(&mutex_resource[i], NULL); + forks[i] = (struct forks){i, + &mutex_resource[i], + &mutex_resource[(i+1) % NUM_THREADS], + &sem_dining}; + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]); + } + + for (i = 0; i < NUM_THREADS; i++) { + pthread_join(thread[i], NULL); + } + + return 0; +} diff --git a/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh new file mode 100644 index 0000000000..1b4113e1e1 --- /dev/null +++ b/teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh @@ -0,0 +1,6 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_ok 3 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 2268 unique states visited; 233 backtracks (3314 transition replays, 5815 states visited overall) \ No newline at end of file diff --git a/teshsuite/mc/mcmini/producer_consumer_deadlock.c b/teshsuite/mc/mcmini/producer_consumer_deadlock.c new file mode 100644 index 0000000000..2cf1ee6a2a --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_deadlock.c @@ -0,0 +1,83 @@ +#include +#include +#include +#include + +int MaxItems; // Maximum items a producer can produce or a consumer can consume +int BufferSize; // Size of the buffer + +sem_t empty; +sem_t full; +int in = 0; +int out = 0; +int *buffer; +pthread_mutex_t mutex; + +int DEBUG = 0; // Debug flag + +static void *producer(void *pno) +{ + int item; + for(int i = 0; i < MaxItems; i++) { + item = rand(); // Produce a random item + pthread_mutex_lock(&mutex); + sem_wait(&empty); + buffer[in] = item; + if(DEBUG) printf("Producer %d: Insert Item %d at %d\n", *((int *)pno),buffer[in],in); + in = (in+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&full); + } + return NULL; +} + +static void *consumer(void *cno) +{ + for(int i = 0; i < MaxItems; i++) { + pthread_mutex_lock(&mutex); + sem_wait(&full); + int item = buffer[out]; + if(DEBUG) printf("Consumer %d: Remove Item %d from %d\n",*((int *)cno),item, out); + out = (out+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&empty); + } + return NULL; +} + +int main(int argc, char* argv[]) { + if(argc != 4){ + printf("Usage: %s MAX_ITEMS BUFFER_SIZE DEBUG\n", argv[0]); + return 1; + } + + MaxItems = atoi(argv[1]); + BufferSize = atoi(argv[2]); + DEBUG = atoi(argv[3]); + + buffer = (int*) malloc(BufferSize * sizeof(int)); + + pthread_t pro[5],con[5]; + pthread_mutex_init(&mutex, NULL); + sem_init(&empty,0,BufferSize); + sem_init(&full,0,0); + + int a[5] = {1,2,3,4,5}; //Just used for numbering the producer and consumer + + for(int i = 0; i < 5; i++) { + pthread_create(&pro[i], NULL, producer, (void *)&a[i]); + } + for(int i = 0; i < 5; i++) { + pthread_create(&con[i], NULL, consumer, (void *)&a[i]); + } + + for(int i = 0; i < 5; i++) { + pthread_join(pro[i], NULL); + } + for(int i = 0; i < 5; i++) { + pthread_join(con[i], NULL); + } + + free(buffer); + return 0; +} diff --git a/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh b/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh new file mode 100644 index 0000000000..06b4b2832a --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_deadlock.tesh @@ -0,0 +1,55 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +! expect return 3 +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-producer_consumer_deadlock 5 3 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED *** +> [0.000000] [mc_global/INFO] ************************** +> [0.000000] [ker_engine/INFO] 11 actors are still running, waiting for something. +> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor (@): " +> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2) +> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted) +> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 5 (thread 4@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 7 (thread 6@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 8 (thread 7@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 9 (thread 8@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 10 (thread 9@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [ker_engine/INFO] Actor 11 (thread 10@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2) +> [0.000000] [mc_global/INFO] Counter-example execution trace: +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0) +> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 7 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 8 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 9 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 10 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_global/INFO] Actor 11 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) +> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;3;4;5;6;7;8;9;10;11' +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 31 unique states visited; 0 backtracks (0 transition replays, 31 states visited overall) diff --git a/teshsuite/mc/mcmini/producer_consumer_ok.c b/teshsuite/mc/mcmini/producer_consumer_ok.c new file mode 100644 index 0000000000..9fc1583dd4 --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_ok.c @@ -0,0 +1,93 @@ +#include +#include +#include +#include +#include + +#define MaxBufferSize 5 + +sem_t empty; +sem_t full; +int in = 0; +int out = 0; +int buffer[MaxBufferSize]; +pthread_mutex_t mutex; +int BufferSize; +int ItemCount; +int DEBUG; + +static void *producer(void *pno) +{ + int item; + for(int i = 0; i < ItemCount; i++) { + item = rand(); // Produce an random item + sem_wait(&empty); + pthread_mutex_lock(&mutex); + buffer[in] = item; + if (DEBUG) { + printf("Producer %d: Insert Item %d at %d\n", + *((int *)pno),buffer[in],in); + } + in = (in+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&full); + } + return NULL; +} + +static void *consumer(void *cno) +{ + for(int i = 0; i < ItemCount; i++) { + sem_wait(&full); + pthread_mutex_lock(&mutex); + int item = buffer[out]; + if (DEBUG) { + printf("Consumer %d: Remove Item %d from %d\n", + *((int *)cno),item, out); + } + out = (out+1)%BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&empty); + } + return NULL; +} + +int main(int argc, char* argv[]) +{ + if (argc < 6) { + printf("Usage: %s \n", argv[0]); + return 1; + } + + int NUM_PRODUCERS = atoi(argv[1]); + int NUM_CONSUMERS = atoi(argv[2]); + ItemCount = atoi(argv[3]); + BufferSize = atoi(argv[4]); + DEBUG = atoi(argv[5]); + + pthread_t pro[NUM_PRODUCERS],con[NUM_CONSUMERS]; + + pthread_mutex_init(&mutex, NULL); + sem_init(&empty,0,BufferSize); + sem_init(&full,0,0); + + int a[NUM_PRODUCERS > NUM_CONSUMERS ? NUM_PRODUCERS : NUM_CONSUMERS]; + + for(int i = 0; i < NUM_PRODUCERS; i++) { + a[i] = i+1; + pthread_create(&pro[i], NULL, producer, (void *)&a[i]); + } + for(int i = 0; i < NUM_CONSUMERS; i++) { + a[i] = i+1; + pthread_create(&con[i], NULL, consumer, (void *)&a[i]); + } + + for(int i = 0; i < NUM_PRODUCERS; i++) { + pthread_join(pro[i], NULL); + } + for(int i = 0; i < NUM_CONSUMERS; i++) { + pthread_join(con[i], NULL); + } + + return 0; +} diff --git a/teshsuite/mc/mcmini/producer_consumer_ok.tesh b/teshsuite/mc/mcmini/producer_consumer_ok.tesh new file mode 100644 index 0000000000..1c201d46a0 --- /dev/null +++ b/teshsuite/mc/mcmini/producer_consumer_ok.tesh @@ -0,0 +1,6 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-producer_consumer_ok 2 2 2 1 0 +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1953 unique states visited; 491 backtracks (12324 transition replays, 14768 states visited overall) \ No newline at end of file diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 133bbd920d..f0b0d87b43 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -564,8 +564,8 @@ set(MC_SRC_STATELESS src/mc/remote/mc_protocol.h src/mc/transition/Transition.hpp - src/mc/transition/TransitionActorJoin.cpp - src/mc/transition/TransitionActorJoin.hpp + src/mc/transition/TransitionActor.cpp + src/mc/transition/TransitionActor.hpp src/mc/transition/TransitionAny.cpp src/mc/transition/TransitionAny.hpp src/mc/transition/TransitionComm.cpp diff --git a/tools/docker/Dockerfile.stable b/tools/docker/Dockerfile.stable index b8986110bd..011ae00c03 100644 --- a/tools/docker/Dockerfile.stable +++ b/tools/docker/Dockerfile.stable @@ -17,6 +17,6 @@ RUN echo "DOWNLOAD_URL: ${DLURL}" && \ make -j4 && \ mkdir debian/ && touch debian/control && dpkg-shlibdeps --ignore-missing-info lib/*.so -llib/ -O/tmp/deps && \ make install && make clean && \ - apt remove -y g++ gcc git valgrind gfortran libboost-dev libboost-all-dev libeigen3-dev cmake dpkg-dev wget python3-dev pybind11-dev && \ + apt remove -y git valgrind libeigen3-dev cmake dpkg-dev wget python3-dev pybind11-dev && \ apt install `sed -e 's/shlibs:Depends=//' -e 's/([^)]*)//g' -e 's/,//g' /tmp/deps` && \ apt autoremove -y && apt autoclean && apt clean diff --git a/tools/docker/Dockerfile.unstable b/tools/docker/Dockerfile.unstable index 6ef5e42c40..c3bf640660 100644 --- a/tools/docker/Dockerfile.unstable +++ b/tools/docker/Dockerfile.unstable @@ -12,6 +12,6 @@ RUN apt-get --allow-releaseinfo-change update && apt -y upgrade && \ make -j4 install && \ mkdir debian/ && touch debian/control && dpkg-shlibdeps --ignore-missing-info lib/*.so -llib/ -O/tmp/deps && \ git reset --hard master && git clean -dfx && \ - apt remove -y g++ gcc git valgrind gfortran libboost-dev libboost-all-dev libeigen3-dev cmake dpkg-dev python3-dev pybind11-dev && \ + apt remove -y git valgrind libeigen3-dev cmake dpkg-dev wget python3-dev pybind11-dev && \ apt install `sed -e 's/shlibs:Depends=//' -e 's/([^)]*)//g' -e 's/,//g' /tmp/deps` && \ apt autoremove -y && apt autoclean && apt clean diff --git a/tools/tesh/tesh.py b/tools/tesh/tesh.py index a0e96d5072..856dab0913 100755 --- a/tools/tesh/tesh.py +++ b/tools/tesh/tesh.py @@ -594,6 +594,7 @@ def main(): re.compile(r"For details see http://code\.google\.com/p/address-sanitizer/issues/detail\?id=189"), re.compile(r"For details see https://github\.com/google/sanitizers/issues/189"), re.compile(r"Python runtime initialized with LC_CTYPE=C .*"), + re.compile(r"sthread is intercepting the execution of \.*"), # Seen on CircleCI re.compile(r"cmake: /usr/local/lib/libcurl\.so\.4: no version information available \(required by cmake\)"), re.compile( @@ -709,7 +710,16 @@ def main(): cmd.add_ignore(line[len("! ignore "):]) else: - fatal_error(f"UNRECOGNIZED OPTION LINE: {line}") + fatal_error(f"UNRECOGNIZED OPTION LINE: {line}\n" + "Valid requests:\n" + " ! output ignore\n" + " ! output sort\n" + " ! output display\n" + " ! setenv XX=YY\n" + " ! ignore XYZ\n" + " ! expect return NN\n" + " ! expect signal NN\n" + " ! timeout NN\n") line = file.readfullline()