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
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.
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
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
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
\ 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)
_ _____ _________
__ _____ _ __ ___(_) ___ _ __ |___ / |___ /___ \
\ \ / / _ \ '__/ __| |/ _ \| '_ \ |_ \ |_ \ __) |
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).
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
+<https://framagit.org/simgrid/simgrid/tree/master/teshsuite/models/wifi_usage_decay/wifi_usage_decay.cpp>`_ and in the `research
+paper <https://hal.archives-ouvertes.fr/hal-03777726>`_.
+
+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 <https://framagit.org/simgrid/simgrid/tree/master/examples/sthread>`_.
+
.. |br| raw:: html
<br />
/* 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 <mutex> /* std::mutex and std::lock_guard */
+#include <mutex> /* std::mutex and std::scoped_lock */
#include <simgrid/s4u.hpp> /* All of S4U */
XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_test, "a sample log category");
static void competitor(int id, sg4::ConditionVariablePtr cv, sg4::MutexPtr mtx, std::shared_ptr<bool> 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!)");
}
}
{
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();
/* 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 <mutex> /* std::mutex and std::lock_guard */
+#include <mutex> /* std::mutex and std::scoped_lock */
#include <simgrid/s4u.hpp> /* All of S4U */
XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_test, "a sample log category");
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";
std::ref(done));
// wait for the worker
- cv->wait(std::unique_lock<sg4::Mutex>(*mutex), [&done]() { return done; });
+ cv->wait(std::unique_lock(*mutex), [&done]() { return done; });
XBT_INFO("data is now '%s'.", data.c_str());
worker->join();
#include "simgrid/s4u.hpp" /* All of S4U */
#include "xbt/config.hpp"
-#include <mutex> /* std::mutex and std::lock_guard */
+#include <mutex> /* std::mutex and std::scoped_lock */
namespace sg4 = simgrid::s4u;
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");
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]));
}
# 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)
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}")
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()
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)
""" 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")
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")
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):
#########################################################################
foreach(x
- mutex-simple)
+ mutex-simple
+ producer-consumer)
if("${CMAKE_SYSTEM}" MATCHES "Linux")
add_executable (pthread-${x} EXCLUDE_FROM_ALL pthread-${x}.c)
--- /dev/null
+# 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
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);
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);
--- /dev/null
+/* 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 <pthread.h>
+#include <semaphore.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#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;
+}
--- /dev/null
+$ 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.
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);
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)
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__) */
*/
ProducerConsumer* set_max_queue_size(unsigned int max_queue_size)
{
- std::unique_lock<s4u::Mutex> lock(*mutex_);
+ const std::lock_guard<s4u::Mutex> lock(*mutex_);
max_queue_size_ = max_queue_size;
return this;
}
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);
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)");
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();
}
}
}
friend s4u::Engine;
std::vector<std::string> cmdline_; // Copy of the argv we got (including argv[0])
+
public:
EngineImpl() = default;
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_);
delete activity;
}
}
+
} // namespace simgrid::kernel::activity
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<s4u::Host*>& get_hosts() const { return hosts_; };
// Already in the queue
}
}
+
void BarrierAcquisitionImpl::finish()
{
xbt_assert(simcalls_.size() == 1, "Unexpected number of simcalls waiting: %zu", simcalls_.size());
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 */
{
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:
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())) {
}
}
-/** @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()) {
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);
enum class CommImplType { SEND, RECEIVE };
+using timeout_action_type = std::unique_ptr<resource::Action, std::function<void(resource::Action*)>>;
+
class XBT_PUBLIC CommImpl : public ActivityImpl_T<CommImpl> {
~CommImpl() override;
- void cleanup_surf();
static std::function<void(CommImpl*, void*, size_t)> copy_data_callback_;
void suspend() override;
void resume() override;
void cancel() override;
- void post() override;
void set_exception(actor::ActorImpl* issuer) override;
void finish() override;
std::function<void(CommImpl*, void*, size_t)> 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;
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);
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()) {
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();
namespace simgrid::kernel::activity {
class XBT_PUBLIC ExecImpl : public ActivityImpl_T<ExecImpl> {
- std::unique_ptr<resource::Action, std::function<void(resource::Action*)>> timeout_detector_{
- nullptr, [](resource::Action* a) { a->unref(); }};
double sharing_penalty_ = 1.0;
double bound_ = 0.0;
std::vector<double> flops_amounts_;
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);
virtual ActivityImpl* migrate(s4u::Host* to);
ExecImpl* start();
- void post() override;
void set_exception(actor::ActorImpl* issuer) override;
void finish() override;
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;
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()) {
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();
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);
resource::DiskImpl* get_disk() const { return disk_; }
IoImpl* start();
- void post() override;
void set_exception(actor::ActorImpl* issuer) override;
void finish() override;
};
/** @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();
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();
}
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<bool(void*, void*, CommImpl*)>& match_fun, void* data);
CommImplPtr find_matching_comm(CommImplType type, const std::function<bool(void*, void*, CommImpl*)>& match_fun,
void* this_user_data, const CommImplPtr& my_synchro, bool done, bool remove_matching);
// Already in the queue
}
}
+
void MutexAcquisitionImpl::finish()
{
xbt_assert(simcalls_.size() == 1, "Unexpected number of simcalls waiting: %zu", simcalls_.size());
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 */
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);
// Already in the queue
}
}
-void SemAcquisitionImpl::post()
-{
- finish();
-}
void SemAcquisitionImpl::finish()
{
xbt_assert(simcalls_.size() == 1, "Unexpected number of simcalls waiting: %zu", simcalls_.size());
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 {
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
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())
}
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();
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();
/* 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) {
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();
void suspend() override;
void resume() override;
void cancel() override;
- void post() override;
void set_exception(actor::ActorImpl* issuer) override;
void finish() override;
};
activity::ActivityImplPtr activity = waiting_synchro_;
activity->cancel();
activity->set_state(activity::State::FAILED);
- activity->post();
+ activity->finish();
activities_.erase(waiting_synchro_);
waiting_synchro_ = nullptr;
* This means there may be a way to store the list once and apply differences
* rather than repeating elements frequently.
*/
- std::vector<std::unique_ptr<Transition>> pending_transitions_;
+ std::vector<std::shared_ptr<Transition>> 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
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<std::unique_ptr<Transition>> transitions)
+ ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector<std::shared_ptr<Transition>> transitions)
: pending_transitions_(std::move(transitions)), aid_(aid), max_consider_(max_consider), enabled_(enabled)
{
}
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);
std::vector<s_mc_message_simcall_probe_one_t> 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<size_t>(received) == size,
+ xbt_assert(static_cast<size_t>(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,
"(currently %d), but only %d transition(s) was/were said to be encoded",
actor.max_considered, actor.n_transitions);
- auto actor_transitions = std::vector<std::unique_ptr<Transition>>(actor.n_transitions);
+ std::vector<std::shared_ptr<Transition>> 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<Transition>(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));
}
}
{
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:");
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);
+ }
}
}
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<aid_t, ActorState> const& get_actors_list() const { return actors_to_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
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 {
* 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 <xbt/asserts.h>
#include <xbt/log.h>
-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<char*>& 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<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
+ 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<State> 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<char*>& args) : Exploration(args) {}
+ // Remove(e, C, D)
+ clean_up_explore(e, C, D);
+}
+
+std::tuple<EventSet, EventSet> 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{<a, > : H }
+ UnfoldingEvent* e_cur = C.get_latest_event();
+ EventSet exC = prev_exC;
+ exC.remove(e_cur);
+
+ // ... fancy computations
+
+ EventSet enC;
+ return std::tuple<EventSet, EventSet>(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<State> 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()
{
std::vector<std::string> UdporChecker::get_textual_trace()
{
+ // TODO: Topologically sort the events of the latest configuration
+ // and iterate through that topological sorting
std::vector<std::string> trace;
return trace;
}
+} // namespace simgrid::mc::udpor
+
+namespace simgrid::mc {
+
Exploration* create_udpor_checker(const std::vector<char*>& args)
{
- return new UdporChecker(args);
+ return new simgrid::mc::udpor::UdporChecker(args);
}
} // namespace simgrid::mc
#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 <optional>
+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<char*>& args);
+
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
-};
-} // namespace simgrid::mc
+ inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(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<State> 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<EventSet, EventSet> 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<State> 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
--- /dev/null
+/* 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 <algorithm>
+#include <stdexcept>
+
+namespace simgrid::mc::udpor {
+
+Configuration::Configuration(std::initializer_list<UnfoldingEvent*> 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
--- /dev/null
+/* 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 <initializer_list>
+
+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<UnfoldingEvent*> 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
--- /dev/null
+/* 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));
+}
--- /dev/null
+/* 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 <iterator>
+
+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<UnfoldingEvent*> 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<UnfoldingEvent*> 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
--- /dev/null
+/* 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 <cstddef>
+#include <initializer_list>
+#include <unordered_set>
+
+namespace simgrid::mc::udpor {
+
+class EventSet {
+private:
+ std::unordered_set<UnfoldingEvent*> 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<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+ explicit EventSet(std::initializer_list<UnfoldingEvent*> 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
--- /dev/null
+/* 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
--- /dev/null
+/* 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 <stack>
+
+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<std::reference_wrapper<const Configuration>>{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
--- /dev/null
+/* 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 <functional>
+#include <optional>
+
+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<std::reference_wrapper<const Configuration>>;
+
+ 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
--- /dev/null
+/* 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));
+ }
+ }
+}
--- /dev/null
+/* 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 <stdexcept>
+
+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<UnfoldingEvent> 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
--- /dev/null
+/* 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 <memory>
+#include <unordered_map>
+
+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<UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+
+public:
+ Unfolding() = default;
+ Unfolding& operator=(Unfolding&&) = default;
+ Unfolding(Unfolding&&) = default;
+
+ void remove(UnfoldingEvent* e);
+ void insert(std::unique_ptr<UnfoldingEvent> e);
+
+ size_t size() const { return this->global_events_.size(); }
+ bool empty() const { return this->global_events_.empty(); }
+};
+
+} // namespace simgrid::mc::udpor
+#endif
--- /dev/null
+/* 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<UnfoldingEvent*> init_list)
+ : UnfoldingEvent(EventSet(std::move(init_list)))
+{
+}
+
+UnfoldingEvent::UnfoldingEvent(EventSet immediate_causes, std::shared_ptr<Transition> 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
--- /dev/null
+/* 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 <initializer_list>
+#include <memory>
+#include <string>
+
+namespace simgrid::mc::udpor {
+
+class UnfoldingEvent {
+public:
+ UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list);
+ UnfoldingEvent(EventSet immediate_causes = EventSet(),
+ std::shared_ptr<Transition> transition = std::make_unique<Transition>());
+
+ 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<Transition> 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
--- /dev/null
+/* 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;
--- /dev/null
+/* 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<UnfoldingEvent>();
+ auto e2 = std::make_unique<UnfoldingEvent>();
+ 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
--- /dev/null
+/* 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
}
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");
}
}
};
// 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<char, SIMCALL_SERIALIZATION_BUFFER_SIZE> buffer;
};
+++ /dev/null
-/* 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 <algorithm>
-
-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
+++ /dev/null
-/* 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 <iostream>
-#include <queue>
-#include <string_view>
-
-/* TODO: many method declared in this module are not implemented */
-
-namespace simgrid::mc {
-
-class UnfoldingEvent;
-using EventSet = std::deque<UnfoldingEvent*>;
-
-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
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;
}
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;
}
/* **************************** 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)
{
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);
#include "simgrid/s4u/Host.hpp"
#include "simgrid/plugins/file_system.h"
+#include <mutex> // std::scoped_lock
+
#define FP_SIZE sizeof(MPI_Offset)
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_io, smpi, "Logging specific to SMPI (RMA operations)");
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;
}
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;
}
/* }*/
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;
}
fh->seek(result, MPI_SEEK_SET);
int ret = fh->op_all<simgrid::smpi::File::read>(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_);
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<void*>(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;
}
fh->seek(result, MPI_SEEK_SET);
int ret = fh->op_all<simgrid::smpi::File::write>(const_cast<void*>(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_);
#include <algorithm>
#include <array>
+#include <mutex> // std::scoped_lock and std::unique_lock
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_request, smpi, "Logging specific to SMPI (request)");
simgrid::smpi::ActorExt* process = smpi_process_remote(simgrid::s4u::Actor::by_pid(dst_));
- simgrid::s4u::MutexPtr mut = process->mailboxes_mutex();
+ std::unique_lock<s4u::Mutex> 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;
&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_);
XBT_DEBUG("sending size of %zu : sleep %f ", size_, sleeptime);
}
- simgrid::s4u::MutexPtr mut = process->mailboxes_mutex();
-
+ std::unique_lock<s4u::Mutex> 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();
boost::static_pointer_cast<kernel::activity::CommImpl>(action_)->set_tracing_category(
smpi_process()->get_tracing_category());
}
-
- if (smpi_cfg_async_small_thresh() != 0 || ((flags_ & MPI_REQ_RMA) != 0))
- mut->unlock();
}
}
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;
{
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;
}
#include "src/mc/mc_replay.hpp"
#include <algorithm>
+#include <mutex> // std::scoped_lock
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_rma, smpi, "Logging specific to SMPI (RMA operations)");
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);
//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();
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);
// 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
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)
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;
}
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)
put(origin_addr, 1, datatype, target_rank,
target_disp, 1, datatype);
}
- send_win->atomic_mut_->unlock();
return MPI_SUCCESS;
}
// 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<int>(requests_.size());
if (size > 0) {
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.
Request::waitall(size, treqs, MPI_STATUSES_IGNORE);
myreqqs.clear();
}
- mut_->unlock();
return size;
}
+/* 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
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()
{
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;
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. */
}
#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;
+/* 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.
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);
+/* 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"
#include <simgrid/s4u/Engine.hpp>
#include <simgrid/s4u/Mutex.hpp>
#include <simgrid/s4u/NetZone.hpp>
+#include <simgrid/s4u/Semaphore.hpp>
#include <xbt/base.h>
#include <xbt/sysdep.h>
intrusive_ptr_release(static_cast<sg4::Mutex*>(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<sg4::Semaphore*>(sem->sem));
+ return 0;
+}
+int sthread_sem_post(sthread_sem_t* sem)
+{
+ static_cast<sg4::Semaphore*>(sem->sem)->release();
+ return 0;
+}
+int sthread_sem_wait(sthread_sem_t* sem)
+{
+ static_cast<sg4::Semaphore*>(sem->sem)->acquire();
+ return 0;
+}
+int sthread_sem_trywait(sthread_sem_t* sem)
+{
+ auto* s = static_cast<sg4::Semaphore*>(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<sg4::Semaphore*>(sem->sem)->acquire_timeout(static_cast<double>(abs_timeout->tv_sec) +
+ static_cast<double>(abs_timeout->tv_nsec) / 1E9)) {
+ errno = ETIMEDOUT;
+ return -1;
+ }
+ return 0;
+}
int sthread_gettimeofday(struct timeval* tv)
{
}
#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;
inline void release()
{
- std::unique_lock lock(mutex_);
+ const std::scoped_lock lock(mutex_);
++capa_;
condition_.notify_one();
}
#include <algorithm>
#include <cstdio>
#include <cstring>
+#include <mutex>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(xbt_dict, xbt, "Dictionaries provide the same functionalities as hash tables");
}
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);
auto* with_context = dynamic_cast<const simgrid::Exception*>(&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<bool>("exception/cutpath")) {
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"),
}
category->initialized = 1;
- log_cat_init_mutex.unlock();
return priority >= category->threshold;
}
template <typename T> void Parmap<T>::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 */
template <typename T> void Parmap<T>::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 <typename T> void Parmap<T>::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 */
template <typename T> void Parmap<T>::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
#include "simgrid/s4u/Mailbox.hpp"
#include "simgrid/s4u/Mutex.hpp"
+#include <mutex> // std::unique_lock
+
XBT_LOG_NEW_DEFAULT_CATEGORY(mutex_handling, "Messages specific for this test");
static int receiver(const char* box_name)
auto* payload = new int(value);
auto mb = simgrid::s4u::Mailbox::by_name(box_name);
+ std::unique_lock<simgrid::s4u::Mutex> lock;
if (mutex)
- mutex->lock();
+ lock = std::unique_lock(*mutex);
mb->put(payload, 8);
-
- if (mutex)
- mutex->unlock();
-
return 0;
}
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)
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...")
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
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
)
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")
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)
