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
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
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
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
- 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
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
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
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
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
#include <string>
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<sg4::Activity>(exec),
- boost::dynamic_pointer_cast<sg4::Activity>(comm),
- boost::dynamic_pointer_cast<sg4::Activity>(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()
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);
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();
#include <string>
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()) {
while (auto completed_one = pending_activities.test_any()) {
if (boost::dynamic_pointer_cast<sg4::Comm>(completed_one))
XBT_INFO("Completed a Comm");
+ if (boost::dynamic_pointer_cast<sg4::Mess>(completed_one))
+ XBT_INFO("Completed a Mess");
if (boost::dynamic_pointer_cast<sg4::Exec>(completed_one))
XBT_INFO("Completed an Exec");
if (boost::dynamic_pointer_cast<sg4::Io>(completed_one))
}
XBT_INFO("Last activity is complete");
delete payload;
+ delete message;
}
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);
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();
> [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.
#include <string>
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<sg4::Activity>(exec),
- boost::dynamic_pointer_cast<sg4::Activity>(comm),
- boost::dynamic_pointer_cast<sg4::Activity>(io)});
+ sg4::ActivitySet pending_activities({exec, comm, io, mess});
XBT_INFO("Wait for asynchronous activities to complete");
while (not pending_activities.empty()) {
if (completed_one != nullptr) {
if (boost::dynamic_pointer_cast<sg4::Comm>(completed_one))
XBT_INFO("Completed a Comm");
+ if (boost::dynamic_pointer_cast<sg4::Mess>(completed_one))
+ XBT_INFO("Completed a Mess");
if (boost::dynamic_pointer_cast<sg4::Exec>(completed_one))
XBT_INFO("Completed an Exec");
if (boost::dynamic_pointer_cast<sg4::Io>(completed_one))
}
XBT_INFO("Last activity is complete");
delete payload;
+ delete message;
}
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);
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();
> [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
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);
std::shared_ptr<simgrid::plugins::Battery::Handler> 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) {
}
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;
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());
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());
});
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());
});
e.run();
+
return 0;
}
\ No newline at end of file
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<sg4::Activity>(bob_compute),
- boost::dynamic_pointer_cast<sg4::Activity>(bob_write),
- boost::dynamic_pointer_cast<sg4::Activity>(carl_read),
- boost::dynamic_pointer_cast<sg4::Activity>(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");
> [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
> [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
> [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
> [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
> [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:
> [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
auto data = t->get_token_from(SA_to_B1)->get_data<double>();
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<double>();
t->deque_token_from(SA_to_B2);
t->set_amount(*data * 10);
+ delete data;
});
// Enqueue firings for tasks without predecessors
! 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.
! 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.
> 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)
! 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.
! 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)
$ 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.
$ 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.
$ 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
> [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
! 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.
$ ./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.
friend void intrusive_ptr_add_ref(SolarPanel* o) { o->refcount_.fetch_add(1, std::memory_order_relaxed); }
#endif
- inline static xbt::signal<void(SolarPanel*)> on_power_change;
+ static xbt::signal<void(SolarPanel*)> on_power_change;
xbt::signal<void(SolarPanel*)> on_this_power_change;
public:
{
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
{
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_;
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));
}
}
#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
const auto* cast_strategy = dynamic_cast<BasicStrategy const*>(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;
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)) {
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();
}
}
}
-std::vector<std::string> Exploration::get_textual_trace()
+std::vector<std::string> Exploration::get_textual_trace(int max_elements)
{
std::vector<std::string> trace;
for (auto const& transition : get_record_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;
}
virtual RecordTrace get_record_trace() = 0;
/** Generate a textual execution trace of the simulated application */
- std::vector<std::string> get_textual_trace();
+ std::vector<std::string> get_textual_trace(int max_elements = -1);
/** Log additional information about the state of the model-checker */
virtual void log_state();
#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"
#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"
std::vector<s_mc_message_actors_status_one_t> 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;
#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"
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);
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;
/* 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"
}
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_) {
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
/* 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"
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
namespace simgrid::plugins {
+xbt::signal<void(SolarPanel*)> SolarPanel::on_power_change;
+
/* SolarPanel */
void SolarPanel::update()
}
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());
{
ActivitySet set;
for (const auto& io : ios)
- set.push(boost::dynamic_pointer_cast<Activity>(io));
+ set.push(io);
auto* ret = set.wait_any_for(timeout).get();
for (size_t i = 0; i < ios.size(); i++)
void sthread_sleep(double seconds)
{
+ XBT_DEBUG("sleep(%lf)", seconds);
simgrid::s4u::this_actor::sleep_for(seconds);
}
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)
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)
--- /dev/null
+#define _REENTRANT
+
+#include <stdio.h>
+#include <unistd.h>
+#include <stdlib.h>
+#include <pthread.h>
+#include <semaphore.h>
+
+// 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<MAX_CUSTOMERS; i++) {
+ Number[i] = i;
+ }
+
+ sem_init(&waitingRoom, 0, numChairs);
+ sem_init(&barberChair, 0, 1);
+ sem_init(&barberPillow, 0, 0);
+ sem_init(&seatBelt, 0, 0);
+
+ pthread_create(&btid, NULL, barber, NULL);
+
+ for (i=0; i<numCustomers; i++) {
+ pthread_create(&tid[i], NULL, customer, (void *)&Number[i]);
+ }
+
+ for (i=0; i<numCustomers; i++) {
+ pthread_join(tid[i],NULL);
+ }
+
+ allDone = 1;
+ sem_post(&barberPillow);
+ pthread_join(btid,NULL);
+}
--- /dev/null
+# 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-barber_shop_deadlock 5 3 0 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 <pid> (<name>@<host>): <status>"
+> [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
--- /dev/null
+#ifdef _REENTRANT
+#undef _REENTRANT
+#endif
+#define _REENTRANT
+
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+// 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 <Num Customers> <Num Chairs> <rand seed> <DEBUG>\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);
+}
--- /dev/null
+# 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)
--- /dev/null
+// Naive dining philosophers solution, which leads to deadlock.
+
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <stdlib.h>
+
+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;
+}
--- /dev/null
+# 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 <pid> (<name>@<host>): <status>"
+> [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
--- /dev/null
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <stdlib.h>
+
+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;
+}
--- /dev/null
+# 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
--- /dev/null
+// Dining philosophers solution with semaphores
+
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdlib.h>
+
+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;
+}
--- /dev/null
+# 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 <pid> (<name>@<host>): <status>"
+> [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)
--- /dev/null
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdlib.h>
+
+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;
+}
--- /dev/null
+# 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
--- /dev/null
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+#include <semaphore.h>
+
+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;
+}
--- /dev/null
+# 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 <pid> (<name>@<host>): <status>"
+> [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)
--- /dev/null
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <pthread.h>
+#include <semaphore.h>
+
+#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 <NUM_PRODUCERS> <NUM_CONSUMERS> <ITEM_COUNT> <BUFFER_SIZE> <DEBUG>\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;
+}
--- /dev/null
+# 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
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
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
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
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(
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()
