SimGrid (3.34.1) not released (Target: fall 2023)
+Python:
+ - Make the host_load plugin available from Python. See examples/python/plugin-host-load
+
----------------------------------------------------------------------------
SimGrid (3.34) June 26. 2023
include examples/python/platform-failures/platform-failures.tesh
include examples/python/platform-profile/platform-profile.py
include examples/python/platform-profile/platform-profile.tesh
+include examples/python/plugin-host-load/plugin-host-load.py
+include examples/python/plugin-host-load/plugin-host-load.tesh
include examples/python/synchro-barrier/synchro-barrier.py
include examples/python/synchro-barrier/synchro-barrier.tesh
include examples/python/synchro-mutex/synchro-mutex.py
});
// The token sent by SA is forwarded by both communication tasks
- SA_to_B1->on_this_start_cb([SA](sg4::Task* t) { t->set_token(t->get_next_token_from(SA)); });
- SA_to_B2->on_this_start_cb([SA](sg4::Task* t) { t->set_token(t->get_next_token_from(SA)); });
+ SA_to_B1->on_this_start_cb([&SA](sg4::Task* t) { t->set_token(t->get_next_token_from(SA)); });
+ SA_to_B2->on_this_start_cb([&SA](sg4::Task* t) { t->set_token(t->get_next_token_from(SA)); });
/* B1 and B2 read the value of the token received by their predecessors
and use it to adapt their amount of work to do.
// Add a function to be called before each firing of comm0
// This function modifies the graph of tasks by adding or removing
// successors to comm0
- comm0->on_this_start_cb([comm0, exec1, exec2, jupiter, fafard](sg4::Task*) {
+ comm0->on_this_start_cb([&comm0, exec1, exec2, jupiter, fafard](const sg4::Task*) {
static int count = 0;
if (count % 2 == 0) {
comm0->set_destination(jupiter);
exec-async exec-basic exec-dvfs exec-remote exec-ptask
task-io task-simple task-switch-host task-variable-load
platform-comm-serialize platform-profile platform-failures
+ plugin-host-load
network-nonlinear clusters-multicpu io-degradation exec-cpu-nonlinear
synchro-barrier synchro-mutex synchro-semaphore)
set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh)
--- /dev/null
+# Copyright (c) 2006-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.
+
+
+from argparse import ArgumentParser
+import sys
+from simgrid import Engine, Host, this_actor, Actor, sg_host_load_plugin_init
+
+def parse():
+ parser = ArgumentParser()
+ parser.add_argument(
+ '--platform',
+ type=str,
+ required=True,
+ help='path to the platform description'
+ )
+ return parser.parse_args()
+
+def execute_load_test():
+ host = Host.by_name('MyHost1')
+ this_actor.info(f'Initial peak speed: {host.speed:.0E} flop/s; number of flops computed so far: {host.computed_flops:.0E} (should be 0) and current average load: {host.avg_load} (should be 0)')
+
+ start = Engine.clock
+ this_actor.info('Sleep for 10 seconds')
+ this_actor.sleep_for(10)
+
+ speed = host.speed
+ this_actor.info(f'Done sleeping {Engine.clock - start}s; peak speed: {host.speed:.0E} flop/s; number of flops computed so far: {host.computed_flops:.0E} (nothing should have changed)')
+
+ # Run an activity
+ start = e.clock
+ this_actor.info(f'Run an activity of {200E6:.0E} flops at current speed of {host.speed:.0E} flop/s')
+ this_actor.execute(200E6)
+
+ this_actor.info(f'Done working on my activity; this took {Engine.clock - start}s; current peak speed: {host.speed:.0E} flop/s (when I started the computation, \
+the speed was set to {speed:.0E} flop/s); number of flops computed so \
+far: {host.computed_flops:.0E}, average load as reported by the HostLoad plugin: {host.avg_load:.5f} (should be {200E6 / (10.5 * speed * host.core_count + (Engine.clock - start - 0.5) * host.speed * host.core_count):.5f})')
+
+ # ========= Change power peak =========
+ pstate = 1
+ host.pstate = pstate
+ this_actor.info(f'========= Requesting pstate {pstate} (speed should be of {host.pstate_speed(pstate):.0E} flop/s and is of {host.speed:.0E} flop/s, average load is {host.avg_load:.5f})')
+
+ # Run a second activity
+ start = Engine.clock
+ this_actor.info(f'Run an activity of {100E6:.0E} flops')
+ this_actor.execute(100E6)
+ this_actor.info(f'Done working on my activity; this took {Engine.clock - start}s; current peak speed: {host.speed:.0E} flop/s; number of flops computed so far: {host.computed_flops:.0E}')
+ Engine
+ start = Engine.clock
+ this_actor.info("========= Requesting a reset of the computation and load counters")
+ host.reset_load()
+ this_actor.info(f'After reset: {host.computed_flops:.0E} flops computed; load is {host.avg_load}')
+ this_actor.info('Sleep for 4 seconds')
+ this_actor.sleep_for(4)
+ this_actor.info(f'Done sleeping {Engine.clock - start}s; peak speed: {host.speed:.0E} flop/s; number of flops computed so far: {host.computed_flops:.0E}')
+
+ # =========== Turn the other host off ==========
+ host2 = Host.by_name('MyHost2')
+ this_actor.info(f'Turning MyHost2 off, and sleeping another 10 seconds. MyHost2 computed {host2.computed_flops:.0E} flops so far and has an average load of {host2.avg_load}')
+ host2.turn_off()
+ start = Engine.clock
+ this_actor.sleep_for(10)
+ this_actor.info(f'Done sleeping {Engine.clock - start}s; peak speed: {host.speed:.0E} flop/s; number of flops computed so far: {host.computed_flops:.0E}')
+
+def change_speed():
+ host = Host.by_name('MyHost1')
+ this_actor.sleep_for(10.5)
+ this_actor.info("I slept until now, but now I'll change the speed of this host while the other actor is still computing! This should slow the computation down.")
+ host.pstate = 2
+
+if __name__ == '__main__':
+ args = parse()
+
+ sg_host_load_plugin_init()
+ e = Engine(sys.argv)
+ e.load_platform(args.platform)
+
+ Actor.create('load_test', e.host_by_name('MyHost1'), execute_load_test)
+ Actor.create('change_speed', e.host_by_name('MyHost1'), change_speed)
+
+ e.run()
+
+ this_actor.info(f'Total simulation time: {Engine.clock}')
+
--- /dev/null
+#!/usr/bin/env tesh
+
+p This tests the Host Load plugin (that allows the user to get the current load of a host and the computed flops)
+
+$ ${pythoncmd:=python3} ${PYTHON_TOOL_OPTIONS:=} ${srcdir:=.}/plugin-host-load.py --platform ${platfdir}/energy_platform.xml
+> [MyHost1:load_test:(1) 0.000000] [python/INFO] Initial peak speed: 1E+08 flop/s; number of flops computed so far: 0E+00 (should be 0) and current average load: 0.0 (should be 0)
+> [MyHost1:load_test:(1) 0.000000] [python/INFO] Sleep for 10 seconds
+> [MyHost1:load_test:(1) 10.000000] [python/INFO] Done sleeping 10.0s; peak speed: 1E+08 flop/s; number of flops computed so far: 0E+00 (nothing should have changed)
+> [MyHost1:load_test:(1) 10.000000] [python/INFO] Run an activity of 2E+08 flops at current speed of 1E+08 flop/s
+> [MyHost1:change_speed:(2) 10.500000] [python/INFO] I slept until now, but now I'll change the speed of this host while the other actor is still computing! This should slow the computation down.
+> [MyHost1:load_test:(1) 18.000000] [python/INFO] Done working on my activity; this took 8.0s; current peak speed: 2E+07 flop/s (when I started the computation, the speed was set to 1E+08 flop/s); number of flops computed so far: 2E+08, average load as reported by the HostLoad plugin: 0.04167 (should be 0.04167)
+> [MyHost1:load_test:(1) 18.000000] [python/INFO] ========= Requesting pstate 1 (speed should be of 5E+07 flop/s and is of 5E+07 flop/s, average load is 0.04167)
+> [MyHost1:load_test:(1) 18.000000] [python/INFO] Run an activity of 1E+08 flops
+> [MyHost1:load_test:(1) 20.000000] [python/INFO] Done working on my activity; this took 2.0s; current peak speed: 5E+07 flop/s; number of flops computed so far: 3E+08
+> [MyHost1:load_test:(1) 20.000000] [python/INFO] ========= Requesting a reset of the computation and load counters
+> [MyHost1:load_test:(1) 20.000000] [python/INFO] After reset: 0E+00 flops computed; load is 0.0
+> [MyHost1:load_test:(1) 20.000000] [python/INFO] Sleep for 4 seconds
+> [MyHost1:load_test:(1) 24.000000] [python/INFO] Done sleeping 4.0s; peak speed: 5E+07 flop/s; number of flops computed so far: 0E+00
+> [MyHost1:load_test:(1) 24.000000] [python/INFO] Turning MyHost2 off, and sleeping another 10 seconds. MyHost2 computed 0E+00 flops so far and has an average load of 0.0
+> [MyHost1:load_test:(1) 34.000000] [python/INFO] Done sleeping 10.0s; peak speed: 5E+07 flop/s; number of flops computed so far: 0E+00
+> [34.000000] [python/INFO] Total simulation time: 34.0
* It is forbidden to change the amount of work once the Activity is started */
Activity* set_remaining(double remains);
- virtual void fire_on_completion() const = 0;
+ virtual void fire_on_start() const = 0;
+ virtual void fire_on_this_start() const = 0;
+ virtual void fire_on_completion() const = 0;
virtual void fire_on_this_completion() const = 0;
- virtual void fire_on_suspend() const = 0;
- virtual void fire_on_this_suspend() const = 0;
- virtual void fire_on_resume() const = 0;
- virtual void fire_on_this_resume() const = 0;
- virtual void fire_on_veto() const = 0;
- virtual void fire_on_this_veto() const = 0;
+ virtual void fire_on_suspend() const = 0;
+ virtual void fire_on_this_suspend() const = 0;
+ virtual void fire_on_resume() const = 0;
+ virtual void fire_on_this_resume() const = 0;
+ virtual void fire_on_veto() = 0;
+ virtual void fire_on_this_veto() = 0;
public:
void start()
std::string name_ = "unnamed";
std::string tracing_category_ = "";
-protected:
+ inline static xbt::signal<void(AnyActivity const&)> on_start;
+ xbt::signal<void(AnyActivity const&)> on_this_start;
inline static xbt::signal<void(AnyActivity const&)> on_completion;
xbt::signal<void(AnyActivity const&)> on_this_completion;
inline static xbt::signal<void(AnyActivity const&)> on_suspend;
inline static xbt::signal<void(AnyActivity&)> on_veto;
xbt::signal<void(AnyActivity&)> on_this_veto;
+protected:
+ void fire_on_start() const override { on_start(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_this_start() const override { on_this_start(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_completion() const override { on_completion(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_this_completion() const override { on_this_completion(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_suspend() const override { on_suspend(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_this_suspend() const override { on_this_suspend(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_resume() const override { on_resume(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_this_resume() const override { on_this_resume(static_cast<const AnyActivity&>(*this)); }
+ void fire_on_veto() override { on_veto(static_cast<AnyActivity&>(*this)); }
+ void fire_on_this_veto() override { on_this_veto(static_cast<AnyActivity&>(*this)); }
+
public:
+ /*! \static Add a callback fired when any activity starts (no veto) */
+ static void on_start_cb(const std::function<void(AnyActivity const&)>& cb) { on_start.connect(cb); }
+ /*! Add a callback fired when this specific activity starts (no veto) */
+ void on_this_start_cb(const std::function<void(AnyActivity const&)>& cb) { on_this_start.connect(cb); }
/*! \static Add a callback fired when any activity completes (either normally, cancelled or failed) */
static void on_completion_cb(const std::function<void(AnyActivity const&)>& cb) { on_completion.connect(cb); }
/*! Add a callback fired when this specific activity completes (either normally, cancelled or failed) */
xbt::signal<void(Comm const&)> on_this_send;
static xbt::signal<void(Comm const&)> on_recv;
xbt::signal<void(Comm const&)> on_this_recv;
- inline static xbt::signal<void(Comm const&)> on_start;
- xbt::signal<void(Comm const&)> on_this_start;
protected:
void fire_on_completion() const override {
}
void fire_on_this_completion() const override {
/* The completion signal of a Comm has to be thrown only once and not by the sender AND the receiver.
- then Comm::on_completion is thrown in the kernel in CommImpl::finish.
+ then Comm::on_this_completion is thrown in the kernel in CommImpl::finish.
*/
}
- void fire_on_suspend() const override { on_suspend(*this); }
- void fire_on_this_suspend() const override { on_this_suspend(*this); }
- void fire_on_resume() const override { on_resume(*this); }
- void fire_on_this_resume() const override { on_this_resume(*this); }
- void fire_on_veto() const override { on_veto(const_cast<Comm&>(*this)); }
- void fire_on_this_veto() const override { on_this_veto(const_cast<Comm&>(*this)); }
+ /* These ensure that the on_completion signals are really thrown */
+ void fire_on_completion_for_real() const { Activity_T<Comm>::fire_on_completion(); }
+ void fire_on_this_completion_for_real() const { Activity_T<Comm>::fire_on_this_completion(); }
public:
/*! \static Add a callback fired when the send of any Comm is posted */
static void on_recv_cb(const std::function<void(Comm const&)>& cb) { on_recv.connect(cb); }
/*! Add a callback fired when the recv of this specific Comm is posted */
void on_this_recv_cb(const std::function<void(Comm const&)>& cb) { on_this_recv.connect(cb); }
- /*! \static Add a callback fired when any Comm starts */
- static void on_start_cb(const std::function<void(Comm const&)>& cb) { on_start.connect(cb); }
- /*! Add a callback fired when this specific Comm starts */
- void on_this_start_cb(const std::function<void(Comm const&)>& cb) { on_this_start.connect(cb); }
CommPtr set_copy_data_callback(const std::function<void(kernel::activity::CommImpl*, void*, size_t)>& callback);
XBT_ATTRIB_DEPRECATED_v338("Please manifest if you actually need this function") static void copy_buffer_callback(
bool parallel_ = false;
- inline static xbt::signal<void(Exec const&)> on_start;
- xbt::signal<void(Exec const&)> on_this_start;
-
protected:
explicit Exec(kernel::activity::ExecImplPtr pimpl);
Exec* do_start() override;
void reset() const;
- void fire_on_completion() const override { on_completion(*this); }
- void fire_on_this_completion() const override { on_this_completion(*this); }
- void fire_on_suspend() const override { on_suspend(*this); }
- void fire_on_this_suspend() const override { on_this_suspend(*this); }
- void fire_on_resume() const override { on_resume(*this); }
- void fire_on_this_resume() const override { on_this_resume(*this); }
- void fire_on_veto() const override { on_veto(const_cast<Exec&>(*this)); }
- void fire_on_this_veto() const override { on_this_veto(const_cast<Exec&>(*this)); }
-
public:
#ifndef DOXYGEN
Exec(Exec const&) = delete;
Exec& operator=(Exec const&) = delete;
#endif
- /*! \static Signal fired each time that any execution actually starts (no veto) */
- static void on_start_cb(const std::function<void(Exec const&)>& cb) { on_start.connect(cb); }
- /*! Signal fired each time that this specific execution actually starts (no veto) */
- void on_this_start_cb(const std::function<void(Exec const&)>& cb) { on_this_start.connect(cb); }
-
/*! \static Initiate the creation of an Exec. Setters have to be called afterwards */
static ExecPtr init();
friend kernel::resource::CpuAction; // signal exec_state_changed
#endif
+ static xbt::signal<void(Host&)> on_creation;
+ static xbt::signal<void(Host const&)> on_destruction;
+ xbt::signal<void(Host const&)> on_this_destruction;
+ static xbt::signal<void(kernel::resource::CpuAction&, kernel::resource::Action::State)> on_exec_state_change;
+
public:
explicit Host(kernel::resource::HostImpl* pimpl) : pimpl_(pimpl) {}
virtual ~Host(); // Call destroy() instead of manually deleting it.
Host* set_netpoint(kernel::routing::NetPoint* netpoint);
- static xbt::signal<void(Host&)> on_creation;
- static xbt::signal<void(Host const&)> on_destruction;
- xbt::signal<void(Host const&)> on_this_destruction;
- static xbt::signal<void(kernel::resource::CpuAction&, kernel::resource::Action::State)> on_exec_state_change;
-
public:
static xbt::signal<void(Host const&)> on_speed_change;
xbt::signal<void(Host const&)> on_this_speed_change;
friend kernel::EngineImpl;
#endif
- inline static xbt::signal<void(Io const&)> on_start;
- xbt::signal<void(Io const&)> on_this_start;
-
protected:
explicit Io(kernel::activity::IoImplPtr pimpl);
Io* do_start() override;
- void fire_on_completion() const override { on_completion(*this); }
- void fire_on_this_completion() const override { on_this_completion(*this); }
- void fire_on_suspend() const override { on_suspend(*this); }
- void fire_on_this_suspend() const override { on_this_suspend(*this); }
- void fire_on_resume() const override { on_resume(*this); }
- void fire_on_this_resume() const override { on_this_resume(*this); }
- void fire_on_veto() const override { on_veto(const_cast<Io&>(*this)); }
- void fire_on_this_veto() const override { on_this_veto(const_cast<Io&>(*this)); }
public:
enum class OpType { READ, WRITE };
- /*! \static Signal fired each time that any I/O actually starts (no veto) */
- static void on_start_cb(const std::function<void(Io const&)>& cb) { on_start.connect(cb); }
- /*! Signal fired each time this specific I/O actually starts (no veto) */
- void on_this_start_cb(const std::function<void(Io const&)>& cb) { on_this_start.connect(cb); }
-
/*! \static Initiate the creation of an I/O. Setters have to be called afterwards */
static IoPtr init();
/*! \static take a vector of s4u::IoPtr and return when one of them is finished.
ActivityPtr previous_activity_;
ActivityPtr current_activity_;
+ inline static xbt::signal<void(Task*)> on_start;
+ xbt::signal<void(Task*)> on_this_start;
+ inline static xbt::signal<void(Task*)> on_completion;
+ xbt::signal<void(Task*)> on_this_completion;
+
protected:
explicit Task(const std::string& name);
virtual ~Task() = default;
void set_current_activity(ActivityPtr a) { current_activity_ = a; }
- inline static xbt::signal<void(Task*)> on_start;
- xbt::signal<void(Task*)> on_this_start;
- inline static xbt::signal<void(Task*)> on_completion;
- xbt::signal<void(Task*)> on_this_completion;
-
public:
const std::string& get_name() const { return name_; }
const char* get_cname() const { return name_.c_str(); }
#include "simgrid/kernel/ProfileBuilder.hpp"
#include "simgrid/kernel/routing/NetPoint.hpp"
+#include "simgrid/plugins/load.h"
#include <simgrid/Exception.hpp>
#include <simgrid/s4u/Actor.hpp>
#include <simgrid/s4u/Barrier.hpp>
py::overload_cast<const std::string&, const std::string&, const std::string&>(&Host::create_disk),
py::call_guard<py::gil_scoped_release>(), "Create a disk")
.def("seal", &Host::seal, py::call_guard<py::gil_scoped_release>(), "Seal this host")
+ .def("turn_off", &Host::turn_off, py::call_guard<py::gil_scoped_release>(), "Turn off this host")
+ .def("turn_on", &Host::turn_on, py::call_guard<py::gil_scoped_release>(), "Turn on this host")
.def_property("pstate", &Host::get_pstate,
py::cpp_function(&Host::set_pstate, py::call_guard<py::gil_scoped_release>()),
"The current pstate (read/write property).")
"")
.def(
"__repr__", [](const Host* h) { return "Host(" + h->get_name() + ")"; },
- "Textual representation of the Host");
+ "Textual representation of the Host.");
+
+ m.def("sg_host_load_plugin_init", [host]() {
+ sg_host_load_plugin_init();
+
+ static_cast<pybind11::class_<simgrid::s4u::Host, std::unique_ptr<simgrid::s4u::Host, pybind11::nodelete>>>(host)
+ .def(
+ "reset_load", [](const Host* h) { sg_host_load_reset(h); }, py::call_guard<py::gil_scoped_release>(),
+ "Reset counters of the host load plugin for this host.")
+ .def_property_readonly(
+ "current_load", [](const Host* h) { return sg_host_get_current_load(h); }, "Current load of the host.")
+ .def_property_readonly(
+ "avg_load", [](const Host* h) { return sg_host_get_avg_load(h); }, "Average load of the host.")
+ .def_property_readonly(
+ "idle_time", [](const Host* h) { return sg_host_get_idle_time(h); }, "Idle time of the host")
+ .def_property_readonly(
+ "total_idle_time", [](const Host* h) { return sg_host_get_total_idle_time(h); },
+ "Total idle time of the host.")
+ .def_property_readonly(
+ "computed_flops", [](const Host* h) { return sg_host_get_computed_flops(h); },
+ "Computed flops of the host.");
+ });
py::enum_<simgrid::s4u::Host::SharingPolicy>(host, "SharingPolicy")
.value("NONLINEAR", simgrid::s4u::Host::SharingPolicy::NONLINEAR)
// Start only Activities with dependencies solved
for (auto const& activity: dag) {
- if (dynamic_cast<Exec*>(activity.get()) != nullptr and activity->dependencies_solved())
+ if (dynamic_cast<Exec*>(activity.get()) != nullptr && activity->dependencies_solved())
activity->start();
}
return dag;
if (get_iface()) {
const auto& piface = static_cast<const s4u::Comm&>(*get_iface());
set_iface(nullptr); // reset iface to protect against multiple trigger of the on_completion signals
- s4u::Comm::on_completion(piface);
- piface.on_this_completion(piface);
+ piface.fire_on_completion_for_real();
+ piface.fire_on_this_completion_for_real();
}
/* Update synchro state */
{
std::unordered_set<aid_t> actors;
for (const auto& [aid, state] : get_actors_list()) {
- if (state.is_todo() or state.is_done()) {
+ if (state.is_todo() || state.is_done()) {
actors.insert(aid);
}
}
// works with ODPOR in the way we intend it to work. There is not a
// good way to perform transition equality in SimGrid; instead, we
// effectively simply check for the presence of an actor in the sleep set.
- if (!get_actors_list().at(out_transition->aid_).has_more_to_consider())
+ if (not get_actors_list().at(out_transition->aid_).has_more_to_consider())
add_sleep_set(std::move(out_transition));
}
}
public:
void copy_from(const Strategy* strategy) override
{
- const BasicStrategy* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
+ const auto* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
xbt_assert(cast_strategy != nullptr);
depth_ = cast_strategy->depth_ - 1;
xbt_assert(depth_ > 0, "The exploration reached a depth greater than %d. We will stop here to prevent weird interaction with DFSExplorer. If you want to change that behaviour, you should augment the size of the search by using --cfg=model-check/max-depth:", _sg_mc_max_depth.get());
public:
void copy_from(const Strategy* strategy) override
{
- const MaxMatchComm* cast_strategy = dynamic_cast<MaxMatchComm const*>(strategy);
+ const auto* cast_strategy = dynamic_cast<MaxMatchComm const*>(strategy);
xbt_assert(cast_strategy != nullptr);
for (auto& [id, val] : cast_strategy->mailbox_)
mailbox_[id] = val;
std::pair<aid_t, int> best_transition(bool must_be_todo) const override
{
- std::pair<aid_t, int> min_found = std::make_pair(-1, value_of_state_+2);
+ std::pair<aid_t, int> min_found = std::make_pair(-1, value_of_state_ + 2);
for (auto const& [aid, actor] : actors_to_run_) {
if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done())
continue;
int aid_value = value_of_state_;
const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
-
- const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr) {
- if (mailbox_.count(cast_recv->get_mailbox()) > 0 and
- mailbox_.at(cast_recv->get_mailbox()) > 0) {
- aid_value--; // This means we have waiting recv corresponding to this recv
- } else {
+
+ if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition)) {
+ if (mailbox_.count(cast_recv->get_mailbox()) > 0 && mailbox_.at(cast_recv->get_mailbox()) > 0) {
+ aid_value--; // This means we have waiting recv corresponding to this recv
+ } else {
aid_value++;
- }
+ }
}
-
- const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr) {
- if (mailbox_.count(cast_send->get_mailbox()) > 0 and
- mailbox_.at(cast_send->get_mailbox()) < 0) {
- aid_value--; // This means we have waiting recv corresponding to this send
- }else {
- aid_value++;
- }
+
+ if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition)) {
+ if (mailbox_.count(cast_send->get_mailbox()) > 0 && mailbox_.at(cast_send->get_mailbox()) < 0) {
+ aid_value--; // This means we have waiting recv corresponding to this send
+ } else {
+ aid_value++;
+ }
}
-
+
if (aid_value < min_found.second)
min_found = std::make_pair(aid, aid_value);
}
return min_found;
}
-
void execute_next(aid_t aid, RemoteApp& app) override
{
const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get();
last_transition_ = transition->type_;
- const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr)
+ if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition))
last_mailbox_ = cast_recv->get_mailbox();
- const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr)
+ if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition))
last_mailbox_ = cast_send->get_mailbox();
}
};
public:
void copy_from(const Strategy* strategy) override
{
- const MinMatchComm* cast_strategy = dynamic_cast<MinMatchComm const*>(strategy);
- xbt_assert(cast_strategy != nullptr);
- for (auto& [id, val] : cast_strategy->mailbox_)
- mailbox_[id] = val;
- if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV)
- mailbox_[cast_strategy->last_mailbox_]--;
- if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND)
- mailbox_[cast_strategy->last_mailbox_]++;
-
- for (auto const& [_, val] : mailbox_)
- value_of_state_ -= std::abs(val);
- xbt_assert(value_of_state_ > 0, "MinMatchComm value shouldn't reach 0");
+ const auto* cast_strategy = dynamic_cast<MinMatchComm const*>(strategy);
+ xbt_assert(cast_strategy != nullptr);
+ for (auto& [id, val] : cast_strategy->mailbox_)
+ mailbox_[id] = val;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV)
+ mailbox_[cast_strategy->last_mailbox_]--;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND)
+ mailbox_[cast_strategy->last_mailbox_]++;
+
+ for (auto const& [_, val] : mailbox_)
+ value_of_state_ -= std::abs(val);
+ xbt_assert(value_of_state_ > 0, "MinMatchComm value shouldn't reach 0");
}
MinMatchComm() = default;
~MinMatchComm() override = default;
std::pair<aid_t, int> best_transition(bool must_be_todo) const override
{
- std::pair<aid_t, int> min_found = std::make_pair(-1, value_of_state_+2);
+ std::pair<aid_t, int> min_found = std::make_pair(-1, value_of_state_ + 2);
for (auto const& [aid, actor] : actors_to_run_) {
if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done())
continue;
int aid_value = value_of_state_;
const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
- const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr) {
- if ((mailbox_.count(cast_recv->get_mailbox()) > 0 and
- mailbox_.at(cast_recv->get_mailbox()) <= 0) or mailbox_.count(cast_recv->get_mailbox()) == 0)
- aid_value--; // This means we don't have waiting recv corresponding to this recv
- else
- aid_value++;
+ if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition)) {
+ if ((mailbox_.count(cast_recv->get_mailbox()) > 0 && mailbox_.at(cast_recv->get_mailbox()) <= 0) ||
+ mailbox_.count(cast_recv->get_mailbox()) == 0)
+ aid_value--; // This means we don't have waiting recv corresponding to this recv
+ else
+ aid_value++;
}
- const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr) {
- if ((mailbox_.count(cast_send->get_mailbox()) > 0 and
- mailbox_.at(cast_send->get_mailbox()) >= 0) or mailbox_.count(cast_send->get_mailbox()) == 0)
- aid_value--;
- else
- aid_value++;
+ if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition)) {
+ if ((mailbox_.count(cast_send->get_mailbox()) > 0 && mailbox_.at(cast_send->get_mailbox()) >= 0) ||
+ mailbox_.count(cast_send->get_mailbox()) == 0)
+ aid_value--;
+ else
+ aid_value++;
}
-
+
if (aid_value < min_found.second)
min_found = std::make_pair(aid, aid_value);
}
const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get();
last_transition_ = transition->type_;
- const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr)
+ if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition))
last_mailbox_ = cast_recv->get_mailbox();
- const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr)
+ if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition))
last_mailbox_ = cast_send->get_mailbox();
}
};
virtual std::pair<aid_t, int> best_transition(bool must_be_todo) const = 0;
/** Returns the best transition among those that should be interleaved. */
- std::pair<aid_t, int> next_transition() { return best_transition(true); }
+ std::pair<aid_t, int> next_transition() const { return best_transition(true); }
/** Allows for the strategy to update its fields knowing that the actor aid will
* be executed and a children strategy will then be created. */
/** Ensure at least one transition is marked as todo among the enabled ones not done.
* If required, it marks as todo the best transition according to the strategy. */
void consider_best() {
- for (auto& [_, actor] :actors_to_run_)
- if (actor.is_todo())
- return;
+ if (std::any_of(begin(actors_to_run_), end(actors_to_run_),
+ [](const auto& actor) { return actor.second.is_todo(); }))
+ return;
aid_t best_aid = best_transition(false).first;
if (best_aid != -1)
actors_to_run_.at(best_aid).mark_todo();
// else raise an error
void consider_one(aid_t aid)
{
- xbt_assert(actors_to_run_.at(aid).is_enabled() and not actors_to_run_.at(aid).is_done(),
+ xbt_assert(actors_to_run_.at(aid).is_enabled() && not actors_to_run_.at(aid).is_done(),
"Tried to mark as TODO actor %ld but it is either not enabled or already done", aid);
actors_to_run_.at(aid).mark_todo();
}
{
unsigned long count = 0;
for (auto& [_, actor] : actors_to_run_)
- if (actor.is_enabled() and not actor.is_done()) {
- actor.mark_todo();
- count++;
- }
+ if (actor.is_enabled() && not actor.is_done()) {
+ actor.mark_todo();
+ count++;
+ }
return count;
}
#include "src/mc/transition/Transition.hpp"
#include "xbt/random.hpp"
-#define MAX_RAND 100000
-
namespace simgrid::mc {
/** Guiding strategy that valuate states randomly */
class UniformStrategy : public Strategy {
+ static constexpr int MAX_RAND = 100000;
+
std::map<aid_t, int> valuation;
public:
}
void copy_from(const Strategy* strategy) override
{
- for (auto& [aid, _] : actors_to_run_)
+ for (auto const& [aid, _] : actors_to_run_)
valuation[aid] = xbt::random::uniform_int(0, MAX_RAND);
}
// Consider only valid actors
for (auto const& [aid, actor] : actors_to_run_) {
- if ((actor.is_todo() or not must_be_todo) and (not actor.is_done()) and actor.is_enabled())
+ if ((actor.is_todo() || not must_be_todo) && (not actor.is_done()) && actor.is_enabled())
possibilities++;
}
chosen = xbt::random::uniform_int(0, possibilities-1);
for (auto const& [aid, actor] : actors_to_run_) {
- if (((not actor.is_todo()) and must_be_todo) or actor.is_done() or (not actor.is_enabled()))
+ if (((not actor.is_todo()) && must_be_todo) || actor.is_done() || (not actor.is_enabled()))
continue;
if (chosen == 0) {
return std::make_pair(aid, valuation.at(aid));
}
/* Actually answer the request: let's execute the selected request (MCed does one step) */
- const auto executed_transition = state->execute_next(next, get_remote_app());
+ auto executed_transition = state->execute_next(next, get_remote_app());
on_transition_execute_signal(state->get_transition_out().get(), get_remote_app());
// If there are processes to interleave and the maximum depth has not been
for (const auto e_race : execution_seq_.get_reversible_races_of(next_E_p)) {
State* prev_state = stack_[e_race].get();
const auto choices = execution_seq_.get_missing_source_set_actors_from(e_race, prev_state->get_backtrack_set());
- if (!choices.empty()) {
+ if (not choices.empty()) {
// NOTE: To incorporate the idea of attempting to select the "best"
// backtrack point into SDPOR, instead of selecting the `first` initial,
// we should instead compute all choices and decide which is best
XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:");
for (const auto& [aid, transition] : state->get_sleep_set())
XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str());
- if (!state->has_empty_tree()) {
+ if (not state->has_empty_tree()) {
return state;
}
}
XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
State& prev_state = *stack_[e];
if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
- const auto result = prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e));
- switch (result) {
+ switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
case odpor::WakeupTree::InsertionResult::root: {
XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
"the execution prior to event `%u`:",
// "U (complicated expression)" portion
const EventSet conflict_union = std::accumulate(
- C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet acc, const UnfoldingEvent* e_prime) {
+ C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet& acc, const UnfoldingEvent* e_prime) {
return acc.make_union(unfolding.get_immediate_conflicts_of(e_prime));
});
{
std::vector<std::string> trace;
for (const auto& t : w) {
- const auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
- trace.push_back(std::move(a));
+ auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
+ trace.emplace_back(std::move(a));
}
return trace;
}
{
std::vector<std::string> trace;
for (const auto& t : this->contents_) {
- const auto a =
- xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str());
- trace.push_back(std::move(a));
+ auto a = xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str());
+ trace.emplace_back(std::move(a));
}
return trace;
}
// 2. disqualified_events.count(e_j) > 0
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
- if (disqualified_events.count(e_j) > 0 and happens_before(e_i, e_j)) {
+ if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) {
disqualified_events.insert(e_i);
break;
}
// happen after `e` is a member of `v`. In addition to marking
// the event in `v`, we also "simulate" running the action `v`
// from E'
- if (not happens_before(e, e_prime) or e_prime == next_E_p) {
+ if (not happens_before(e, e_prime) || e_prime == next_E_p) {
// First, push the transition onto the hypothetical execution
E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
}
}
}
- xbt_assert(!I_E_prime_v.empty(),
+ xbt_assert(not I_E_prime_v.empty(),
"For any non-empty execution, we know that "
"at minimum one actor is an initial since "
"some execution is possible with respect to a "
if (disqualified_actors.count(q) > 0) { // Did we already note that `q` is not an initial?
continue;
}
- const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
- return E_prime_v.happens_before(e_star, e_star_in_E_prime_v);
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_star_in_E_prime_v);
});
if (is_initial) {
// If the sleep set already contains `q`, we're done:
//
// Note the form of `v` in the pseudocode:
// `v := notdep(e, E).e'^
- {
- E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
- v.push_back(get_event_with_handle(e_prime).get_transition());
-
- const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
- v_handles.push_back(e_prime_in_E_prime_v);
-
- const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
- return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
- });
- if (is_initial) {
- if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {
- return std::nullopt;
- } else {
- WI_E_prime_v.insert(q);
- }
+ E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
+ v.push_back(get_event_with_handle(e_prime).get_transition());
+
+ const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
+ v_handles.push_back(e_prime_in_E_prime_v);
+
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_prime_in_E_prime_v);
+ });
+ if (is_initial) {
+ if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {
+ return std::nullopt;
+ } else {
+ WI_E_prime_v.insert(q);
}
}
- {
- const Execution pre_E_e = get_prefix_before(e);
- const auto sleeping_actors = state_at_e.get_sleeping_actors();
-
- // Check if any enabled actor that is independent with
- // this execution after `v` is contained in the sleep set
- for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
- const bool is_in_WI_E =
- astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition());
- const bool is_in_sleep_set = sleeping_actors.count(aid) > 0;
-
- // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set.
- // This implies that the intersection between the two is non-empty
- if (is_in_WI_E && is_in_sleep_set) {
- return std::nullopt;
- }
- }
+
+ const Execution pre_E_e = get_prefix_before(e);
+ const auto sleeping_actors = state_at_e.get_sleeping_actors();
+
+ // Check if any enabled actor that is independent with
+ // this execution after `v` is contained in the sleep set
+ for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
+ const bool is_in_WI_E =
+ astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition());
+ const bool is_in_sleep_set = sleeping_actors.count(aid) > 0;
+
+ // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set.
+ // This implies that the intersection between the two is non-empty
+ if (is_in_WI_E && is_in_sleep_set)
+ return std::nullopt;
}
+
return v;
}
auto w_now = w;
for (const auto& next_E_p : v) {
- const aid_t p = next_E_p->aid_;
-
// Is `p in `I_[E](w)`?
- if (E_v.is_initial_after_execution_of(w_now, p)) {
+ if (const aid_t p = next_E_p->aid_; E_v.is_initial_after_execution_of(w_now, p)) {
// Remove `p` from w and continue
// INVARIANT: If `p` occurs in `w`, it had better refer to the same
return false;
}
-} // namespace simgrid::mc::odpor
\ No newline at end of file
+} // namespace simgrid::mc::odpor
const bool e_j_before_e_k = execution.happens_before(e_j, e_k);
const bool e_i_before_e_k = execution.happens_before(e_i, e_k);
// Logical equivalent of `e_i_before_e_j ^ e_j_before_e_k --> e_i_before_e_k`
- REQUIRE((!(e_i_before_e_j and e_j_before_e_k) or e_i_before_e_k));
+ REQUIRE((not(e_i_before_e_j && e_j_before_e_k) || e_i_before_e_k));
}
}
}
using Handler = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
using HandlerMap = std::unordered_map<Action, Handler>;
- const static HandlerMap handlers =
- HandlerMap{{Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
- {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
- {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
- {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
- {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
- {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
- {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
- {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
- {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
- {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
- {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
- {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
- {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
- {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
- {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
- {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
- {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
- {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
- {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
+ const static HandlerMap handlers = {
+ {Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
+ {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
+ {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
+ {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
+ {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
+ {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
+ {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
+ {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
+ {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
+ {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
+ {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
+ {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
+ {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
+ {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
+ {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
+ {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
+ {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
+ {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
+ {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
const auto* e2_action = E.get_transition_for_handle(e2);
if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
}
}
-bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// ActorJoin races with another event iff its target `T` is the same as
// the actor executing the other transition. Clearly, then, we could not join
return false;
}
-bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// BarrierAsyncLock is always enabled
return true;
}
bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
- const Transition* e2)
+ const Transition* /*e2*/)
{
// If the other event is a barrier lock event, then we
// are not reversible; otherwise we are reversible.
return e1_action != Transition::Type::BARRIER_ASYNC_LOCK;
}
-bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// CommRecv is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// CommSend is always enabled
return true;
}
bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
- const Transition* e2)
+ const Transition* /*e2*/)
{
// If the other event is a communication event, then we
// are not reversible; otherwise we are reversible.
const auto e1_action = E.get_transition_for_handle(e1)->type_;
- return e1_action != Transition::Type::COMM_ASYNC_SEND and e1_action != Transition::Type::COMM_ASYNC_RECV;
+ return e1_action != Transition::Type::COMM_ASYNC_SEND && e1_action != Transition::Type::COMM_ASYNC_RECV;
}
-bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// CommTest is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// MutexAsyncLock is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// MutexTest is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// MutexTrylock is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// MutexUnlock is always enabled
return true;
}
bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
- const Transition* e2)
+ const Transition* /*e2*/)
{
// TODO: Get the semantics correct here
const auto e1_action = E.get_transition_for_handle(e1)->type_;
- return e1_action != Transition::Type::MUTEX_ASYNC_LOCK and e1_action != Transition::Type::MUTEX_UNLOCK;
+ return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK;
}
-bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// SemAsyncLock is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// SemUnlock is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// TODO: Get the semantics correct here
return false;
}
-bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// Object access is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// Random is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// TestAny is always enabled
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1,
- const Transition* e2)
+bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle /*e1*/,
+ const Transition* /*e2*/)
{
// TODO: We need to check if any of the transitions
// waited on occurred before `e1`
#include <algorithm>
#include <exception>
+#include <memory>
#include <queue>
namespace simgrid::mc::odpor {
// and instead track this with the iterator
PartialExecution seq_;
const WakeupTreeNode* cur_node = this;
- while (cur_node != nullptr and !cur_node->is_root()) {
+ while (cur_node != nullptr && not cur_node->is_root()) {
seq_.push_front(cur_node->action_);
cur_node = cur_node->parent_;
}
}
}
-WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode({}))) {}
+WakeupTree::WakeupTree() : WakeupTree(std::make_unique<WakeupTreeNode>()) {}
WakeupTree::WakeupTree(std::unique_ptr<WakeupTreeNode> root) : root_(root.get())
{
this->insert_node(std::move(root));
{
std::vector<std::string> trace;
for (const auto* child : root_->children_) {
- const auto t = child->get_action();
- const auto message = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
- trace.push_back(std::move(message));
+ const auto t = child->get_action();
+ auto message = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
+ trace.emplace_back(std::move(message));
}
return trace;
}
WakeupTreeNode* WakeupTree::make_node(std::shared_ptr<Transition> u)
{
- auto node = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(std::move(u)));
+ auto node = std::make_unique<WakeupTreeNode>(std::move(u));
auto* node_handle = node.get();
this->nodes_[node_handle] = std::move(node);
return node_handle;
shortest_sequence.has_value()) {
// Insert the sequence as a child of `node`, but only
// if the node is not already a leaf
- if (not node->is_leaf() or node == this->root_) {
+ if (not node->is_leaf() || node == this->root_) {
// NOTE: It's entirely possible that the shortest
// sequence we are inserting is empty. Consider the
// following two cases:
*/
class WakeupTreeNode {
private:
- explicit WakeupTreeNode(std::shared_ptr<Transition> u) : action_(u) {}
-
WakeupTreeNode* parent_ = nullptr;
/** An ordered list of children of for this node in the tree */
friend WakeupTreeIterator;
public:
+ explicit WakeupTreeNode(std::shared_ptr<Transition> u) : action_(u) {}
+
+ WakeupTreeNode() = default;
~WakeupTreeNode() = default;
WakeupTreeNode(const WakeupTreeNode&) = delete;
WakeupTreeNode(WakeupTreeNode&&) = default;
Configuration::Configuration(const EventSet& events) : events_(events)
{
- if (!events_.is_valid_configuration()) {
+ if (not events_.is_valid_configuration()) {
throw std::invalid_argument("The events do not form a valid configuration");
}
this->latest_event_mapping[e->get_actor()] = e;
// Preserves the property that the configuration is causally closed
- if (auto history = History(e); !this->events_.contains(history)) {
+ if (auto history = History(e); not this->events_.contains(history)) {
throw std::invalid_argument("The newly added event has dependencies "
"which are missing from this configuration");
}
// 2. `e` itself must not conflict with any events of
// the configuration; otherwise adding the event would
// violate the invariant that a configuration is conflict-free
- return contains(e->get_history()) and (not e->conflicts_with_any(this->events_));
+ return contains(e->get_history()) && (not e->conflicts_with_any(this->events_));
}
bool Configuration::is_compatible_with(const History& history) const
// we know that the prior set `S` covered the entire history of C and
// was maximal. Subsequent sets will miss events earlier in the
// topological ordering that appear in `S`
- EventSet minimally_reproducible_events = EventSet();
+ EventSet minimally_reproducible_events;
for (const auto& maximal_set : maximal_subsets_iterator_wrapper<Configuration>(*this)) {
if (maximal_set.size() > minimally_reproducible_events.size()) {
for (const auto& event_in_spike : spikes) {
events.push_back(*event_in_spike);
}
- return EventSet(std::move(events));
+ return EventSet(events);
};
const auto alternative =
std::find_if(comb.combinations_begin(), comb.combinations_end(),
SECTION("Forward direction")
{
- auto ordered_events = C.get_topologically_sorted_events();
- const EventSet ordered_event_set = EventSet(std::move(ordered_events));
+ const auto ordered_event_set = EventSet(C.get_topologically_sorted_events());
REQUIRE(events_seen == ordered_event_set);
}
SECTION("Reverse direction")
{
- auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
- const EventSet ordered_event_set = EventSet(std::move(ordered_events));
+ const auto ordered_event_set = EventSet(C.get_topologically_sorted_events_of_reverse_graph());
REQUIRE(events_seen == ordered_event_set);
}
}
// The first alternative that is found is the one that is chosen. Since
// traversal over the elements of an unordered_set<> are not guaranteed,
// both {e0, e4} and {e0, e7} are valid alternatives
- REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) or
+ REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) ||
alternative.value().get_events() == EventSet({e0_handle, e7_handle})));
}
const auto alternative = C.compute_alternative_to(D_plus_e, U);
REQUIRE(alternative.has_value());
- REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e7_handle}) or
- alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle}) or
+ REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e7_handle}) ||
+ alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle}) ||
alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle, e8_handle})));
}
namespace simgrid::mc::udpor {
-EventSet::EventSet(Configuration&& config) : EventSet(config.get_events()) {}
+EventSet::EventSet(const Configuration& config) : EventSet(config.get_events()) {}
void EventSet::remove(const UnfoldingEvent* e)
{
temporarily_marked_events.insert(evt);
EventSet immediate_causes = evt->get_immediate_causes();
- if (!immediate_causes.empty() && immediate_causes.is_subset_of(temporarily_marked_events)) {
+ if (not immediate_causes.empty() && immediate_causes.is_subset_of(temporarily_marked_events)) {
throw std::invalid_argument("Attempted to perform a topological sort on a configuration "
"whose contents contain a cycle. The configuration (and the graph "
"connecting all of the events) is an invalid event structure");
return contents;
}
-} // namespace simgrid::mc::udpor
\ No newline at end of file
+} // namespace simgrid::mc::udpor
EventSet& operator=(const EventSet&) = default;
EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
- explicit EventSet(Configuration&& config);
- explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end()) {}
- explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+ explicit EventSet(const Configuration& config);
+ explicit EventSet(const std::vector<const UnfoldingEvent*>& raw_events)
+ : events_(raw_events.begin(), raw_events.end())
+ {
+ }
+ explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(std::move(raw_events)) {}
explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
auto begin() const { return this->events_.begin(); }
EventSet C_copy = C;
EventSet D_copy = D;
- std::vector<const UnfoldingEvent*> actual_A = std::move(A).move_into_vector();
- std::vector<const UnfoldingEvent*> actual_B = std::move(B).move_into_vector();
- std::vector<const UnfoldingEvent*> actual_C = std::move(C).move_into_vector();
- std::vector<const UnfoldingEvent*> actual_D = std::move(D).move_into_vector();
+ const std::vector<const UnfoldingEvent*> actual_A = std::move(A).move_into_vector();
+ const std::vector<const UnfoldingEvent*> actual_B = std::move(B).move_into_vector();
+ const std::vector<const UnfoldingEvent*> actual_C = std::move(C).move_into_vector();
+ const std::vector<const UnfoldingEvent*> actual_D = std::move(D).move_into_vector();
- EventSet A_copy_remade(std::move(actual_A));
- EventSet B_copy_remade(std::move(actual_B));
- EventSet C_copy_remade(std::move(actual_C));
- EventSet D_copy_remade(std::move(actual_D));
+ EventSet A_copy_remade(actual_A);
+ EventSet B_copy_remade(actual_B);
+ EventSet C_copy_remade(actual_C);
+ EventSet D_copy_remade(actual_D);
REQUIRE(A_copy == A_copy_remade);
REQUIRE(B_copy == B_copy_remade);
return subset_local;
}();
- {
- // To test this, we verify that at each point none of the events
- // that follow after any particular event `e` are contained in
- // `e`'s history
- EventSet invalid_events = subset;
- const auto ordered_events = subset.get_topological_ordering();
-
- std::for_each(ordered_events.begin(), ordered_events.end(), [&](const UnfoldingEvent* e) {
- History history(e);
- for (const auto* e_hist : history) {
- if (e_hist == e)
- continue;
- REQUIRE_FALSE(invalid_events.contains(e_hist));
- }
- invalid_events.remove(e);
- });
+ // To test this, we verify that at each point none of the events
+ // that follow after any particular event `e` are contained in
+ // `e`'s history
+ EventSet invalid_events = subset;
+ for (const auto* e : subset.get_topological_ordering()) {
+ for (const auto* e_hist : History(e)) {
+ if (e_hist == e)
+ continue;
+ REQUIRE_FALSE(invalid_events.contains(e_hist));
+ }
+ invalid_events.remove(e);
}
- {
- // To test this, we verify that at each point none of the events
- // that we've processed in the ordering are ever seen again
- // in anybody else's history
- EventSet events_seen;
- const auto ordered_events = subset.get_topological_ordering_of_reverse_graph();
-
- std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) {
- History history(e);
-
- for (const auto* e_hist : history) {
- // Unlike the test above, we DO want to ensure
- // that `e` itself ALSO isn't yet seen
-
- // If this event has been "seen" before,
- // this implies that event `e` appears later
- // in the list than one of its ancestors
- REQUIRE_FALSE(events_seen.contains(e_hist));
- }
- events_seen.insert(e);
- });
+
+ // To test this, we verify that at each point none of the events
+ // that we've processed in the ordering are ever seen again
+ // in anybody else's history
+ EventSet events_seen;
+ for (const auto* e : subset.get_topological_ordering_of_reverse_graph()) {
+ for (const auto* e_hist : History(e)) {
+ // Unlike the test above, we DO want to ensure
+ // that `e` itself ALSO isn't yet seen
+
+ // If this event has been "seen" before,
+ // this implies that event `e` appears later
+ // in the list than one of its ancestors
+ REQUIRE_FALSE(events_seen.contains(e_hist));
+ }
+ events_seen.insert(e);
}
}
}
namespace simgrid::mc::udpor {
EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, Unfolding* U,
- const std::shared_ptr<Transition> action)
+ std::shared_ptr<Transition> action)
{
using Action = Transition::Type;
using Handler = std::function<EventSet(const Configuration&, Unfolding*, const std::shared_ptr<Transition>)>;
using HandlerMap = std::unordered_map<Action, Handler>;
- const static HandlerMap handlers =
- HandlerMap{{Action::COMM_ASYNC_RECV, &ExtensionSetCalculator::partially_extend_CommRecv},
- {Action::COMM_ASYNC_SEND, &ExtensionSetCalculator::partially_extend_CommSend},
- {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait},
- {Action::COMM_TEST, &ExtensionSetCalculator::partially_extend_CommTest},
- {Action::MUTEX_ASYNC_LOCK, &ExtensionSetCalculator::partially_extend_MutexAsyncLock},
- {Action::MUTEX_UNLOCK, &ExtensionSetCalculator::partially_extend_MutexUnlock},
- {Action::MUTEX_WAIT, &ExtensionSetCalculator::partially_extend_MutexWait},
- {Action::MUTEX_TEST, &ExtensionSetCalculator::partially_extend_MutexTest},
- {Action::ACTOR_JOIN, &ExtensionSetCalculator::partially_extend_ActorJoin}};
+ const static HandlerMap handlers = {
+ {Action::COMM_ASYNC_RECV, &ExtensionSetCalculator::partially_extend_CommRecv},
+ {Action::COMM_ASYNC_SEND, &ExtensionSetCalculator::partially_extend_CommSend},
+ {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait},
+ {Action::COMM_TEST, &ExtensionSetCalculator::partially_extend_CommTest},
+ {Action::MUTEX_ASYNC_LOCK, &ExtensionSetCalculator::partially_extend_MutexAsyncLock},
+ {Action::MUTEX_UNLOCK, &ExtensionSetCalculator::partially_extend_MutexUnlock},
+ {Action::MUTEX_WAIT, &ExtensionSetCalculator::partially_extend_MutexWait},
+ {Action::MUTEX_TEST, &ExtensionSetCalculator::partially_extend_MutexTest},
+ {Action::ACTOR_JOIN, &ExtensionSetCalculator::partially_extend_ActorJoin}};
if (const auto handler = handlers.find(action->type_); handler != handlers.end()) {
return handler->second(C, U, std::move(action));
}
EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, Unfolding* U,
- const std::shared_ptr<Transition> action)
+ std::shared_ptr<Transition> action)
{
EventSet exC;
- const auto send_action = std::static_pointer_cast<CommSendTransition>(std::move(action));
+ const auto send_action = std::static_pointer_cast<CommSendTransition>(action);
const auto pre_event_a_C = C.pre_event(send_action->aid_);
const unsigned sender_mailbox = send_action->get_mailbox();
// Com contains a matching c' = AsyncReceive(m, _) with `action`
for (const auto e : C) {
const bool transition_type_check = [&]() {
- if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- async_send != nullptr) {
- return async_send->get_mailbox() == sender_mailbox;
- }
+ const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+ return async_send && async_send->get_mailbox() == sender_mailbox;
// TODO: Add `TestAny` dependency
- return false;
}();
if (transition_type_check) {
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
+ EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
// TODO: Check D_K(a, lambda(e)) (only matters in the case of CommTest)
const auto e_prime = U->discover_event(std::move(K), send_action);
}
EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
- const std::shared_ptr<Transition> action)
+ std::shared_ptr<Transition> action)
{
EventSet exC;
- const auto recv_action = std::static_pointer_cast<CommRecvTransition>(std::move(action));
+ const auto recv_action = std::static_pointer_cast<CommRecvTransition>(action);
const unsigned recv_mailbox = recv_action->get_mailbox();
const auto pre_event_a_C = C.pre_event(recv_action->aid_);
// Com contains a matching c' = AsyncReceive(m, _) with a
for (const auto e : C) {
const bool transition_type_check = [&]() {
- if (const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) {
- return true;
- }
+ const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
+ return async_recv && async_recv->get_mailbox() == recv_mailbox;
// TODO: Add `TestAny` dependency
- return false;
}();
if (transition_type_check) {
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
+ EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
// TODO: Check D_K(a, lambda(e)) (ony matters in the case of TestAny)
if (true) {
{
EventSet exC;
- const auto wait_action = std::static_pointer_cast<CommWaitTransition>(std::move(action));
+ const auto wait_action = std::static_pointer_cast<CommWaitTransition>(action);
const auto wait_comm = wait_action->get_comm();
const auto pre_event_a_C = C.pre_event(wait_action->aid_);
// whose transition is the `CommRecv` or `CommSend` whose resulting
// communication this `CommWait` waits on
const auto issuer = std::find_if(C.begin(), C.end(), [&](const UnfoldingEvent* e) {
- if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- e_issuer_receive != nullptr) {
+ if (const auto* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
return e_issuer_receive->aid_ == wait_action->aid_ && wait_comm == e_issuer_receive->get_comm();
}
- if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- e_issuer_send != nullptr) {
+ if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
}
// as needed to reach the receive/send number that is `issuer`.
// ...
// ...
- if (const CommRecvTransition* e_issuer_receive =
- dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
- e_issuer_receive != nullptr) {
+ if (const auto* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition())) {
const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
// Check from the config -> how many sends have there been
const unsigned send_position =
std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send != nullptr) {
- return e_send->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+ return e_send && e_send->get_mailbox() == issuer_mailbox;
});
// Check from e_issuer -> what place is the issuer in?
const unsigned receive_position =
std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
- const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- if (e_receive != nullptr) {
- return e_receive->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
+ return e_receive && e_receive->get_mailbox() == issuer_mailbox;
});
if (send_position >= receive_position) {
exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
}
- } else if (const CommSendTransition* e_issuer_send =
- dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
- e_issuer_send != nullptr) {
+ } else if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition())) {
const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
// Check from e_issuer -> what place is the issuer in?
const unsigned send_position =
std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send != nullptr) {
- return e_send->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+ return e_send && e_send->get_mailbox() == issuer_mailbox;
});
// Check from the config -> how many sends have there been
const unsigned receive_position =
std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
- const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- if (e_receive != nullptr) {
- return e_receive->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
+ return e_receive && e_receive->get_mailbox() == issuer_mailbox;
});
if (send_position <= receive_position) {
}
// 3. foreach event e in C do
- if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
- e_issuer_send != nullptr) {
+ if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition())) {
for (const auto e : C) {
// If the provider of the communication for `CommWait` is a
// `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
}
const auto issuer_mailbox = e_issuer_send->get_mailbox();
- const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- if (e_recv->get_mailbox() != issuer_mailbox) {
+ if (const auto* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
+ e_recv->get_mailbox() != issuer_mailbox) {
continue;
}
// `WaitAny()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
}
// What send # is the issuer
- const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send != nullptr) {
- return e_send->get_mailbox() == issuer_mailbox;
- }
- return false;
- });
+ const unsigned send_position =
+ std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto ev) {
+ const auto* e_send = dynamic_cast<const CommSendTransition*>(ev->get_transition());
+ return e_send && e_send->get_mailbox() == issuer_mailbox;
+ });
// What receive # is the event `e`?
- const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
- const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- if (e_receive != nullptr) {
- return e_receive->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto ev) {
+ const auto* e_receive = dynamic_cast<const CommRecvTransition*>(ev->get_transition());
+ return e_receive && e_receive->get_mailbox() == issuer_mailbox;
});
if (send_position == receive_position) {
exC.insert(U->discover_event(std::move(K), wait_action));
}
}
- } else if (const CommRecvTransition* e_issuer_recv =
- dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
- e_issuer_recv != nullptr) {
+ } else if (const auto* e_issuer_recv = dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition())) {
for (const auto e : C) {
// If the provider of the communication for `CommWait` is a
// `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
}
const auto issuer_mailbox = e_issuer_recv->get_mailbox();
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send->get_mailbox() != issuer_mailbox) {
+ if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+ e_send->get_mailbox() != issuer_mailbox) {
continue;
}
// `WaitAny()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
}
// What receive # is the event `e`?
- const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send != nullptr) {
- return e_send->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto ev) {
+ const auto* e_send = dynamic_cast<const CommSendTransition*>(ev->get_transition());
+ return e_send && e_send->get_mailbox() == issuer_mailbox;
});
// What send # is the issuer
const unsigned receive_position =
- std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
- const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- if (e_receive != nullptr) {
- return e_receive->get_mailbox() == issuer_mailbox;
- }
- return false;
+ std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto ev) {
+ const auto* e_receive = dynamic_cast<const CommRecvTransition*>(ev->get_transition());
+ return e_receive && e_receive->get_mailbox() == issuer_mailbox;
});
if (send_position == receive_position) {
{
EventSet exC;
- const auto test_action = std::static_pointer_cast<CommTestTransition>(std::move(action));
+ const auto test_action = std::static_pointer_cast<CommTestTransition>(action);
const auto test_comm = test_action->get_comm();
const auto test_aid = test_action->aid_;
const auto pre_event_a_C = C.pre_event(test_action->aid_);
// whose transition is the `CommRecv` or `CommSend` whose resulting
// communication this `CommTest` tests on
const auto issuer = std::find_if(C.begin(), C.end(), [=](const UnfoldingEvent* e) {
- if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- e_issuer_receive != nullptr) {
+ if (const auto* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
return e_issuer_receive->aid_ == test_aid && test_comm == e_issuer_receive->get_comm();
}
- if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- e_issuer_send != nullptr) {
+ if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
return e_issuer_send->aid_ == test_aid && test_comm == e_issuer_send->get_comm();
}
const History e_issuer_history(e_issuer);
// 3. foreach event e in C do
- if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
- e_issuer_send != nullptr) {
+ if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition())) {
for (const auto e : C) {
// If the provider of the communication for `CommTest` is a
// `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
const auto issuer_mailbox = e_issuer_send->get_mailbox();
- if (const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
+ if (const auto* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
e_recv->get_mailbox() != issuer_mailbox) {
continue;
}
// `CommTest()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
}
// What send # is the issuer
- const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send != nullptr) {
- return e_send->get_mailbox() == issuer_mailbox;
- }
- return false;
- });
+ const unsigned send_position =
+ std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto ev) {
+ const auto* e_send = dynamic_cast<const CommSendTransition*>(ev->get_transition());
+ return e_send && e_send->get_mailbox() == issuer_mailbox;
+ });
// What receive # is the event `e`?
- const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
- const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- if (e_receive != nullptr) {
- return e_receive->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto ev) {
+ const auto* e_receive = dynamic_cast<const CommRecvTransition*>(ev->get_transition());
+ return e_receive && e_receive->get_mailbox() == issuer_mailbox;
});
if (send_position == receive_position) {
exC.insert(U->discover_event(std::move(K), test_action));
}
}
- } else if (const CommRecvTransition* e_issuer_recv =
- dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
- e_issuer_recv != nullptr) {
+ } else if (const auto* e_issuer_recv = dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition())) {
for (const auto e : C) {
// If the provider of the communication for `CommTest` is a
// `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
}
const auto issuer_mailbox = e_issuer_recv->get_mailbox();
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send->get_mailbox() != issuer_mailbox) {
+ if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+ e_send->get_mailbox() != issuer_mailbox) {
continue;
}
// `WaitAny()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
}
// What receive # is the event `e`?
- const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
- const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
- if (e_send != nullptr) {
- return e_send->get_mailbox() == issuer_mailbox;
- }
- return false;
+ const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto ev) {
+ const auto* e_send = dynamic_cast<const CommSendTransition*>(ev->get_transition());
+ return e_send && e_send->get_mailbox() == issuer_mailbox;
});
// What send # is the issuer
const unsigned receive_position =
- std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
- const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
- if (e_receive != nullptr) {
- return e_receive->get_mailbox() == issuer_mailbox;
- }
- return false;
+ std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto ev) {
+ const auto* e_receive = dynamic_cast<const CommRecvTransition*>(ev->get_transition());
+ return e_receive && e_receive->get_mailbox() == issuer_mailbox;
});
if (send_position == receive_position) {
std::shared_ptr<Transition> action)
{
EventSet exC;
- const auto mutex_lock = std::static_pointer_cast<MutexTransition>(std::move(action));
+ const auto mutex_lock = std::static_pointer_cast<MutexTransition>(action);
const auto pre_event_a_C = C.pre_event(mutex_lock->aid_);
// for each event e in C
// for each event e in C
for (const auto e : C) {
// Check for other locks on the same mutex
- if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
- e_mutex != nullptr) {
- if (e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) {
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
- exC.insert(U->discover_event(std::move(K), mutex_lock));
- }
+ if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+ e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) {
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
+ exC.insert(U->discover_event(std::move(K), mutex_lock));
}
}
return exC;
std::shared_ptr<Transition> action)
{
EventSet exC;
- const auto mutex_unlock = std::static_pointer_cast<MutexTransition>(std::move(action));
+ const auto mutex_unlock = std::static_pointer_cast<MutexTransition>(action);
const auto pre_event_a_C = C.pre_event(mutex_unlock->aid_);
// for each event e in C
// for each event e in C
for (const auto e : C) {
// Check for MutexTest
- if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
- e_mutex != nullptr) {
- if (e_mutex->type_ == Transition::Type::MUTEX_TEST || e_mutex->type_ == Transition::Type::MUTEX_WAIT) {
- // TODO: Check if dependent or not
- // This entails getting information about
- // the relative position of the mutex in the queue, which
- // again means we need more context...
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
- exC.insert(U->discover_event(std::move(K), mutex_unlock));
- }
+ if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+ e_mutex->type_ == Transition::Type::MUTEX_TEST || e_mutex->type_ == Transition::Type::MUTEX_WAIT) {
+ // TODO: Check if dependent or not
+ // This entails getting information about
+ // the relative position of the mutex in the queue, which
+ // again means we need more context...
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
+ exC.insert(U->discover_event(std::move(K), mutex_unlock));
}
}
return exC;
std::shared_ptr<Transition> action)
{
EventSet exC;
- const auto mutex_wait = std::static_pointer_cast<MutexTransition>(std::move(action));
+ const auto mutex_wait = std::static_pointer_cast<MutexTransition>(action);
const auto pre_event_a_C = C.pre_event(mutex_wait->aid_);
// for each event e in C
// for each event e in C
for (const auto e : C) {
// Check for any unlocks
- if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+ if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) {
// TODO: Check if dependent or not
// This entails getting information about
// the relative position of the mutex in the queue, which
// again means we need more context...
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
exC.insert(U->discover_event(std::move(K), mutex_wait));
}
}
std::shared_ptr<Transition> action)
{
EventSet exC;
- const auto mutex_test = std::static_pointer_cast<MutexTransition>(std::move(action));
+ const auto mutex_test = std::static_pointer_cast<MutexTransition>(action);
const auto pre_event_a_C = C.pre_event(mutex_test->aid_);
// for each event e in C
// 1. If lambda(e) := pre(a) -> add it. Note that if
- // pre_evevnt_a_C.has_value() == false, this implies `C` is
+ // pre_event_a_C.has_value() == false, this implies `C` is
// empty or which we treat as implicitly containing the bottom event
if (pre_event_a_C.has_value()) {
const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_test);
// for each event e in C
for (const auto e : C) {
// Check for any unlocks
- if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+ if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) {
// TODO: Check if dependent or not
// This entails getting information about
// the relative position of the mutex in the queue, which
// again means we need more context...
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ auto K = EventSet({e, pre_event_a_C.value_or(e)});
exC.insert(U->discover_event(std::move(K), mutex_test));
}
}
{
EventSet exC;
- const auto join_action = std::static_pointer_cast<ActorJoinTransition>(std::move(action));
- const auto pre_event_a_C = C.pre_event(join_action->aid_);
+ const auto join_action = std::static_pointer_cast<ActorJoinTransition>(action);
// Handling ActorJoin is very simple: it is independent with all
// other transitions. Thus the only event it could possibly depend
// on is pre(a, C) or the root
- if (pre_event_a_C.has_value()) {
+ if (const auto pre_event_a_C = C.pre_event(join_action->aid_); pre_event_a_C.has_value()) {
const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), join_action);
exC.insert(e_prime);
} else {
static EventSet partially_extend_ActorJoin(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
public:
- static EventSet partially_extend(const Configuration&, Unfolding*, const std::shared_ptr<Transition>);
+ static EventSet partially_extend(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
};
} // namespace simgrid::mc::udpor
// --- ex({⊥}) ---
const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_send);
- { // Assert that event `a` has been added
- UnfoldingEvent e_send(EventSet(), comm_send);
- REQUIRE(incremental_exC_send.size() == 1);
- REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
- REQUIRE(U.size() == 1);
- }
+ // Assert that event `a` has been added
+ UnfoldingEvent e_send(EventSet(), comm_send);
+ REQUIRE(incremental_exC_send.size() == 1);
+ REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
+ REQUIRE(U.size() == 1);
const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_recv);
- { // Assert that event `b` has been added
- UnfoldingEvent e_recv(EventSet(), comm_recv);
- REQUIRE(incremental_exC_recv.size() == 1);
- REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
- REQUIRE(U.size() == 2);
- }
+ // Assert that event `b` has been added
+ UnfoldingEvent e_recv(EventSet(), comm_recv);
+ REQUIRE(incremental_exC_recv.size() == 1);
+ REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
+ REQUIRE(U.size() == 2);
// --- ex({⊥}) ---
// 2. UDPOR will then attempt to expand ex({⊥, a}) or ex({⊥, b}). Both have
// --- ex({⊥, a}) ---
const auto incremental_exC_recv2 = ExtensionSetCalculator::partially_extend(Configuration({e_a}), &U, comm_recv);
- { // Assert that no event has been added and that
- // e_b is contained in the extension set
- UnfoldingEvent e_send(EventSet(), comm_send);
- REQUIRE(incremental_exC_recv2.size() == 1);
- REQUIRE(incremental_exC_recv2.contains(e_b));
+ // Assert that no event has been added and that
+ // e_b is contained in the extension set
+ REQUIRE(incremental_exC_recv2.size() == 1);
+ REQUIRE(incremental_exC_recv2.contains(e_b));
- // Here, `e_a` shouldn't be added again
- REQUIRE(U.size() == 2);
- }
+ // Here, `e_a` shouldn't be added again
+ REQUIRE(U.size() == 2);
// --- ex({⊥, a}) ---
// --- ex({⊥, b}) ---
const auto incremental_exC_send2 = ExtensionSetCalculator::partially_extend(Configuration({e_b}), &U, comm_send);
- { // Assert that no event has been added and that
- // e_a is contained in the extension set
- REQUIRE(incremental_exC_send2.size() == 1);
- REQUIRE(incremental_exC_send2.contains(e_a));
+ // Assert that no event has been added and that
+ // e_a is contained in the extension set
+ REQUIRE(incremental_exC_send2.size() == 1);
+ REQUIRE(incremental_exC_send2.contains(e_a));
- // Here, `e_b` shouldn't be added again
- REQUIRE(U.size() == 2);
- }
+ // Here, `e_b` shouldn't be added again
+ REQUIRE(U.size() == 2);
// --- ex({⊥, b}) ---
// 3. Expanding from ex({⊥, a, b}) brings in both `CommWait` events since they
// --- ex({⊥, a, b}) ---
const auto incremental_exC_wait_actor_1 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_1);
- { // Assert that events `c` has been added
- UnfoldingEvent e_wait_1(EventSet({e_a, e_b}), comm_wait_1);
- REQUIRE(incremental_exC_wait_actor_1.size() == 1);
- REQUIRE(incremental_exC_wait_actor_1.contains_equivalent_to(&e_wait_1));
- REQUIRE(U.size() == 3);
- }
+ // Assert that events `c` has been added
+ UnfoldingEvent e_wait_1(EventSet({e_a, e_b}), comm_wait_1);
+ REQUIRE(incremental_exC_wait_actor_1.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_1.contains_equivalent_to(&e_wait_1));
+ REQUIRE(U.size() == 3);
const auto incremental_exC_wait_actor_2 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_2);
- { // Assert that events `d` has been added
- UnfoldingEvent e_wait_2(EventSet({e_a, e_b}), comm_wait_2);
- REQUIRE(incremental_exC_wait_actor_2.size() == 1);
- REQUIRE(incremental_exC_wait_actor_2.contains_equivalent_to(&e_wait_2));
- REQUIRE(U.size() == 4);
- }
+ // Assert that events `d` has been added
+ UnfoldingEvent e_wait_2(EventSet({e_a, e_b}), comm_wait_2);
+ REQUIRE(incremental_exC_wait_actor_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_2.contains_equivalent_to(&e_wait_2));
+ REQUIRE(U.size() == 4);
// --- ex({⊥, a, b}) ---
// 4. Expanding from either wait action should simply yield the other event
// --- ex({⊥, a, b, d}) ---
const auto incremental_exC_wait_actor_1_2 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_d}), &U, comm_wait_1);
- { // Assert that no event has been added and that
- // `e_c` is contained in the extension set
- REQUIRE(incremental_exC_wait_actor_1_2.size() == 1);
- REQUIRE(incremental_exC_wait_actor_1_2.contains(e_c));
- REQUIRE(U.size() == 4);
- }
+ // Assert that no event has been added and that
+ // `e_c` is contained in the extension set
+ REQUIRE(incremental_exC_wait_actor_1_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_1_2.contains(e_c));
+ REQUIRE(U.size() == 4);
// --- ex({⊥, a, b, d}) ---
// --- ex({⊥, a, b, c}) ---
const auto incremental_exC_wait_actor_2_2 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_c}), &U, comm_wait_2);
- { // Assert that no event has been added and that
- // `e_d` is contained in the extension set
- REQUIRE(incremental_exC_wait_actor_2_2.size() == 1);
- REQUIRE(incremental_exC_wait_actor_2_2.contains(e_d));
- REQUIRE(U.size() == 4);
- }
+ // Assert that no event has been added and that
+ // `e_d` is contained in the extension set
+ REQUIRE(incremental_exC_wait_actor_2_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_2_2.contains(e_d));
+ REQUIRE(U.size() == 4);
// --- ex({⊥, a, b, c}) ---
-}
\ No newline at end of file
+}
bool UnfoldingEvent::related_to(const UnfoldingEvent* other) const
{
- return this->in_history_of(other) or other->in_history_of(this);
+ return this->in_history_of(other) || other->in_history_of(this);
}
bool UnfoldingEvent::in_history_of(const UnfoldingEvent* other) const
[&](const UnfoldingEvent* e) { return e->is_dependent_with(other); });
const bool conflicts_with_other = std::any_of(unique_to_other.begin(), unique_to_other.end(),
[&](const UnfoldingEvent* e) { return e->is_dependent_with(this); });
- return conflicts_with_me or conflicts_with_other;
+ return conflicts_with_me || conflicts_with_other;
}
bool UnfoldingEvent::conflicts_with_any(const EventSet& events) const
auto combined_events = History(EventSet{this, other}).get_all_events();
// See the definition of immediate conflicts in the original paper on UDPOR
- {
- combined_events.remove(this);
- if (not combined_events.is_valid_configuration()) {
- return false;
- }
- combined_events.insert(this);
- }
+ combined_events.remove(this);
+ if (not combined_events.is_valid_configuration())
+ return false;
+ combined_events.insert(this);
- {
- combined_events.remove(other);
- if (not combined_events.is_valid_configuration()) {
- return false;
- }
- combined_events.insert(other);
- }
+ combined_events.remove(other);
+ if (not combined_events.is_valid_configuration())
+ return false;
+ combined_events.insert(other);
return true;
}
namespace simgrid::mc::udpor {
-maximal_subsets_iterator::maximal_subsets_iterator(const EventSet& events, std::optional<node_filter_function> filter,
+maximal_subsets_iterator::maximal_subsets_iterator(const EventSet& events,
+ const std::optional<node_filter_function>& filter,
std::optional<size_t> maximum_subset_size)
: maximum_subset_size(maximum_subset_size), current_maximal_set({EventSet()})
{
- const auto candidate_ordering = events.get_topological_ordering_of_reverse_graph();
+ auto candidate_ordering = events.get_topological_ordering_of_reverse_graph();
if (filter.has_value()) {
// Only store the events in the ordering that "matter" to us
std::copy_if(std::move_iterator(candidate_ordering.begin()), std::move_iterator(candidate_ordering.end()),
}
const auto next_event_ref = [&]() {
- if (!has_started_searching) {
+ if (not has_started_searching) {
has_started_searching = true;
return bookkeeper.find_next_candidate_event(topological_ordering.begin(), topological_ordering.end());
} else {
maximal_subsets_iterator() = default;
explicit maximal_subsets_iterator(const Configuration& config,
- std::optional<node_filter_function> filter = std::nullopt,
- std::optional<size_t> maximum_subset_size = std::nullopt)
+ const std::optional<node_filter_function>& filter = std::nullopt,
+ std::optional<size_t> maximum_subset_size = std::nullopt)
: maximal_subsets_iterator(config.get_events(), filter, maximum_subset_size)
{
}
- explicit maximal_subsets_iterator(const EventSet& events, std::optional<node_filter_function> filter = std::nullopt,
- std::optional<size_t> maximum_subset_size = std::nullopt);
+ explicit maximal_subsets_iterator(const EventSet& events,
+ const std::optional<node_filter_function>& filter = std::nullopt,
+ std::optional<size_t> maximum_subset_size = std::nullopt);
private:
std::vector<const UnfoldingEvent*> topological_ordering;
bool equal(const maximal_subsets_iterator& other) const { return current_maximal_set == other.current_maximal_set; }
const EventSet& dereference() const
{
- static const EventSet empty_set = EventSet();
+ static const EventSet empty_set;
if (current_maximal_set.has_value()) {
return current_maximal_set.value();
}
"model-check/strategy",
"Specify the the kind of heuristic to use for guided model-checking",
"none",
- {{"none", "No specific strategy: simply pick the first available transistion and act as a DFS."},
+ {{"none", "No specific strategy: simply pick the first available transition and act as a DFS."},
{"max_match_comm", "Try to minimize the number of in-fly communication by appairing matching send and receive."},
- {"min_match_comm", "Try to maximize the number of in-fly communication by not appairing matching send and receive."},
- {"uniform", "No specific strategy: choices are made randomly based on a uniform sampling."}
- }};
+ {"min_match_comm",
+ "Try to maximize the number of in-fly communication by not appairing matching send and receive."},
+ {"uniform", "No specific strategy: choices are made randomly based on a uniform sampling."}}};
simgrid::config::Flag<int> _sg_mc_random_seed{"model-check/rand-seed",
"give a specific random seed to initialize the uniform distribution", 0,
Transition* get_current_transition() const { return transitions_.at(times_considered_); }
bool result() const
{
- for (Transition* transition : transitions_) {
- CommTestTransition* tested_transition = static_cast<CommTestTransition*>(transition);
- if (tested_transition->get_sender() != -1 and tested_transition->get_receiver() != -1)
- return true;
- }
- return false;
+ return std::any_of(begin(transitions_), end(transitions_), [](const Transition* transition) {
+ const auto* tested_transition = static_cast<const CommTestTransition*>(transition);
+ return (tested_transition->get_sender() != -1 && tested_transition->get_receiver() != -1);
+ });
}
};
simgrid::kernel::actor::simcall_answered([this] {
double now = simgrid::s4u::Engine::get_clock();
double time_delta_real = now - last_updated_;
- if (time_delta_real <= 0 or not is_active())
+ if (time_delta_real <= 0 || not is_active())
return;
double time_delta_until_event = next_event_ - last_updated_;
bool event = next_event_ != -1 and time_delta_until_event <= time_delta_real;
if (now <= last_updated_)
return;
double power_w = conversion_efficiency_ * area_m2_ * solar_irradiance_w_per_m2_;
- if (min_power_w_ > 0 and power_w_ < min_power_w_)
+ if (min_power_w_ > 0 && power_w_ < min_power_w_)
power_w = 0;
- if (max_power_w_ > 0 and power_w_ > max_power_w_)
+ if (max_power_w_ > 0 && power_w_ > max_power_w_)
power_w = max_power_w_;
power_w_ = power_w;
if (eval_cost_) {
{
ensure_plugin_inited();
return host->extension<Photovoltaic>()->get_power();
-}
\ No newline at end of file
+}
xbt_assert(src_buff_ == nullptr && dst_buff_ == nullptr,
"Direct host-to-host communications cannot carry any data.");
XBT_DEBUG("host-to-host Comm. Pimpl already created and set, just start it.");
- on_start(*this);
- on_this_start(*this);
+ fire_on_start();
+ fire_on_this_start();
kernel::actor::simcall_answered([this] {
pimpl_->set_state(kernel::activity::State::READY);
boost::static_pointer_cast<kernel::activity::CommImpl>(pimpl_)->start();
pimpl_->set_actor(sender_);
// Only throw the signal when both sides are here and the status is READY
if (pimpl_->get_state() != kernel::activity::State::WAITING) {
- on_start(*this);
- on_this_start(*this);
+ fire_on_start();
+ fire_on_this_start();
}
}
pimpl_->suspend();
state_ = State::STARTED;
- on_start(*this);
- on_this_start(*this);
+ fire_on_start();
+ fire_on_this_start();
return this;
}
pimpl_->suspend();
state_ = State::STARTED;
- on_start(*this);
- on_this_start(*this);
+ fire_on_start();
+ fire_on_this_start();
return this;
}
void Task::receive(Task* source)
{
XBT_DEBUG("Task %s received a token from %s", name_.c_str(), source->name_.c_str());
- auto source_count = predecessors_[source]++;
+ auto source_count = predecessors_[source];
+ predecessors_[source]++;
if (tokens_received_.size() <= queued_firings_ + source_count)
- tokens_received_.push_back({});
+ tokens_received_.emplace_back();
tokens_received_[queued_firings_ + source_count][source] = source->token_;
bool enough_tokens = true;
for (auto const& [key, val] : predecessors_)
on_start(this);
working_ = true;
queued_firings_ = std::max(queued_firings_ - 1, 0);
- if (tokens_received_.size() > 0)
+ if (not tokens_received_.empty())
tokens_received_.pop_front();
}
template <typename Iterator> void powerset_iterator<Iterator>::increment()
{
- if (!current_subset_iter.has_value() || !current_subset_iter_end.has_value() || !current_subset_iter.has_value() ||
- !iterator_end.has_value()) {
+ if (not current_subset_iter.has_value() || not current_subset_iter_end.has_value() ||
+ not current_subset_iter.has_value() || not iterator_end.has_value()) {
return; // We've traversed all subsets at this point, or we're the "last" iterator
}
template <typename Iterator> bool subsets_iterator<Iterator>::equal(const subsets_iterator<Iterator>& other) const
{
- if (this->end == std::nullopt and other.end == std::nullopt) {
+ if (this->end == std::nullopt && other.end == std::nullopt) {
return true;
}
if (this->k != other.k) {
if (this->k == 0) { // this->k == other.k == 0
return true;
}
- return this->end != std::nullopt and other.end != std::nullopt and this->P[0] == other.P[0];
+ return this->end != std::nullopt && other.end != std::nullopt && this->P[0] == other.P[0];
}
template <typename Iterator> const std::vector<Iterator>& subsets_iterator<Iterator>::dereference() const
++current_subset[k - 1];
++P[k - 1];
- const auto end = this->end.value();
- const bool shift_other_elements = current_subset[k - 1] == end;
+ const bool shift_other_elements = current_subset[k - 1] == end.value();
if (shift_other_elements) {
if (k == 1) {
// We're done in the case that k = 1; here, we've iterated
// through the list once, which is all that is needed
- this->end = std::nullopt;
+ end = std::nullopt;
return;
}
// element can be located. Thus, if `P[0] > (n - k)`, this means
// we've sucessfully iterated through all subsets so we're done
if (P[0] > (n - k)) {
- this->end = std::nullopt;
+ end = std::nullopt;
return;
}
SECTION("Each element of each subset is distinct and appears half of the time in all subsets iteration")
{
// Each element is expected to be found in half of the sets
- const unsigned k = static_cast<unsigned>(example_vec.size());
+ const auto k = static_cast<unsigned>(example_vec.size());
const int expected_count = integer_power(2, k - 1);
std::unordered_map<int, int> element_counts(k);
const auto has_effect =
std::none_of(collections.begin(), collections.end(), [](const auto& c) { return c.get().empty(); });
- if (has_effect and (not collections.empty())) {
+ if (has_effect && (not collections.empty())) {
std::transform(collections.begin(), collections.end(), std::back_inserter(current_subset),
[](const auto& c) { return c.get().cbegin(); });
underlying_collections = std::move(collections);
{
// Termination occurs when `current_subset := the empty set`
// or if we have nothing to iterate over
- if (current_subset.empty() or underlying_collections.empty()) {
+ if (current_subset.empty() || underlying_collections.empty()) {
return;
}
(name, path, binary, filename) = sys.argv
for test in mbi.parse_one_code(filename):
- execcmd = test['cmd'].replace("mpirun", f"{path}/smpi_script/bin/smpirun -wrapper '{path}/bin/simgrid-mc --log=mc_safety.t:info' -platform ./cluster.xml -analyze --cfg=smpi/barrier-finalization:on --cfg=smpi/list-leaks:10 --cfg=model-check/max-depth:10000")
+ execcmd = test['cmd'].replace("mpirun", f"{path}/smpi_script/bin/smpirun -wrapper '{path}/bin/simgrid-mc --cfg=model-check/reduction:odpor --log=mc_safety.t:info' -platform ./cluster.xml -analyze --cfg=smpi/barrier-finalization:on --cfg=smpi/list-leaks:10 --cfg=model-check/max-depth:10000")
execcmd = execcmd.replace('${EXE}', binary)
execcmd = execcmd.replace('$zero_buffer', "--cfg=smpi/buffering:zero")
execcmd = execcmd.replace('$infty_buffer', "--cfg=smpi/buffering:infty")
