From: mlaurent Date: Fri, 24 Feb 2023 14:42:51 +0000 (+0100) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.34~436^2 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/3203afd846219ef8b41cadda945ea0a98103c46f?hp=13f8c10bd72f90cb6f70e9a03ce37dcbf6e01226 Merge branch 'master' of https://framagit.org/simgrid/simgrid --- diff --git a/ChangeLog b/ChangeLog index 0d62c29c1a..a60dfcf6b0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -15,10 +15,13 @@ S4U: Comm::set_payload_size() to change the size of the simulated data. - New function: Engine::flatify_platform(), to get a fully detailed vision of the configured platform. + - Full simDAG integration: Activity::start() actually starts only when all dependencies + are fullfiled. If it cannot be started right away, it will start as soon as it becomes + possible. Kernel: - - optimize an internal datastructure, leading to a potentially big - performance gain (in particular with many detached comms) + - optimize an internal datastructure (use a set instead of a list for ongoing activities), + leading to a potentially big performance gain, in particular with many detached comms. MPI: - New option smpi/barrier-collectives to add a barrier to some collectives @@ -40,9 +43,16 @@ Models: with the default host model, as it should. - Rename option "surf/precision" to "precision/timing" for clarity. - Rename option "maxmin/precision" to "precision/work-amount" for clarity. + - New function: Engine::flatify_platform() to debug your platform. sthread: - Implement pthread_join in MC mode. + - Implement semaphore functions in sthread. + +Model checking: + - Synchronize the MBI tests with upstream. + - Show the full actor bactraces when replaying a MC trace (with model-check/replay) + and the status of all actors on deadlocks in MC mode. XBT: - simgrid::xbt::cmdline and simgrid::xbt::binary_name are gone. diff --git a/MANIFEST.in b/MANIFEST.in index d0b59a996a..105d326266 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -597,9 +597,12 @@ include examples/smpi/trace_simple/trace_simple.c include examples/smpi/trace_simple/trace_simple.tesh include examples/sthread/pthread-mc-mutex-simple.tesh include examples/sthread/pthread-mc-mutex-simpledeadlock.tesh +include examples/sthread/pthread-mc-producer-consumer.tesh include examples/sthread/pthread-mutex-simple.c include examples/sthread/pthread-mutex-simple.tesh include examples/sthread/pthread-mutex-simpledeadlock.c +include examples/sthread/pthread-producer-consumer.c +include examples/sthread/pthread-producer-consumer.tesh include examples/sthread/sthread-mutex-simple.c include examples/sthread/sthread-mutex-simple.tesh include teshsuite/catch_simgrid.hpp @@ -2148,6 +2151,22 @@ include src/mc/explo/LivenessChecker.hpp include src/mc/explo/UdporChecker.cpp include src/mc/explo/UdporChecker.hpp include src/mc/explo/simgrid_mc.cpp +include src/mc/explo/udpor/Configuration.cpp +include src/mc/explo/udpor/Configuration.hpp +include src/mc/explo/udpor/Configuration_test.cpp +include src/mc/explo/udpor/EventSet.cpp +include src/mc/explo/udpor/EventSet.hpp +include src/mc/explo/udpor/EventSet_test.cpp +include src/mc/explo/udpor/History.cpp +include src/mc/explo/udpor/History.hpp +include src/mc/explo/udpor/History_test.cpp +include src/mc/explo/udpor/Unfolding.cpp +include src/mc/explo/udpor/Unfolding.hpp +include src/mc/explo/udpor/UnfoldingEvent.cpp +include src/mc/explo/udpor/UnfoldingEvent.hpp +include src/mc/explo/udpor/UnfoldingEvent_test.cpp +include src/mc/explo/udpor/Unfolding_test.cpp +include src/mc/explo/udpor/udpor_forward.hpp include src/mc/inspect/DwarfExpression.cpp include src/mc/inspect/DwarfExpression.hpp include src/mc/inspect/Frame.cpp @@ -2212,8 +2231,6 @@ include src/mc/transition/TransitionRandom.cpp include src/mc/transition/TransitionRandom.hpp include src/mc/transition/TransitionSynchro.cpp include src/mc/transition/TransitionSynchro.hpp -include src/mc/udpor_global.cpp -include src/mc/udpor_global.hpp include src/plugins/ProducerConsumer.cpp include src/plugins/chaos_monkey.cpp include src/plugins/file_system/s4u_FileSystem.cpp diff --git a/NEWS b/NEWS index 7752c9f2fc..fe01ae8b50 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,11 @@ __ _____ _ __ ___(_) ___ _ __ |___ / |___ /___ / \ V / __/ | \__ \ | (_) | | | | ___) | ___) |__) | \_/ \___|_| |___/_|\___/|_| |_| |____(_)____/____/ (not released yet) + + * MSG and Java are gone (EOL was scheduled for 2020) + * Introduce a fluid I/O model, mixing I/O and network, to represent streaming from disk + * Fix the DPOR reduction, toward sound verifications. + * (+ MANY internal refactoring, bug fixes and MANY documentation improvement) _ _____ _________ __ _____ _ __ ___(_) ___ _ __ |___ / |___ /___ \ \ \ / / _ \ '__/ __| |/ _ \| '_ \ |_ \ |_ \ __) | diff --git a/docs/source/Release_Notes.rst b/docs/source/Release_Notes.rst index 479d7a48ac..55ab2e5d08 100644 --- a/docs/source/Release_Notes.rst +++ b/docs/source/Release_Notes.rst @@ -571,15 +571,20 @@ stochastic generator of external load has been reintroduced. Version 3.33 (not released yet) ------------------------------- -**On the maintainance front,** we removed the ancient MSG interface which end-of-life was scheduled for 2020, the Java -bindings that was MSG-only and support for native builds on Windows (WSL is now required). Keeping SimGrid alive while -adding new features require to remove old, unused stuff. The very rare users impacted by these removals are urged to +**On the maintainance front,** we removed the ancient MSG interface which end-of-life was scheduled for 2020, the Java bindings +that was MSG-only, support for native builds on Windows (WSL is now required) and support for 32 bits platforms. Keeping SimGrid +alive while adding new features require to remove old, unused stuff. The very rare users impacted by these removals are urged to move to the new API and systems. +We also conducted many internal refactorings to remove any occurence of "surf" and "simix". SimGrid v3.12 used a layered design +where simix was providing synchronizations to actors, on top of surf which was computing the models. These features are now +provided in modules, not layers. Surf became the kernel::{lmm, resource, routing, timer, xml} modules while simix became +the kernel::{activity, actor, context} modules. + **On the model front,** we realized an idea that has been on the back of our minds for quite some time. The question was: could we use something in the line of the ptask model, that mixes computations and network transfers in a single fluid activity, to simulate a *fluid I/O stream activity* that would consume both disk and network resources? This -remained an open question for years, mainly because the implementation of the ptask doesn't rely on the LMM solver as +remained an open question for years, mainly because the implementation of the ptask does not rely on the LMM solver as the other models do. The *fair bottleneck* solver is convenient, but with less solid theoretical bases and the development of its replacement (the *bmf solver*) is still ongoing. However, this combination of I/Os and communications seemed easier as these activities share the same unit (bytes). @@ -590,11 +595,36 @@ creates a classical NetworkAction, but add some I/O-related constraints to it. A and done! A single activity mixing I/Os and communications can be created whose progress is limited by the resource (Disk or Link) of least bandwidth value. +We also modified the Wi-Fi model so that the total capacity of a link depends on the amout of flows on that link, accordingly to +the result of some ns-3 experiments. This model can be more accurate for congestioned Wi-Fi links, but its calibration is more +demanding, as shown in the `example +`_ and in the `research +paper `_. + +We also worked on the usability of our models, by actually writing the long overdue documentation of our TCP models and by renaming +some options for clarity (old names are still accepted as aliases). A new function ``s4u::Engine::flatify_platform()`` dumps an +XML representation that is inefficient (all zones are flatified) but easier to read (routes are explicitely defined). You should +not use the output as a regular input file, but it will prove useful to double-check the your platform. + **On the interface front**, the new ``Io::streamto()`` function has been inspired by the existing ``Comm::sendto()`` function (which also derives from the ptask model). The user can specify a ``src_disk`` on a ``src_host`` and a ``dst_disk`` on a ``dst_host`` to stream data of a given ``size``. Note that disks are optional, allowing users to simulate some kind of "disk-to-memory" or "memory-to-disk" I/O streams. +As usual on that front, some functions were deprecated and will be removed in 4 versions, while some old deprecated functions +were removed in this version. + +**On the model checking front**, we are almost done with the ongoing refactoring to ensure that the model-checker don't read +directly the memory of the application beside checkpoint/restore and state equality. Instead, the network protocol is used to +retrieve the information, which makes the code much easier to read and understand. We fixed a bug in the DPOR reduction which +resulted in some failures to be missed by the exploration. We started implementing the UDPOR (Unfoldings DPOR) reduction +algorithm, and it will certainly be part of the next release. + +We also extended the sthread module, which allows to intercept simple code that use pthread mutex and semaphores to simulate and +verify it. You do not even need to recompile your code, as it uses LD_PRELOAD to intercept on the target functions. This module +is still rather young, but it could already reveal useful to verify the code written by students in a class on UNIX IPC and +synchronization. Check `the examples `_. + .. |br| raw:: html
diff --git a/examples/cpp/synchro-condition-variable-waituntil/s4u-synchro-condition-variable-waituntil.cpp b/examples/cpp/synchro-condition-variable-waituntil/s4u-synchro-condition-variable-waituntil.cpp index 0edd2ab68d..67d1ac27b1 100644 --- a/examples/cpp/synchro-condition-variable-waituntil/s4u-synchro-condition-variable-waituntil.cpp +++ b/examples/cpp/synchro-condition-variable-waituntil/s4u-synchro-condition-variable-waituntil.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 /* std::mutex and std::lock_guard */ +#include /* std::mutex and std::scoped_lock */ #include /* All of S4U */ XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_test, "a sample log category"); @@ -12,13 +12,12 @@ namespace sg4 = simgrid::s4u; static void competitor(int id, sg4::ConditionVariablePtr cv, sg4::MutexPtr mtx, std::shared_ptr ready) { XBT_INFO("Entering the race..."); - std::unique_lock lck(*mtx); + std::unique_lock lock(*mtx); while (not *ready) { auto now = sg4::Engine::get_clock(); - if (cv->wait_until(lck, now + (id+1)*0.25) == std::cv_status::timeout) { + if (cv->wait_until(lock, now + (id + 1) * 0.25) == std::cv_status::timeout) { XBT_INFO("Out of wait_until (timeout)"); - } - else { + } else { XBT_INFO("Out of wait_until (YAY!)"); } } @@ -29,7 +28,7 @@ static void go(sg4::ConditionVariablePtr cv, sg4::MutexPtr mtx, std::shared_ptr< { XBT_INFO("Are you ready? ..."); sg4::this_actor::sleep_for(3); - std::unique_lock lck(*mtx); + const std::scoped_lock lock(*mtx); XBT_INFO("Go go go!"); *ready = true; cv->notify_all(); diff --git a/examples/cpp/synchro-condition-variable/s4u-synchro-condition-variable.cpp b/examples/cpp/synchro-condition-variable/s4u-synchro-condition-variable.cpp index cf1a1db372..b471b658d8 100644 --- a/examples/cpp/synchro-condition-variable/s4u-synchro-condition-variable.cpp +++ b/examples/cpp/synchro-condition-variable/s4u-synchro-condition-variable.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 /* std::mutex and std::lock_guard */ +#include /* std::mutex and std::scoped_lock */ #include /* All of S4U */ XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_test, "a sample log category"); @@ -11,7 +11,7 @@ namespace sg4 = simgrid::s4u; static void worker_fun(sg4::ConditionVariablePtr cv, sg4::MutexPtr mutex, std::string& data, bool& done) { - std::unique_lock lock(*mutex); + const std::scoped_lock lock(*mutex); XBT_INFO("Start processing data which is '%s'.", data.c_str()); data += " after processing"; @@ -34,7 +34,7 @@ static void master_fun() std::ref(done)); // wait for the worker - cv->wait(std::unique_lock(*mutex), [&done]() { return done; }); + cv->wait(std::unique_lock(*mutex), [&done]() { return done; }); XBT_INFO("data is now '%s'.", data.c_str()); worker->join(); diff --git a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp index 429fccd068..bab673122f 100644 --- a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp +++ b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp @@ -5,7 +5,7 @@ #include "simgrid/s4u.hpp" /* All of S4U */ #include "xbt/config.hpp" -#include /* std::mutex and std::lock_guard */ +#include /* std::mutex and std::scoped_lock */ namespace sg4 = simgrid::s4u; @@ -29,14 +29,14 @@ static void worker(sg4::MutexPtr mutex, int& result) mutex->unlock(); } -static void workerLockGuard(sg4::MutexPtr mutex, int& result) +static void workerScopedLock(sg4::MutexPtr mutex, int& result) { - // Simply use the std::lock_guard like this + // Simply use the std::scoped_lock like this // It's like a lock() that would do the unlock() automatically when getting out of scope - std::lock_guard lock(*mutex); + const std::scoped_lock lock(*mutex); // then you are in a safe zone - XBT_INFO("Hello s4u, I'm ready to compute after a lock_guard"); + XBT_INFO("Hello s4u, I'm ready to compute after a scoped_lock"); // update the results result += 1; XBT_INFO("I'm done, good bye"); @@ -54,7 +54,7 @@ int main(int argc, char** argv) for (int i = 0; i < cfg_actor_count; i++) { sg4::MutexPtr mutex = sg4::Mutex::create(); - sg4::Actor::create("worker", sg4::Host::by_name("Jupiter"), workerLockGuard, mutex, std::ref(result[i])); + sg4::Actor::create("worker", sg4::Host::by_name("Jupiter"), workerScopedLock, mutex, std::ref(result[i])); sg4::Actor::create("worker", sg4::Host::by_name("Tremblay"), worker, mutex, std::ref(result[i])); } diff --git a/examples/python/app-masterworkers/app-masterworkers.py b/examples/python/app-masterworkers/app-masterworkers.py index 4c146f2761..856d9e387e 100644 --- a/examples/python/app-masterworkers/app-masterworkers.py +++ b/examples/python/app-masterworkers/app-masterworkers.py @@ -56,7 +56,7 @@ def worker(*args): # main-begin if __name__ == '__main__': - assert len(sys.argv) > 2, f"Usage: python app-masterworkers.py platform_file deployment_file" + assert len(sys.argv) > 2, "Usage: python app-masterworkers.py platform_file deployment_file" e = Engine(sys.argv) diff --git a/examples/python/comm-failure/comm-failure.py b/examples/python/comm-failure/comm-failure.py index 91ec73d3b5..4b70b33f7a 100644 --- a/examples/python/comm-failure/comm-failure.py +++ b/examples/python/comm-failure/comm-failure.py @@ -18,14 +18,14 @@ def sender(mailbox1_name: str, mailbox2_name: str) -> None: this_actor.info(f"Initiating asynchronous send to {mailbox2.name}") comm2: Comm = mailbox2.put_async(666, 2) - this_actor.info(f"Calling wait_any..") + this_actor.info("Calling wait_any..") pending_comms = [comm1, comm2] try: index = Comm.wait_any([comm1, comm2]) this_actor.info(f"Wait any returned index {index} (comm to {pending_comms[index].mailbox.name})") except NetworkFailureException: - this_actor.info(f"Sender has experienced a network failure exception, so it knows that something went wrong") - this_actor.info(f"Now it needs to figure out which of the two comms failed by looking at their state:") + this_actor.info("Sender has experienced a network failure exception, so it knows that something went wrong") + this_actor.info("Now it needs to figure out which of the two comms failed by looking at their state:") this_actor.info(f" Comm to {comm1.mailbox.name} has state: {comm1.state_str}") this_actor.info(f" Comm to {comm2.mailbox.name} has state: {comm2.state_str}") diff --git a/examples/python/comm-suspend/comm-suspend.py b/examples/python/comm-suspend/comm-suspend.py index badf0911f1..85646ed4d6 100644 --- a/examples/python/comm-suspend/comm-suspend.py +++ b/examples/python/comm-suspend/comm-suspend.py @@ -43,7 +43,7 @@ def sender(): comm.resume() comm.wait() this_actor.info(f"There is {comm.remaining:.0f} bytes to transfer after the communication completion.") - this_actor.info(f"Suspending a completed activity is a no-op.") + this_actor.info("Suspending a completed activity is a no-op.") comm.suspend() diff --git a/examples/python/platform-failures/platform-failures.py b/examples/python/platform-failures/platform-failures.py index 51766582d4..9850ab45c7 100644 --- a/examples/python/platform-failures/platform-failures.py +++ b/examples/python/platform-failures/platform-failures.py @@ -82,7 +82,7 @@ def sleeper(): this_actor.info("done sleeping.") if __name__ == '__main__': - assert len(sys.argv) > 2, f"Usage: python app-masterworkers.py platform_file deployment_file" + assert len(sys.argv) > 2, "Usage: python app-masterworkers.py platform_file deployment_file" e = Engine(sys.argv) diff --git a/examples/python/synchro-barrier/synchro-barrier.py b/examples/python/synchro-barrier/synchro-barrier.py index f1f6fae65f..6b81a1d7b0 100644 --- a/examples/python/synchro-barrier/synchro-barrier.py +++ b/examples/python/synchro-barrier/synchro-barrier.py @@ -30,7 +30,7 @@ def worker(barrier: Barrier): """ Wait on the barrier and exits. :param barrier: Barrier to be awaited """ - this_actor.info(f"Waiting on the barrier") + this_actor.info("Waiting on the barrier") barrier.wait() this_actor.info("Bye") @@ -45,7 +45,7 @@ def master(actor_count: int): this_actor.info(f"Spawning {workers_count} workers") for i in range(workers_count): Actor.create(f"worker-{i}", Host.by_name("Jupiter"), worker, barrier) - this_actor.info(f"Waiting on the barrier") + this_actor.info("Waiting on the barrier") barrier.wait() this_actor.info("Bye") diff --git a/examples/python/synchro-mutex/synchro-mutex.py b/examples/python/synchro-mutex/synchro-mutex.py index 298de0bb70..1a202ba875 100644 --- a/examples/python/synchro-mutex/synchro-mutex.py +++ b/examples/python/synchro-mutex/synchro-mutex.py @@ -35,9 +35,9 @@ class ResultHolder: def worker_context_manager(mutex: Mutex, result: ResultHolder): # When using a context manager, the lock and the unlock are automatic. This is the easiest approach with mutex: - this_actor.info(f"Hello simgrid, I'm ready to compute after acquiring the mutex from a context manager") + this_actor.info("Hello simgrid, I'm ready to compute after acquiring the mutex from a context manager") result.value += 1 - this_actor.info(f"I'm done, good bye") + this_actor.info("I'm done, good bye") def worker(mutex: Mutex, result: ResultHolder): diff --git a/examples/sthread/CMakeLists.txt b/examples/sthread/CMakeLists.txt index a59d61f650..d53f419c2c 100644 --- a/examples/sthread/CMakeLists.txt +++ b/examples/sthread/CMakeLists.txt @@ -5,7 +5,8 @@ find_package(Threads REQUIRED) ######################################################################### foreach(x - mutex-simple) + mutex-simple + producer-consumer) if("${CMAKE_SYSTEM}" MATCHES "Linux") add_executable (pthread-${x} EXCLUDE_FROM_ALL pthread-${x}.c) diff --git a/examples/sthread/pthread-mc-producer-consumer.tesh b/examples/sthread/pthread-mc-producer-consumer.tesh new file mode 100644 index 0000000000..c2714170ea --- /dev/null +++ b/examples/sthread/pthread-mc-producer-consumer.tesh @@ -0,0 +1,7 @@ +# We ignore the LD_PRELOAD lines from the expected output because they contain the build path +! ignore .*LD_PRELOAD.* + +$ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q +> [0.000000] [sthread/INFO] Starting the simulation. +> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1819 unique states visited; 108 backtracks (6808 transition replays, 4882 states visited overall) \ No newline at end of file diff --git a/examples/sthread/pthread-mutex-simple.c b/examples/sthread/pthread-mutex-simple.c index d97bfe8ca1..1d391418ba 100644 --- a/examples/sthread/pthread-mutex-simple.c +++ b/examples/sthread/pthread-mutex-simple.c @@ -21,8 +21,8 @@ int main(int argc, char* argv[]) int id[2] = {0, 1}; pthread_t thread1; pthread_t thread2; - pthread_create(&thread1, NULL, thread_fun, (void*)&id[0]); - pthread_create(&thread2, NULL, thread_fun, (void*)&id[1]); + pthread_create(&thread1, NULL, thread_fun, &id[0]); + pthread_create(&thread2, NULL, thread_fun, &id[1]); fprintf(stderr, "All threads are started.\n"); pthread_join(thread1, NULL); pthread_join(thread2, NULL); diff --git a/examples/sthread/pthread-mutex-simpledeadlock.c b/examples/sthread/pthread-mutex-simpledeadlock.c index 433852af05..09be6c11ea 100644 --- a/examples/sthread/pthread-mutex-simpledeadlock.c +++ b/examples/sthread/pthread-mutex-simpledeadlock.c @@ -39,8 +39,8 @@ int main(int argc, char* argv[]) int id[2] = {0, 1}; pthread_t thread1; pthread_t thread2; - pthread_create(&thread1, NULL, thread_fun1, (void*)&id[0]); - pthread_create(&thread2, NULL, thread_fun2, (void*)&id[1]); + pthread_create(&thread1, NULL, thread_fun1, &id[0]); + pthread_create(&thread2, NULL, thread_fun2, &id[1]); fprintf(stderr, "All threads are started.\n"); pthread_join(thread1, NULL); pthread_join(thread2, NULL); diff --git a/examples/sthread/pthread-producer-consumer.c b/examples/sthread/pthread-producer-consumer.c new file mode 100644 index 0000000000..8fd1a0b16b --- /dev/null +++ b/examples/sthread/pthread-producer-consumer.c @@ -0,0 +1,84 @@ +/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +/* Simple producer/consumer example with pthreads and semaphores */ + +#include +#include +#include +#include +#include + +#define AmountProduced 3 /* Amount of items produced by a producer */ +#define AmountConsumed 3 /* Amount of items consumed by a consumer */ +#define ProducerCount 2 /* Amount of producer threads*/ +#define ConsumerCount 2 /* Amount of consumer threads*/ +#define BufferSize 4 /* Size of the buffer */ + +sem_t empty; +sem_t full; +int in = 0; +int out = 0; +int buffer[BufferSize]; +pthread_mutex_t mutex; +int do_output = 1; + +static void* producer(void* id) +{ + for (int i = 0; i < AmountProduced; i++) { + sem_wait(&empty); + pthread_mutex_lock(&mutex); + buffer[in] = i; + if (do_output) + fprintf(stderr, "Producer %d: Insert Item %d at %d\n", *((int*)id), buffer[in], in); + in = (in + 1) % BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&full); + } + return NULL; +} +static void* consumer(void* id) +{ + for (int i = 0; i < AmountConsumed; i++) { + sem_wait(&full); + pthread_mutex_lock(&mutex); + int item = buffer[out]; + if (do_output) + fprintf(stderr, "Consumer %d: Remove Item %d from %d\n", *((int*)id), item, out); + out = (out + 1) % BufferSize; + pthread_mutex_unlock(&mutex); + sem_post(&empty); + } + return NULL; +} + +int main(int argc, char** argv) +{ + if (argc == 2 && strcmp(argv[1], "-q") == 0) + do_output = 0; + pthread_t pro[2]; + pthread_t con[2]; + pthread_mutex_init(&mutex, NULL); + sem_init(&empty, 0, BufferSize); + sem_init(&full, 0, 0); + + int ids[10] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}; // The identity of each thread (for debug messages) + + for (int i = 0; i < ProducerCount; i++) + pthread_create(&pro[i], NULL, producer, &ids[i]); + for (int i = 0; i < ConsumerCount; i++) + pthread_create(&con[i], NULL, consumer, &ids[i]); + + for (int i = 0; i < ProducerCount; i++) + pthread_join(pro[i], NULL); + for (int i = 0; i < ConsumerCount; i++) + pthread_join(con[i], NULL); + + pthread_mutex_destroy(&mutex); + sem_destroy(&empty); + sem_destroy(&full); + + return 0; +} diff --git a/examples/sthread/pthread-producer-consumer.tesh b/examples/sthread/pthread-producer-consumer.tesh new file mode 100644 index 0000000000..0c035f018e --- /dev/null +++ b/examples/sthread/pthread-producer-consumer.tesh @@ -0,0 +1,15 @@ +$ env ASAN_OPTIONS=verify_asan_link_order=0:$ASAN_OPTIONS LD_PRELOAD=${libdir:=.}/libsthread.so ./pthread-producer-consumer +> [0.000000] [sthread/INFO] Starting the simulation. +> Producer 1: Insert Item 0 at 0 +> Producer 2: Insert Item 0 at 1 +> Consumer 1: Remove Item 0 from 0 +> Producer 1: Insert Item 1 at 2 +> Consumer 2: Remove Item 0 from 1 +> Producer 2: Insert Item 1 at 3 +> Consumer 1: Remove Item 1 from 2 +> Producer 1: Insert Item 2 at 0 +> Consumer 2: Remove Item 1 from 3 +> Producer 2: Insert Item 2 at 1 +> Consumer 1: Remove Item 2 from 0 +> Consumer 2: Remove Item 2 from 1 +> [0.000000] [sthread/INFO] All threads exited. Terminating the simulation. diff --git a/examples/sthread/sthread-mutex-simple.c b/examples/sthread/sthread-mutex-simple.c index 76fa009c94..dccec547f7 100644 --- a/examples/sthread/sthread-mutex-simple.c +++ b/examples/sthread/sthread-mutex-simple.c @@ -21,8 +21,8 @@ int main(int argc, char* argv[]) int id[2] = {0, 1}; sthread_t thread1; sthread_t thread2; - sthread_create(&thread1, NULL, thread_fun, (void*)&id[0]); - sthread_create(&thread2, NULL, thread_fun, (void*)&id[1]); + sthread_create(&thread1, NULL, thread_fun, &id[0]); + sthread_create(&thread2, NULL, thread_fun, &id[1]); fprintf(stderr, "All threads are started.\n"); sthread_join(thread1, NULL); sthread_join(thread2, NULL); diff --git a/include/simgrid/Exception.hpp b/include/simgrid/Exception.hpp index 5747ce1f44..ca94f51416 100644 --- a/include/simgrid/Exception.hpp +++ b/include/simgrid/Exception.hpp @@ -32,7 +32,7 @@ class ThrowPoint { public: ThrowPoint() = default; explicit ThrowPoint(const char* file, int line, const char* function, Backtrace&& bt, std::string&& actor_name, - int pid) + aid_t pid) : file_(file) , line_(line) , function_(function) @@ -47,7 +47,7 @@ public: const char* function_ = nullptr; Backtrace backtrace_; std::string procname_ = ""; /**< Name of the process who thrown this */ - int pid_ = 0; /**< PID of the process who thrown this */ + aid_t pid_ = 0; /**< PID of the process who thrown this */ }; /** Create a ThrowPoint with (__FILE__, __LINE__, __func__) */ diff --git a/include/simgrid/plugins/ProducerConsumer.hpp b/include/simgrid/plugins/ProducerConsumer.hpp index 1ecaa1e6b1..55dc6d6644 100644 --- a/include/simgrid/plugins/ProducerConsumer.hpp +++ b/include/simgrid/plugins/ProducerConsumer.hpp @@ -104,7 +104,7 @@ public: */ ProducerConsumer* set_max_queue_size(unsigned int max_queue_size) { - std::unique_lock lock(*mutex_); + const std::lock_guard lock(*mutex_); max_queue_size_ = max_queue_size; return this; } diff --git a/src/kernel/EngineImpl.cpp b/src/kernel/EngineImpl.cpp index 6b2da71b62..ff519e4b04 100644 --- a/src/kernel/EngineImpl.cpp +++ b/src/kernel/EngineImpl.cpp @@ -178,8 +178,7 @@ void EngineImpl::initialize(int* argc, char** argv) simgrid::mc::AppSide::initialize(); #endif - static bool inited = false; - if (not inited) { + if (static bool inited = false; not inited) { inited = true; xbt_log_init(argc, argv); @@ -364,7 +363,7 @@ void EngineImpl::handle_ended_actions() const if (action->get_activity()->get_actor() == maestro_) action->get_activity()->get_iface()->complete(s4u::Activity::State::FAILED); - activity::ActivityImplPtr(action->get_activity())->post(); + activity::ActivityImplPtr(action->get_activity())->finish(); } } XBT_DEBUG("Handling the terminated actions (if any)"); @@ -377,7 +376,7 @@ void EngineImpl::handle_ended_actions() const if (action->get_activity()->get_actor() == maestro_) action->get_activity()->get_iface()->complete(s4u::Activity::State::FINISHED); - activity::ActivityImplPtr(action->get_activity())->post(); + activity::ActivityImplPtr(action->get_activity())->finish(); } } } diff --git a/src/kernel/EngineImpl.hpp b/src/kernel/EngineImpl.hpp index ab1ea0711f..68624091c3 100644 --- a/src/kernel/EngineImpl.hpp +++ b/src/kernel/EngineImpl.hpp @@ -58,6 +58,7 @@ class EngineImpl { friend s4u::Engine; std::vector cmdline_; // Copy of the argv we got (including argv[0]) + public: EngineImpl() = default; diff --git a/src/kernel/activity/ActivityImpl.cpp b/src/kernel/activity/ActivityImpl.cpp index 5d7c92222a..f425dc8eff 100644 --- a/src/kernel/activity/ActivityImpl.cpp +++ b/src/kernel/activity/ActivityImpl.cpp @@ -115,9 +115,9 @@ void ActivityImpl::wait_for(actor::ActorImpl* issuer, double timeout) sleep_action->set_activity(comm); if (issuer == comm->src_actor_) - comm->src_timeout_ = sleep_action; + comm->src_timeout_.reset(sleep_action); else - comm->dst_timeout_ = sleep_action; + comm->dst_timeout_.reset(sleep_action); } else { SynchroImplPtr synchro(new SynchroImpl([this, issuer]() { this->unregister_simcall(&issuer->simcall_); @@ -236,4 +236,5 @@ void intrusive_ptr_release(ActivityImpl* activity) delete activity; } } + } // namespace simgrid::kernel::activity diff --git a/src/kernel/activity/ActivityImpl.hpp b/src/kernel/activity/ActivityImpl.hpp index d974e2963f..cbabdcdc03 100644 --- a/src/kernel/activity/ActivityImpl.hpp +++ b/src/kernel/activity/ActivityImpl.hpp @@ -79,11 +79,8 @@ public: virtual void resume(); virtual void cancel(); - virtual void post() = 0; // Called by the main loop when the activity is marked as terminated or failed by its model. - // Setups the status, clean things up, and call finish() virtual void set_exception(actor::ActorImpl* issuer) = 0; // Raising exceptions and stuff - virtual void finish() = 0; // Unlock all simcalls blocked on that activity, either because it was marked as done by - // the model or because it terminated without waiting for the model + virtual void finish() = 0; // Setups the status, clean things up, unlock all simcalls blocked on that activity. s4u::Host* get_host() const { return hosts_.front(); } const std::vector& get_hosts() const { return hosts_; }; diff --git a/src/kernel/activity/BarrierImpl.cpp b/src/kernel/activity/BarrierImpl.cpp index af28aedd0b..7b6436e819 100644 --- a/src/kernel/activity/BarrierImpl.cpp +++ b/src/kernel/activity/BarrierImpl.cpp @@ -28,6 +28,7 @@ void BarrierAcquisitionImpl::wait_for(actor::ActorImpl* issuer, double timeout) // Already in the queue } } + void BarrierAcquisitionImpl::finish() { xbt_assert(simcalls_.size() == 1, "Unexpected number of simcalls waiting: %zu", simcalls_.size()); diff --git a/src/kernel/activity/BarrierImpl.hpp b/src/kernel/activity/BarrierImpl.hpp index dd59753329..c4dd9e03a6 100644 --- a/src/kernel/activity/BarrierImpl.hpp +++ b/src/kernel/activity/BarrierImpl.hpp @@ -32,9 +32,6 @@ public: bool test(actor::ActorImpl* issuer = nullptr) override; void wait_for(actor::ActorImpl* issuer, double timeout) override; - void post() override - { /* no model action */ - } void finish() override; void set_exception(actor::ActorImpl* issuer) override { /* nothing to do */ diff --git a/src/kernel/activity/CommImpl.cpp b/src/kernel/activity/CommImpl.cpp index 96439ae8bb..3a0b63c28e 100644 --- a/src/kernel/activity/CommImpl.cpp +++ b/src/kernel/activity/CommImpl.cpp @@ -96,7 +96,7 @@ CommImpl::~CommImpl() { XBT_DEBUG("Really free communication %p in state %s (detached = %d)", this, get_state_str(), detached_); - cleanup_surf(); + clean_action(); if (detached_ && get_state() != State::DONE) { /* the communication has failed and was detached: @@ -139,7 +139,7 @@ CommImpl* CommImpl::start() XBT_DEBUG("Communication from '%s' to '%s' failed to start because of a link failure", from_->get_cname(), to_->get_cname()); set_state(State::LINK_FAILURE); - post(); + finish(); } else if ((src_actor_ != nullptr && src_actor_->is_suspended()) || (dst_actor_ != nullptr && dst_actor_->is_suspended())) { @@ -397,52 +397,6 @@ void CommImpl::cancel() } } -/** @brief This is part of the cleanup process, probably an internal command */ -void CommImpl::cleanup_surf() -{ - clean_action(); - - if (src_timeout_) { - src_timeout_->unref(); - src_timeout_ = nullptr; - } - - if (dst_timeout_) { - dst_timeout_->unref(); - dst_timeout_ = nullptr; - } -} - -void CommImpl::post() -{ - on_completion(*this); - - /* Update synchro state */ - if (src_timeout_ && src_timeout_->get_state() == resource::Action::State::FINISHED) - set_state(State::SRC_TIMEOUT); - else if (dst_timeout_ && dst_timeout_->get_state() == resource::Action::State::FINISHED) - set_state(State::DST_TIMEOUT); - else if ((from_ && not from_->is_on()) || (src_timeout_ && src_timeout_->get_state() == resource::Action::State::FAILED)) - set_state(State::SRC_HOST_FAILURE); - else if ((to_ && not to_->is_on()) || (dst_timeout_ && dst_timeout_->get_state() == resource::Action::State::FAILED)) - set_state(State::DST_HOST_FAILURE); - else if (model_action_ && model_action_->get_state() == resource::Action::State::FAILED) { - set_state(State::LINK_FAILURE); - } else if (get_state() == State::RUNNING) { - xbt_assert(from_ && from_->is_on()); - xbt_assert(to_ && to_->is_on()); - set_state(State::DONE); - } - - XBT_DEBUG("CommImpl::post(): comm %p, state %s, src_proc %p, dst_proc %p, detached: %d", this, get_state_str(), - src_actor_.get(), dst_actor_.get(), detached_); - - /* destroy the model actions associated with the communication activity */ - cleanup_surf(); - - /* Answer all simcalls associated with the synchro */ - finish(); -} void CommImpl::set_exception(actor::ActorImpl* issuer) { switch (get_state()) { @@ -510,7 +464,32 @@ void CommImpl::set_exception(actor::ActorImpl* issuer) void CommImpl::finish() { - XBT_DEBUG("CommImpl::finish() in state %s", get_state_str()); + XBT_DEBUG("CommImpl::finish() comm %p, state %s, src_proc %p, dst_proc %p, detached: %d", this, get_state_str(), + src_actor_.get(), dst_actor_.get(), detached_); + + on_completion(*this); + + /* Update synchro state */ + if (src_timeout_ && src_timeout_->get_state() == resource::Action::State::FINISHED) + set_state(State::SRC_TIMEOUT); + else if (dst_timeout_ && dst_timeout_->get_state() == resource::Action::State::FINISHED) + set_state(State::DST_TIMEOUT); + else if ((from_ && not from_->is_on()) || + (src_timeout_ && src_timeout_->get_state() == resource::Action::State::FAILED)) + set_state(State::SRC_HOST_FAILURE); + else if ((to_ && not to_->is_on()) || (dst_timeout_ && dst_timeout_->get_state() == resource::Action::State::FAILED)) + set_state(State::DST_HOST_FAILURE); + else if (model_action_ && model_action_->get_state() == resource::Action::State::FAILED) { + set_state(State::LINK_FAILURE); + } else if (get_state() == State::RUNNING) { + xbt_assert(from_ && from_->is_on()); + xbt_assert(to_ && to_->is_on()); + set_state(State::DONE); + } + + /* destroy the model actions associated with the communication activity */ + clean_action(); + /* If the synchro is still in a rendez-vous point then remove from it */ if (mbox_) mbox_->remove(this); diff --git a/src/kernel/activity/CommImpl.hpp b/src/kernel/activity/CommImpl.hpp index c2758ab718..32fef45acf 100644 --- a/src/kernel/activity/CommImpl.hpp +++ b/src/kernel/activity/CommImpl.hpp @@ -14,9 +14,10 @@ namespace simgrid::kernel::activity { enum class CommImplType { SEND, RECEIVE }; +using timeout_action_type = std::unique_ptr>; + class XBT_PUBLIC CommImpl : public ActivityImpl_T { ~CommImpl() override; - void cleanup_surf(); static std::function copy_data_callback_; @@ -69,7 +70,6 @@ public: void suspend() override; void resume() override; void cancel() override; - void post() override; void set_exception(actor::ActorImpl* issuer) override; void finish() override; @@ -80,8 +80,9 @@ expectations of the other side, too. See */ std::function copy_data_fun; /* Model actions */ - resource::Action* src_timeout_ = nullptr; /* represents the timeout set by the sender */ - resource::Action* dst_timeout_ = nullptr; /* represents the timeout set by the receiver */ + timeout_action_type src_timeout_{nullptr, [](resource::Action* a) { a->unref(); }}; /* timeout set by the sender */ + timeout_action_type dst_timeout_{nullptr, [](resource::Action* a) { a->unref(); }}; /* timeout set by the receiver */ + actor::ActorImplPtr src_actor_ = nullptr; actor::ActorImplPtr dst_actor_ = nullptr; diff --git a/src/kernel/activity/ExecImpl.cpp b/src/kernel/activity/ExecImpl.cpp index 88432f686d..6d66a12f54 100644 --- a/src/kernel/activity/ExecImpl.cpp +++ b/src/kernel/activity/ExecImpl.cpp @@ -41,15 +41,6 @@ ExecImpl& ExecImpl::set_hosts(const std::vector& hosts) return *this; } -ExecImpl& ExecImpl::set_timeout(double timeout) -{ - if (timeout >= 0 && not MC_is_active() && not MC_record_replay_is_active()) { - timeout_detector_.reset(get_host()->get_cpu()->sleep(timeout)); - timeout_detector_->set_activity(this); - } - return *this; -} - ExecImpl& ExecImpl::set_flops_amount(double flops_amount) { flops_amounts_.assign(1, flops_amount); @@ -142,36 +133,6 @@ ExecImpl& ExecImpl::update_sharing_penalty(double sharing_penalty) return *this; } -void ExecImpl::post() -{ - xbt_assert(model_action_ != nullptr); - if (auto const& hosts = get_hosts(); - std::any_of(hosts.begin(), hosts.end(), [](const s4u::Host* host) { return not host->is_on(); })) { - /* If one of the hosts running the synchro failed, notice it. This way, the asking - * process can be killed if it runs on that host itself */ - set_state(State::FAILED); - } else if (model_action_->get_state() == resource::Action::State::FAILED) { - /* If all the hosts are running the synchro didn't fail, then the synchro was canceled */ - set_state(State::CANCELED); - } else if (timeout_detector_ && timeout_detector_->get_state() == resource::Action::State::FINISHED && - model_action_->get_remains() > 0.0) { - model_action_->set_state(resource::Action::State::FAILED); - set_state(State::TIMEOUT); - } else { - set_state(State::DONE); - } - - clean_action(); - timeout_detector_.reset(); - if (get_actor() != nullptr) { - get_actor()->activities_.erase(this); - } - if (get_state() != State::FAILED && cb_id_ >= 0) - s4u::Host::on_state_change.disconnect(cb_id_); - /* Answer all simcalls associated with the synchro */ - finish(); -} - void ExecImpl::set_exception(actor::ActorImpl* issuer) { switch (get_state()) { @@ -199,6 +160,28 @@ void ExecImpl::set_exception(actor::ActorImpl* issuer) void ExecImpl::finish() { XBT_DEBUG("ExecImpl::finish() in state %s", get_state_str()); + if (model_action_ != nullptr) { + if (auto const& hosts = get_hosts(); + std::any_of(hosts.begin(), hosts.end(), [](const s4u::Host* host) { return not host->is_on(); })) { + /* If one of the hosts running the synchro failed, notice it. This way, the asking + * process can be killed if it runs on that host itself */ + set_state(State::FAILED); + } else if (model_action_->get_state() == resource::Action::State::FAILED) { + /* If all the hosts are running the synchro didn't fail, then the synchro was canceled */ + set_state(State::CANCELED); + } else { + set_state(State::DONE); + } + + clean_action(); + } + + if (get_actor() != nullptr) + get_actor()->activities_.erase(this); + + if (get_state() != State::FAILED && cb_id_ >= 0) + s4u::Host::on_state_change.disconnect(cb_id_); + while (not simcalls_.empty()) { actor::Simcall* simcall = simcalls_.front(); simcalls_.pop_front(); diff --git a/src/kernel/activity/ExecImpl.hpp b/src/kernel/activity/ExecImpl.hpp index d75bf41ae8..286bf33cc1 100644 --- a/src/kernel/activity/ExecImpl.hpp +++ b/src/kernel/activity/ExecImpl.hpp @@ -14,8 +14,6 @@ namespace simgrid::kernel::activity { class XBT_PUBLIC ExecImpl : public ActivityImpl_T { - std::unique_ptr> timeout_detector_{ - nullptr, [](resource::Action* a) { a->unref(); }}; double sharing_penalty_ = 1.0; double bound_ = 0.0; std::vector flops_amounts_; @@ -26,7 +24,6 @@ class XBT_PUBLIC ExecImpl : public ActivityImpl_T { public: ExecImpl(); - ExecImpl& set_timeout(double timeout) override; ExecImpl& set_bound(double bound); ExecImpl& set_sharing_penalty(double sharing_penalty); ExecImpl& update_sharing_penalty(double sharing_penalty); @@ -49,7 +46,6 @@ public: virtual ActivityImpl* migrate(s4u::Host* to); ExecImpl* start(); - void post() override; void set_exception(actor::ActorImpl* issuer) override; void finish() override; diff --git a/src/kernel/activity/IoImpl.cpp b/src/kernel/activity/IoImpl.cpp index d270c4fbb7..1a7e46fd9e 100644 --- a/src/kernel/activity/IoImpl.cpp +++ b/src/kernel/activity/IoImpl.cpp @@ -38,14 +38,6 @@ IoImpl& IoImpl::update_sharing_penalty(double sharing_penalty) return *this; } -IoImpl& IoImpl::set_timeout(double timeout) -{ - const s4u::Host* host = get_disk()->get_host(); - timeout_detector_ = host->get_cpu()->sleep(timeout); - timeout_detector_->set_activity(this); - return *this; -} - IoImpl& IoImpl::set_type(s4u::Io::OpType type) { type_ = type; @@ -103,36 +95,6 @@ IoImpl* IoImpl::start() return this; } -void IoImpl::post() -{ - performed_ioops_ = model_action_->get_cost(); - if (model_action_->get_state() == resource::Action::State::FAILED) { - if (host_ && dst_host_) { // this is an I/O stream - if (not host_->is_on()) - set_state(State::SRC_HOST_FAILURE); - else if (not dst_host_->is_on()) - set_state(State::DST_HOST_FAILURE); - } else if ((disk_ && not disk_->is_on()) || (dst_disk_ && not dst_disk_->is_on())) - set_state(State::FAILED); - else - set_state(State::CANCELED); - } else if (timeout_detector_ && timeout_detector_->get_state() == resource::Action::State::FINISHED && - model_action_->get_remains() > 0.0) { - model_action_->set_state(resource::Action::State::FAILED); - set_state(State::TIMEOUT); - } else { - set_state(State::DONE); - } - - clean_action(); - if (timeout_detector_) { - timeout_detector_->unref(); - timeout_detector_ = nullptr; - } - - /* Answer all simcalls associated with the synchro */ - finish(); -} void IoImpl::set_exception(actor::ActorImpl* issuer) { switch (get_state()) { @@ -162,6 +124,25 @@ void IoImpl::set_exception(actor::ActorImpl* issuer) void IoImpl::finish() { XBT_DEBUG("IoImpl::finish() in state %s", get_state_str()); + if (model_action_ != nullptr) { + performed_ioops_ = model_action_->get_cost(); + if (model_action_->get_state() == resource::Action::State::FAILED) { + if (host_ && dst_host_) { // this is an I/O stream + if (not host_->is_on()) + set_state(State::SRC_HOST_FAILURE); + else if (not dst_host_->is_on()) + set_state(State::DST_HOST_FAILURE); + } else if ((disk_ && not disk_->is_on()) || (dst_disk_ && not dst_disk_->is_on())) + set_state(State::FAILED); + else + set_state(State::CANCELED); + } else { + set_state(State::DONE); + } + + clean_action(); + } + while (not simcalls_.empty()) { actor::Simcall* simcall = simcalls_.front(); simcalls_.pop_front(); diff --git a/src/kernel/activity/IoImpl.hpp b/src/kernel/activity/IoImpl.hpp index 0e3dd9fa28..6562f2e393 100644 --- a/src/kernel/activity/IoImpl.hpp +++ b/src/kernel/activity/IoImpl.hpp @@ -20,13 +20,11 @@ class XBT_PUBLIC IoImpl : public ActivityImpl_T { sg_size_t size_ = 0; s4u::Io::OpType type_ = s4u::Io::OpType::READ; sg_size_t performed_ioops_ = 0; - resource::Action* timeout_detector_ = nullptr; public: IoImpl(); IoImpl& set_sharing_penalty(double sharing_penalty); - IoImpl& set_timeout(double timeout) override; IoImpl& set_size(sg_size_t size); IoImpl& set_type(s4u::Io::OpType type); IoImpl& set_disk(resource::DiskImpl* disk); @@ -42,7 +40,6 @@ public: resource::DiskImpl* get_disk() const { return disk_; } IoImpl* start(); - void post() override; void set_exception(actor::ActorImpl* issuer) override; void finish() override; }; diff --git a/src/kernel/activity/MailboxImpl.cpp b/src/kernel/activity/MailboxImpl.cpp index 7bbb8152ce..cb49f3b2b8 100644 --- a/src/kernel/activity/MailboxImpl.cpp +++ b/src/kernel/activity/MailboxImpl.cpp @@ -71,14 +71,14 @@ void MailboxImpl::remove(const CommImplPtr& comm) /** @brief Removes all communication activities from a mailbox */ -void MailboxImpl::clear( bool do_post ) +void MailboxImpl::clear(bool do_finish) { // CommImpl::cancel() will remove the comm from the mailbox.. for (auto comm : done_comm_queue_) { comm->cancel(); comm->set_state(State::FAILED); - if(do_post) - comm->post(); + if (do_finish) + comm->finish(); } done_comm_queue_.clear(); @@ -87,8 +87,8 @@ void MailboxImpl::clear( bool do_post ) if (comm->get_state() == State::WAITING && not comm->is_detached()) { comm->cancel(); comm->set_state(State::FAILED); - if(do_post) - comm->post(); + if (do_finish) + comm->finish(); } else comm_queue_.pop_back(); } diff --git a/src/kernel/activity/MailboxImpl.hpp b/src/kernel/activity/MailboxImpl.hpp index fb84db7855..199fcd12cc 100644 --- a/src/kernel/activity/MailboxImpl.hpp +++ b/src/kernel/activity/MailboxImpl.hpp @@ -53,7 +53,7 @@ public: void push(CommImplPtr comm); void push_done(CommImplPtr done_comm) { done_comm_queue_.push_back(done_comm); } void remove(const CommImplPtr& comm); - void clear(bool do_post ); + void clear(bool do_finish); CommImplPtr iprobe(int type, const std::function& match_fun, void* data); CommImplPtr find_matching_comm(CommImplType type, const std::function& match_fun, void* this_user_data, const CommImplPtr& my_synchro, bool done, bool remove_matching); diff --git a/src/kernel/activity/MutexImpl.cpp b/src/kernel/activity/MutexImpl.cpp index 27a7bf9c00..43a511b9d3 100644 --- a/src/kernel/activity/MutexImpl.cpp +++ b/src/kernel/activity/MutexImpl.cpp @@ -30,6 +30,7 @@ void MutexAcquisitionImpl::wait_for(actor::ActorImpl* issuer, double timeout) // Already in the queue } } + void MutexAcquisitionImpl::finish() { xbt_assert(simcalls_.size() == 1, "Unexpected number of simcalls waiting: %zu", simcalls_.size()); diff --git a/src/kernel/activity/MutexImpl.hpp b/src/kernel/activity/MutexImpl.hpp index a614a775db..3eebec2b12 100644 --- a/src/kernel/activity/MutexImpl.hpp +++ b/src/kernel/activity/MutexImpl.hpp @@ -50,9 +50,6 @@ public: bool test(actor::ActorImpl* issuer = nullptr) override; void wait_for(actor::ActorImpl* issuer, double timeout) override; - void post() override - { /* no model action */ - } void finish() override; void set_exception(actor::ActorImpl* issuer) override { /* nothing to do */ diff --git a/src/kernel/activity/SemaphoreImpl.cpp b/src/kernel/activity/SemaphoreImpl.cpp index 2bb639663d..8cba364a5d 100644 --- a/src/kernel/activity/SemaphoreImpl.cpp +++ b/src/kernel/activity/SemaphoreImpl.cpp @@ -29,7 +29,7 @@ void SemAcquisitionImpl::wait_for(actor::ActorImpl* issuer, double timeout) this->register_simcall(&issuer_->simcall_); // Block on that acquisition if (granted_) { - post(); + finish(); } else if (timeout > 0) { model_action_ = get_issuer()->get_host()->get_cpu()->sleep(timeout); model_action_->set_activity(this); @@ -38,10 +38,6 @@ void SemAcquisitionImpl::wait_for(actor::ActorImpl* issuer, double timeout) // Already in the queue } } -void SemAcquisitionImpl::post() -{ - finish(); -} void SemAcquisitionImpl::finish() { xbt_assert(simcalls_.size() == 1, "Unexpected number of simcalls waiting: %zu", simcalls_.size()); @@ -108,7 +104,7 @@ void SemaphoreImpl::release() acqui->granted_ = true; if (acqui == acqui->get_issuer()->waiting_synchro_) - acqui->post(); + acqui->finish(); // else, the issuer is not blocked on this acquisition so no need to release it } else { diff --git a/src/kernel/activity/SemaphoreImpl.hpp b/src/kernel/activity/SemaphoreImpl.hpp index fb69aad60c..ebb439ba49 100644 --- a/src/kernel/activity/SemaphoreImpl.hpp +++ b/src/kernel/activity/SemaphoreImpl.hpp @@ -35,7 +35,6 @@ public: bool test(actor::ActorImpl* issuer = nullptr) override { return granted_; } void wait_for(actor::ActorImpl* issuer, double timeout) override; - void post() override; void finish() override; void cancel() override; void set_exception(actor::ActorImpl* issuer) override diff --git a/src/kernel/activity/SleepImpl.cpp b/src/kernel/activity/SleepImpl.cpp index 5c5b88bca5..6a529e8cd6 100644 --- a/src/kernel/activity/SleepImpl.cpp +++ b/src/kernel/activity/SleepImpl.cpp @@ -33,7 +33,11 @@ SleepImpl* SleepImpl::start() return this; } -void SleepImpl::post() +void SleepImpl::set_exception(actor::ActorImpl* issuer) +{ + /* FIXME: Really, nothing bad can happen while we sleep? */ +} +void SleepImpl::finish() { if (model_action_->get_state() == resource::Action::State::FAILED) { if (host_ && not host_->is_on()) @@ -45,15 +49,6 @@ void SleepImpl::post() } clean_action(); - /* Answer all simcalls associated with the synchro */ - finish(); -} -void SleepImpl::set_exception(actor::ActorImpl* issuer) -{ - /* FIXME: Really, nothing bad can happen while we sleep? */ -} -void SleepImpl::finish() -{ XBT_DEBUG("SleepImpl::finish() in state %s", get_state_str()); while (not simcalls_.empty()) { const actor::Simcall* simcall = simcalls_.front(); diff --git a/src/kernel/activity/SleepImpl.hpp b/src/kernel/activity/SleepImpl.hpp index eca98d2064..42aed855ad 100644 --- a/src/kernel/activity/SleepImpl.hpp +++ b/src/kernel/activity/SleepImpl.hpp @@ -17,7 +17,6 @@ class XBT_PUBLIC SleepImpl : public ActivityImpl_T { public: SleepImpl& set_host(s4u::Host* host); SleepImpl& set_duration(double duration); - void post() override; void set_exception(actor::ActorImpl* issuer) override; void finish() override; SleepImpl* start(); diff --git a/src/kernel/activity/Synchro.cpp b/src/kernel/activity/Synchro.cpp index 2067f07973..aa57662850 100644 --- a/src/kernel/activity/Synchro.cpp +++ b/src/kernel/activity/Synchro.cpp @@ -49,17 +49,6 @@ void SynchroImpl::cancel() /* I cannot cancel raw synchros directly. */ } -void SynchroImpl::post() -{ - if (model_action_->get_state() == resource::Action::State::FAILED) - set_state(State::FAILED); - else if (model_action_->get_state() == resource::Action::State::FINISHED) - set_state(State::SRC_TIMEOUT); - - clean_action(); - /* Answer all simcalls associated with the synchro */ - finish(); -} void SynchroImpl::set_exception(actor::ActorImpl* issuer) { if (get_state() == State::FAILED) { @@ -74,6 +63,13 @@ void SynchroImpl::set_exception(actor::ActorImpl* issuer) void SynchroImpl::finish() { XBT_DEBUG("SynchroImpl::finish() in state %s", get_state_str()); + if (model_action_->get_state() == resource::Action::State::FAILED) + set_state(State::FAILED); + else if (model_action_->get_state() == resource::Action::State::FINISHED) + set_state(State::SRC_TIMEOUT); + + clean_action(); + xbt_assert(simcalls_.size() == 1, "Unexpected number of simcalls waiting: %zu", simcalls_.size()); actor::Simcall* simcall = simcalls_.front(); simcalls_.pop_front(); diff --git a/src/kernel/activity/Synchro.hpp b/src/kernel/activity/Synchro.hpp index de958cca8b..a2f8daa57a 100644 --- a/src/kernel/activity/Synchro.hpp +++ b/src/kernel/activity/Synchro.hpp @@ -27,7 +27,6 @@ public: void suspend() override; void resume() override; void cancel() override; - void post() override; void set_exception(actor::ActorImpl* issuer) override; void finish() override; }; diff --git a/src/kernel/actor/ActorImpl.cpp b/src/kernel/actor/ActorImpl.cpp index 05de3b4fb6..c2e2b489c2 100644 --- a/src/kernel/actor/ActorImpl.cpp +++ b/src/kernel/actor/ActorImpl.cpp @@ -183,7 +183,7 @@ void ActorImpl::exit() activity::ActivityImplPtr activity = waiting_synchro_; activity->cancel(); activity->set_state(activity::State::FAILED); - activity->post(); + activity->finish(); activities_.erase(waiting_synchro_); waiting_synchro_ = nullptr; diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index 495cf0eb47..eda280894b 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -53,7 +53,7 @@ class ActorState { * This means there may be a way to store the list once and apply differences * rather than repeating elements frequently. */ - std::vector> pending_transitions_; + std::vector> pending_transitions_; /* Possible exploration status of an actor transition in a state. * Either the checker did not consider the transition, or it was considered and still to do, or considered and @@ -86,7 +86,7 @@ class ActorState { public: ActorState(aid_t aid, bool enabled, unsigned int max_consider) : ActorState(aid, enabled, max_consider, {}) {} - ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector> transitions) + ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector> transitions) : pending_transitions_(std::move(transitions)), aid_(aid), max_consider_(max_consider), enabled_(enabled) { } diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index ad68366e9a..9007e82f57 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -171,13 +171,13 @@ void RemoteApp::get_actors_status(std::map& whereto) const model_checker_->channel().send(MessageType::ACTORS_STATUS); s_mc_message_actors_status_answer_t answer; - ssize_t received = model_checker_->channel().receive(answer); - xbt_assert(received != -1, "Could not receive message"); - xbt_assert(received == sizeof(answer) && answer.type == MessageType::ACTORS_STATUS_REPLY, - "Received unexpected message %s (%i, size=%i) " - "expected MessageType::ACTORS_STATUS_REPLY (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)received, (int)MessageType::ACTORS_STATUS_REPLY, - (int)sizeof(answer)); + ssize_t answer_size = model_checker_->channel().receive(answer); + xbt_assert(answer_size != -1, "Could not receive message"); + xbt_assert(answer_size == sizeof answer && answer.type == MessageType::ACTORS_STATUS_REPLY, + "Received unexpected message %s (%i, size=%zd) " + "expected MessageType::ACTORS_STATUS_REPLY (%i, size=%zu)", + to_c_str(answer.type), (int)answer.type, answer_size, (int)MessageType::ACTORS_STATUS_REPLY, + sizeof answer); // Message sanity checks xbt_assert(answer.count >= 0, "Received an ACTOR_STATUS_REPLY message with an actor count of '%d' < 0", answer.count); @@ -206,17 +206,16 @@ void RemoteApp::get_actors_status(std::map& whereto) const std::vector probes(answer.transition_count); if (answer.transition_count > 0) { for (auto& probe : probes) { - size_t size = sizeof(s_mc_message_simcall_probe_one_t); - ssize_t received = model_checker_->channel().receive(&probe, size); + ssize_t received = model_checker_->channel().receive(probe); xbt_assert(received >= 0, "Could not receive response to ACTORS_PROBE message (%s)", strerror(errno)); - xbt_assert(static_cast(received) == size, + xbt_assert(static_cast(received) == sizeof probe, "Could not receive response to ACTORS_PROBE message (%zd bytes received != %zu bytes expected", - received, size); + received, sizeof probe); } } whereto.clear(); - auto probes_iter = std::move_iterator(probes.begin()); + std::move_iterator probes_iter(probes.begin()); for (const auto& actor : status) { xbt_assert(actor.n_transitions == 0 || actor.n_transitions == actor.max_considered, @@ -225,14 +224,13 @@ void RemoteApp::get_actors_status(std::map& whereto) const "(currently %d), but only %d transition(s) was/were said to be encoded", actor.max_considered, actor.n_transitions); - auto actor_transitions = std::vector>(actor.n_transitions); + std::vector> actor_transitions; for (int times_considered = 0; times_considered < actor.n_transitions; times_considered++, probes_iter++) { std::stringstream stream((*probes_iter).buffer.data()); - auto transition = std::unique_ptr(deserialize_transition(actor.aid, times_considered, stream)); - actor_transitions[times_considered] = std::move(transition); + actor_transitions.emplace_back(deserialize_transition(actor.aid, times_considered, stream)); } - XBT_DEBUG("Received %d transitions for actor %ld", actor.n_transitions, actor.aid); + XBT_DEBUG("Received %zu transitions for actor %ld", actor_transitions.size(), actor.aid); whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered, std::move(actor_transitions)); } } @@ -241,13 +239,13 @@ void RemoteApp::check_deadlock() const { xbt_assert(model_checker_->channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state"); s_mc_message_int_t message; - ssize_t s = model_checker_->channel().receive(message); - xbt_assert(s != -1, "Could not receive message"); - xbt_assert(s == sizeof(message) && message.type == MessageType::DEADLOCK_CHECK_REPLY, - "Received unexpected message %s (%i, size=%i) " - "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%i)", - to_c_str(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY, - (int)sizeof(message)); + ssize_t received = model_checker_->channel().receive(message); + xbt_assert(received != -1, "Could not receive message"); + xbt_assert(received == sizeof message && message.type == MessageType::DEADLOCK_CHECK_REPLY, + "Received unexpected message %s (%i, size=%zd) " + "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%zu)", + to_c_str(message.type), (int)message.type, received, (int)MessageType::DEADLOCK_CHECK_REPLY, + sizeof message); if (message.value != 0) { XBT_CINFO(mc_global, "Counter-example execution trace:"); diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index a9d97afd1b..14f0208c38 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -61,12 +61,12 @@ std::size_t State::count_todo() const return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); }); } -void State::mark_all_todo() +void State::mark_all_enabled_todo() { - for (auto& [aid, actor] : actors_to_run_) { - - if (actor.is_enabled() and not actor.is_done() and not actor.is_todo()) - actor.mark_todo(); + for (auto const& [aid, _] : this->get_actors_list()) { + if (this->is_actor_enabled(aid) and not is_actor_done(aid)) { + this->mark_todo(aid); + } } } diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 168ee8de44..f96d540aef 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -59,9 +59,8 @@ public: long get_num() const { return num_; } std::size_t count_todo() const; void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); } - void mark_done(aid_t actor) { actors_to_run_.at(actor).mark_done();} - void mark_all_todo(); - bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); } + void mark_all_enabled_todo(); + bool is_actor_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); } Transition* get_transition() const; void set_transition(Transition* t) { transition_ = t; } std::map const& get_actors_list() const { return actors_to_run_; } diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index a98f32dc27..43dd7ce29b 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -184,7 +184,7 @@ void DFSExplorer::run() if (visited_state_ == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ for (auto const& [aid, _] : next_state->get_actors_list()) { - if (next_state->is_actor_enabled(aid) and not next_state->is_done(aid)) { + if (next_state->is_actor_enabled(aid) and not next_state->is_actor_done(aid)) { next_state->mark_todo(aid); if (reduction_mode_ == ReductionMode::dpor) break; // With DPOR, we take the first enabled transition @@ -245,13 +245,13 @@ void DFSExplorer::backtrack() XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num()); if (prev_state->is_actor_enabled(issuer_id)){ - if (not prev_state->is_done(issuer_id)) + if (not prev_state->is_actor_done(issuer_id)) prev_state->mark_todo(issuer_id); else XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id); } else { XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled transition as todo", issuer_id); - prev_state->mark_all_todo(); + prev_state->mark_all_enabled_todo(); } break; } else { diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 812a2e6e72..ff61f17a39 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -4,15 +4,199 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/UdporChecker.hpp" +#include "src/mc/api/State.hpp" +#include #include -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety verification "); +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR"); -namespace simgrid::mc { +namespace simgrid::mc::udpor { + +UdporChecker::UdporChecker(const std::vector& args) : Exploration(args) +{ + /* Create initial data structures, if any ...*/ + + // TODO: Initialize state structures for the search +} + +void UdporChecker::run() +{ + XBT_INFO("Starting a UDPOR exploration"); + // NOTE: `A`, `D`, and `C` are derived from the + // original UDPOR paper [1], while `prev_exC` arises + // from the incremental computation of ex(C) from [3] + Configuration C_root; + + // TODO: Move computing the root configuration into a method on the Unfolding + auto initial_state = get_current_state(); + auto root_event = std::make_unique(EventSet(), std::make_shared()); + auto* root_event_handle = root_event.get(); + unfolding.insert(std::move(root_event)); + C_root.add_event(root_event_handle); + + explore(std::move(C_root), EventSet(), EventSet(), std::move(initial_state), EventSet()); + + XBT_INFO("UDPOR exploration terminated -- model checking completed"); +} + +void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr stateC, EventSet prev_exC) +{ + // Perform the incremental computation of exC + // + // TODO: This method will have side effects on + // the unfolding, but the naming of the method + // suggests it is doesn't have side effects. We should + // reconcile this in the future + auto [exC, enC] = compute_extension(C, prev_exC); + + // If enC is a subset of D, intuitively + // there aren't any enabled transitions + // which are "worth" exploring since their + // exploration would lead to a so-called + // "sleep-set blocked" trace. + if (enC.is_subset_of(D)) { + + if (C.get_events().size() > 0) { + + // g_var::nb_traces++; + + // TODO: Log here correctly + // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces); + // ... + // ... + } + + // When `en(C)` is empty, intuitively this means that there + // are no enabled transitions that can be executed from the + // state reached by `C` (denoted `state(C)`), i.e. by some + // execution of the transitions in C obeying the causality + // relation. Here, then, we would be in a deadlock. + if (enC.empty()) { + get_remote_app().check_deadlock(); + } + + return; + } + + // TODO: Add verbose logging about which event is being explored + + UnfoldingEvent* e = select_next_unfolding_event(A, enC); + xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n" + "UDPOR guarantees that an event will be chosen at each point in\n" + "the search, yet no events were actually chosen\n" + "*********************************\n\n"); + + // Move the application into stateCe and actually make note of that state + move_to_stateCe(*stateC, *e); + auto stateCe = record_current_state(); + + // Ce := C + {e} + Configuration Ce = C; + Ce.add_event(e); + + A.remove(e); + exC.remove(e); + + // Explore(C + {e}, D, A \ {e}) + explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC)); + + // D <-- D + {e} + D.insert(e); + + // TODO: Determine a value of K to use or don't use it at all + constexpr unsigned K = 10; + auto J = compute_partial_alternative(D, C, K); + if (!J.empty()) { + J.subtract(C.get_events()); + + // Before searching the "right half", we need to make + // sure the program actually reflects the fact + // that we are searching again from `stateC` (the recursive + // search moved the program into `stateCe`) + restore_program_state_to(*stateC); + + // Explore(C, D + {e}, J \ C) + explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC)); + } + + // D <-- D - {e} + D.remove(e); -UdporChecker::UdporChecker(const std::vector& args) : Exploration(args) {} + // Remove(e, C, D) + clean_up_explore(e, C, D); +} + +std::tuple UdporChecker::compute_extension(const Configuration& C, const EventSet& prev_exC) const +{ + // See eqs. 5.7 of section 5.2 of [3] + // C = C' + {e_cur}, i.e. C' = C - {e_cur} + // + // Then + // + // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{ : H } + UnfoldingEvent* e_cur = C.get_latest_event(); + EventSet exC = prev_exC; + exC.remove(e_cur); + + // ... fancy computations + + EventSet enC; + return std::tuple(exC, enC); +} + +void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e) +{ + const aid_t next_actor = e.get_transition()->aid_; + + // TODO: Add the trace if possible for reporting a bug + xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n" + "In reaching this execution path, UDPOR ensures that at least one\n" + "one transition of the state of an visited event is enabled, yet no\n" + "state was actually enabled. Please report this as a bug.\n" + "*********************************\n\n"); + state.execute_next(next_actor); +} + +void UdporChecker::restore_program_state_to(const State& stateC) +{ + // TODO: Perform state regeneration in the same manner as is done + // in the DFSChecker.cpp +} + +std::unique_ptr UdporChecker::record_current_state() +{ + auto next_state = this->get_current_state(); -void UdporChecker::run() {} + // In UDPOR, we care about all enabled transitions in a given state + next_state->mark_all_enabled_todo(); + + return next_state; +} + +UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC) +{ + if (!enC.empty()) { + return *(enC.begin()); + } + + for (const auto& event : A) { + if (enC.contains(event)) { + return event; + } + } + return nullptr; +} + +EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const +{ + // TODO: Compute k-partial alternatives using [2] + return EventSet(); +} + +void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D) +{ + // TODO: Perform clean up here +} RecordTrace UdporChecker::get_record_trace() { @@ -22,13 +206,19 @@ RecordTrace UdporChecker::get_record_trace() std::vector UdporChecker::get_textual_trace() { + // TODO: Topologically sort the events of the latest configuration + // and iterate through that topological sorting std::vector trace; return trace; } +} // namespace simgrid::mc::udpor + +namespace simgrid::mc { + Exploration* create_udpor_checker(const std::vector& args) { - return new UdporChecker(args); + return new simgrid::mc::udpor::UdporChecker(args); } } // namespace simgrid::mc diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index f0262003cb..7f56d6d3d5 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -8,18 +8,171 @@ #define SIMGRID_MC_UDPOR_CHECKER_HPP #include "src/mc/explo/Exploration.hpp" +#include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/Unfolding.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" #include "src/mc/mc_record.hpp" -namespace simgrid::mc { +#include +namespace simgrid::mc::udpor { + +/** + * @brief Performs exploration of a concurrent system via the + * UDPOR algorithm + * + * The `UdporChecker` implementation is based primarily off three papers, + * herein referred to as [1], [2], and [3] respectively, as well as the + * current implementation of `tiny_simgrid`: + * + * 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al. + * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al. + * 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..." + */ class XBT_PRIVATE UdporChecker : public Exploration { public: explicit UdporChecker(const std::vector& args); + void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; -}; -} // namespace simgrid::mc + inline std::unique_ptr get_current_state() { return std::make_unique(get_remote_app()); } + +private: + /** + * The total number of events created whilst exploring the unfolding + */ + /* FIXME: private fields are not used + uint32_t nb_events = 0; + uint32_t nb_traces = 0; + */ + + /** + * @brief The "relevant" portions of the unfolding that must be kept around to ensure that + * UDPOR properly searches the state space + * + * The set `U` is a global variable which is maintained by UDPOR + * to keep track of "just enough" information about the unfolding + * to compute *alternatives* (see the paper for more details). + * + * @invariant: When a new event is created by UDPOR, it is inserted into + * this set. All new events that are created by UDPOR have causes that + * also exist in U and are valid for the duration of the search. + * + * If an event is discarded instead of moved from set `U` to set `G`, + * the event and its contents will be discarded. + */ + EventSet U; + + /** + * @brief The "irrelevant" portions of the unfolding that do not need to be kept + * around to ensure that UDPOR functions correctly + * + * The set `G` is another global variable maintained by the UDPOR algorithm which + * is used to keep track of all events which used to be important to UDPOR + */ + EventSet G; + + /** + * @brief UDPOR's current "view" of the program it is exploring + */ + Unfolding unfolding = Unfolding(); + +private: + /** + * @brief Explores the unfolding of the concurrent system + * represented by the ModelChecker instance "mcmodel_checker" + * + * This function performs the actual search following the + * UDPOR algorithm according to [1]. + * + * @param C the current configuration from which UDPOR will be used + * to explore expansions of the concurrent system being modeled + * @param D the set of events that should not be considered by UDPOR + * while performing its searches, in order to avoid sleep-set blocked + * executions. See [1] for more details + * @param A the set of events to "guide" UDPOR in the correct direction + * when it returns back to a node in the unfolding and must decide among + * events to select from `ex(C)`. See [1] for more details + * @param stateC the state of the program after having executed `C`, + * viz. `state(C)` using the notation of [1] + * + * TODO: Add the optimization where we can check if e == e_prior + * to prevent repeated work when computing ex(C) + */ + void explore(Configuration C, EventSet D, EventSet A, std::unique_ptr stateC, EventSet prev_exC); + + /** + * @brief Identifies the next event from the unfolding of the concurrent system + * that should next be explored as an extension of a configuration with + * enabled events `enC` + * + * @param A The set of events `A` maintained by the UDPOR algorithm to help + * determine how events should be selected. See the original paper [1] for more details + * + * @param enC The set `enC` of enabled events from the extension set `exC` used + * by the UDPOR algorithm to select new events to search. See the original + * paper [1] for more details + */ + UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); + + /** + * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration + * `C` as an incremental computation from the the previous computation of `ex(C)` + * + * A central component to UDPOR is the computation of the set `ex(C)`. The + * extension set `ex(C)` of a configuration `C` is defined as the set of events + * outside of `C` whose full dependency chain is contained in `C` (see [1] + * for more details). + * + * In general, computing `ex(C)` is very expensive. In paper [3], The Anh Pham + * shows a method of incremental computation of the set `ex(C)` under the + * conclusions afforded under the computation model in consideration, of which + * SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently. + * Intuitively, the idea is to take advantage of the fact that you can avoid a lot + * of repeated computation by exploiting the aforementioned properties (in [3]) in + * what is effectively a dynamic programming optimization. See [3] for more details + * + * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are + * computed + * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for + * the configuration `C' := C - {e}` + * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively + */ + std::tuple compute_extension(const Configuration& C, const EventSet& prev_exC) const; + + /** + * + */ + EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const; + + /** + * + */ + void move_to_stateCe(State& stateC, const UnfoldingEvent& e); + + /** + * @brief Creates a new snapshot of the state of the progam undergoing + * model checking + * + * @returns the handle used to uniquely identify this state later in the + * exploration of the unfolding. You provide this handle to an event in the + * unfolding to regenerate past states + */ + std::unique_ptr record_current_state(); + + /** + * + */ + void restore_program_state_to(const State& stateC); + + /** + * + */ + void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D); +}; +} // namespace simgrid::mc::udpor #endif diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp new file mode 100644 index 0000000000..46bc8c568d --- /dev/null +++ b/src/mc/explo/udpor/Configuration.cpp @@ -0,0 +1,46 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/History.hpp" + +#include +#include + +namespace simgrid::mc::udpor { + +Configuration::Configuration(std::initializer_list events) : Configuration(EventSet(std::move(events))) +{ +} + +Configuration::Configuration(EventSet events) : events_(events) +{ + if (!events_.is_valid_configuration()) { + throw std::invalid_argument("The events do not form a valid configuration"); + } +} + +void Configuration::add_event(UnfoldingEvent* e) +{ + if (e == nullptr) { + throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead"); + } + + if (this->events_.contains(e)) { + return; + } + + this->events_.insert(e); + this->newest_event = e; + + // Preserves the property that the configuration is valid + History history(e); + if (!this->events_.contains(history)) { + throw std::invalid_argument("The newly added event has dependencies " + "which are missing from this configuration"); + } +} + +} // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp new file mode 100644 index 0000000000..a1d37c5d8e --- /dev/null +++ b/src/mc/explo/udpor/Configuration.hpp @@ -0,0 +1,78 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_UDPOR_CONFIGURATION_HPP +#define SIMGRID_MC_UDPOR_CONFIGURATION_HPP + +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/udpor_forward.hpp" + +#include + +namespace simgrid::mc::udpor { + +class Configuration { +public: + Configuration() = default; + Configuration(const Configuration&) = default; + Configuration& operator=(Configuration const&) = default; + Configuration(Configuration&&) = default; + + Configuration(EventSet events); + Configuration(std::initializer_list events); + + auto begin() const { return this->events_.begin(); } + auto end() const { return this->events_.end(); } + + bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); } + const EventSet& get_events() const { return this->events_; } + UnfoldingEvent* get_latest_event() const { return this->newest_event; } + + /** + * @brief Insert a new event into the configuration + * + * When the newly added event is inserted into the configuration, + * an assertion is made to ensure that the configuration remains + * valid, i.e. that the newly added event's dependencies are contained + * within the configuration. + * + * @param e the event to add to the configuration. If the event is + * already a part of the configuration, calling this method has no + * effect. + * + * @throws an invalid argument exception is raised should the event + * be missing one of its dependencies + * + * @note: UDPOR technically enforces the invariant that all newly-added events + * will ensure that the configuration is valid. We perform extra checks to ensure + * that UDPOR is implemented as expected. There is a performance penalty that + * should be noted: checking for maximality requires ensuring that all events in the + * configuration have their dependencies containes within the configuration, which + * essentially means performing a BFS/DFS over the configuration using a History object. + * However, since the slowest part of UDPOR involves enumerating all + * subsets of maximal events and computing k-partial alternatives (the + * latter definitively an NP-hard problem when optimal), Amdahl's law suggests + * we shouldn't focus so much on this (let alone the additional benefit of the + * assertions) + */ + void add_event(UnfoldingEvent* e); + +private: + /** + * @brief The most recent event added to the configuration + */ + UnfoldingEvent* newest_event = nullptr; + + /** + * @brief The events which make up this configuration + * + * @invariant For each event `e` in `events_`, the set of + * dependencies of `e` is also contained in `events_` + */ + EventSet events_; +}; + +} // namespace simgrid::mc::udpor +#endif diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp new file mode 100644 index 0000000000..3ba27957ab --- /dev/null +++ b/src/mc/explo/udpor/Configuration_test.cpp @@ -0,0 +1,122 @@ +/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/3rd-party/catch.hpp" +#include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" + +using namespace simgrid::mc::udpor; + +TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations") +{ + // The following tests concern the given event structure: + // e1 + // / + // e2 + // / + // e3 + // / / + // e4 e5 + UnfoldingEvent e1; + UnfoldingEvent e2{&e1}; + UnfoldingEvent e3{&e2}; + UnfoldingEvent e4{&e3}, e5{&e3}; + + SECTION("Creating a configuration without events") + { + Configuration C; + REQUIRE(C.get_events().empty()); + REQUIRE(C.get_latest_event() == nullptr); + } + + SECTION("Creating a configuration with events") + { + // 5 choose 0 = 1 test + REQUIRE_NOTHROW(Configuration({&e1})); + + // 5 choose 1 = 5 tests + REQUIRE_THROWS_AS(Configuration({&e2}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e3}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e4}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e5}), std::invalid_argument); + + // 5 choose 2 = 10 tests + REQUIRE_NOTHROW(Configuration({&e1, &e2})); + REQUIRE_THROWS_AS(Configuration({&e1, &e3}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1, &e4}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e2, &e3}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e2, &e4}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e2, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e3, &e4}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e3, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e4, &e5}), std::invalid_argument); + + // 5 choose 3 = 10 tests + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3})); + REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e4}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e4}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1, &e4, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e4}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e2, &e4, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e3, &e4, &e5}), std::invalid_argument); + + // 5 choose 4 = 5 tests + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4})); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e5})); + REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e4, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e4, &e5}), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e4, &e5}), std::invalid_argument); + + // 5 choose 5 = 1 test + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4, &e5})); + } +} + +TEST_CASE("simgrid::mc::udpor::Configuration: Adding Events") +{ + // The following tests concern the given event structure: + // e1 + // / + // e2 + // / + // / / + // e3 e4 + UnfoldingEvent e1; + UnfoldingEvent e2{&e1}; + UnfoldingEvent e3{&e2}; + UnfoldingEvent e4{&e2}; + + REQUIRE_THROWS_AS(Configuration().add_event(nullptr), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration().add_event(&e2), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration().add_event(&e3), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration().add_event(&e4), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1}).add_event(&e3), std::invalid_argument); + REQUIRE_THROWS_AS(Configuration({&e1}).add_event(&e4), std::invalid_argument); + + REQUIRE_NOTHROW(Configuration().add_event(&e1)); + REQUIRE_NOTHROW(Configuration({&e1}).add_event(&e1)); + REQUIRE_NOTHROW(Configuration({&e1}).add_event(&e2)); + REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e1)); + REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e2)); + REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e3)); + REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e4)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e1)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e2)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e3)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e4)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e1)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e2)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e3)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e4)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e1)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e2)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e3)); + REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e4)); +} diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp new file mode 100644 index 0000000000..6f486b7732 --- /dev/null +++ b/src/mc/explo/udpor/EventSet.cpp @@ -0,0 +1,137 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/History.hpp" + +#include + +namespace simgrid::mc::udpor { + +EventSet::EventSet(Configuration&& config) : EventSet(std::move(config.get_events())) {} + +void EventSet::remove(UnfoldingEvent* e) +{ + this->events_.erase(e); +} + +void EventSet::subtract(const EventSet& other) +{ + this->events_ = std::move(subtracting(other).events_); +} + +void EventSet::subtract(const Configuration& config) +{ + subtract(config.get_events()); +} + +EventSet EventSet::subtracting(const EventSet& other) const +{ + std::unordered_set result = this->events_; + + for (UnfoldingEvent* e : other.events_) + result.erase(e); + + return EventSet(std::move(result)); +} + +EventSet EventSet::subtracting(const Configuration& config) const +{ + return subtracting(config.get_events()); +} + +EventSet EventSet::subtracting(UnfoldingEvent* e) const +{ + auto result = this->events_; + result.erase(e); + return EventSet(std::move(result)); +} + +void EventSet::insert(UnfoldingEvent* e) +{ + this->events_.insert(e); +} + +void EventSet::form_union(const EventSet& other) +{ + this->events_ = std::move(make_union(other).events_); +} + +void EventSet::form_union(const Configuration& config) +{ + form_union(config.get_events()); +} + +EventSet EventSet::make_union(UnfoldingEvent* e) const +{ + auto result = this->events_; + result.insert(e); + return EventSet(std::move(result)); +} + +EventSet EventSet::make_union(const EventSet& other) const +{ + std::unordered_set result = this->events_; + + for (UnfoldingEvent* e : other.events_) + result.insert(e); + + return EventSet(std::move(result)); +} + +EventSet EventSet::make_union(const Configuration& config) const +{ + return make_union(config.get_events()); +} + +size_t EventSet::size() const +{ + return this->events_.size(); +} + +bool EventSet::empty() const +{ + return this->events_.empty(); +} + +bool EventSet::contains(UnfoldingEvent* e) const +{ + return this->events_.find(e) != this->events_.end(); +} + +bool EventSet::is_subset_of(const EventSet& other) const +{ + // If there is some element not contained in `other`, then + // the set difference will contain that element and the + // result won't be empty + return subtracting(other).empty(); +} + +bool EventSet::is_valid_configuration() const +{ + /// @invariant: A collection of events `E` is a configuration + /// if and only if following while following the history of + /// each event `e` of `E`you remain in `E`. In other words, you + /// only see events from set `E` + /// + /// The proof is based on the definition of a configuration + /// which requires that all + const History history(*this); + return this->contains(history); +} + +bool EventSet::contains(const History& history) const +{ + return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); }); +} + +bool EventSet::is_maximal_event_set() const +{ + const History history(*this); + return *this == history.get_all_maximal_events(); +} + +} // namespace simgrid::mc::udpor \ No newline at end of file diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp new file mode 100644 index 0000000000..e640f0c9de --- /dev/null +++ b/src/mc/explo/udpor/EventSet.hpp @@ -0,0 +1,75 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_UDPOR_EVENT_SET_HPP +#define SIMGRID_MC_UDPOR_EVENT_SET_HPP + +#include "src/mc/explo/udpor/udpor_forward.hpp" + +#include +#include +#include + +namespace simgrid::mc::udpor { + +class EventSet { +private: + std::unordered_set events_; + +public: + EventSet() = default; + EventSet(const EventSet&) = default; + EventSet& operator=(const EventSet&) = default; + EventSet& operator=(EventSet&&) = default; + EventSet(EventSet&&) = default; + explicit EventSet(Configuration&& config); + explicit EventSet(std::unordered_set&& raw_events) : events_(raw_events) {} + explicit EventSet(std::initializer_list event_list) : events_(std::move(event_list)) {} + + auto begin() const { return this->events_.begin(); } + auto end() const { return this->events_.end(); } + auto cbegin() const { return this->events_.cbegin(); } + auto cend() const { return this->events_.cend(); } + + void remove(UnfoldingEvent*); + void subtract(const EventSet&); + void subtract(const Configuration&); + EventSet subtracting(UnfoldingEvent*) const; + EventSet subtracting(const EventSet&) const; + EventSet subtracting(const Configuration&) const; + + void insert(UnfoldingEvent*); + void form_union(const EventSet&); + void form_union(const Configuration&); + EventSet make_union(UnfoldingEvent*) const; + EventSet make_union(const EventSet&) const; + EventSet make_union(const Configuration&) const; + + size_t size() const; + bool empty() const; + bool contains(UnfoldingEvent*) const; + bool contains(const History&) const; + bool is_subset_of(const EventSet&) const; + + bool operator==(const EventSet& other) const { return this->events_ == other.events_; } + bool operator!=(const EventSet& other) const { return this->events_ != other.events_; } + +public: + /** + * @brief Whether or not this set of events could + * represent a configuration + */ + bool is_valid_configuration() const; + + /** + * @brief Whether or not this set of events is + * a *maximal event set*, i.e. whether each element + * of the set causes none of the others + */ + bool is_maximal_event_set() const; +}; + +} // namespace simgrid::mc::udpor +#endif diff --git a/src/mc/explo/udpor/EventSet_test.cpp b/src/mc/explo/udpor/EventSet_test.cpp new file mode 100644 index 0000000000..77a555d2f4 --- /dev/null +++ b/src/mc/explo/udpor/EventSet_test.cpp @@ -0,0 +1,715 @@ +/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/3rd-party/catch.hpp" +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" + +using namespace simgrid::mc::udpor; + +TEST_CASE("simgrid::mc::udpor::EventSet: Initial conditions when creating sets") +{ + SECTION("Initialization with no elements") + { + SECTION("Default initializer") + { + EventSet event_set; + REQUIRE(event_set.size() == 0); + REQUIRE(event_set.empty()); + } + + SECTION("Set initializer") + { + EventSet event_set({}); + REQUIRE(event_set.size() == 0); + REQUIRE(event_set.empty()); + } + + SECTION("List initialization") + { + EventSet event_set{}; + REQUIRE(event_set.size() == 0); + REQUIRE(event_set.empty()); + } + } + + SECTION("Initialization with one or more elements") + { + UnfoldingEvent e1, e2, e3; + + SECTION("Set initializer") + { + EventSet event_set({&e1, &e2, &e3}); + REQUIRE(event_set.size() == 3); + REQUIRE(event_set.contains(&e1)); + REQUIRE(event_set.contains(&e2)); + REQUIRE(event_set.contains(&e3)); + REQUIRE_FALSE(event_set.empty()); + } + + SECTION("List initialization") + { + UnfoldingEvent e1, e2, e3; + EventSet event_set{&e1, &e2, &e3}; + REQUIRE(event_set.size() == 3); + REQUIRE(event_set.contains(&e1)); + REQUIRE(event_set.contains(&e2)); + REQUIRE(event_set.contains(&e3)); + REQUIRE_FALSE(event_set.empty()); + } + } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Insertions") +{ + EventSet event_set; + UnfoldingEvent e1, e2, e3; + + SECTION("Inserting unique elements") + { + event_set.insert(&e1); + REQUIRE(event_set.size() == 1); + REQUIRE(event_set.contains(&e1)); + REQUIRE_FALSE(event_set.empty()); + + event_set.insert(&e2); + REQUIRE(event_set.size() == 2); + REQUIRE(event_set.contains(&e2)); + REQUIRE_FALSE(event_set.empty()); + + SECTION("Check contains inserted elements") + { + REQUIRE(event_set.contains(&e1)); + REQUIRE(event_set.contains(&e2)); + REQUIRE_FALSE(event_set.contains(&e3)); + } + } + + SECTION("Inserting duplicate elements") + { + event_set.insert(&e1); + REQUIRE(event_set.size() == 1); + REQUIRE(event_set.contains(&e1)); + REQUIRE_FALSE(event_set.empty()); + + event_set.insert(&e1); + REQUIRE(event_set.size() == 1); + REQUIRE(event_set.contains(&e1)); + REQUIRE_FALSE(event_set.empty()); + + SECTION("Check contains inserted elements") + { + REQUIRE(event_set.contains(&e1)); + REQUIRE_FALSE(event_set.contains(&e2)); + REQUIRE_FALSE(event_set.contains(&e3)); + } + } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Deletions") +{ + UnfoldingEvent e1, e2, e3, e4; + EventSet event_set({&e1, &e2, &e3}); + + SECTION("Remove an element already present") + { + REQUIRE(event_set.contains(&e1)); + + // event_set = {e2, e3} + event_set.remove(&e1); + + // Check that + // 1. the size decreases by exactly 1 + // 2. the set remains unempty + // 3. the other elements are still contained in the set + REQUIRE(event_set.size() == 2); + REQUIRE_FALSE(event_set.contains(&e1)); + REQUIRE(event_set.contains(&e2)); + REQUIRE(event_set.contains(&e3)); + REQUIRE_FALSE(event_set.empty()); + + SECTION("Remove a single element more than once") + { + // event_set = {e2, e3} + event_set.remove(&e1); + REQUIRE(event_set.size() == 2); + REQUIRE_FALSE(event_set.contains(&e1)); + REQUIRE(event_set.contains(&e2)); + REQUIRE(event_set.contains(&e3)); + REQUIRE_FALSE(event_set.empty()); + } + + SECTION("Remove more than one element") + { + // event_set = {e3} + event_set.remove(&e2); + + REQUIRE(event_set.size() == 1); + REQUIRE_FALSE(event_set.contains(&e1)); + REQUIRE_FALSE(event_set.contains(&e2)); + REQUIRE(event_set.contains(&e3)); + REQUIRE_FALSE(event_set.empty()); + + // event_set = {} + event_set.remove(&e3); + + REQUIRE(event_set.size() == 0); + REQUIRE_FALSE(event_set.contains(&e1)); + REQUIRE_FALSE(event_set.contains(&e2)); + REQUIRE_FALSE(event_set.contains(&e3)); + REQUIRE(event_set.empty()); + } + } + + SECTION("Remove an element absent from the set") + { + REQUIRE_FALSE(event_set.contains(&e4)); + + // event_set = {e1, e2, e3} + event_set.remove(&e4); + REQUIRE(event_set.size() == 3); + REQUIRE(event_set.contains(&e1)); + REQUIRE(event_set.contains(&e2)); + REQUIRE(event_set.contains(&e3)); + + // Ensure e4 isn't somehow added + REQUIRE_FALSE(event_set.contains(&e4)); + REQUIRE_FALSE(event_set.empty()); + } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Set Equality") +{ + UnfoldingEvent e1, e2, e3, e4; + EventSet A{&e1, &e2, &e3}, B{&e1, &e2, &e3}, C{&e1, &e2, &e3}; + + SECTION("Equality implies containment") + { + REQUIRE(A == B); + + for (const auto& e : A) { + REQUIRE(B.contains(e)); + } + + for (const auto& e : B) { + REQUIRE(A.contains(e)); + } + } + + SECTION("Containment implies equality") + { + for (const auto& e : A) { + REQUIRE(B.contains(e)); + } + + for (const auto& e : C) { + REQUIRE(C.contains(e)); + } + + REQUIRE(A == C); + } + + SECTION("Equality is an equivalence relation") + { + // Reflexive + REQUIRE(A == A); + REQUIRE(B == B); + REQUIRE(C == C); + + // Symmetric + REQUIRE(A == B); + REQUIRE(B == A); + REQUIRE(A == C); + REQUIRE(C == A); + REQUIRE(B == C); + REQUIRE(C == B); + + // Transitive + REQUIRE(A == B); + REQUIRE(B == C); + REQUIRE(A == C); + } + + SECTION("Equality after copy (assignment + constructor)") + { + EventSet A_copy = A; + EventSet A_copy2(A); + + REQUIRE(A == A_copy); + REQUIRE(A == A_copy2); + } + + SECTION("Equality after move constructor") + { + EventSet A_copy = A; + EventSet A_move(std::move(A)); + REQUIRE(A_move == A_copy); + } + + SECTION("Equality after move-assignment") + { + EventSet A_copy = A; + EventSet A_move = std::move(A); + REQUIRE(A_move == A_copy); + } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Set Union Tests") +{ + UnfoldingEvent e1, e2, e3, e4; + + // C = A + B + EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3}; + + SECTION("Unions with no effect") + { + EventSet A_copy = A; + + SECTION("Self union") + { + // A = A union A + EventSet A_union = A.make_union(A); + REQUIRE(A == A_copy); + + A.form_union(A); + REQUIRE(A == A_copy); + } + + SECTION("Union with empty set") + { + // A = A union empty set + EventSet A_union = A.make_union(EventSet()); + REQUIRE(A == A_union); + + A.form_union(EventSet()); + REQUIRE(A == A_copy); + } + + SECTION("Union with an equivalent set") + { + // A = A union B if B == A + EventSet A_equiv{&e1, &e2, &e3}; + REQUIRE(A == A_equiv); + + EventSet A_union = A.make_union(A_equiv); + REQUIRE(A_union == A_copy); + + A.form_union(A_equiv); + REQUIRE(A == A_copy); + } + + SECTION("Union with a subset") + { + // A = A union D if D is a subset of A + EventSet A_union = A.make_union(D); + REQUIRE(A == A_union); + + A.form_union(D); + REQUIRE(A == A_copy); + } + } + + SECTION("Unions with partial overlaps") + { + EventSet A_union_B = A.make_union(B); + REQUIRE(A_union_B == C); + + A.form_union(B); + REQUIRE(A == C); + + EventSet B_union_D = B.make_union(D); + REQUIRE(B_union_D == C); + + B.form_union(D); + REQUIRE(B == C); + } + + SECTION("Set union properties") + { + SECTION("Union operator is symmetric") + { + EventSet A_union_B = A.make_union(B); + EventSet B_union_A = B.make_union(A); + REQUIRE(A_union_B == B_union_A); + } + + SECTION("Union operator commutes") + { + // The last SECTION tested pair-wise + // equivalence, so we only check + // one of each pai + EventSet AD = A.make_union(D); + EventSet AC = A.make_union(C); + EventSet CD = D.make_union(C); + + EventSet ADC = AD.make_union(C); + EventSet ACD = AC.make_union(D); + EventSet CDA = CD.make_union(A); + + REQUIRE(ADC == ACD); + REQUIRE(ACD == CDA); + + // Test `form_union()` in the same way + + EventSet A_copy = A; + EventSet C_copy = C; + EventSet D_copy = D; + + A.form_union(C_copy); + A.form_union(D_copy); + + D.form_union(A_copy); + D.form_union(C_copy); + + C.form_union(A); + C.form_union(D); + + REQUIRE(A == D); + REQUIRE(C == D); + REQUIRE(A == C); + } + } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Set Difference Tests") +{ + UnfoldingEvent e1, e2, e3, e4; + + // C = A + B + // A is a subset of C + // B is a subset of C + // D is a subset of A and C + // E is a subset of B and C + // F is a subset of A, C, and D + EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3}, E{&e4}, F{&e1}; + + SECTION("Difference with no effect") + { + SECTION("Difference with empty set") + { + EventSet A_copy = A.subtracting(EventSet()); + REQUIRE(A == A_copy); + + A.subtract(EventSet()); + REQUIRE(A == A_copy); + } + + SECTION("Difference with empty intersection") + { + // A intersection E = empty set + EventSet A_copy = A.subtracting(E); + REQUIRE(A == A_copy); + + A.subtract(E); + REQUIRE(A == A_copy); + + EventSet D_copy = D.subtracting(E); + REQUIRE(D == D_copy); + + D.subtract(E); + REQUIRE(D == D_copy); + } + } + + SECTION("Difference with some overlap") + { + // A - B = {&e1} = F + EventSet A_minus_B = A.subtracting(B); + REQUIRE(A_minus_B == F); + + // B - D = {&e2, &e4} + EventSet B_minus_D = B.subtracting(D); + REQUIRE(B_minus_D == EventSet({&e2, &e4})); + } + + SECTION("Difference with complete overlap") + { + SECTION("Difference with same set gives empty set") + { + REQUIRE(A.subtracting(A) == EventSet()); + REQUIRE(B.subtracting(B) == EventSet()); + REQUIRE(C.subtracting(C) == EventSet()); + REQUIRE(D.subtracting(D) == EventSet()); + REQUIRE(E.subtracting(E) == EventSet()); + REQUIRE(F.subtracting(F) == EventSet()); + } + + SECTION("Difference with superset gives empty set") + { + REQUIRE(A.subtracting(C) == EventSet()); + REQUIRE(B.subtracting(C) == EventSet()); + REQUIRE(D.subtracting(A) == EventSet()); + REQUIRE(D.subtracting(C) == EventSet()); + REQUIRE(E.subtracting(B) == EventSet()); + REQUIRE(E.subtracting(C) == EventSet()); + REQUIRE(F.subtracting(A) == EventSet()); + REQUIRE(F.subtracting(C) == EventSet()); + REQUIRE(F.subtracting(D) == EventSet()); + } + } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Subset Tests") +{ + UnfoldingEvent e1, e2, e3, e4; + + // A is a subset of C only + // B is a subset of C only + // D is a subset of C and A + // D is NOT a subset of B + // B is NOT a subset of D + // ... + EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3}, E{&e2, &e3}, F{&e1, &e2, &e3}; + + SECTION("Subset operator properties") + { + SECTION("Subset operator is not commutative") + { + REQUIRE(A.is_subset_of(C)); + REQUIRE_FALSE(C.is_subset_of(A)); + + SECTION("Commutativity implies equality and vice versa") + { + REQUIRE(A.is_subset_of(F)); + REQUIRE(F.is_subset_of(A)); + REQUIRE(A == F); + + REQUIRE(C == C); + REQUIRE(A.is_subset_of(F)); + REQUIRE(F.is_subset_of(A)); + } + } + + SECTION("Subset operator is transitive") + { + REQUIRE(D.is_subset_of(A)); + REQUIRE(A.is_subset_of(C)); + REQUIRE(D.is_subset_of(C)); + REQUIRE(E.is_subset_of(B)); + REQUIRE(B.is_subset_of(C)); + REQUIRE(E.is_subset_of(C)); + } + + SECTION("Subset operator is reflexive") + { + REQUIRE(A.is_subset_of(A)); + REQUIRE(B.is_subset_of(B)); + REQUIRE(C.is_subset_of(C)); + REQUIRE(D.is_subset_of(D)); + REQUIRE(E.is_subset_of(E)); + REQUIRE(F.is_subset_of(F)); + } + } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Testing Configurations") +{ + // The following tests concern the given event structure: + // e1 + // / / + // e2 e5 + // / / / + // e3 e4 e6 + // The tests enumerate all possible subsets of the events + // in the structure and test whether those subsets are + // maximal and/or valid configurations + UnfoldingEvent e1; + UnfoldingEvent e2{&e1}, e5{&e1}; + UnfoldingEvent e3{&e2}, e4{&e2}; + UnfoldingEvent e6{&e5}; + + SECTION("Valid Configurations") + { + SECTION("The empty set is valid") + { + REQUIRE(EventSet().is_valid_configuration()); + } + + SECTION("The set with only the root event is valid") + { + REQUIRE(EventSet({&e1}).is_valid_configuration()); + } + + SECTION("All sets of maximal events are valid configurations") + { + REQUIRE(EventSet({&e1}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e3}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e4}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e5}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e5, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e5}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e5, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e3, &e4}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e3, &e5}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e4, &e5}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_valid_configuration()); + } + } + + SECTION("Configuration checks") + { + // 6 choose 0 = 1 test + REQUIRE(EventSet().is_valid_configuration()); + + // 6 choose 1 = 6 tests + REQUIRE(EventSet({&e1}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e4}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e6}).is_valid_configuration()); + + // 6 choose 2 = 15 tests + REQUIRE(EventSet({&e1, &e2}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e4}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e4}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3, &e4}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e4, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e5, &e6}).is_valid_configuration()); + + // 6 choose 3 = 20 tests + REQUIRE(EventSet({&e1, &e2, &e3}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e4}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e4, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e4, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3, &e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3, &e4, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e4, &e5, &e6}).is_valid_configuration()); + + // 6 choose 4 = 15 tests + REQUIRE(EventSet({&e1, &e2, &e3, &e4}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e3, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e4, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e4, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e3, &e4, &e5, &e6}).is_valid_configuration()); + + // 6 choose 5 = 6 tests + REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e3, &e5, &e6}).is_valid_configuration()); + REQUIRE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5, &e6}).is_valid_configuration()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5, &e6}).is_valid_configuration()); + + // 6 choose 6 = 1 test + REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_valid_configuration()); + } + + SECTION("Maximal event sets") + { + // 6 choose 0 = 1 test + REQUIRE(EventSet().is_maximal_event_set()); + + // 6 choose 1 = 6 tests + REQUIRE(EventSet({&e1}).is_maximal_event_set()); + REQUIRE(EventSet({&e2}).is_maximal_event_set()); + REQUIRE(EventSet({&e3}).is_maximal_event_set()); + REQUIRE(EventSet({&e4}).is_maximal_event_set()); + REQUIRE(EventSet({&e5}).is_maximal_event_set()); + REQUIRE(EventSet({&e6}).is_maximal_event_set()); + + // 6 choose 2 = 15 tests + REQUIRE_FALSE(EventSet({&e1, &e2}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e4}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e4}).is_maximal_event_set()); + REQUIRE(EventSet({&e2, &e5}).is_maximal_event_set()); + REQUIRE(EventSet({&e2, &e6}).is_maximal_event_set()); + REQUIRE(EventSet({&e3, &e4}).is_maximal_event_set()); + REQUIRE(EventSet({&e3, &e5}).is_maximal_event_set()); + REQUIRE(EventSet({&e3, &e6}).is_maximal_event_set()); + REQUIRE(EventSet({&e4, &e5}).is_maximal_event_set()); + REQUIRE(EventSet({&e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e5, &e6}).is_maximal_event_set()); + + // 6 choose 3 = 20 tests + REQUIRE_FALSE(EventSet({&e1, &e2, &e3}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e4}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e4, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e4, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e5, &e6}).is_maximal_event_set()); + REQUIRE(EventSet({&e3, &e4, &e5}).is_maximal_event_set()); + REQUIRE(EventSet({&e3, &e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e3, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e4, &e5, &e6}).is_maximal_event_set()); + + // 6 choose 4 = 15 tests + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e4, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e4, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e3, &e4, &e5, &e6}).is_maximal_event_set()); + + // 6 choose 5 = 6 tests + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5, &e6}).is_maximal_event_set()); + REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5, &e6}).is_maximal_event_set()); + + // 6 choose 6 = 1 test + REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_maximal_event_set()); + } +} \ No newline at end of file diff --git a/src/mc/explo/udpor/History.cpp b/src/mc/explo/udpor/History.cpp new file mode 100644 index 0000000000..544980a8cf --- /dev/null +++ b/src/mc/explo/udpor/History.cpp @@ -0,0 +1,92 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/udpor/History.hpp" +#include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" + +#include + +namespace simgrid::mc::udpor { + +History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config) + : frontier(initial_events), maximal_events(initial_events), configuration(config) +{ + // NOTE: Only events in the initial set of events can ever hope to have + // a chance at being a maximal event, since all other events in + // the search are generate by looking at dependencies of these events + // and all subsequent events that are added by the iterator +} + +History::Iterator& History::Iterator::operator++() +{ + if (not frontier.empty()) { + // "Pop" the event at the "front" + UnfoldingEvent* e = *frontier.begin(); + frontier.remove(e); + + // If there is a configuration and if the + // event is in it, skip it: the event and + // all of its immediate causes do not need to + // be searched since the configuration contains + // them (configuration invariant) + if (configuration.has_value() && configuration->get().contains(e)) { + return *this; + } + + // Mark this event as seen + current_history.insert(e); + + // Perform the expansion with all viable expansions + EventSet candidates = e->get_immediate_causes(); + + maximal_events.subtract(candidates); + + candidates.subtract(current_history); + frontier.form_union(std::move(candidates)); + } + return *this; +} + +EventSet History::get_all_events() const +{ + auto first = this->begin(); + const auto last = this->end(); + + for (; first != last; ++first) + ; + + return first.current_history; +} + +EventSet History::get_all_maximal_events() const +{ + auto first = this->begin(); + const auto last = this->end(); + + for (; first != last; ++first) + ; + + return first.maximal_events; +} + +bool History::contains(UnfoldingEvent* e) const +{ + return std::any_of(this->begin(), this->end(), [=](UnfoldingEvent* e_hist) { return e == e_hist; }); +} + +EventSet History::get_event_diff_with(const Configuration& config) const +{ + auto wrapped_config = std::optional>{config}; + auto first = Iterator(events_, std::move(wrapped_config)); + const auto last = this->end(); + + for (; first != last; ++first) + ; + + return first.current_history; +} + +} // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/History.hpp b/src/mc/explo/udpor/History.hpp new file mode 100644 index 0000000000..e667424175 --- /dev/null +++ b/src/mc/explo/udpor/History.hpp @@ -0,0 +1,139 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_UDPOR_HISTORY_HPP +#define SIMGRID_MC_UDPOR_HISTORY_HPP + +#include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/udpor_forward.hpp" + +#include +#include + +namespace simgrid::mc::udpor { + +/** + * @brief Conceptually describes the local configuration(s) of + * an event or a collection of events, encoding the history of + * the events without needing to actually fully compute all of + * the events contained in the history + * + * When you create an instance of `History`, you are effectively + * making a "lazy" configuration whose elements are the set of + * causes of a given event (if the `History` constists of a single + * event) or the union of all causes of all events (if the + * `History` consists of a set of events). + * + * Using a `History` object to represent the history of a set of + * events is more efficient (and reads more easily) than first + * computing the entire history of each of the events separately + * and combining the results. The former can take advantage of the + * fact that the histories of a set of events overlap greatly, and + * thus only a single BFS/DFS search over the event structure needs + * to be performed instead of many isolated searches for each event. + * + * The same observation also allows you to compute the difference between + * a configuration and a history of a set of events. This is used + * in UDPOR, for example, when determing the difference J / C and + * when using K-partial alternatives (which computes J as the union + * of histories of events) + */ +class History { +private: + /** + * @brief The events whose history this instance describes + */ + EventSet events_; + +public: + History(const History&) = default; + History& operator=(History const&) = default; + History(History&&) = default; + + explicit History(UnfoldingEvent* e) : events_({e}) {} + explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {} + + auto begin() const { return Iterator(events_); } + auto end() const { return Iterator(EventSet()); } + + /** + * @brief Whether or not the given event is contained in the history + * + * @note If you only need to determine whether a few events are contained + * in a history, prefer this method. If, however, you wish to repeatedly + * determine over time (e.g. over the course of a computation) whether + * some event is part of the history, it may be better to first compute + * all events (see `History::get_all_events()`) and reuse this set + * + * @param e the event to check + * @returns whether or not `e` is contained in the collection + */ + bool contains(UnfoldingEvent* e) const; + + /** + * @brief Computes all events in the history described by this instance + * + * Sometimes, it is useful to compute the entire set of events that + * comprise the history of some event `e` of some set of events `E`. + * This method performs that computation. + * + * @returns the set of all causal dependencies of all events this + * history represents. Equivalently, the method returns the full + * dependency graph for all events in this history + */ + EventSet get_all_events() const; + + /** + * @brief Computes all events in the history described by this instance + * which are maximal (intuitively, those events which cause no others + * or are the "most recent") + */ + EventSet get_all_maximal_events() const; + + EventSet get_event_diff_with(const Configuration& config) const; + +private: + /** + * @brief An iterator which traverses the history of a set of events + */ + struct Iterator { + public: + Iterator& operator++(); + auto operator->() { return frontier.begin().operator->(); } + auto operator*() const { return *frontier.begin(); } + + // If what the iterator sees next is the same, we consider them + // to be the same iterator. This way, once the iterator has completed + // its search, it will be "equal" to an iterator searching nothing + bool operator==(const Iterator& other) { return this->frontier == other.frontier; } + bool operator!=(const Iterator& other) { return not(this->operator==(other)); } + + using iterator_category = std::forward_iterator_tag; + using difference_type = int; // # of steps between + using value_type = UnfoldingEvent*; + using pointer = value_type*; + using reference = value_type&; + using optional_configuration = std::optional>; + + Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt); + + private: + /// @brief Points in the graph from where to continue the search + EventSet frontier; + + /// @brief What the iterator currently believes to be the + /// entire history of the events in the graph it traverses + EventSet current_history = EventSet(); + + /// @brief What the iterator currently believes + EventSet maximal_events; + optional_configuration configuration; + friend History; + }; +}; + +} // namespace simgrid::mc::udpor +#endif diff --git a/src/mc/explo/udpor/History_test.cpp b/src/mc/explo/udpor/History_test.cpp new file mode 100644 index 0000000000..0cbe87881a --- /dev/null +++ b/src/mc/explo/udpor/History_test.cpp @@ -0,0 +1,212 @@ +/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/3rd-party/catch.hpp" +#include "src/mc/explo/udpor/History.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" + +using namespace simgrid::mc::udpor; + +TEST_CASE("simgrid::mc::udpor::History: History generation") +{ + // The following tests concern the given event tree + // e1 + // / / + // e2 e6 + // | \ \ / / + // e3 e4 e5 e7 + UnfoldingEvent e1; + UnfoldingEvent e2{&e1}, e6{&e1}; + UnfoldingEvent e3{&e2}, e4{&e2}; + UnfoldingEvent e5{&e2, &e6}, e7{&e6}; + + SECTION("History with no events") + { + History history; + REQUIRE(history.get_all_events() == EventSet()); + REQUIRE_FALSE(history.contains(&e1)); + REQUIRE_FALSE(history.contains(&e2)); + REQUIRE_FALSE(history.contains(&e3)); + REQUIRE_FALSE(history.contains(&e4)); + REQUIRE_FALSE(history.contains(&e5)); + REQUIRE_FALSE(history.contains(&e6)); + REQUIRE_FALSE(history.contains(&e7)); + } + + SECTION("Histories with a single event") + { + SECTION("Root event's history has a single event") + { + History history(&e1); + REQUIRE(history.get_all_events() == EventSet({&e1})); + } + + SECTION("Check node e2") + { + History history(&e2); + REQUIRE(history.get_all_events() == EventSet({&e1, &e2})); + REQUIRE(history.contains(&e1)); + REQUIRE(history.contains(&e2)); + REQUIRE_FALSE(history.contains(&e3)); + REQUIRE_FALSE(history.contains(&e4)); + REQUIRE_FALSE(history.contains(&e5)); + REQUIRE_FALSE(history.contains(&e6)); + REQUIRE_FALSE(history.contains(&e7)); + } + + SECTION("Check node e3") + { + History history(&e3); + REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e3})); + REQUIRE(history.contains(&e1)); + REQUIRE(history.contains(&e2)); + REQUIRE(history.contains(&e3)); + REQUIRE_FALSE(history.contains(&e4)); + REQUIRE_FALSE(history.contains(&e5)); + REQUIRE_FALSE(history.contains(&e6)); + REQUIRE_FALSE(history.contains(&e7)); + } + + SECTION("Check node e4") + { + History history(&e4); + REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e4})); + REQUIRE(history.contains(&e1)); + REQUIRE(history.contains(&e2)); + REQUIRE_FALSE(history.contains(&e3)); + REQUIRE(history.contains(&e4)); + REQUIRE_FALSE(history.contains(&e5)); + REQUIRE_FALSE(history.contains(&e6)); + REQUIRE_FALSE(history.contains(&e7)); + } + + SECTION("Check node e5") + { + History history(&e5); + REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e6, &e5})); + REQUIRE(history.contains(&e1)); + REQUIRE(history.contains(&e2)); + REQUIRE_FALSE(history.contains(&e3)); + REQUIRE_FALSE(history.contains(&e4)); + REQUIRE(history.contains(&e5)); + REQUIRE(history.contains(&e6)); + REQUIRE_FALSE(history.contains(&e7)); + } + + SECTION("Check node e6") + { + History history(&e6); + REQUIRE(history.get_all_events() == EventSet({&e1, &e6})); + REQUIRE(history.contains(&e1)); + REQUIRE_FALSE(history.contains(&e2)); + REQUIRE_FALSE(history.contains(&e3)); + REQUIRE_FALSE(history.contains(&e4)); + REQUIRE_FALSE(history.contains(&e5)); + REQUIRE(history.contains(&e6)); + REQUIRE_FALSE(history.contains(&e7)); + } + + SECTION("Check node e7") + { + History history(&e7); + REQUIRE(history.get_all_events() == EventSet({&e1, &e6, &e7})); + REQUIRE(history.contains(&e1)); + REQUIRE_FALSE(history.contains(&e2)); + REQUIRE_FALSE(history.contains(&e3)); + REQUIRE_FALSE(history.contains(&e4)); + REQUIRE_FALSE(history.contains(&e5)); + REQUIRE(history.contains(&e6)); + REQUIRE(history.contains(&e7)); + } + } + + SECTION("Histories with multiple nodes") + { + SECTION("Nodes contained in the same branch") + { + History history_e1e2(EventSet({&e1, &e2})); + REQUIRE(history_e1e2.get_all_events() == EventSet({&e1, &e2})); + REQUIRE(history_e1e2.contains(&e1)); + REQUIRE(history_e1e2.contains(&e2)); + REQUIRE_FALSE(history_e1e2.contains(&e3)); + REQUIRE_FALSE(history_e1e2.contains(&e4)); + REQUIRE_FALSE(history_e1e2.contains(&e5)); + REQUIRE_FALSE(history_e1e2.contains(&e6)); + REQUIRE_FALSE(history_e1e2.contains(&e7)); + + History history_e1e3(EventSet({&e1, &e3})); + REQUIRE(history_e1e3.get_all_events() == EventSet({&e1, &e2, &e3})); + REQUIRE(history_e1e3.contains(&e1)); + REQUIRE(history_e1e3.contains(&e2)); + REQUIRE(history_e1e3.contains(&e3)); + REQUIRE_FALSE(history_e1e3.contains(&e4)); + REQUIRE_FALSE(history_e1e3.contains(&e5)); + REQUIRE_FALSE(history_e1e3.contains(&e6)); + REQUIRE_FALSE(history_e1e3.contains(&e7)); + + History history_e6e7(EventSet({&e6, &e7})); + REQUIRE(history_e6e7.get_all_events() == EventSet({&e1, &e6, &e7})); + REQUIRE(history_e6e7.contains(&e1)); + REQUIRE_FALSE(history_e6e7.contains(&e2)); + REQUIRE_FALSE(history_e6e7.contains(&e3)); + REQUIRE_FALSE(history_e6e7.contains(&e4)); + REQUIRE_FALSE(history_e6e7.contains(&e5)); + REQUIRE(history_e6e7.contains(&e6)); + REQUIRE(history_e6e7.contains(&e7)); + } + + SECTION("Nodes with the same ancestor") + { + History history_e3e5(EventSet({&e3, &e5})); + REQUIRE(history_e3e5.get_all_events() == EventSet({&e1, &e2, &e3, &e5, &e6})); + REQUIRE(history_e3e5.contains(&e1)); + REQUIRE(history_e3e5.contains(&e2)); + REQUIRE(history_e3e5.contains(&e3)); + REQUIRE_FALSE(history_e3e5.contains(&e4)); + REQUIRE(history_e3e5.contains(&e5)); + REQUIRE(history_e3e5.contains(&e6)); + REQUIRE_FALSE(history_e3e5.contains(&e7)); + } + + SECTION("Nodes with different ancestors") + { + History history_e4e7(EventSet({&e4, &e7})); + REQUIRE(history_e4e7.get_all_events() == EventSet({&e1, &e2, &e4, &e6, &e7})); + REQUIRE(history_e4e7.contains(&e1)); + REQUIRE(history_e4e7.contains(&e2)); + REQUIRE_FALSE(history_e4e7.contains(&e3)); + REQUIRE(history_e4e7.contains(&e4)); + REQUIRE_FALSE(history_e4e7.contains(&e5)); + REQUIRE(history_e4e7.contains(&e6)); + REQUIRE(history_e4e7.contains(&e7)); + } + + SECTION("Large number of nodes") + { + History history_e2356(EventSet({&e2, &e3, &e5, &e6})); + REQUIRE(history_e2356.get_all_events() == EventSet({&e1, &e2, &e3, &e5, &e6})); + REQUIRE(history_e2356.contains(&e1)); + REQUIRE(history_e2356.contains(&e2)); + REQUIRE(history_e2356.contains(&e3)); + REQUIRE_FALSE(history_e2356.contains(&e4)); + REQUIRE(history_e2356.contains(&e5)); + REQUIRE(history_e2356.contains(&e6)); + REQUIRE_FALSE(history_e2356.contains(&e7)); + } + + SECTION("History of the entire graph yields the entire graph") + { + History history(EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7})); + REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7})); + REQUIRE(history.contains(&e1)); + REQUIRE(history.contains(&e2)); + REQUIRE(history.contains(&e3)); + REQUIRE(history.contains(&e4)); + REQUIRE(history.contains(&e5)); + REQUIRE(history.contains(&e6)); + REQUIRE(history.contains(&e7)); + } + } +} diff --git a/src/mc/explo/udpor/Unfolding.cpp b/src/mc/explo/udpor/Unfolding.cpp new file mode 100644 index 0000000000..abe9f26e7e --- /dev/null +++ b/src/mc/explo/udpor/Unfolding.cpp @@ -0,0 +1,36 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/udpor/Unfolding.hpp" + +#include + +namespace simgrid::mc::udpor { + +void Unfolding::remove(UnfoldingEvent* e) +{ + if (e == nullptr) { + throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL"); + } + this->global_events_.erase(e); +} + +void Unfolding::insert(std::unique_ptr e) +{ + UnfoldingEvent* handle = e.get(); + auto loc = this->global_events_.find(handle); + if (loc != this->global_events_.end()) { + // This is bad: someone wrapped the raw event address twice + // in two different unique ptrs and attempted to + // insert it into the unfolding... + throw std::invalid_argument("Attempted to insert an unfolding event owned twice." + "This will result in a double free error and must be fixed."); + } + + // Map the handle to its owner + this->global_events_[handle] = std::move(e); +} + +} // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/Unfolding.hpp b/src/mc/explo/udpor/Unfolding.hpp new file mode 100644 index 0000000000..471e04330a --- /dev/null +++ b/src/mc/explo/udpor/Unfolding.hpp @@ -0,0 +1,42 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP +#define SIMGRID_MC_UDPOR_UNFOLDING_HPP + +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" +#include "src/mc/explo/udpor/udpor_forward.hpp" + +#include +#include + +namespace simgrid::mc::udpor { + +class Unfolding { +private: + /** + * @brief All of the events that are currently are a part of the unfolding + * + * @invariant Each unfolding event maps itself to the owner of that event, + * i.e. the unique pointer that owns the address. The Unfolding owns all + * of the addresses that are referenced by EventSet instances and Configuration + * instances. UDPOR guarantees that events are persisted for as long as necessary + */ + std::unordered_map> global_events_; + +public: + Unfolding() = default; + Unfolding& operator=(Unfolding&&) = default; + Unfolding(Unfolding&&) = default; + + void remove(UnfoldingEvent* e); + void insert(std::unique_ptr e); + + size_t size() const { return this->global_events_.size(); } + bool empty() const { return this->global_events_.empty(); } +}; + +} // namespace simgrid::mc::udpor +#endif diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp new file mode 100644 index 0000000000..ee6de7cba1 --- /dev/null +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -0,0 +1,37 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" + +namespace simgrid::mc::udpor { + +UnfoldingEvent::UnfoldingEvent(std::initializer_list init_list) + : UnfoldingEvent(EventSet(std::move(init_list))) +{ +} + +UnfoldingEvent::UnfoldingEvent(EventSet immediate_causes, std::shared_ptr transition) + : associated_transition(std::move(transition)), immediate_causes(std::move(immediate_causes)) +{ +} + +bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const +{ + const bool same_actor = associated_transition->aid_ == other.associated_transition->aid_; + if (!same_actor) + return false; + + // TODO: Add in information to determine which step in the sequence this actor was executed + + // All unfolding event objects are created in reference to + // an Unfolding object which owns them. Hence, the references + // they contain to other events in the unfolding can + // be used as intrinsic identities (i.e. we don't need to + // recursively check if each of our causes has a `==` in + // the other event's causes) + return this->immediate_causes == other.immediate_causes; +} + +} // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp new file mode 100644 index 0000000000..2bd29e991b --- /dev/null +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -0,0 +1,75 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_UDPOR_UNFOLDING_EVENT_HPP +#define SIMGRID_MC_UDPOR_UNFOLDING_EVENT_HPP + +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/udpor_forward.hpp" +#include "src/mc/transition/Transition.hpp" + +#include +#include +#include + +namespace simgrid::mc::udpor { + +class UnfoldingEvent { +public: + UnfoldingEvent(std::initializer_list init_list); + UnfoldingEvent(EventSet immediate_causes = EventSet(), + std::shared_ptr transition = std::make_unique()); + + UnfoldingEvent(const UnfoldingEvent&) = default; + UnfoldingEvent& operator=(UnfoldingEvent const&) = default; + UnfoldingEvent(UnfoldingEvent&&) = default; + + EventSet get_history() const; + bool in_history_of(const UnfoldingEvent* otherEvent) const; + + bool conflicts_with(const UnfoldingEvent* otherEvent) const; + bool conflicts_with(const Configuration& config) const; + bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const; + + const EventSet& get_immediate_causes() const { return this->immediate_causes; } + Transition* get_transition() const { return this->associated_transition.get(); } + + bool operator==(const UnfoldingEvent&) const; + +private: + /** + * @brief The transition that UDPOR "attaches" to this + * specific event for later use while computing e.g. extension + * sets + * + * The transition points to that of a particular actor + * in the state reached by the configuration C (recall + * this is denoted `state(C)`) that excludes this event. + * In other words, this transition was the "next" event + * of the actor that executes it in `state(C)`. + */ + std::shared_ptr associated_transition; + + /** + * @brief The "immediate" causes of this event. + * + * An event `e` is an immediate cause of an event `e'` if + * + * 1. e < e' + * 2. There is no event `e''` in E such that + * `e < e''` and `e'' < e'` + * + * Intuitively, an immediate cause "happened right before" + * this event was executed. It is sufficient to store + * only the immediate causes of any event `e`, as any indirect + * causes of that event would either be an indirect cause + * or an immediate cause of the immediate causes of `e`, and + * so on. + */ + EventSet immediate_causes; +}; + +} // namespace simgrid::mc::udpor +#endif \ No newline at end of file diff --git a/src/mc/explo/udpor/UnfoldingEvent_test.cpp b/src/mc/explo/udpor/UnfoldingEvent_test.cpp new file mode 100644 index 0000000000..1623fd3eab --- /dev/null +++ b/src/mc/explo/udpor/UnfoldingEvent_test.cpp @@ -0,0 +1,9 @@ +/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/3rd-party/catch.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" + +using namespace simgrid::mc::udpor; diff --git a/src/mc/explo/udpor/Unfolding_test.cpp b/src/mc/explo/udpor/Unfolding_test.cpp new file mode 100644 index 0000000000..4e6f627309 --- /dev/null +++ b/src/mc/explo/udpor/Unfolding_test.cpp @@ -0,0 +1,41 @@ +/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/3rd-party/catch.hpp" +#include "src/mc/explo/udpor/Unfolding.hpp" + +using namespace simgrid::mc::udpor; + +TEST_CASE("simgrid::mc::udpor::Unfolding: Creating an unfolding") +{ + Unfolding unfolding; + REQUIRE(unfolding.size() == 0); + REQUIRE(unfolding.empty()); +} + +TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an unfolding") +{ + Unfolding unfolding; + auto e1 = std::make_unique(); + auto e2 = std::make_unique(); + auto e1_handle = e1.get(); + auto e2_handle = e2.get(); + + unfolding.insert(std::move(e1)); + REQUIRE(unfolding.size() == 1); + REQUIRE_FALSE(unfolding.empty()); + + unfolding.insert(std::move(e2)); + REQUIRE(unfolding.size() == 2); + REQUIRE_FALSE(unfolding.empty()); + + unfolding.remove(e1_handle); + REQUIRE(unfolding.size() == 1); + REQUIRE_FALSE(unfolding.empty()); + + unfolding.remove(e2_handle); + REQUIRE(unfolding.size() == 0); + REQUIRE(unfolding.empty()); +} \ No newline at end of file diff --git a/src/mc/explo/udpor/udpor_forward.hpp b/src/mc/explo/udpor/udpor_forward.hpp new file mode 100644 index 0000000000..10082359fb --- /dev/null +++ b/src/mc/explo/udpor/udpor_forward.hpp @@ -0,0 +1,24 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +/** @file mc_forward.hpp + * + * Forward definitions for MC types specific to UDPOR + */ + +#ifndef SIMGRID_MC_UDPOR_FORWARD_HPP +#define SIMGRID_MC_UDPOR_FORWARD_HPP + +namespace simgrid::mc::udpor { + +class EventSet; +class Configuration; +class History; +class Unfolding; +class UnfoldingEvent; + +} // namespace simgrid::mc::udpor + +#endif diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 9db7806dc8..a32ece169d 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -217,10 +217,8 @@ void AppSide::handle_actors_status() const } XBT_DEBUG("Deliver ACTOR_TRANSITION_PROBE payload"); - for (const auto& probe : probes) { - size_t size = sizeof(s_mc_message_simcall_probe_one_t); - xbt_assert(channel_.send(&probe, size) == 0, "Could not send ACTOR_TRANSITION_PROBE payload (%zu bytes)", size); - } + for (const auto& probe : probes) + xbt_assert(channel_.send(probe) == 0, "Could not send ACTOR_TRANSITION_PROBE payload"); } } diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h index 8636b5c2d5..435d60db7d 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -118,8 +118,8 @@ struct s_mc_message_actors_status_one_t { // an array of `s_mc_message_actors_st }; // Answer from an actor to the question "what are you about to run?" -struct s_mc_message_simcall_probe_one_t { // an array of `s_mc_message_simcall_probe_one_t[n_transitions] - // is sent right after a `s_mc_message_actors_status_one_t` +struct s_mc_message_simcall_probe_one_t { // a series of `s_mc_message_simcall_probe_one_t` + // is sent right after `s_mc_message_actors_status_one_t[]` std::array buffer; }; diff --git a/src/mc/udpor_global.cpp b/src/mc/udpor_global.cpp deleted file mode 100644 index be3726b885..0000000000 --- a/src/mc/udpor_global.cpp +++ /dev/null @@ -1,33 +0,0 @@ -/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#include "udpor_global.hpp" -#include "xbt/log.h" -#include - -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor_global, mc, "udpor_global"); - -namespace simgrid::mc { - -EventSet EvtSetTools::makeUnion(const EventSet& s1, const EventSet& s2) -{ - EventSet res = s1; - for (auto evt : s2) - EvtSetTools::pushBack(res, evt); - return res; -} - -void EvtSetTools::pushBack(EventSet& events, UnfoldingEvent* e) -{ - if (not EvtSetTools::contains(events, e)) - events.push_back(e); -} - -bool EvtSetTools::contains(const EventSet& events, const UnfoldingEvent* e) -{ - return std::any_of(events.begin(), events.end(), [e](const UnfoldingEvent* evt) { return *evt == *e; }); -} - -} // namespace simgrid::mc diff --git a/src/mc/udpor_global.hpp b/src/mc/udpor_global.hpp deleted file mode 100644 index 1b3e90ea78..0000000000 --- a/src/mc/udpor_global.hpp +++ /dev/null @@ -1,98 +0,0 @@ -/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#ifndef SIMGRID_MC_UDPOR_GLOBAL_HPP -#define SIMGRID_MC_UDPOR_GLOBAL_HPP - -#include -#include -#include - -/* TODO: many method declared in this module are not implemented */ - -namespace simgrid::mc { - -class UnfoldingEvent; -using EventSet = std::deque; - -class EvtSetTools { -public: - static bool contains(const EventSet& events, const UnfoldingEvent* e); - static UnfoldingEvent* find(const EventSet& events, const UnfoldingEvent* e); - static void subtract(EventSet& events, EventSet const& otherSet); - static bool depends(const EventSet& events, const EventSet& otherSet); - static bool isEmptyIntersection(EventSet evtS1, EventSet evtS2); - static EventSet makeUnion(const EventSet& s1, const EventSet& s2); - static void pushBack(EventSet& events, UnfoldingEvent* e); - static void remove(EventSet& events, UnfoldingEvent* e); - static EventSet minus(EventSet events, UnfoldingEvent* e); - static EventSet plus(EventSet events, UnfoldingEvent* e); -}; - -struct s_evset_in_t { - EventSet causuality_events; - EventSet cause; - EventSet ancestorSet; -}; - -class Configuration { -public: - EventSet events_; - EventSet maxEvent; // Events recently added to events_ - EventSet actorMaxEvent; // maximal events of the actors in current configuration - UnfoldingEvent* lastEvent; // The last added event - - Configuration plus_config(UnfoldingEvent*) const; - void createEvts(Configuration C, EventSet& result, const std::string& trans_tag, s_evset_in_t ev_sets, bool chk, - UnfoldingEvent* immPreEvt); - void updateMaxEvent(UnfoldingEvent*); // update maximal events of the configuration and actors - UnfoldingEvent* findActorMaxEvt(int actorId); // find maximal event of a Actor whose id = actorId - - UnfoldingEvent* findTestedComm(const UnfoldingEvent* testEvt); // find comm tested by action testTrans - - Configuration() = default; - Configuration(const Configuration&) = default; - Configuration& operator=(Configuration const&) = default; - Configuration(Configuration&&) = default; -}; - -class UnfoldingEvent { -public: - UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes, int sid = -1); - UnfoldingEvent(const UnfoldingEvent&) = default; - UnfoldingEvent& operator=(UnfoldingEvent const&) = default; - UnfoldingEvent(UnfoldingEvent&&) = default; - - EventSet getHistory() const; - - bool isConflict(UnfoldingEvent* event, UnfoldingEvent* otherEvent) const; - bool concernSameComm(const UnfoldingEvent* event, const UnfoldingEvent* otherEvent) const; - - // check otherEvent is in my history ? - bool inHistory(UnfoldingEvent* otherEvent) const; - - bool isImmediateConflict1(UnfoldingEvent* evt, UnfoldingEvent* otherEvt) const; - - bool conflictWithConfig(UnfoldingEvent* event, Configuration const& config) const; - bool operator==(const UnfoldingEvent&) const { return false; }; - void print() const; - - inline int get_state_id() const { return state_id; } - inline void set_state_id(int sid) { state_id = sid; } - - inline std::string get_transition_tag() const { return transition_tag; } - inline void set_transition_tag(std::string_view tr_tag) { transition_tag = tr_tag; } - -private: - EventSet causes; // used to store directed ancestors of event e - int id = -1; - int state_id{-1}; - std::string transition_tag{""}; // The tag of the last transition that lead to creating the event - bool transition_is_IReceive(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const; - bool transition_is_ISend(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const; - bool check_tr_concern_same_comm(bool& chk1, bool& chk2, UnfoldingEvent* evt1, UnfoldingEvent* evt2) const; -}; -} // namespace simgrid::mc -#endif diff --git a/src/s4u/s4u_Actor.cpp b/src/s4u/s4u_Actor.cpp index 1e022aa5ea..3e84903f38 100644 --- a/src/s4u/s4u_Actor.cpp +++ b/src/s4u/s4u_Actor.cpp @@ -413,7 +413,7 @@ ExecPtr exec_async(double flops) aid_t get_pid() { - auto* self = simgrid::kernel::actor::ActorImpl::self(); + const auto* self = simgrid::kernel::actor::ActorImpl::self(); return self ? self->get_pid() : 0; } @@ -429,7 +429,7 @@ std::string get_name() const char* get_cname() { - auto* self = simgrid::kernel::actor::ActorImpl::self(); + const auto* self = simgrid::kernel::actor::ActorImpl::self(); return self ? self->get_cname() : nullptr; } diff --git a/src/s4u/s4u_Engine.cpp b/src/s4u/s4u_Engine.cpp index de66d412c8..a782de7a2d 100644 --- a/src/s4u/s4u_Engine.cpp +++ b/src/s4u/s4u_Engine.cpp @@ -592,7 +592,7 @@ Engine* Engine::set_default_comm_data_copy_callback( /* **************************** Public C interface *************************** */ void simgrid_init(int* argc, char** argv) { - simgrid::s4u::Engine::get_instance(argc, argv); + static simgrid::s4u::Engine e(argc, argv); } void simgrid_load_platform(const char* file) { diff --git a/src/s4u/s4u_Exec.cpp b/src/s4u/s4u_Exec.cpp index 9ea3b10720..c0fcdc06b6 100644 --- a/src/s4u/s4u_Exec.cpp +++ b/src/s4u/s4u_Exec.cpp @@ -31,11 +31,12 @@ void Exec::reset() const ExecPtr Exec::init() { auto pimpl = kernel::activity::ExecImplPtr(new kernel::activity::ExecImpl()); + /* Allow parallel execs to fail if any of their hosts fail */ unsigned int cb_id = Host::on_state_change.connect([pimpl](s4u::Host const& h) { if (not h.is_on() && pimpl->get_state() == kernel::activity::State::RUNNING && std::find(pimpl->get_hosts().begin(), pimpl->get_hosts().end(), &h) != pimpl->get_hosts().end()) { pimpl->set_state(kernel::activity::State::FAILED); - pimpl->post(); + pimpl->finish(); } }); pimpl->set_cb_id(cb_id); diff --git a/src/smpi/mpi/smpi_file.cpp b/src/smpi/mpi/smpi_file.cpp index 57b61704e3..0a78eedeab 100644 --- a/src/smpi/mpi/smpi_file.cpp +++ b/src/smpi/mpi/smpi_file.cpp @@ -17,6 +17,8 @@ #include "simgrid/s4u/Host.hpp" #include "simgrid/plugins/file_system.h" +#include // std::scoped_lock + #define FP_SIZE sizeof(MPI_Offset) XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_io, smpi, "Logging specific to SMPI (RMA operations)"); @@ -117,9 +119,8 @@ int File::get_position(MPI_Offset* offset) const int File::get_position_shared(MPI_Offset* offset) const { - shared_mutex_->lock(); + const std::scoped_lock lock(*shared_mutex_); *offset = *shared_file_pointer_/etype_->get_extent(); - shared_mutex_->unlock(); return MPI_SUCCESS; } @@ -146,10 +147,9 @@ int File::seek(MPI_Offset offset, int whence) int File::seek_shared(MPI_Offset offset, int whence) { - shared_mutex_->lock(); + const std::scoped_lock lock(*shared_mutex_); seek(offset, whence); *shared_file_pointer_ = file_->tell(); - shared_mutex_->unlock(); return MPI_SUCCESS; } @@ -184,11 +184,11 @@ int File::read(MPI_File fh, void* /*buf*/, int count, const Datatype* datatype, /* }*/ int File::read_shared(MPI_File fh, void* buf, int count, const Datatype* datatype, MPI_Status* status) { - fh->shared_mutex_->lock(); - fh->seek(*(fh->shared_file_pointer_), MPI_SEEK_SET); - read(fh, buf, count, datatype, status); - *(fh->shared_file_pointer_) = fh->file_->tell(); - fh->shared_mutex_->unlock(); + if (const std::scoped_lock lock(*fh->shared_mutex_); true) { + fh->seek(*(fh->shared_file_pointer_), MPI_SEEK_SET); + read(fh, buf, count, datatype, status); + *(fh->shared_file_pointer_) = fh->file_->tell(); + } fh->seek(*(fh->shared_file_pointer_), MPI_SEEK_SET); return MPI_SUCCESS; } @@ -210,9 +210,8 @@ int File::read_ordered(MPI_File fh, void* buf, int count, const Datatype* dataty fh->seek(result, MPI_SEEK_SET); int ret = fh->op_all(buf, count, datatype, status); if (fh->comm_->rank() == fh->comm_->size() - 1) { - fh->shared_mutex_->lock(); + const std::scoped_lock lock(*fh->shared_mutex_); *(fh->shared_file_pointer_)=fh->file_->tell(); - fh->shared_mutex_->unlock(); } char c; simgrid::smpi::colls::bcast(&c, 1, MPI_BYTE, fh->comm_->size() - 1, fh->comm_); @@ -241,14 +240,13 @@ int File::write(MPI_File fh, void* /*buf*/, int count, const Datatype* datatype, int File::write_shared(MPI_File fh, const void* buf, int count, const Datatype* datatype, MPI_Status* status) { - fh->shared_mutex_->lock(); + const std::scoped_lock lock(*fh->shared_mutex_); XBT_DEBUG("Write shared on %s - Shared ptr before : %lld", fh->file_->get_path(), *(fh->shared_file_pointer_)); fh->seek(*(fh->shared_file_pointer_), MPI_SEEK_SET); write(fh, const_cast(buf), count, datatype, status); *(fh->shared_file_pointer_) = fh->file_->tell(); XBT_DEBUG("Write shared on %s - Shared ptr after : %lld", fh->file_->get_path(), *(fh->shared_file_pointer_)); fh->seek(*(fh->shared_file_pointer_), MPI_SEEK_SET); - fh->shared_mutex_->unlock(); return MPI_SUCCESS; } @@ -268,9 +266,8 @@ int File::write_ordered(MPI_File fh, const void* buf, int count, const Datatype* fh->seek(result, MPI_SEEK_SET); int ret = fh->op_all(const_cast(buf), count, datatype, status); if (fh->comm_->rank() == fh->comm_->size() - 1) { - fh->shared_mutex_->lock(); + const std::scoped_lock lock(*fh->shared_mutex_); *(fh->shared_file_pointer_)=fh->file_->tell(); - fh->shared_mutex_->unlock(); } char c; simgrid::smpi::colls::bcast(&c, 1, MPI_BYTE, fh->comm_->size() - 1, fh->comm_); diff --git a/src/smpi/mpi/smpi_request.cpp b/src/smpi/mpi/smpi_request.cpp index 1a24c54631..f2a700da71 100644 --- a/src/smpi/mpi/smpi_request.cpp +++ b/src/smpi/mpi/smpi_request.cpp @@ -24,6 +24,7 @@ #include #include +#include // std::scoped_lock and std::unique_lock XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_request, smpi, "Logging specific to SMPI (request)"); @@ -463,9 +464,9 @@ void Request::start() simgrid::smpi::ActorExt* process = smpi_process_remote(simgrid::s4u::Actor::by_pid(dst_)); - simgrid::s4u::MutexPtr mut = process->mailboxes_mutex(); + std::unique_lock mut_lock; if (smpi_cfg_async_small_thresh() != 0 || (flags_ & MPI_REQ_RMA) != 0) - mut->lock(); + mut_lock = std::unique_lock(*process->mailboxes_mutex()); bool is_probe = ((flags_ & MPI_REQ_PROBE) != 0); flags_ |= MPI_REQ_PROBE; @@ -520,9 +521,6 @@ void Request::start() &observer); XBT_DEBUG("recv simcall posted"); - - if (smpi_cfg_async_small_thresh() != 0 || (flags_ & MPI_REQ_RMA) != 0) - mut->unlock(); } else { /* the RECV flag was not set, so this is a send */ const simgrid::smpi::ActorExt* process = smpi_process_remote(simgrid::s4u::Actor::by_pid(dst_)); xbt_assert(process, "Actor pid=%ld is gone??", dst_); @@ -574,10 +572,9 @@ void Request::start() XBT_DEBUG("sending size of %zu : sleep %f ", size_, sleeptime); } - simgrid::s4u::MutexPtr mut = process->mailboxes_mutex(); - + std::unique_lock mut_lock; if (smpi_cfg_async_small_thresh() != 0 || (flags_ & MPI_REQ_RMA) != 0) - mut->lock(); + mut_lock = std::unique_lock(*process->mailboxes_mutex()); if (not(smpi_cfg_async_small_thresh() != 0 || (flags_ & MPI_REQ_RMA) != 0)) { mailbox = process->mailbox(); @@ -629,9 +626,6 @@ void Request::start() boost::static_pointer_cast(action_)->set_tracing_category( smpi_process()->get_tracing_category()); } - - if (smpi_cfg_async_small_thresh() != 0 || ((flags_ & MPI_REQ_RMA) != 0)) - mut->unlock(); } } @@ -1093,9 +1087,8 @@ int Request::wait(MPI_Request * request, MPI_Status * status) if ((*request)->flags_ & MPI_REQ_GENERALIZED) { if (not((*request)->flags_ & MPI_REQ_COMPLETE)) { - ((*request)->generalized_funcs)->mutex->lock(); - ((*request)->generalized_funcs)->cond->wait(((*request)->generalized_funcs)->mutex); - ((*request)->generalized_funcs)->mutex->unlock(); + const std::scoped_lock lock(*(*request)->generalized_funcs->mutex); + (*request)->generalized_funcs->cond->wait((*request)->generalized_funcs->mutex); } MPI_Status tmp_status; MPI_Status* mystatus; @@ -1331,10 +1324,9 @@ int Request::grequest_complete(MPI_Request request) { if ((not(request->flags_ & MPI_REQ_GENERALIZED)) || request->generalized_funcs->mutex == nullptr) return MPI_ERR_REQUEST; - request->generalized_funcs->mutex->lock(); + const std::scoped_lock lock(*request->generalized_funcs->mutex); request->flags_ |= MPI_REQ_COMPLETE; // in case wait would be called after complete request->generalized_funcs->cond->notify_one(); - request->generalized_funcs->mutex->unlock(); return MPI_SUCCESS; } diff --git a/src/smpi/mpi/smpi_win.cpp b/src/smpi/mpi/smpi_win.cpp index c40ac06d17..7b33c80243 100644 --- a/src/smpi/mpi/smpi_win.cpp +++ b/src/smpi/mpi/smpi_win.cpp @@ -17,6 +17,7 @@ #include "src/mc/mc_replay.hpp" #include +#include // std::scoped_lock XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_rma, smpi, "Logging specific to SMPI (RMA operations)"); @@ -239,16 +240,14 @@ int Win::put(const void *origin_addr, int origin_count, MPI_Datatype origin_data if(request!=nullptr){ *request=sreq; }else{ - mut_->lock(); + const std::scoped_lock lock(*mut_); requests_.push_back(sreq); - mut_->unlock(); } //push request to receiver's win - recv_win->mut_->lock(); + const std::scoped_lock recv_lock(*recv_win->mut_); recv_win->requests_.push_back(rreq); rreq->start(); - recv_win->mut_->unlock(); } else { XBT_DEBUG("Entering MPI_Put from myself to myself, rank %d", target_rank); Datatype::copy(origin_addr, origin_count, origin_datatype, recv_addr, target_count, target_datatype); @@ -283,9 +282,9 @@ int Win::get( void *origin_addr, int origin_count, MPI_Datatype origin_datatype, //start the send, with another process than us as sender. sreq->start(); // push request to sender's win - send_win->mut_->lock(); - send_win->requests_.push_back(sreq); - send_win->mut_->unlock(); + if (const std::scoped_lock send_lock(*send_win->mut_); true) { + send_win->requests_.push_back(sreq); + } //start recv rreq->start(); @@ -293,9 +292,8 @@ int Win::get( void *origin_addr, int origin_count, MPI_Datatype origin_datatype, if(request!=nullptr){ *request=rreq; }else{ - mut_->lock(); + const std::scoped_lock lock(*mut_); requests_.push_back(rreq); - mut_->unlock(); } } else { Datatype::copy(send_addr, target_count, target_datatype, origin_addr, origin_count, origin_datatype); @@ -334,17 +332,16 @@ int Win::accumulate(const void *origin_addr, int origin_count, MPI_Datatype orig // start send sreq->start(); // push request to receiver's win - recv_win->mut_->lock(); - recv_win->requests_.push_back(rreq); - rreq->start(); - recv_win->mut_->unlock(); + if (const std::scoped_lock recv_lock(*recv_win->mut_); true) { + recv_win->requests_.push_back(rreq); + rreq->start(); + } if (request != nullptr) { *request = sreq; } else { - mut_->lock(); + const std::scoped_lock lock(*mut_); requests_.push_back(sreq); - mut_->unlock(); } // FIXME: The current implementation fails to ensure the correct ordering of the accumulate requests. The following @@ -367,7 +364,7 @@ int Win::get_accumulate(const void* origin_addr, int origin_count, MPI_Datatype XBT_DEBUG("Entering MPI_Get_accumulate from %d", target_rank); //need to be sure ops are correctly ordered, so finish request here ? slow. MPI_Request req = MPI_REQUEST_NULL; - send_win->atomic_mut_->lock(); + const std::scoped_lock lock(*send_win->atomic_mut_); get(result_addr, result_count, result_datatype, target_rank, target_disp, target_count, target_datatype, &req); if (req != MPI_REQUEST_NULL) @@ -377,7 +374,6 @@ int Win::get_accumulate(const void* origin_addr, int origin_count, MPI_Datatype target_disp, target_count, target_datatype, op, &req); if (req != MPI_REQUEST_NULL) Request::wait(&req, MPI_STATUS_IGNORE); - send_win->atomic_mut_->unlock(); return MPI_SUCCESS; } @@ -391,7 +387,7 @@ int Win::compare_and_swap(const void* origin_addr, const void* compare_addr, voi XBT_DEBUG("Entering MPI_Compare_and_swap with %d", target_rank); MPI_Request req = MPI_REQUEST_NULL; - send_win->atomic_mut_->lock(); + const std::scoped_lock lock(*send_win->atomic_mut_); get(result_addr, 1, datatype, target_rank, target_disp, 1, datatype, &req); if (req != MPI_REQUEST_NULL) @@ -400,7 +396,6 @@ int Win::compare_and_swap(const void* origin_addr, const void* compare_addr, voi put(origin_addr, 1, datatype, target_rank, target_disp, 1, datatype); } - send_win->atomic_mut_->unlock(); return MPI_SUCCESS; } @@ -614,7 +609,7 @@ int Win::finish_comms(){ // Without this, the vector could get redimensioned when another process pushes. // This would result in the array used by Request::waitall() to be invalidated. // Another solution would be to copy the data and cleanup the vector *before* Request::waitall - mut_->lock(); + const std::scoped_lock lock(*mut_); //Finish own requests int size = static_cast(requests_.size()); if (size > 0) { @@ -622,13 +617,12 @@ int Win::finish_comms(){ Request::waitall(size, treqs, MPI_STATUSES_IGNORE); requests_.clear(); } - mut_->unlock(); return size; } int Win::finish_comms(int rank){ // See comment about the mutex in finish_comms() above - mut_->lock(); + const std::scoped_lock lock(*mut_); // Finish own requests // Let's see if we're either the destination or the sender of this request // because we only wait for requests that we are responsible for. @@ -646,7 +640,6 @@ int Win::finish_comms(int rank){ Request::waitall(size, treqs, MPI_STATUSES_IGNORE); myreqqs.clear(); } - mut_->unlock(); return size; } diff --git a/src/sthread/sthread.c b/src/sthread/sthread.c index 3552ec231a..4d04e09f62 100644 --- a/src/sthread/sthread.c +++ b/src/sthread/sthread.c @@ -1,3 +1,8 @@ +/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + /* SimGrid's pthread interposer. Redefinition of the pthread symbols (see the comment in sthread.h) */ #define _GNU_SOURCE @@ -31,6 +36,9 @@ static sem_t* (*raw_sem_open)(const char*, int); static int (*raw_sem_init)(sem_t*, int, unsigned int); static int (*raw_sem_wait)(sem_t*); static int (*raw_sem_post)(sem_t*); +static int (*raw_sem_destroy)(sem_t*); +static int (*raw_sem_trywait)(sem_t*); +static int (*raw_sem_timedwait)(sem_t*, const struct timespec*); static void intercepter_init() { @@ -50,6 +58,9 @@ static void intercepter_init() raw_sem_init = dlsym(RTLD_NEXT, "sem_init"); raw_sem_wait = dlsym(RTLD_NEXT, "sem_wait"); raw_sem_post = dlsym(RTLD_NEXT, "sem_post"); + raw_sem_destroy = dlsym(RTLD_NEXT, "sem_destroy"); + raw_sem_trywait = dlsym(RTLD_NEXT, "sem_trywait"); + raw_sem_timedwait = dlsym(RTLD_NEXT, "sem_timedwait"); } static int sthread_inside_simgrid = 1; @@ -155,6 +166,84 @@ int pthread_mutex_destroy(pthread_mutex_t* mutex) sthread_enable(); return res; } +int sem_init(sem_t* sem, int pshared, unsigned int value) +{ + if (raw_sem_init == NULL) + intercepter_init(); + + if (sthread_inside_simgrid) + return raw_sem_init(sem, pshared, value); + + sthread_disable(); + int res = sthread_sem_init((sthread_sem_t*)sem, pshared, value); + sthread_enable(); + return res; +} +int sem_destroy(sem_t* sem) +{ + if (raw_sem_destroy == NULL) + intercepter_init(); + + if (sthread_inside_simgrid) + return raw_sem_destroy(sem); + + sthread_disable(); + int res = sthread_sem_destroy((sthread_sem_t*)sem); + sthread_enable(); + return res; +} +int sem_post(sem_t* sem) +{ + if (raw_sem_post == NULL) + intercepter_init(); + + if (sthread_inside_simgrid) + return raw_sem_post(sem); + + sthread_disable(); + int res = sthread_sem_post((sthread_sem_t*)sem); + sthread_enable(); + return res; +} +int sem_wait(sem_t* sem) +{ + if (raw_sem_wait == NULL) + intercepter_init(); + + if (sthread_inside_simgrid) + return raw_sem_wait(sem); + + sthread_disable(); + int res = sthread_sem_wait((sthread_sem_t*)sem); + sthread_enable(); + return res; +} +int sem_trywait(sem_t* sem) +{ + if (raw_sem_trywait == NULL) + intercepter_init(); + + if (sthread_inside_simgrid) + return raw_sem_trywait(sem); + + sthread_disable(); + int res = sthread_sem_trywait((sthread_sem_t*)sem); + sthread_enable(); + return res; +} +int sem_timedwait(sem_t* sem, const struct timespec* abs_timeout) +{ + if (raw_sem_timedwait == NULL) + intercepter_init(); + + if (sthread_inside_simgrid) + return raw_sem_timedwait(sem, abs_timeout); + + sthread_disable(); + int res = sthread_sem_timedwait((sthread_sem_t*)sem, abs_timeout); + sthread_enable(); + return res; +} /* Glibc < 2.31 uses type "struct timezone *" for the second parameter of gettimeofday. Other implementations use "void *" instead. */ @@ -210,24 +299,6 @@ int usleep(useconds_t usec) } #if 0 -int sem_init(sem_t *sem, int pshared, unsigned int value) { - int res; - - res=raw_sem_init(sem,pshared,value); - return res; -} - -int sem_wait(sem_t *sem) { - int res; - - res = raw_sem_wait(sem); - return res; -} - -int sem_post(sem_t *sem) { - return raw_sem_post(sem); -} - int pthread_cond_init(pthread_cond_t *cond, pthread_condattr_t *cond_attr) { *cond = sg_cond_init(); return 0; diff --git a/src/sthread/sthread.h b/src/sthread/sthread.h index 3bda35c236..da9b453dce 100644 --- a/src/sthread/sthread.h +++ b/src/sthread/sthread.h @@ -1,3 +1,8 @@ +/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + /* SimGrid's pthread interposer. Intercepts most of the pthread and semaphore calls to model-check them. * * Intercepting on pthread is somewhat complicated by the fact that pthread is used everywhere in the system headers. @@ -35,6 +40,16 @@ int sthread_mutex_trylock(sthread_mutex_t* mutex); int sthread_mutex_unlock(sthread_mutex_t* mutex); int sthread_mutex_destroy(sthread_mutex_t* mutex); +typedef struct { + void* sem; +} sthread_sem_t; +int sthread_sem_init(sthread_sem_t* sem, int pshared, unsigned int value); +int sthread_sem_destroy(sthread_sem_t* sem); +int sthread_sem_post(sthread_sem_t* sem); +int sthread_sem_wait(sthread_sem_t* sem); +int sthread_sem_trywait(sthread_sem_t* sem); +int sthread_sem_timedwait(sthread_sem_t* sem, const struct timespec* abs_timeout); + int sthread_gettimeofday(struct timeval* tv); void sthread_sleep(double seconds); diff --git a/src/sthread/sthread_impl.cpp b/src/sthread/sthread_impl.cpp index c4aa27d0c8..807623177e 100644 --- a/src/sthread/sthread_impl.cpp +++ b/src/sthread/sthread_impl.cpp @@ -1,3 +1,8 @@ +/* Copyright (c) 2002-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + /* SimGrid's pthread interposer. Actual implementation of the symbols (see the comment in sthread.h) */ #include "smpi/smpi.h" @@ -7,6 +12,7 @@ #include #include #include +#include #include #include @@ -146,6 +152,48 @@ int sthread_mutex_destroy(sthread_mutex_t* mutex) intrusive_ptr_release(static_cast(mutex->mutex)); return 0; } +int sthread_sem_init(sthread_sem_t* sem, int /*pshared*/, unsigned int value) +{ + auto s = sg4::Semaphore::create(value); + intrusive_ptr_add_ref(s.get()); + + sem->sem = s.get(); + return 0; +} +int sthread_sem_destroy(sthread_sem_t* sem) +{ + intrusive_ptr_release(static_cast(sem->sem)); + return 0; +} +int sthread_sem_post(sthread_sem_t* sem) +{ + static_cast(sem->sem)->release(); + return 0; +} +int sthread_sem_wait(sthread_sem_t* sem) +{ + static_cast(sem->sem)->acquire(); + return 0; +} +int sthread_sem_trywait(sthread_sem_t* sem) +{ + auto* s = static_cast(sem->sem); + if (s->would_block()) { + errno = EAGAIN; + return -1; + } + s->acquire(); + return 0; +} +int sthread_sem_timedwait(sthread_sem_t* sem, const struct timespec* abs_timeout) +{ + if (static_cast(sem->sem)->acquire_timeout(static_cast(abs_timeout->tv_sec) + + static_cast(abs_timeout->tv_nsec) / 1E9)) { + errno = ETIMEDOUT; + return -1; + } + return 0; +} int sthread_gettimeofday(struct timeval* tv) { @@ -165,24 +213,6 @@ void sthread_sleep(double seconds) } #if 0 -int sem_init(sem_t *sem, int pshared, unsigned int value) { - int res; - - res=raw_sem_init(sem,pshared,value); - return res; -} - -int sem_wait(sem_t *sem) { - int res; - - res = raw_sem_wait(sem); - return res; -} - -int sem_post(sem_t *sem) { - return raw_sem_post(sem); -} - int pthread_cond_init(pthread_cond_t *cond, pthread_condattr_t *cond_attr) { *cond = sg_cond_init(); return 0; diff --git a/src/xbt/OsSemaphore.hpp b/src/xbt/OsSemaphore.hpp index 2b7e1f25b6..821075f6b0 100644 --- a/src/xbt/OsSemaphore.hpp +++ b/src/xbt/OsSemaphore.hpp @@ -22,7 +22,7 @@ public: inline void release() { - std::unique_lock lock(mutex_); + const std::scoped_lock lock(mutex_); ++capa_; condition_.notify_one(); } diff --git a/src/xbt/dict.cpp b/src/xbt/dict.cpp index bbc45999c5..f1e73d31dc 100644 --- a/src/xbt/dict.cpp +++ b/src/xbt/dict.cpp @@ -17,6 +17,7 @@ #include #include #include +#include XBT_LOG_NEW_DEFAULT_SUBCATEGORY(xbt_dict, xbt, "Dictionaries provide the same functionalities as hash tables"); @@ -32,6 +33,8 @@ static void xbt_dict_postexit() } static void xbt_dict_preinit() { + static std::mutex init_mutex; + const std::scoped_lock lock(init_mutex); if (dict_elm_mallocator == nullptr) { dict_elm_mallocator = xbt_mallocator_new(256, dict_elm_mallocator_new_f, dict_elm_mallocator_free_f, dict_elm_mallocator_reset_f); diff --git a/src/xbt/exception.cpp b/src/xbt/exception.cpp index 51e9649d72..e8048f88f0 100644 --- a/src/xbt/exception.cpp +++ b/src/xbt/exception.cpp @@ -37,7 +37,7 @@ void log_exception(e_xbt_log_priority_t prio, const char* context, std::exceptio auto* with_context = dynamic_cast(&exception); if (with_context != nullptr) { - XBT_LOG(prio, "%s %s by %s/%d: %s", context, name.c_str(), with_context->throw_point().procname_.c_str(), + XBT_LOG(prio, "%s %s by %s/%ld: %s", context, name.c_str(), with_context->throw_point().procname_.c_str(), with_context->throw_point().pid_, exception.what()); // Do we have a backtrace? if (not simgrid::config::get_value("exception/cutpath")) { diff --git a/src/xbt/log.cpp b/src/xbt/log.cpp index 65c5dae424..d21ea0e07b 100644 --- a/src/xbt/log.cpp +++ b/src/xbt/log.cpp @@ -235,7 +235,7 @@ int _xbt_log_cat_init(xbt_log_category_t category, e_xbt_log_priority_t priority return priority >= category->threshold; static std::recursive_mutex log_cat_init_mutex; - log_cat_init_mutex.lock(); + const std::scoped_lock lock(log_cat_init_mutex); XBT_DEBUG("Initializing category '%s' (firstChild=%s, nextSibling=%s)", category->name, (category->firstChild ? category->firstChild->name : "none"), @@ -279,7 +279,6 @@ int _xbt_log_cat_init(xbt_log_category_t category, e_xbt_log_priority_t priority } category->initialized = 1; - log_cat_init_mutex.unlock(); return priority >= category->threshold; } diff --git a/src/xbt/parmap.hpp b/src/xbt/parmap.hpp index d8b5eb722c..7c02fa1dd7 100644 --- a/src/xbt/parmap.hpp +++ b/src/xbt/parmap.hpp @@ -309,7 +309,7 @@ template void Parmap::worker_main(ThreadData* data) template void Parmap::PosixSynchro::master_signal() { - std::unique_lock lk(ready_mutex); + const std::scoped_lock lock(ready_mutex); this->parmap.thread_counter = 1; this->parmap.work_round++; /* wake all workers */ @@ -318,14 +318,14 @@ template void Parmap::PosixSynchro::master_signal() template void Parmap::PosixSynchro::master_wait() { - std::unique_lock lk(done_mutex); + std::unique_lock lock(done_mutex); /* wait for all workers to be ready */ - done_cond.wait(lk, [this]() { return this->parmap.thread_counter >= this->parmap.num_workers; }); + done_cond.wait(lock, [this]() { return this->parmap.thread_counter >= this->parmap.num_workers; }); } template void Parmap::PosixSynchro::worker_signal() { - std::unique_lock lk(done_mutex); + const std::scoped_lock lock(done_mutex); this->parmap.thread_counter++; if (this->parmap.thread_counter == this->parmap.num_workers) { /* all workers have finished, wake the controller */ @@ -335,9 +335,9 @@ template void Parmap::PosixSynchro::worker_signal() template void Parmap::PosixSynchro::worker_wait(unsigned expected_round) { - std::unique_lock lk(ready_mutex); + std::unique_lock lock(ready_mutex); /* wait for more work */ - ready_cond.wait(lk, [this, expected_round]() { return this->parmap.work_round == expected_round; }); + ready_cond.wait(lock, [this, expected_round]() { return this->parmap.work_round == expected_round; }); } #if HAVE_FUTEX_H diff --git a/teshsuite/mc/mutex-handling/mutex-handling.cpp b/teshsuite/mc/mutex-handling/mutex-handling.cpp index 22224b656d..adb9519796 100644 --- a/teshsuite/mc/mutex-handling/mutex-handling.cpp +++ b/teshsuite/mc/mutex-handling/mutex-handling.cpp @@ -24,6 +24,8 @@ #include "simgrid/s4u/Mailbox.hpp" #include "simgrid/s4u/Mutex.hpp" +#include // std::unique_lock + XBT_LOG_NEW_DEFAULT_CATEGORY(mutex_handling, "Messages specific for this test"); static int receiver(const char* box_name) @@ -45,14 +47,11 @@ static int sender(const char* box_name, simgrid::s4u::MutexPtr mutex, int value) auto* payload = new int(value); auto mb = simgrid::s4u::Mailbox::by_name(box_name); + std::unique_lock lock; if (mutex) - mutex->lock(); + lock = std::unique_lock(*mutex); mb->put(payload, 8); - - if (mutex) - mutex->unlock(); - return 0; } diff --git a/teshsuite/s4u/CMakeLists.txt b/teshsuite/s4u/CMakeLists.txt index 70317ad1d1..83969f8392 100644 --- a/teshsuite/s4u/CMakeLists.txt +++ b/teshsuite/s4u/CMakeLists.txt @@ -17,7 +17,7 @@ foreach(x actor actor-autorestart actor-suspend storage_client_server listen_async pid trace-integration seal-platform - vm-live-migration vm-suicide issue71) + vm-live-migration vm-suicide issue71) if(NOT DEFINED ${x}_sources) set(${x}_sources ${x}/${x}.cpp) diff --git a/teshsuite/s4u/monkey-masterworkers/monkey-masterworkers.py b/teshsuite/s4u/monkey-masterworkers/monkey-masterworkers.py index 3287b2ee1d..6db4f0c462 100644 --- a/teshsuite/s4u/monkey-masterworkers/monkey-masterworkers.py +++ b/teshsuite/s4u/monkey-masterworkers/monkey-masterworkers.py @@ -63,7 +63,7 @@ def worker(my_id): assert Engine.clock < deadline, f"Failed to run all tasks in less than {deadline} seconds. Is this an infinite loop?" try: - this_actor.info(f"Waiting a message on mailbox") + this_actor.info("Waiting a message on mailbox") compute_cost = mailbox.get() this_actor.info("Start execution...") diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 58af6c463d..7ab49a15bc 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -523,6 +523,18 @@ set(MC_SRC src/mc/explo/UdporChecker.cpp src/mc/explo/UdporChecker.hpp + src/mc/explo/udpor/Configuration.hpp + src/mc/explo/udpor/Configuration.cpp + src/mc/explo/udpor/EventSet.cpp + src/mc/explo/udpor/EventSet.hpp + src/mc/explo/udpor/History.cpp + src/mc/explo/udpor/History.hpp + src/mc/explo/udpor/UnfoldingEvent.cpp + src/mc/explo/udpor/UnfoldingEvent.hpp + src/mc/explo/udpor/Unfolding.cpp + src/mc/explo/udpor/Unfolding.hpp + src/mc/explo/udpor/udpor_forward.hpp + src/mc/inspect/DwarfExpression.cpp src/mc/inspect/DwarfExpression.hpp src/mc/inspect/Frame.cpp @@ -589,8 +601,6 @@ set(MC_SRC src/mc/mc_forward.hpp src/mc/mc_private.hpp src/mc/mc_record.cpp - src/mc/udpor_global.cpp - src/mc/udpor_global.hpp src/xbt/mmalloc/mm_interface.c ) diff --git a/tools/cmake/Modules/FindNS3.cmake b/tools/cmake/Modules/FindNS3.cmake index 1c477439ab..7154c2bb3b 100644 --- a/tools/cmake/Modules/FindNS3.cmake +++ b/tools/cmake/Modules/FindNS3.cmake @@ -42,7 +42,7 @@ if(NS3_FOUND) # Starting from 3.36, ns3 provides a working pkg-config file, maki else() set(NS3_HINT ${ns3_path} CACHE PATH "Path to search for NS3 lib and include") - set(NS3_KNOWN_VERSIONS "3-dev" "3.28" "3.29" "3.30" "3.31" "3.32" "3.33" "3.34" "3.35") + set(NS3_KNOWN_VERSIONS "3-dev" "3.28" "3.29" "3.30" "3.31" "3.32" "3.33" "3.34" "3.35") # subsequent versions use pkg-config foreach (_ns3_ver ${NS3_KNOWN_VERSIONS}) list(APPEND _ns3_LIB_SEARCH_DIRS "ns${_ns3_ver}-core" "ns${_ns3_ver}-core-optimized" "ns${_ns3_ver}-core-debug" "ns${_ns3_ver}-core-default") diff --git a/tools/cmake/Tests.cmake b/tools/cmake/Tests.cmake index a7182fec9d..ba1e45f9de 100644 --- a/tools/cmake/Tests.cmake +++ b/tools/cmake/Tests.cmake @@ -127,10 +127,18 @@ set(UNIT_TESTS src/xbt/unit-tests_main.cpp src/xbt/random_test.cpp src/xbt/xbt_str_test.cpp src/kernel/lmm/maxmin_test.cpp) + +set(MC_UNIT_TESTS src/mc/sosp/Snapshot_test.cpp + src/mc/sosp/PageStore_test.cpp + src/mc/explo/udpor/EventSet_test.cpp + src/mc/explo/udpor/Unfolding_test.cpp + src/mc/explo/udpor/UnfoldingEvent_test.cpp + src/mc/explo/udpor/History_test.cpp + src/mc/explo/udpor/Configuration_test.cpp) if (SIMGRID_HAVE_MC) - set(UNIT_TESTS ${UNIT_TESTS} src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp) + set(UNIT_TESTS ${UNIT_TESTS} ${MC_UNIT_TESTS}) else() - set(EXTRA_DIST ${EXTRA_DIST} src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp) + set(EXTRA_DIST ${EXTRA_DIST} ${MC_UNIT_TESTS}) endif() if (SIMGRID_HAVE_EIGEN3) set(UNIT_TESTS ${UNIT_TESTS} src/kernel/lmm/bmf_test.cpp)