name: Configure, build and test da stuff
command: |
mkdir _build && cd _build
- cmake -Denable_documentation=OFF -Denable_coverage=ON -Denable_model-checking=OFF -Denable_compile_optimizations=OFF -Denable_smpi=ON -Denable_smpi_MPICH3_testsuite=OFF -Denable_compile_warnings=ON ..
+ cmake -Denable_documentation=OFF -Denable_coverage=OFF -Denable_model-checking=OFF -Denable_compile_optimizations=OFF -Denable_smpi=ON -Denable_smpi_MPICH3_testsuite=OFF -Denable_compile_warnings=ON ..
make -j4 tests && ctest -j4 --output-on-failure
add_custom_target(tests COMMENT "Recompiling the tests")
add_custom_target(tests-mc COMMENT "Recompiling the MC tests and tools.")
add_dependencies(tests tests-mc)
+add_custom_target(tests-ns3 COMMENT "Recompiling the ns3 tests and tools.")
+add_dependencies(tests tests-ns3)
### Build some Maintainer files
include(${CMAKE_HOME_DIRECTORY}/tools/cmake/MaintainerMode.cmake)
- Full simDAG integration: Activity::start() actually starts only when all dependencies
are fullfiled. If it cannot be started right away, it will start as soon as it becomes
possible.
+ - Allow to set a concurrency limit on disks and hosts, as it was already the case for links.
Kernel:
- optimize an internal datastructure (use a set instead of a list for ongoing activities),
- Synchronize the MBI tests with upstream.
- Show the full actor bactraces when replaying a MC trace (with model-check/replay)
and the status of all actors on deadlocks in MC mode.
+ - The safety/stateless aspects of the MC are now enabled by default in all simgrid builds.
+ Liveness and stateful aspects are still controled by the enabling_model-checking
+ configuration option.
+ - Stateless model-checking is now usable on any system, including Mac OSX and ARM processors.
XBT:
- simgrid::xbt::cmdline and simgrid::xbt::binary_name are gone.
include src/mc/explo/udpor/EventSet.cpp
include src/mc/explo/udpor/EventSet.hpp
include src/mc/explo/udpor/EventSet_test.cpp
+include src/mc/explo/udpor/ExtensionSetCalculator.cpp
+include src/mc/explo/udpor/ExtensionSetCalculator.hpp
include src/mc/explo/udpor/History.cpp
include src/mc/explo/udpor/History.hpp
include src/mc/explo/udpor/History_test.cpp
set(tesh_files ${tesh_files} ${CMAKE_HOME_DIRECTORY}/examples/cpp/network-ns3/s4u-network-ns3-timed.tesh)
endif()
+foreach (example network-ns3 network-ns3-wifi)
+ add_dependencies(tests-ns3 s4u-${example})
+endforeach()
+
else()
# Even if ns3 is not found, we need to override the teshfile name and make sure that everything gets included in the archive
set(_network-ns3_teshfile ${CMAKE_HOME_DIRECTORY}/examples/cpp/network-ns3/s4u-network-ns3-notime.tesh)
XBT_LOG_NEW_DEFAULT_CATEGORY(dag_scheduling, "Logging specific to this example");
namespace sg4 = simgrid::s4u;
-struct HostAttribute {
- /* Earliest time at which a host is ready to execute a task */
- double available_at = 0.0;
- sg4::Exec* last_scheduled_task = nullptr;
-};
-
-static double sg_host_get_available_at(const sg4::Host* host)
-{
- return host->get_data<HostAttribute>()->available_at;
-}
-
-static void sg_host_set_available_at(const sg4::Host* host, double time)
-{
- host->get_data<HostAttribute>()->available_at = time;
-}
-
-static sg4::Exec* sg_host_get_last_scheduled_task(const sg4::Host* host)
-{
- return host->get_data<HostAttribute>()->last_scheduled_task;
-}
-
-static void sg_host_set_last_scheduled_task(const sg4::Host* host, sg4::ExecPtr task)
-{
- host->get_data<HostAttribute>()->last_scheduled_task = task.get();
-}
-
-static bool dependency_exists(const sg4::Exec* src, sg4::Exec* dst)
-{
- const auto& dependencies = src->get_dependencies();
- const auto& successors = src->get_successors();
- return (std::find(successors.begin(), successors.end(), dst) != successors.end() ||
- dependencies.find(dst) != dependencies.end());
-}
-
static std::vector<sg4::Exec*> get_ready_tasks(const std::vector<sg4::ActivityPtr>& dax)
{
std::vector<sg4::Exec*> ready_tasks;
if (comm->get_remaining() <= 1e-6) {
redist_time = 0;
} else {
- redist_time =
- sg_host_get_route_latency(source, host) + comm->get_remaining() / sg_host_get_route_bandwidth(source, host);
+ double bandwidth = std::numeric_limits<double>::max();
+ auto [links, latency] = source->route_to(host);
+ for (auto const& link : links)
+ bandwidth = std::min(bandwidth, link->get_bandwidth());
+
+ redist_time = latency + comm->get_remaining() / bandwidth;
}
// We use the user data field to store the finish time of the predecessor of the comm, i.e., its potential start
// time
if (last_data_available < data_available)
last_data_available = data_available;
}
-
- return std::max(sg_host_get_available_at(host), last_data_available) + task->get_remaining() / host->get_speed();
+ return std::max(*host->get_data<double>(), last_data_available) + task->get_remaining() / host->get_speed();
}
static sg4::Host* get_best_host(const sg4::ExecPtr exec)
{
- std::vector<sg4::Host*> hosts = sg4::Engine::get_instance()->get_all_hosts();
- auto best_host = hosts.front();
- double min_EFT = finish_on_at(exec, best_host);
+ sg4::Host* best_host = nullptr;
+ double min_EFT = std::numeric_limits<double>::max();
- for (const auto& h : hosts) {
- double EFT = finish_on_at(exec, h);
- XBT_DEBUG("%s finishes on %s at %f", exec->get_cname(), h->get_cname(), EFT);
+ for (const auto& host : sg4::Engine::get_instance()->get_all_hosts()) {
+ double EFT = finish_on_at(exec, host);
+ XBT_DEBUG("%s finishes on %s at %f", exec->get_cname(), host->get_cname(), EFT);
if (EFT < min_EFT) {
min_EFT = EFT;
- best_host = h;
+ best_host = host;
}
}
return best_host;
}
-static void schedule_on(sg4::ExecPtr exec, sg4::Host* host)
+static void schedule_on(sg4::ExecPtr exec, sg4::Host* host, double busy_until = 0.0)
{
exec->set_host(host);
+ // We use the user data field to store up to when the host is busy
+ delete host->get_data<double>(); // In case we're erasing a previous value
+ host->set_data(new double(busy_until));
// we can also set the destination of all the input comms of this exec
for (const auto& pred : exec->get_dependencies()) {
auto* comm = dynamic_cast<sg4::Comm*>(pred.get());
e.load_platform(argv[1]);
- /* Allocating the host attribute */
- unsigned long total_nhosts = e.get_host_count();
- const auto hosts = e.get_all_hosts();
- std::vector<HostAttribute> host_attributes(total_nhosts);
- for (unsigned long i = 0; i < total_nhosts; i++)
- hosts[i]->set_data(&host_attributes[i]);
-
+ /* Mark all hosts as sequential, as it ought to be in such a scheduling example.
+ *
+ * It means that the hosts can only compute one thing at a given time. If an execution already takes place on a given
+ * host, any subsequently started execution will be queued until after the first execution terminates */
+ for (auto const& host : e.get_all_hosts()) {
+ host->set_concurrency_limit(1);
+ host->set_data(new double(0.0));
+ }
/* load the DAX file */
auto dax = sg4::create_DAG_from_DAX(argv[2]);
}
XBT_INFO("Schedule %s on %s", selected_task->get_cname(), selected_host->get_cname());
- schedule_on(selected_task, selected_host);
-
- /*
- * tasks can be executed concurrently when they can by default.
- * Yet schedulers take decisions assuming that tasks wait for resource availability to start.
- * The solution (well crude hack is to keep track of the last task scheduled on a host and add a special type of
- * dependency if needed to force the sequential execution meant by the scheduler.
- * If the last scheduled task is already done, has failed or is a predecessor of the current task, no need for a
- * new dependency
- */
-
- if (auto last_scheduled_task = sg_host_get_last_scheduled_task(selected_host);
- last_scheduled_task && (last_scheduled_task->get_state() != sg4::Activity::State::FINISHED) &&
- (last_scheduled_task->get_state() != sg4::Activity::State::FAILED) &&
- not dependency_exists(sg_host_get_last_scheduled_task(selected_host), selected_task))
- last_scheduled_task->add_successor(selected_task);
-
- sg_host_set_last_scheduled_task(selected_host, selected_task);
- sg_host_set_available_at(selected_host, min_finish_time);
+ schedule_on(selected_task, selected_host, min_finish_time);
ready_tasks.clear();
e.run();
}
+ /* Cleanup memory */
+ for (auto const& h : e.get_all_hosts())
+ delete h->get_data<double>();
+
XBT_INFO("Simulation Time: %f", simgrid_get_clock());
return 0;
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 4).
-> [Checker] Execution came to an end at 1;1;0 (state: 3, depth: 3)
-> [Checker] Backtracking from 1;1;0
+> [Checker] Execution came to an end at 1;1 (state: 3, depth: 3)
+> [Checker] Backtracking from 1;1
> [Checker] DFS exploration ended. 3 unique states visited; 0 backtracks (3 transition replays, 0 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 2 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 6).
-> [Checker] Execution came to an end at 1;2;1;2;0 (state: 5, depth: 5)
-> [Checker] Backtracking from 1;2;1;2;0
+> [Checker] Execution came to an end at 1;2;1;2 (state: 5, depth: 5)
+> [Checker] Backtracking from 1;2;1;2
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 6, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
> [Checker] BARRIER_WAIT(barrier: 0) (state=8)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 6).
-> [Checker] Execution came to an end at 2;1;1;2;0 (state: 9, depth: 5)
-> [Checker] Backtracking from 2;1;1;2;0
+> [Checker] Execution came to an end at 2;1;1;2 (state: 9, depth: 5)
+> [Checker] Backtracking from 2;1;1;2
> [Checker] DFS exploration ended. 9 unique states visited; 1 backtracks (10 transition replays, 0 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] BARRIER_WAIT(barrier: 0) (state=6)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 1;2;3;1;2;3;0 (state: 7, depth: 7)
-> [Checker] Backtracking from 1;2;3;1;2;3;0
+> [Checker] Execution came to an end at 1;2;3;1;2;3 (state: 7, depth: 7)
+> [Checker] Backtracking from 1;2;3;1;2;3
> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 1;3;2;1;2;3;0 (state: 12, depth: 7)
-> [Checker] Backtracking from 1;3;2;1;2;3;0
+> [Checker] Execution came to an end at 1;3;2;1;2;3 (state: 12, depth: 7)
+> [Checker] Backtracking from 1;3;2;1;2;3
> [Checker] DFS exploration ended. 12 unique states visited; 1 backtracks (14 transition replays, 1 states visited overall)
\ No newline at end of file
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 1;1;1;2;2;2;0 (state: 7, depth: 7)
-> [Checker] Backtracking from 1;1;1;2;2;2;0
+> [Checker] Execution came to an end at 1;1;1;2;2;2 (state: 7, depth: 7)
+> [Checker] Backtracking from 1;1;1;2;2;2
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 8, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=10)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=12)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 13, depth: 7)
-> [Checker] Backtracking from 2;1;2;2;1;1;0
+> [Checker] Execution came to an end at 2;1;2;2;1;1 (state: 13, depth: 7)
+> [Checker] Backtracking from 2;1;2;2;1;1
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=14)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 17, depth: 7)
-> [Checker] Backtracking from 1;1;2;1;2;2;0
+> [Checker] Execution came to an end at 1;1;2;1;2;2 (state: 17, depth: 7)
+> [Checker] Backtracking from 1;1;2;1;2;2
> [Checker] DFS exploration ended. 17 unique states visited; 2 backtracks (21 transition replays, 2 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
> [0.000000] [mc_global/INFO] Counter-example execution trace:
> [0.000000] [mc_global/INFO] 1: iSend(mbox=2)
> [0.000000] [mc_global/INFO] 2: iSend(mbox=0)
-> [0.000000] [mc_global/INFO] 0:
-> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2;0'
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 3 unique states visited; 0 backtracks (3 transition replays, 0 states visited overall)
> Execution failed with code 3.
> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
> [0.000000] [mc_global/INFO] 3: MUTEX_WAIT(mutex: 1, owner: 3)
> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
-> [0.000000] [mc_global/INFO] 0:
-> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3;0'
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 1 backtracks (22 transition replays, 2 states visited overall)
\ No newline at end of file
Disk* set_state_profile(kernel::profile::Profile* profile);
Disk* set_read_bandwidth_profile(kernel::profile::Profile* profile);
Disk* set_write_bandwidth_profile(kernel::profile::Profile* profile);
+ /**
+ * @brief Set the max amount of operations (either read or write) that can take place on this disk at the same time
+ *
+ * Use -1 to set no limit.
+ */
+ Disk* set_concurrency_limit(int limit);
+ int get_concurrency_limit() const;
IoPtr io_init(sg_size_t size, s4u::Io::OpType type) const;
Host* set_state_profile(kernel::profile::Profile* p);
Host* set_speed_profile(kernel::profile::Profile* p);
+ /**
+ * @brief Set the max amount of executions that can take place on this host at the same time
+ *
+ * Use -1 to set no limit.
+ */
+ Host* set_concurrency_limit(int limit);
+ int get_concurrency_limit() const;
+
/** @brief Convert the CPU's speed from string to double */
static std::vector<double> convert_pstate_speed_vector(const std::vector<std::string>& speed_per_state);
/**
void route_to(const Host* dest, std::vector<Link*>& links, double* latency) const;
void route_to(const Host* dest, std::vector<kernel::resource::StandardLinkImpl*>& links, double* latency) const;
+ std::pair<std::vector<Link*>, double> route_to(const Host* dest) const;
/**
* @brief Seal this host
/* A constructor accepting a map of valid values -> their description,
* and producing an informative error message when an invalid value is passed, or when help is passed as a value.
*/
+ Flag(const char* name, const char* desc, xbt::type_identity_t<T> value,
+ const std::map<std::string, std::string, std::less<>>& valid_values)
+ : value_(value), name_(name)
+ {
+ simgrid::config::bind_flag(value_, name, desc, valid_values, [](std::string) {});
+ }
+
+ /* As earlier, a constructor accepting a map of valid values -> their description,
+ * and producing an informative error message when an invalid value is passed, or when help is passed as a value.
+ * But also take a callback that is invoked before the verification of parameter name validity.
+ */
template <class F>
Flag(const char* name, const char* desc, xbt::type_identity_t<T> value,
const std::map<std::string, std::string, std::less<>>& valid_values, F callback)
install_signal_handlers();
- /* register a function to be called after the environment creation */
- s4u::Engine::on_platform_created_cb([this]() { this->presolve(); });
-
if (cfg_dbg_clean_atexit)
atexit(shutdown);
}
sg_platf_parser_finalize();
simgrid_parse_open(file);
- simgrid_parse();
+ simgrid_parse(false);
simgrid_parse_close();
}
}
}
-void EngineImpl::presolve() const
-{
- XBT_DEBUG("Consume all trace events occurring before the starting time.");
- double next_event_date;
- while ((next_event_date = profile::future_evt_set.next_date()) != -1.0) {
- if (next_event_date > now_)
- break;
-
- double value = -1.0;
- resource::Resource* resource = nullptr;
- while (auto* event = profile::future_evt_set.pop_leq(next_event_date, &value, &resource)) {
- if (value >= 0)
- resource->apply_event(event, value);
- }
- }
-
- XBT_DEBUG("Set every models in the right state by updating them to 0.");
- for (auto const& model : models_)
- model->update_actions_state(now_, 0.0);
-}
-
double EngineImpl::solve(double max_date) const
{
double time_delta = -1.0; /* duration */
void display_all_actor_status() const;
void run_all_actors();
- /* @brief Finish simulation initialization
- * This function must be called before the first call to solve()
- */
- void presolve() const;
/** @brief Performs a part of the simulation
* @param max_date Maximum date to update the simulation to, or -1
* @return the elapsed time, or -1.0 if no event could be executed
/* setup the profile file with latency events (peak latency changes due to external load).
* Profile must contain absolute values */
virtual void set_latency_profile(kernel::profile::Profile* profile) = 0;
- /** @brief Set the concurrency limit for this link */
- virtual void set_concurrency_limit(int limit) const = 0;
- /** @brief Get the concurrency limit of this link */
- virtual int get_concurrency_limit() const = 0;
};
} // namespace simgrid::kernel::resource
lmm::Constraint* get_constraint() const { return constraint_; }
+ /** @brief Set the concurrency limit for this resource */
+ virtual void set_concurrency_limit(int limit) const
+ {
+ if (limit != -1)
+ get_constraint()->reset_concurrency_maximum();
+ get_constraint()->set_concurrency_limit(limit);
+ }
+
+ /** @brief Get the concurrency limit of this resource */
+ virtual int get_concurrency_limit() const { return get_constraint()->get_concurrency_limit(); }
+
/** @brief returns the current load due to activities (in flops per second, byte per second or similar)
*
* The load due to external usages modeled by profile files is ignored.*/
}
}
-void StandardLinkImpl::set_concurrency_limit(int limit) const
-{
- if (limit != -1) {
- get_constraint()->reset_concurrency_maximum();
- }
- get_constraint()->set_concurrency_limit(limit);
-}
-int StandardLinkImpl::get_concurrency_limit() const
-{
- return get_constraint()->get_concurrency_limit();
-}
-
} // namespace simgrid::kernel::resource
/* setup the profile file with latency events (peak latency changes due to external load).
* Profile must contain absolute values */
void set_latency_profile(kernel::profile::Profile* profile) override;
-
- void set_concurrency_limit(int limit) const override;
- int get_concurrency_limit() const override;
};
} // namespace simgrid::kernel::resource
namespace simgrid {
namespace kernel::resource {
-static bool ns3_is_initialized = false;
NetworkNS3Model::NetworkNS3Model(const std::string& name) : NetworkModel(name)
{
s4u::Engine::on_platform_created_cb([]() {
/* Create the ns3 topology based on routing strategy */
- ns3::GlobalRouteManager::DeleteGlobalRoutes(); // just in case this callback is called twice
ns3::GlobalRouteManager::BuildGlobalRoutingDatabase();
ns3::GlobalRouteManager::InitializeRoutes();
- ns3_is_initialized = true;
});
routing::on_cluster_creation.connect(&clusterCreation_cb);
routing::NetZoneImpl::on_route_creation.connect(&routeCreation_cb);
#if SIMGRID_HAVE_NS3_GetNextEventTime
/* If the ns-3 model is idempotent, it won't get updated in next_occurring_event() */
- if (not ns3_is_initialized) {
- XBT_DEBUG("PRESOLVE, I SEE YOU. Don't run ns3 until after all initializations are done.");
- return;
- }
-
if (delta >= 0) {
XBT_DEBUG("DO START simulator delta: %f (current simgrid time: %f; current ns3 time: %f)", delta,
simgrid::kernel::EngineImpl::get_clock(), ns3::Simulator::Now().GetSeconds());
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/kernel/resource/profile/FutureEvtSet.hpp"
+#include "src/kernel/resource/Resource.hpp"
#include "src/kernel/resource/profile/Event.hpp"
#include "src/kernel/resource/profile/Profile.hpp"
+#include <simgrid/s4u/Engine.hpp>
namespace simgrid::kernel::profile {
/** @brief Schedules an event to a future date */
void FutureEvtSet::add_event(double date, Event* evt)
{
+ if (heap_.empty())
+ s4u::Engine::on_platform_created_cb([this]() {
+ /* Handle the events of time = 0 right after the platform creation */
+ double next_event_date;
+ while ((next_event_date = this->next_date()) != -1.0) {
+ if (next_event_date > 0)
+ break;
+
+ double value = -1.0;
+ resource::Resource* resource = nullptr;
+ while (auto* event = this->pop_leq(next_event_date, &value, &resource)) {
+ if (value >= 0)
+ resource->apply_event(event, value);
+ }
+ }
+ });
+
heap_.emplace(date, evt);
}
XBT_PUBLIC double simgrid_parse_get_double(const std::string& s);
XBT_PUBLIC int simgrid_parse_get_int(const std::string& s);
-XBT_PUBLIC void simgrid_parse(); /* Entry-point to the parser */
+XBT_PUBLIC void simgrid_parse(bool fire_on_platform_created_callback); /* Entry-point to the parser */
XBT_PUBLIC void parse_platform_file(const std::string& file);
#endif
std::string simgrid_parsed_filename; // Currently parsed file (for the error messages)
static std::vector<simgrid::s4u::LinkInRoute> parsed_link_list; /* temporary store of current link list of a route */
+static bool fire_on_platform_created_callback;
+
/* Helping functions */
void simgrid_parse_assert(bool cond, const std::string& msg)
{
}
void ETag_simgrid_parse_platform()
{
- simgrid::s4u::Engine::on_platform_created();
+ if (fire_on_platform_created_callback)
+ simgrid::s4u::Engine::on_platform_created();
}
void STag_simgrid_parse_prop()
}
/* Call the lexer to parse the currently opened file */
-void simgrid_parse()
+void simgrid_parse(bool fire_on_platform_created_callback_param)
{
+ fire_on_platform_created_callback = fire_on_platform_created_callback_param;
bool err = simgrid_parse_lex();
simgrid_parse_assert(not err, "Flex returned an error code");
simgrid_parse_open(file);
/* Do the actual parsing */
- simgrid_parse();
+ simgrid_parse(true);
simgrid_parse_close();
}
return this->pending_transitions_[times_considered].get();
}
- inline void set_transition(std::unique_ptr<Transition> t, unsigned times_considered)
+ inline void set_transition(std::shared_ptr<Transition> t, unsigned times_considered)
{
xbt_assert(times_considered < this->pending_transitions_.size(),
"Actor %ld does not have a state available transition with `times_considered = %u`, "
checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(app_args_, need_memory_introspection);
initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, *checker_side_->get_remote_memory());
#else
- xbt_die("SimGrid was compiled without MC support.");
+ xbt_die("SimGrid MC was compiled without memory introspection support.");
#endif
} else {
master_socket_ = socket(AF_UNIX,
#ifdef __APPLE__
- SOCK_STREAM, /* Mac OSX does not have AF_UNIX + SOCK_SEQPACKET, even if that's faster*/
+ SOCK_STREAM, /* Mac OSX does not have AF_UNIX + SOCK_SEQPACKET, even if that's faster */
#else
SOCK_SEQPACKET,
#endif
// <----- send ACTORS_STATUS_REPLY_COUNT
// <----- send `N` ACTORS_STATUS_REPLY_TRANSITION (s_mc_message_actors_status_one_t)
// <----- send `M` ACTORS_STATUS_REPLY_SIMCALL (s_mc_message_simcall_probe_one_t)
+ //
+ // Note that we also receive disabled transitions, because UDPOR needs it.
+
checker_side_->get_channel().send(MessageType::ACTORS_STATUS);
s_mc_message_actors_status_answer_t answer;
for (const auto& actor : status) {
std::vector<std::shared_ptr<Transition>> actor_transitions;
- int n_transitions = actor.enabled ? actor.max_considered : 0;
+ int n_transitions = actor.max_considered;
for (int times_considered = 0; times_considered < n_transitions; times_considered++) {
s_mc_message_simcall_probe_one_t probe;
ssize_t received = checker_side_->get_channel().receive(probe);
"--cfg=model-check/replay:'%s'",
explo->get_record_trace().to_string().c_str());
explo->log_state();
- throw DeadlockError();
+ throw McError(ExitStatus::DEADLOCK);
}
}
void restore_initial_state();
void wait_for_requests();
- /** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */
+ /** Ask to the application to check for a deadlock. If so, do an error message and throw a McError(DEADLOCK). */
void check_deadlock() const;
/** Ask the application to run post-mortem analysis, and maybe to stop ASAP */
XBT_VERB("Creating a guide for the state");
if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
- if (_sg_mc_strategy == "nb_wait")
+ else if (_sg_mc_strategy == "nb_wait")
strategy_ = std::make_shared<WaitStrategy>();
+ else
+ THROW_IMPOSSIBLE;
recipe_ = std::list<Transition*>();
{
if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
- if (_sg_mc_strategy == "nb_wait")
+ else if (_sg_mc_strategy == "nb_wait")
strategy_ = std::make_shared<WaitStrategy>();
+ else
+ THROW_IMPOSSIBLE;
*strategy_ = *(parent_state->strategy_);
recipe_ = std::list(parent_state_->get_recipe());
}
// This should be done in GuidedState, or at least interact with it
-void State::execute_next(aid_t next, RemoteApp& app)
+std::shared_ptr<Transition> State::execute_next(aid_t next, RemoteApp& app)
{
// First, warn the guide, so it knows how to build a proper child state
strategy_->execute_next(next, app);
// about a transition AFTER it has executed.
transition_ = just_executed;
- auto executed_transition = std::unique_ptr<Transition>(just_executed);
- actor_state.set_transition(std::move(executed_transition), times_considered);
-
+ const auto executed_transition = std::shared_ptr<Transition>(just_executed);
+ actor_state.set_transition(executed_transition, times_considered);
app.wait_for_requests();
+
+ return executed_transition;
}
} // namespace simgrid::mc
static long expended_states_; /* Count total amount of states, for stats */
/**
- * @brief An empty transition that leads to this state by default
- */
- const std::unique_ptr<Transition> default_transition_ = std::make_unique<Transition>();
-
- /**
- * @brief The outgoing transition: what was the last transition that
- * we took to leave this state?
+ * @brief The outgoing transition: what was the last transition that we took to leave this state?
*
- * The owner of the transition is the `ActorState` instance which exists in this state,
- * or a reference to the internal default transition `Transition()` if no transition has been
- * set
+ * The owner of the transition is the `ActorState` instance which exists in this state.
*/
- Transition* transition_ = default_transition_.get();
+ Transition* transition_ = nullptr;
/** @brief A list of transition to be replayed in order to get in this state. */
std::list<Transition*> recipe_;
internal cost of the transition is returned */
std::pair<aid_t, int> next_transition_guided() const;
- /* Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
- * next_transition() */
- void execute_next(aid_t next, RemoteApp& app);
+ /**
+ * @brief Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
+ * next_transition()
+ */
+ std::shared_ptr<Transition> execute_next(aid_t next, RemoteApp& app);
long get_num() const { return num_; }
std::size_t count_todo() const;
class BasicStrategy : public Strategy {
public:
BasicStrategy() = default;
- ~BasicStrategy() = default;
+ ~BasicStrategy() override = default;
BasicStrategy(const BasicStrategy&) = delete;
BasicStrategy& operator=(const BasicStrategy&)
{ /* nothing to copy over while cloning */
public:
WaitStrategy() = default;
- ~WaitStrategy() = default;
+ ~WaitStrategy() override = default;
WaitStrategy(const BasicStrategy&) = delete;
WaitStrategy& operator=(const WaitStrategy& guide)
{
XBT_INFO("*********************************************************");
XBT_INFO("%s", send_diff.c_str());
exploration_.log_state();
- exploration_.system_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
+ throw McError(ExitStatus::NON_DETERMINISM);
} else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) {
XBT_INFO("****************************************************");
XBT_INFO("***** Non-deterministic communications pattern *****");
if (not recv_diff.empty())
XBT_INFO("%s", recv_diff.c_str());
exploration_.log_state();
- exploration_.system_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
+ throw McError(ExitStatus::NON_DETERMINISM);
}
}
}
get_record_trace().to_string().c_str());
log_state();
- throw TerminationError();
+ throw McError(ExitStatus::NON_TERMINATION);
}
}
#endif
for (auto const& transition : stack_.back()->get_recipe()) {
trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str()));
}
- trace.push_back(xbt::string_printf("%ld: %s", stack_.back()->get_transition()->aid_,
- stack_.back()->get_transition()->to_string().c_str()));
+ if (const auto* trans = stack_.back()->get_transition(); trans != nullptr)
+ trace.push_back(xbt::string_printf("%ld: %s", trans->aid_, trans->to_string().c_str()));
return trace;
}
aid_t issuer_id = state->get_transition()->aid_;
stack_t tmp_stack = stack_;
while (not tmp_stack.empty()) {
- if (State* prev_state = tmp_stack.back().get();
+ if (const State* prev_state = tmp_stack.back().get();
state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
prev_state->get_transition()->to_string().c_str(), issuer_id);
XBT_INFO("Stack trace not shown because there is no memory introspection.");
}
- system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+ throw McError(ExitStatus::PROGRAM_CRASH);
}
XBT_ATTRIB_NORETURN void Exploration::report_assertion_failure()
{
"--cfg=model-check/replay:'%s'",
get_record_trace().to_string().c_str());
log_state();
- system_exit(SIMGRID_MC_EXIT_SAFETY);
-}
-
-void Exploration::system_exit(int status) const
-{
- ::exit(status);
+ throw McError(ExitStatus::SAFETY);
}
}; // namespace simgrid::mc
#include "simgrid/forward.h"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_record.hpp"
#include <xbt/Extendable.hpp>
/** Produce an error message indicating that a property was violated */
XBT_ATTRIB_NORETURN void report_assertion_failure();
- /** Kill the application and the model-checker (which exits with `status`)*/
- XBT_ATTRIB_NORETURN void system_exit(int status) const;
-
/* These methods are callbacks called by the model-checking engine
* to get and display information about the current state of the
* model-checking algorithm: */
{
std::vector<std::string> trace;
for (std::shared_ptr<Pair> const& pair : exploration_stack_)
- trace.push_back(pair->app_state_->get_transition()->to_string());
+ if (pair->app_state_->get_transition() != nullptr)
+ trace.push_back(pair->app_state_->get_transition()->to_string());
return trace;
}
reached_pair = this->insert_acceptance_pair(current_pair.get());
if (reached_pair == nullptr) {
this->show_acceptance_cycle(current_pair->depth);
- throw LivenessError();
+ throw McError(ExitStatus::LIVENESS);
}
}
#include "src/mc/explo/UdporChecker.hpp"
#include "src/mc/api/State.hpp"
#include "src/mc/explo/udpor/Comb.hpp"
+#include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
#include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+#include <numeric>
#include <xbt/asserts.h>
#include <xbt/log.h>
+#include <xbt/string.hpp>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
namespace simgrid::mc::udpor {
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true)
-{
- // Initialize the map
-}
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
void UdporChecker::run()
{
XBT_INFO("Starting a UDPOR exploration");
- // NOTE: `A`, `D`, and `C` are derived from the
- // original UDPOR paper [1], while `prev_exC` arises
- // from the incremental computation of ex(C) from [3]
- Configuration C_root;
-
- // TODO: Move computing the root configuration into a method on the Unfolding
- auto initial_state = get_current_state();
- auto root_event = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
- auto* root_event_handle = root_event.get();
- unfolding.insert(std::move(root_event));
- C_root.add_event(root_event_handle);
-
- explore(C_root, EventSet(), EventSet(), std::move(initial_state), EventSet());
-
+ state_stack.clear();
+ state_stack.push_back(get_current_state());
+ explore(Configuration(), EventSet(), EventSet(), EventSet());
XBT_INFO("UDPOR exploration terminated -- model checking completed");
}
-void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC,
- EventSet prev_exC)
+void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC)
{
- auto exC = compute_exC(C, *stateC, prev_exC);
+ auto& stateC = *state_stack.back();
+ auto exC = compute_exC(C, stateC, prev_exC);
const auto enC = compute_enC(C, exC);
+ XBT_DEBUG("explore(C, D, A) with:\n"
+ "C\t := %s \n"
+ "D\t := %s \n"
+ "A\t := %s \n"
+ "ex(C)\t := %s \n"
+ "en(C)\t := %s \n",
+ C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str(), exC.to_string().c_str(),
+ enC.to_string().c_str());
+ XBT_DEBUG("ex(C) has %zu elements, of which %zu are in en(C)", exC.size(), enC.size());
// If enC is a subset of D, intuitively
// there aren't any enabled transitions
// exploration would lead to a so-called
// "sleep-set blocked" trace.
if (enC.is_subset_of(D)) {
- if (not C.get_events().empty()) {
- // Report information...
- }
+ XBT_DEBUG("en(C) is a subset of the sleep set D (size %zu); if we "
+ "kept exploring, we'd hit a sleep-set blocked trace",
+ D.size());
+ XBT_DEBUG("The current configuration has %zu elements", C.get_events().size());
// When `en(C)` is empty, intuitively this means that there
// are no enabled transitions that can be executed from the
// possibility is that we've finished running everything, and
// we wouldn't be in deadlock then)
if (enC.empty()) {
+ XBT_VERB("Maximal configuration detected. Checking for deadlock...");
get_remote_app().check_deadlock();
}
return;
}
-
- // TODO: Add verbose logging about which event is being explored
-
- const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
+ UnfoldingEvent* e = select_next_unfolding_event(A, enC);
xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
"UDPOR guarantees that an event will be chosen at each point in\n"
"the search, yet no events were actually chosen\n"
"*********************************\n\n");
-
- // Move the application into stateCe and make note of that state
- move_to_stateCe(*stateC, *e);
- auto stateCe = record_current_state();
+ XBT_DEBUG("Selected event `%s` (%zu dependencies) to extend the configuration", e->to_string().c_str(),
+ e->get_immediate_causes().size());
// Ce := C + {e}
Configuration Ce = C;
exC.remove(e);
// Explore(C + {e}, D, A \ {e})
- explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
+
+ // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
+ move_to_stateCe(&stateC, e);
+ state_stack.push_back(record_current_state());
+
+ explore(Ce, D, std::move(A), std::move(exC));
+
+ // Prepare to move the application back one state.
+ // We need only remove the state from the stack here: if we perform
+ // another `Explore()` after computing an alternative, at that
+ // point we'll actually create a fresh RemoteProcess
+ state_stack.pop_back();
// D <-- D + {e}
D.insert(e);
- constexpr unsigned K = 10;
- if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
+ XBT_DEBUG("Checking for the existence of an alternative...");
+ if (auto J = C.compute_alternative_to(D, this->unfolding); J.has_value()) {
// Before searching the "right half", we need to make
// sure the program actually reflects the fact
- // that we are searching again from `stateC` (the recursive
- // search moved the program into `stateCe`)
- restore_program_state_to(*stateC);
+ // that we are searching again from `state(C)`. While the
+ // stack of states is properly adjusted to represent
+ // `state(C)` all together, the RemoteApp is currently sitting
+ // at some *future* state with resepct to `state(C)` since the
+ // recursive calls have moved it there.
+ restore_program_state_with_current_stack();
// Explore(C, D + {e}, J \ C)
auto J_minus_C = J.value().get_events().subtracting(C.get_events());
- explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
+
+ XBT_DEBUG("Alternative detected! The alternative is:\n"
+ "J\t := %s \n"
+ "J / C := %s\n"
+ "UDPOR is going to explore it...",
+ J.value().to_string().c_str(), J_minus_C.to_string().c_str());
+ explore(C, D, std::move(J_minus_C), std::move(prev_exC));
+ } else {
+ XBT_DEBUG("No alternative detected with:\n"
+ "C\t := %s \n"
+ "D\t := %s \n"
+ "A\t := %s \n",
+ C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str());
}
// D <-- D - {e}
for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
for (const auto& transition : actor_state.get_enabled_transitions()) {
- // First check for a specialized function that can compute the extension
- // set "quickly" based on its type. Otherwise, fall back to computing
- // the set "by hand"
- const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
- if (specialized_extension_function != incremental_extension_functions.end()) {
- exC.form_union((specialized_extension_function->second)(C, transition));
- } else {
- exC.form_union(this->compute_exC_by_enumeration(C, transition));
- }
+ XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
+ EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
+ exC.form_union(extension);
}
}
return exC;
}
-EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
-{
- // Here we're computing the following:
- //
- // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
- //
- // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
- EventSet incremental_exC;
-
- for (auto begin =
- maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
- begin != maximal_subsets_iterator(); ++begin) {
- const EventSet& maximal_subset = *begin;
-
- // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
- // We leave the implementation as-is to ensure that any addition would be simple
- // if it were ever added
- const bool enabled_at_config_k = false;
-
- if (enabled_at_config_k) {
- auto candidate_handle = std::make_unique<UnfoldingEvent>(maximal_subset, action);
- if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) {
- // This is a new event (i.e. one we haven't yet seen)
- unfolding.insert(std::move(candidate_handle));
- incremental_exC.insert(candidate_event);
- }
- }
- }
- return incremental_exC;
-}
-
EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
{
EventSet enC;
for (const auto e : exC) {
- if (not e->conflicts_with(C)) {
+ if (C.is_compatible_with(e)) {
enC.insert(e);
}
}
return enC;
}
-void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
+void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e)
{
- const aid_t next_actor = e.get_transition()->aid_;
+ const aid_t next_actor = e->get_transition()->aid_;
// TODO: Add the trace if possible for reporting a bug
xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
"one transition of the state of an visited event is enabled, yet no\n"
"state was actually enabled. Please report this as a bug.\n"
"*********************************\n\n");
- state.execute_next(next_actor, get_remote_app());
+ auto latest_transition_by_next_actor = state->execute_next(next_actor, get_remote_app());
+
+ // The transition that is associated with the event was just
+ // executed, so it's possible that the new version of the transition
+ // (i.e. the one after execution) has *more* information than
+ // that which existed *prior* to execution.
+ //
+ //
+ // ------- !!!!! UDPOR INVARIANT !!!!! -------
+ //
+ // At this point, we are leveraging the fact that
+ // UDPOR will not contain more than one copy of any
+ // transition executed by any actor for any
+ // particular step taken by that actor. That is,
+ // if transition `i` of the `j`th actor is contained in the
+ // configuration `C` currently under consideration
+ // by UDPOR, then only one and only one copy exists in `C`
+ //
+ // This means that we can referesh the transitions associated
+ // with each event lazily, i.e. only after we have chosen the
+ // event to continue our execution.
+ e->set_transition(std::move(latest_transition_by_next_actor));
}
-void UdporChecker::restore_program_state_to(const State& stateC)
+void UdporChecker::restore_program_state_with_current_stack()
{
+ XBT_DEBUG("Restoring state using the current stack");
get_remote_app().restore_initial_state();
- // TODO: We need to have the stack of past states available at this
- // point. Since the method is recursive, we'll need to keep track of
- // this as we progress
+
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (const std::unique_ptr<State>& state : state_stack) {
+ if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
+ break;
+ state->get_transition()->replay(get_remote_app());
+ }
}
std::unique_ptr<State> UdporChecker::record_current_state()
return next_state;
}
-const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
+UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
{
- if (!enC.empty()) {
- return *(enC.begin());
+ if (enC.empty()) {
+ throw std::invalid_argument("There are no unfolding events to select. "
+ "Are you sure that you checked that en(C) was not "
+ "empty before attempting to select an event from it?");
+ }
+
+ if (A.empty()) {
+ return const_cast<UnfoldingEvent*>(*(enC.begin()));
}
for (const auto& event : A) {
if (enC.contains(event)) {
- return event;
+ return const_cast<UnfoldingEvent*>(event);
}
}
return nullptr;
void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
{
- const EventSet C_union_D = C.get_events().make_union(D);
- const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
- const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
+ // The "clean-up set" conceptually represents
+ // those events which will no longer be considered
+ // by UDPOR during its exploration. The concept is
+ // introduced to avoid modification during iteration
+ // over the current unfolding to determine who needs to
+ // be removed. Since sets are unordered, it's quite possible
+ // that e.g. two events `e` and `e'` such that `e < e'`
+ // which are determined eligible for removal are removed
+ // in the order `e` and then `e'`. Determining that `e'`
+ // needs to be removed requires that its history be in
+ // tact to e.g. compute the conflicts with the event.
+ //
+ // Thus, we compute the set and remove all of the events
+ // at once in lieu of removing events while iterating over them.
+ // We can hypothesize that processing the events in reverse
+ // topological order would prevent any issues concerning
+ // the order in which are processed
+ EventSet clean_up_set;
+
+ // Q_(C, D, U) = C u D u U (complicated expression)
+ // See page 9 of "Unfolding-based Partial Order Reduction"
+
+ // "C u D" portion
+ const EventSet C_union_D = C.get_events().make_union(D);
+
+ // "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) {
+ return acc.make_union(unfolding.get_immediate_conflicts_of(e_prime));
+ });
+
+ const EventSet Q_CDU = C_union_D.make_union(conflict_union.get_local_config());
+
+ XBT_DEBUG("Computed Q_CDU as '%s'", Q_CDU.to_string().c_str());
// Move {e} \ Q_CDU from U to G
- if (Q_CDU.contains(e)) {
- this->unfolding.remove(e);
+ if (not Q_CDU.contains(e)) {
+ XBT_DEBUG("Moving %s from U to G...", e->to_string().c_str());
+ clean_up_set.insert(e);
}
// foreach ê in #ⁱ_U(e)
- for (const auto* e_hat : es_immediate_conflicts) {
+ for (const auto* e_hat : this->unfolding.get_immediate_conflicts_of(e)) {
// Move [ê] \ Q_CDU from U to G
- const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
- this->unfolding.remove(to_remove);
+ const EventSet to_remove = e_hat->get_local_config().subtracting(Q_CDU);
+ XBT_DEBUG("Moving {%s} from U to G...", to_remove.to_string().c_str());
+ clean_up_set.form_union(to_remove);
}
+
+ // TODO: We still perhaps need to
+ // figure out how to deal with the fact that the previous
+ // extension sets computed for past configurations
+ // contain events that may be removed from `U`. Perhaps
+ // it would be best to keep them around forever (they
+ // are moved to `G` after all and can be discarded at will,
+ // which means they may never have to be removed at all).
+ //
+ // Of course, the benefit of moving them into the set `G`
+ // is that the computation for immediate conflicts becomes
+ // more efficient (we have to search all of `U` for such conflicts,
+ // and there would be no reason to search those events
+ // that UDPOR has marked as no longer being important)
+ // For now, there appear to be no "obvious" issues (although
+ // UDPOR's behavior is often far from obvious...)
+ this->unfolding.mark_finished(clean_up_set);
}
RecordTrace UdporChecker::get_record_trace()
{
RecordTrace res;
+ for (auto const& state : state_stack)
+ res.push_back(state->get_transition());
return res;
}
std::vector<std::string> UdporChecker::get_textual_trace()
{
- // TODO: Topologically sort the events of the latest configuration
- // and iterate through that topological sorting
std::vector<std::string> trace;
+ for (auto const& state : state_stack) {
+ const auto* t = state->get_transition();
+ trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
+ }
return trace;
}
#include "src/mc/mc_record.hpp"
#include <functional>
+#include <list>
#include <optional>
namespace simgrid::mc::udpor {
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
-
- inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
+ std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
private:
Unfolding unfolding = Unfolding();
- /**
- * @brief A collection of specialized functions which can incrementally
- * compute the extension of a configuration based on the action taken
- */
- using ExtensionFunction = std::function<EventSet(const Configuration&, const std::shared_ptr<Transition>)>;
- std::unordered_map<Transition::Type, ExtensionFunction> incremental_extension_functions =
- std::unordered_map<Transition::Type, ExtensionFunction>();
+ // The current sequence of states that the checker has
+ // visited in order to reach the current configuration
+ std::list<std::unique_ptr<State>> state_stack;
/**
* @brief Explores the unfolding of the concurrent system
* @param A the set of events to "guide" UDPOR in the correct direction
* when it returns back to a node in the unfolding and must decide among
* events to select from `ex(C)`. See [1] for more details
- * @param stateC the state of the program after having executed `C`,
- * viz. `state(C)` using the notation of [1]
*
* TODO: Add the optimization where we can check if e == e_prior
* to prevent repeated work when computing ex(C)
*/
- void explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
+ void explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC);
/**
* @brief Identifies the next event from the unfolding of the concurrent system
* by the UDPOR algorithm to select new events to search. See the original
* paper [1] for more details
*/
- const UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
+ UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
/**
* @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
* @returns the extension set `ex(C)` of `C`
*/
EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC);
-
- /**
- * @brief Computes a portion of the extension set of a configuration given
- * some action `action` by directly enumerating all maximal subsets of C
- * (i.e. without specializations based on the action)
- */
- EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
-
EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
/**
*
*/
- void move_to_stateCe(State& stateC, const UnfoldingEvent& e);
+ void move_to_stateCe(State* stateC, UnfoldingEvent* e);
/**
- * @brief Creates a new snapshot of the state of the progam undergoing
- * model checking
- *
- * @returns the handle used to uniquely identify this state later in the
- * exploration of the unfolding. You provide this handle to an event in the
- * unfolding to regenerate past states
+ * @brief Creates a new snapshot of the state of the application
+ * as it currently looks
*/
std::unique_ptr<State> record_current_state();
/**
+ * @brief Move the application side into the state at the top of the
+ * state stack provided
+ *
+ * As UDPOR performs its search, it moves the application-side along with
+ * it so that the application is always providing the checker with
+ * the correct information about what each actor is running (and whether
+ * those actors are enabled) at the state reached by the configuration it
+ * decides to search.
*
+ * When UDPOR decides to "backtrack" (e.g. after reaching a configuration
+ * whose en(C) is empty), before it attempts to continue the search by taking
+ * a different path from a configuration it visited in the past, it must ensure
+ * that the application-side has moved back into `state(C)`.
+ *
+ * The search may have moved the application arbitrarily deep into its execution,
+ * and the search may backtrack arbitrarily closer to the beginning of the execution.
+ * The UDPOR implementation in SimGrid ensures that the stack is updated appropriately,
+ * but the process must still be regenerated.
*/
- void restore_program_state_to(const State& stateC);
+ void restore_program_state_with_current_stack();
/**
- *
+ * @brief Perform the functionality of the `Remove(e, C, D)` function in [1]
*/
void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
};
#endif
explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, cfg_use_DPOR()));
+ ExitStatus status;
try {
explo->run();
- } catch (const DeadlockError&) {
- return SIMGRID_MC_EXIT_DEADLOCK;
- } catch (const TerminationError&) {
- return SIMGRID_MC_EXIT_NON_TERMINATION;
- } catch (const LivenessError&) {
- return SIMGRID_MC_EXIT_LIVENESS;
+ status = ExitStatus::SUCCESS;
+ } catch (const McError& e) {
+ status = e.value;
}
- return SIMGRID_MC_EXIT_SUCCESS;
+ return static_cast<int>(status);
}
#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+#include "src/xbt/utils/iter/variable_for_loop.hpp"
#include "xbt/asserts.h"
#include <algorithm>
{
}
-Configuration::Configuration(const UnfoldingEvent* e) : Configuration(e->get_history())
+Configuration::Configuration(const UnfoldingEvent* e) : Configuration(e->get_local_config())
{
// The local configuration should always be a valid configuration. We
// check the invariant regardless as a sanity check
}
+Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {}
+
Configuration::Configuration(const EventSet& events) : events_(events)
{
if (!events_.is_valid_configuration()) {
throw std::invalid_argument("The events do not form a valid configuration");
}
-}
-Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {}
+ // Since we add in topological order under `<`, we know that the "most-recent"
+ // transition executed by each actor will appear last
+ for (const UnfoldingEvent* e : get_topologically_sorted_events()) {
+ this->latest_event_mapping[e->get_actor()] = e;
+ }
+}
void Configuration::add_event(const UnfoldingEvent* e)
{
throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead");
}
+ // The event is already a member of the configuration: there's
+ // nothing to do in this case
if (this->events_.contains(e)) {
return;
}
// Preserves the property that the configuration is conflict-free
- if (e->conflicts_with(*this)) {
+ if (e->conflicts_with_any(this->events_)) {
throw std::invalid_argument("The newly added event conflicts with the events already "
"contained in the configuration. Adding this event violates "
"the property that a configuration is conflict-free");
}
this->events_.insert(e);
- this->newest_event = e;
+ this->newest_event = e;
+ 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)) {
bool Configuration::is_compatible_with(const UnfoldingEvent* e) const
{
- return not e->conflicts_with(*this);
+ // 1. `e`'s history must be contained in the configuration;
+ // otherwise adding the event would violate the invariant
+ // that a configuration is causally-closed
+ //
+ // 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_));
}
bool Configuration::is_compatible_with(const History& history) const
{
- return std::none_of(history.begin(), history.end(),
- [&](const UnfoldingEvent* e) { return e->conflicts_with(*this); });
+ // Note: We don't need to check if the `C` will be causally-closed
+ // after adding `history` to it since a) `C` itself is already
+ // causally-closed and b) the history is already causally closed
+ const auto event_diff = history.get_event_diff_with(*this);
+
+ // The events that are contained outside of the configuration
+ // must themselves be free of conflicts.
+ if (not event_diff.is_conflict_free()) {
+ return false;
+ }
+
+ // Now we need only ensure that there are no conflicts
+ // between events of the configuration and the events
+ // that lie outside of the configuration. There is no
+ // need to check if there are conflicts in `C`: we already
+ // know that it's conflict free
+ const auto begin = simgrid::xbt::variable_for_loop<const EventSet>{{event_diff}, {this->events_}};
+ const auto end = simgrid::xbt::variable_for_loop<const EventSet>();
+ return std::none_of(begin, end, [=](const auto event_pair) {
+ const UnfoldingEvent* e1 = *event_pair[0];
+ const UnfoldingEvent* e2 = *event_pair[1];
+ return e1->conflicts_with(e2);
+ });
}
std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
size_t k) const
{
// 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
- const auto D_hat = [&]() {
- const size_t size = std::min(k, D.size());
- std::vector<const UnfoldingEvent*> D_hat(size);
+ const size_t k_alt_size = std::min(k, D.size());
+ const auto D_hat = [&k_alt_size, &D]() {
+ std::vector<const UnfoldingEvent*> D_hat(k_alt_size);
// TODO: Since any subset suffices for computing `k`-partial alternatives,
// potentially select intelligently here (e.g. perhaps pick events
// with transitions that we know are totally independent). This may be
// UDPOR
//
// For now, simply pick the first `k` events
- std::copy_n(D.begin(), size, D_hat.begin());
+ std::copy_n(D.begin(), k_alt_size, D_hat.begin());
return D_hat;
}();
Comb comb(k);
for (const auto* e : U) {
- for (unsigned i = 0; i < k; i++) {
+ for (size_t i = 0; i < k_alt_size; i++) {
const UnfoldingEvent* e_i = D_hat[i];
if (const auto e_local_config = History(e);
e_i->conflicts_with(e) and (not D.intersects(e_local_config)) and is_compatible_with(e_local_config)) {
return Configuration(History(map_events(*alternative)));
}
+std::optional<const UnfoldingEvent*> Configuration::get_latest_event_of(aid_t aid) const
+{
+ if (const auto latest_event = latest_event_mapping.find(aid); latest_event != latest_event_mapping.end()) {
+ return std::optional<const UnfoldingEvent*>{latest_event->second};
+ }
+ return std::nullopt;
+}
+
+std::optional<const Transition*> Configuration::get_latest_action_of(aid_t aid) const
+{
+ if (const auto latest_event = get_latest_event_of(aid); latest_event.has_value()) {
+ return std::optional<const Transition*>{latest_event.value()->get_transition()};
+ }
+ return std::nullopt;
+}
+
} // namespace simgrid::mc::udpor
#include "src/mc/explo/udpor/udpor_forward.hpp"
#include <optional>
+#include <string>
+#include <unordered_map>
namespace simgrid::mc::udpor {
auto cend() const { return this->events_.cend(); }
bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
+ bool contains(const EventSet& events) const { return events.is_subset_of(this->events_); }
const EventSet& get_events() const { return this->events_; }
const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
+ std::string to_string() const { return this->events_.to_string(); }
/**
* @brief Insert a new event into the configuration
/**
* @brief Whether or not the given event can be added to
- * this configuration while keeping the set of events causally closed
- * and conflict-free
+ * this configuration while preserving that the configuration
+ * is causally closed and conflict-free
+ *
+ * A configuration `C` is compatible with an event iff
+ * the event can be added to `C` while preserving that
+ * the configuration is causally closed and conflict-free.
+ *
+ * The method effectively answers the following question:
+ *
+ * "Is `C + {e}` a valid configuration?"
*/
bool is_compatible_with(const UnfoldingEvent* e) const;
* @brief Whether or not the events in the given history can be added to
* this configuration while keeping the set of events causally closed
* and conflict-free
+ *
+ * A configuration `C` is compatible with a history iff all
+ * events of the history can be added to `C` while preserving
+ * that the configuration is causally closed and conflict-free.
+ *
+ * The method effectively answers the following question:
+ *
+ * "Is `C + (U_i [e_i])` a valid configuration?"
*/
bool is_compatible_with(const History& history) const;
*/
EventSet get_minimally_reproducible_events() const;
+ /**
+ * @brief Determines the event in the configuration whose associated
+ * transition is the latest of the given actor
+ *
+ * @invariant: At most one event in the configuration will correspond
+ * to `preEvt(C, a)` for any action `a`. This can be argued by contradiction.
+ *
+ * If there were more than one event (`e` and `e'`) in any configuration whose
+ * associated transitions `a` were run by the same actor at the same step, then they
+ * could not be causally related (`<`) since `a` could not be enabled in
+ * both subconfigurations C' and C'' containing the hypothetical events
+ * `e` and `e` + `e'`. Since they would not be contained in each other's histories,
+ * they would be in conflict, which cannot happen between any pair of events
+ * in a configuration. Thus `e` and `e'` cannot exist simultaneously
+ */
+ std::optional<const UnfoldingEvent*> get_latest_event_of(aid_t) const;
+ /**
+ * @brief Determines the most recent transition of the given actor
+ * in this configuration, or `pre(a)` as denoted in the thesis of
+ * The Anh Pham
+ *
+ * Conceptually, the execution of an interleaving of the transitions
+ * (i.e. a topological ordering) of a configuration yields a unique
+ * state `state(C)`. Since actions taken by the same actor are always
+ * dependent with one another, any such interleaving always yields a
+ * unique
+ *
+ * @returns the most recent transition of the given actor
+ * in this configuration, or `std::nullopt` if there are no transitions
+ * in this configuration run by the given actor
+ */
+ std::optional<const Transition*> get_latest_action_of(aid_t aid) const;
+ std::optional<const UnfoldingEvent*> pre_event(aid_t aid) const { return get_latest_event_of(aid); }
+
private:
/**
* @brief The most recent event added to the configuration
*
* @invariant For each event `e` in `events_`, the set of
* dependencies of `e` is also contained in `events_`
+ *
+ * @invariant For each pair of events `e` and `e'` in
+ * `events_`, `e` and `e'` are not in conflict
*/
EventSet events_;
+
+ /**
+ * @brief Maps actors to the latest events which
+ * are executed by the actor
+ *
+ * @invariant: The events that are contained in the map
+ * are also contained in the set `events_`
+ */
+ std::unordered_map<aid_t, const UnfoldingEvent*> latest_event_mapping;
};
} // namespace simgrid::mc::udpor
#include <unordered_map>
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
// e3
// / /
// e4 e5
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>(4));
SECTION("Creating a configuration without events")
{
// /
// / /
// e3 e4
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>(3));
REQUIRE_THROWS_AS(Configuration().add_event(nullptr), std::invalid_argument);
REQUIRE_THROWS_AS(Configuration().add_event(&e2), std::invalid_argument);
// e3
// /
// e4
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(4));
SECTION("Topological ordering for entire set")
{
// e4 e6
// /
// e5
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>(5));
+ UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>(6));
SECTION("Topological ordering for subsets")
{
// / / /
// / / /
// [ e12 ]
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e8(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e4}), std::make_shared<IndependentAction>());
- UnfoldingEvent e7(EventSet({&e2, &e8}), std::make_shared<IndependentAction>());
- UnfoldingEvent e9(EventSet({&e6, &e7}), std::make_shared<IndependentAction>());
- UnfoldingEvent e10(EventSet({&e7}), std::make_shared<IndependentAction>());
- UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>());
- UnfoldingEvent e12(EventSet({&e5, &e9, &e10}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e8(EventSet({&e1}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(5));
+ UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>(6));
+ UnfoldingEvent e6(EventSet({&e4}), std::make_shared<IndependentAction>(7));
+ UnfoldingEvent e7(EventSet({&e2, &e8}), std::make_shared<IndependentAction>(8));
+ UnfoldingEvent e9(EventSet({&e6, &e7}), std::make_shared<IndependentAction>(9));
+ UnfoldingEvent e10(EventSet({&e7}), std::make_shared<IndependentAction>(10));
+ UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>(11));
+ UnfoldingEvent e12(EventSet({&e5, &e9, &e10}), std::make_shared<IndependentAction>(12));
Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12};
SECTION("Test every combination of the maximal configuration (forward graph)")
// e3 e6
// / / /
// e4 e7 e8
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>());
- UnfoldingEvent e7(EventSet({&e6}), std::make_shared<IndependentAction>());
- UnfoldingEvent e8(EventSet({&e6}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>(5));
+ UnfoldingEvent e7(EventSet({&e6}), std::make_shared<IndependentAction>(6));
+ UnfoldingEvent e8(EventSet({&e6}), std::make_shared<IndependentAction>(7));
SECTION("Iteration over an empty configuration yields only the empty set")
{
// | e11 e12 e13 e14 e15
// | / / / / / /
// +-> e16 e17 e18
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e7(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e8(EventSet({&e4}), std::make_shared<IndependentAction>());
- UnfoldingEvent e9(EventSet({&e4, &e5, &e6}), std::make_shared<IndependentAction>());
- UnfoldingEvent e10(EventSet({&e6, &e7}), std::make_shared<IndependentAction>());
- UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>());
- UnfoldingEvent e12(EventSet({&e8}), std::make_shared<IndependentAction>());
- UnfoldingEvent e13(EventSet({&e9}), std::make_shared<IndependentAction>());
- UnfoldingEvent e14(EventSet({&e9}), std::make_shared<IndependentAction>());
- UnfoldingEvent e15(EventSet({&e10}), std::make_shared<IndependentAction>());
- UnfoldingEvent e16(EventSet({&e5, &e11}), std::make_shared<IndependentAction>());
- UnfoldingEvent e17(EventSet({&e12, &e13, &e14}), std::make_shared<IndependentAction>());
- UnfoldingEvent e18(EventSet({&e14, &e15}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e5(EventSet({&e2}), std::make_shared<IndependentAction>(5));
+ UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>(6));
+ UnfoldingEvent e7(EventSet({&e3}), std::make_shared<IndependentAction>(7));
+ UnfoldingEvent e8(EventSet({&e4}), std::make_shared<IndependentAction>(8));
+ UnfoldingEvent e9(EventSet({&e4, &e5, &e6}), std::make_shared<IndependentAction>(9));
+ UnfoldingEvent e10(EventSet({&e6, &e7}), std::make_shared<IndependentAction>(10));
+ UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>(11));
+ UnfoldingEvent e12(EventSet({&e8}), std::make_shared<IndependentAction>(12));
+ UnfoldingEvent e13(EventSet({&e9}), std::make_shared<IndependentAction>(13));
+ UnfoldingEvent e14(EventSet({&e9}), std::make_shared<IndependentAction>(14));
+ UnfoldingEvent e15(EventSet({&e10}), std::make_shared<IndependentAction>(15));
+ UnfoldingEvent e16(EventSet({&e5, &e11}), std::make_shared<IndependentAction>(16));
+ UnfoldingEvent e17(EventSet({&e12, &e13, &e14}), std::make_shared<IndependentAction>(17));
+ UnfoldingEvent e18(EventSet({&e14, &e15}), std::make_shared<IndependentAction>(18));
Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12, &e13, &e14, &e15, &e16, &e17, &e18};
SECTION("Every subset iterated over is maximal")
}
}
-TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Reader/Writer Example")
+TEST_CASE("simgrid::mc::udpor::Configuration: Latest Transitions")
+{
+ // The following tests concern the given event structure (labeled as "event(actor)")
+ // e1(1)
+ // / /
+ // e2(1) e3(2)
+ // / // /
+ // e4(3) e5(2) e6(1)
+ // / /
+ // e7(1) e8(1)
+ const auto t1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto t2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto t3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto t4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto t5 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto t6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto t7 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto t8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+
+ const UnfoldingEvent e1(EventSet(), t1);
+ const UnfoldingEvent e2(EventSet({&e1}), t2);
+ const UnfoldingEvent e3(EventSet({&e1}), t3);
+ const UnfoldingEvent e4(EventSet({&e2}), t4);
+ const UnfoldingEvent e5(EventSet({&e2, &e3}), t5);
+ const UnfoldingEvent e6(EventSet({&e3}), t6);
+ const UnfoldingEvent e7(EventSet({&e5}), t7);
+ const UnfoldingEvent e8(EventSet({&e5}), t8);
+
+ SECTION("Test that the latest events are correct on initialization")
+ {
+ SECTION("Empty configuration has no events")
+ {
+ Configuration C;
+ REQUIRE_FALSE(C.get_latest_event_of(1).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+
+ REQUIRE_FALSE(C.get_latest_action_of(1).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+ }
+
+ SECTION("Missing two actors")
+ {
+ Configuration C{&e1};
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e1);
+
+ REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t1.get());
+
+ REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+ }
+
+ SECTION("Two events with one actor yields the latest event")
+ {
+ Configuration C{&e1, &e2};
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e2);
+
+ REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t2.get());
+
+ REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+ }
+
+ SECTION("Two events with two actors")
+ {
+ Configuration C{&e1, &e3};
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e1);
+
+ REQUIRE(C.get_latest_event_of(2).has_value());
+ REQUIRE(C.get_latest_event_of(2).value() == &e3);
+
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t1.get());
+
+ REQUIRE(C.get_latest_action_of(2).has_value());
+ REQUIRE(C.get_latest_action_of(2).value() == t3.get());
+
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+ }
+
+ SECTION("Three different actors actors")
+ {
+ Configuration C{&e1, &e2, &e3, &e4, &e5};
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e2);
+
+ REQUIRE(C.get_latest_event_of(2).has_value());
+ REQUIRE(C.get_latest_event_of(2).value() == &e5);
+
+ REQUIRE(C.get_latest_event_of(3).has_value());
+ REQUIRE(C.get_latest_event_of(3).value() == &e4);
+
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t2.get());
+
+ REQUIRE(C.get_latest_action_of(2).has_value());
+ REQUIRE(C.get_latest_action_of(2).value() == t5.get());
+
+ REQUIRE(C.get_latest_action_of(3).has_value());
+ REQUIRE(C.get_latest_action_of(3).value() == t4.get());
+ }
+ }
+
+ SECTION("Test that the latest events are correct when adding new events")
+ {
+ Configuration C;
+ REQUIRE_FALSE(C.get_latest_event_of(1).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(1).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+
+ C.add_event(&e1);
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e1);
+ REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t1.get());
+ REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+
+ C.add_event(&e2);
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e2);
+ REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t2.get());
+ REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+
+ C.add_event(&e3);
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e2);
+ REQUIRE(C.get_latest_event_of(2).has_value());
+ REQUIRE(C.get_latest_event_of(2).value() == &e3);
+ REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t2.get());
+ REQUIRE(C.get_latest_action_of(2).has_value());
+ REQUIRE(C.get_latest_action_of(2).value() == t3.get());
+ REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
+
+ C.add_event(&e4);
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e2);
+ REQUIRE(C.get_latest_event_of(2).has_value());
+ REQUIRE(C.get_latest_event_of(2).value() == &e3);
+ REQUIRE(C.get_latest_event_of(3).has_value());
+ REQUIRE(C.get_latest_event_of(3).value() == &e4);
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t2.get());
+ REQUIRE(C.get_latest_action_of(2).has_value());
+ REQUIRE(C.get_latest_action_of(2).value() == t3.get());
+ REQUIRE(C.get_latest_action_of(3).has_value());
+ REQUIRE(C.get_latest_action_of(3).value() == t4.get());
+
+ C.add_event(&e5);
+ REQUIRE(C.get_latest_event_of(1).has_value());
+ REQUIRE(C.get_latest_event_of(1).value() == &e2);
+ REQUIRE(C.get_latest_event_of(2).has_value());
+ REQUIRE(C.get_latest_event_of(2).value() == &e5);
+ REQUIRE(C.get_latest_event_of(3).has_value());
+ REQUIRE(C.get_latest_event_of(3).value() == &e4);
+ REQUIRE(C.get_latest_action_of(1).has_value());
+ REQUIRE(C.get_latest_action_of(1).value() == t2.get());
+ REQUIRE(C.get_latest_action_of(2).has_value());
+ REQUIRE(C.get_latest_action_of(2).value() == t5.get());
+ REQUIRE(C.get_latest_action_of(3).has_value());
+ REQUIRE(C.get_latest_action_of(3).value() == t4.get());
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::Configuration: Computing Full Alternatives in Reader/Writer Example")
{
// The following tests concern the given event structure that is given as
// an example in figure 1 of the original UDPOR paper.
// then `e4`, and then `e7`
Unfolding U;
- auto e0 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<ConditionallyDependentAction>());
+ auto e0 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 0));
auto e0_handle = e0.get();
- auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<DependentAction>());
+ auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e1_handle = e1.get();
- auto e2 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e2 = std::make_unique<UnfoldingEvent>(
+ EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
auto e2_handle = e2.get();
- auto e3 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e3 = std::make_unique<UnfoldingEvent>(
+ EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
auto e3_handle = e3.get();
- auto e4 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e4 = std::make_unique<UnfoldingEvent>(
+ EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
auto e4_handle = e4.get();
- auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}), std::make_shared<DependentAction>());
+ auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e5_handle = e5.get();
- auto e6 = std::make_unique<UnfoldingEvent>(EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e6 = std::make_unique<UnfoldingEvent>(
+ EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
auto e6_handle = e6.get();
- auto e7 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e7 = std::make_unique<UnfoldingEvent>(
+ EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
auto e7_handle = e7.get();
- auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}), std::make_shared<DependentAction>());
+ auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e8_handle = e8.get();
- auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}), std::make_shared<DependentAction>());
+ auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e9_handle = e9.get();
- auto e10 = std::make_unique<UnfoldingEvent>(EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e10 = std::make_unique<UnfoldingEvent>(
+ EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
auto e10_handle = e10.get();
SECTION("Alternative computation call 1")
return std::any_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
}
+bool EventSet::intersects(const EventSet& other) const
+{
+ return std::any_of(other.begin(), other.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
+}
+
+EventSet EventSet::get_largest_maximal_subset() const
+{
+ const History history(*this);
+ return history.get_all_maximal_events();
+}
+
bool EventSet::is_maximal() const
{
// A set of events is maximal if no event from
// the original set is ruled out when traversing
// the history of the events
- const History history(*this);
- return *this == history.get_all_maximal_events();
+ return *this == this->get_largest_maximal_subset();
}
bool EventSet::is_conflict_free() const
return topological_events;
}
+std::string EventSet::to_string() const
+{
+ std::string contents;
+
+ for (const auto* event : *this) {
+ contents += event->to_string();
+ contents += " + ";
+ }
+
+ return contents;
+}
+
std::vector<const UnfoldingEvent*> EventSet::move_into_vector() const&&
{
std::vector<const UnfoldingEvent*> contents;
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <algorithm>
#include <cstddef>
#include <initializer_list>
#include <unordered_set>
#include <vector>
+#include <xbt/asserts.h>
namespace simgrid::mc::udpor {
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(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
+ explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end())
+ {
+ xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
+ }
+ explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events)
+ {
+ xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
+ }
+ explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list))
+ {
+ xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
+ }
auto begin() const { return this->events_.begin(); }
auto end() const { return this->events_.end(); }
bool empty() const;
bool contains(const UnfoldingEvent*) const;
bool contains(const History&) const;
+ bool intersects(const EventSet&) const;
bool intersects(const History&) const;
bool is_subset_of(const EventSet&) const;
bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }
+ std::string to_string() const;
/**
* @brief Whether or not this set of events could
*/
bool is_conflict_free() const;
+ /**
+ * @brief Produces the largest subset of this
+ * set of events which is maximal
+ */
+ EventSet get_largest_maximal_subset() const;
+
/**
* @brief Orders the events of the set such that
* "more recent" events (i.e. those that are farther down in
// The tests enumerate all possible subsets of the events
// in the structure and test whether those subsets are
// maximal and/or valid configurations
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>(5));
SECTION("Valid Configurations")
{
SECTION("No conflicts throughout the whole structure with independent actions")
{
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>(5));
// 6 choose 0 = 1 test
CHECK(EventSet().is_conflict_free());
SECTION("Conditional conflicts")
{
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e1}), std::make_shared<DependentAction>());
- UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e1}), std::make_shared<DependentAction>(4));
+ UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>(5));
// 6 choose 0 = 1 test
// There are no events even to be in conflict with
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
+
+#include <functional>
+#include <unordered_map>
+#include <xbt/asserts.h>
+#include <xbt/ex.h>
+
+using namespace simgrid::mc;
+
+namespace simgrid::mc::udpor {
+
+EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, Unfolding* U,
+ const 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}};
+
+ if (const auto handler = handlers.find(action->type_); handler != handlers.end()) {
+ return handler->second(C, U, std::move(action));
+ } else {
+ xbt_assert(false,
+ "There is currently no specialized computation for the transition "
+ "'%s' for computing extension sets in UDPOR, so the model checker cannot "
+ "determine how to proceed. Please submit a bug report requesting "
+ "that the transition be supported in SimGrid using UDPOR and consider "
+ "using the other model-checking algorithms supported by SimGrid instead "
+ "in the meantime",
+ action->to_string().c_str());
+ DIE_IMPOSSIBLE;
+ }
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, Unfolding* U,
+ const std::shared_ptr<Transition> action)
+{
+ EventSet exC;
+
+ const auto send_action = std::static_pointer_cast<CommSendTransition>(std::move(action));
+ const auto pre_event_a_C = C.pre_event(send_action->aid_);
+ const unsigned sender_mailbox = send_action->get_mailbox();
+
+ // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
+ // NOTE: If `preEvt(a, C)` doesn't exist, we're effectively asking
+ // about `config({})`
+ if (pre_event_a_C.has_value()) {
+ const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), send_action);
+ exC.insert(e_prime);
+ } else {
+ const auto e_prime = U->discover_event(EventSet(), send_action);
+ exC.insert(e_prime);
+ }
+
+ // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
+ // Com contains a matching c' = AsyncReceive(m, _) with a
+ 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;
+ }
+ // 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();
+
+ // TODO: Check D_K(a, lambda(e))
+ if (true) {
+ const auto e_prime = U->discover_event(std::move(K), send_action);
+ exC.insert(e_prime);
+ }
+ }
+ }
+
+ // TODO: Add `TestAny` dependency case
+ return exC;
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
+ const std::shared_ptr<Transition> action)
+{
+ EventSet exC;
+
+ // TODO: if this is the first action by the actor, no such previous event exists.
+ // How do we react here? Do we say we're dependent with the root event?
+ const auto recv_action = std::static_pointer_cast<CommRecvTransition>(std::move(action));
+ const unsigned recv_mailbox = recv_action->get_mailbox();
+ const auto pre_event_a_C = C.pre_event(recv_action->aid_);
+
+ // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
+ if (pre_event_a_C.has_value()) {
+ const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action);
+ exC.insert(e_prime);
+ } else {
+ const auto e_prime = U->discover_event(EventSet(), recv_action);
+ exC.insert(e_prime);
+ }
+
+ // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
+ // 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;
+ }
+ // 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();
+
+ // TODO: Check D_K(a, lambda(e))
+ if (true) {
+ const auto e_prime = U->discover_event(std::move(K), recv_action);
+ exC.insert(e_prime);
+ }
+ }
+ }
+
+ // TODO: Add `TestAny` dependency case
+ return exC;
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& C, Unfolding* U,
+ std::shared_ptr<Transition> action)
+{
+ EventSet exC;
+
+ const auto wait_action = std::static_pointer_cast<CommWaitTransition>(std::move(action));
+ const auto wait_comm = wait_action->get_comm();
+ const auto pre_event_a_C = C.pre_event(wait_action->aid_);
+
+ // Determine the _issuer_ of the communication of the `CommWait` event
+ // in `C`. The issuer of the `CommWait` in `C` is the event in `C`
+ // 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) {
+ 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) {
+ return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
+ }
+
+ return false;
+ });
+ xbt_assert(issuer != C.end(),
+ "Invariant violation! A (supposedly) enabled `CommWait` transition "
+ "waiting on commiunication %lu should not be enabled: the receive/send "
+ "transition which generated the communication is not an action taken "
+ "to reach state(C) (the state of the configuration), which should "
+ "be an impossibility if `%s` is enabled. Please report this as "
+ "a bug in SimGrid's UDPOR implementation",
+ wait_action->get_comm(), wait_action->to_string(false).c_str());
+ const UnfoldingEvent* e_issuer = *issuer;
+ const History e_issuer_history(e_issuer);
+
+ // 1. if `a` is enabled at state(config({preEvt(a,C)})), then
+ // create `e' := <a, config({preEvt(a,C)})>` and add `e'` to `ex(C)`
+ //
+ // First, if `pre_event_a_C == std::nullopt`, then there is nothing to
+ // do: `CommWait` will never be enabled in the empty configuration (at
+ // least two actions must be executed before)
+ if (pre_event_a_C.has_value(); const auto unwrapped_pre_event = pre_event_a_C.value()) {
+
+ // A necessary condition is that the issuer be present in
+ // config({preEvt(a, C)}); otherwise, the `CommWait` could not
+ // be enabled since the communication on which it waits would not
+ // have been created for it!
+ if (const auto config_pre_event = History(unwrapped_pre_event); config_pre_event.contains(e_issuer)) {
+ // If the issuer is a `CommRecv` (resp. `CommSend`), then we check that there
+ // are at least as many `CommSend` (resp. `CommRecv`) transitions in `config_pre_event`
+ // 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) {
+
+ 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;
+ });
+
+ // 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;
+ });
+
+ 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) {
+
+ 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;
+ });
+
+ // 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;
+ });
+
+ if (send_position <= receive_position) {
+ exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
+ }
+
+ } else {
+ xbt_assert(false,
+ "The transition which created the communication on which `%s` waits "
+ "is neither an async send nor an async receive. The current UDPOR "
+ "implementation does not know how to check if `CommWait` is enabled in "
+ "this case. Was a new transition added?",
+ e_issuer->get_transition()->to_string().c_str());
+ }
+ }
+ }
+
+ // 3. foreach event e in C do
+ for (const auto e : C) {
+ if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
+ e_issuer_send != nullptr) {
+
+ // If the provider of the communication for `CommWait` is a
+ // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
+ // All other actions would be independent with the wait action (including
+ // another `CommSend` to the same mailbox: `CommWait` is "waiting" for its
+ // corresponding receive action)
+ if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
+ continue;
+ }
+
+ 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) {
+ continue;
+ }
+
+ // If the `issuer` is not in `config(K)`, this implies that
+ // `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)});
+ const auto config_K = History(K);
+ if (not config_K.contains(e_issuer)) {
+ continue;
+ }
+
+ // TODO: Compute the send and receive positions
+
+ // 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;
+ });
+
+ // 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;
+ });
+
+ 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) {
+
+ // If the provider of the communication for `CommWait` is a
+ // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
+ // All other actions would be independent with the wait action (including
+ // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
+ // corresponding send action)
+ if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
+ continue;
+ }
+
+ 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) {
+ continue;
+ }
+
+ // If the `issuer` is not in `config(K)`, this implies that
+ // `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)});
+ 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;
+ });
+
+ // 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;
+ });
+
+ if (send_position == receive_position) {
+ exC.insert(U->discover_event(std::move(K), wait_action));
+ }
+ }
+ }
+
+ return exC;
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U,
+ std::shared_ptr<Transition> test_action)
+{
+ return EventSet();
+}
+
+} // namespace simgrid::mc::udpor
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_EVENTSETCALCULATOR_HPP
+#define SIMGRID_MC_UDPOR_EVENTSETCALCULATOR_HPP
+
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionActorJoin.hpp"
+#include "src/mc/transition/TransitionAny.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
+#include "src/mc/transition/TransitionObjectAccess.hpp"
+#include "src/mc/transition/TransitionRandom.hpp"
+#include "src/mc/transition/TransitionSynchro.hpp"
+
+#include <memory>
+
+namespace simgrid::mc::udpor {
+
+/**
+ * @brief Computes incrementally the portion of the extension set for a new configuration `C`
+ */
+struct ExtensionSetCalculator final {
+private:
+ static EventSet partially_extend_CommSend(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+ static EventSet partially_extend_CommRecv(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+ static EventSet partially_extend_CommWait(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+ static EventSet partially_extend_CommTest(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+
+public:
+ static EventSet partially_extend(const Configuration&, Unfolding*, const std::shared_ptr<Transition>);
+};
+
+} // namespace simgrid::mc::udpor
+#endif
#include <boost/iterator/iterator_facade.hpp>
#include <functional>
+#include <initializer_list>
#include <optional>
namespace simgrid::mc::udpor {
History& operator=(History const&) = default;
History(History&&) = default;
- explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {}
explicit History(const UnfoldingEvent* e) : events_({e}) {}
+ explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {}
+ explicit History(std::initializer_list<const UnfoldingEvent*> list) : events_(std::move(list)) {}
auto begin() const { return Iterator(events_); }
auto end() const { return Iterator(EventSet()); }
*/
EventSet get_all_maximal_events() const;
+ /**
+ * @brief Computes the set of events that are not contained
+ * in the given configuration
+ *
+ * A configuration is a causally-closed, conflict-free set
+ * of events. Thus, you can determine which events lie outside
+ * of a configuration during the search more efficiently: the moment
+ * you discover an event contained in the configuration, you
+ * do not need to search that event or any of its ancestors as
+ * they will all be contained in the configuration
+ */
EventSet get_event_diff_with(const Configuration& config) const;
private:
namespace simgrid::mc::udpor {
-void Unfolding::remove(const EventSet& events)
+void Unfolding::mark_finished(const EventSet& events)
{
for (const auto e : events) {
- remove(e);
+ mark_finished(e);
}
}
-void Unfolding::remove(const UnfoldingEvent* e)
+void Unfolding::mark_finished(const UnfoldingEvent* e)
{
if (e == nullptr) {
throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL");
}
- this->global_events_.erase(e);
- this->event_handles.remove(e);
+ this->U.remove(e);
+ this->G.insert(e);
}
-void Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
+const UnfoldingEvent* Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
{
const UnfoldingEvent* handle = e.get();
if (auto loc = this->global_events_.find(handle); loc != this->global_events_.end()) {
"This will result in a double free error and must be fixed.");
}
- // Map the handle to its owner
- this->event_handles.insert(handle);
- this->global_events_[handle] = std::move(e);
-}
+ // Attempt to search first for an event in `U`. If it exists, we use that event
+ // instead of `e` since it is semantically equivalent to `e` (i.e. `e` is
+ // effectively already contained in the unfolding)
+ if (auto loc = std::find_if(U.begin(), U.end(), [=](const auto e_i) { return *e_i == *handle; }); loc != U.end()) {
+ // Return the handle to that event and ignore adding in a duplicate event
+ return *loc;
+ }
-bool Unfolding::contains_event_equivalent_to(const UnfoldingEvent* e) const
-{
- // Notice the use of `==` equality here. `e` may not be contained in the
- // unfolding; but some event which is "equivalent" to it could be.
- for (const auto event : *this) {
- if (*event == *e) {
- return true;
- }
+ // Then look for `e` in `G`. It's possible `e` was already constructed
+ // in the past, in which case we can simply re-use it.
+ //
+ // Note, though, that in this case we must move the event in `G` into
+ // `U`: we've inserted `e` into the unfolding, so we expect it to be in `U`
+ if (auto loc = std::find_if(G.begin(), G.end(), [=](const auto e_i) { return *e_i == *handle; }); loc != G.end()) {
+ const auto e_equiv = *loc;
+ G.remove(e_equiv);
+ U.insert(e_equiv);
+ return e_equiv;
}
- return false;
+
+ // Otherwise `e` is truly a "new" event
+ this->U.insert(handle);
+ this->event_handles.insert(handle);
+ this->global_events_[handle] = std::move(e);
+ return handle;
}
EventSet Unfolding::get_immediate_conflicts_of(const UnfoldingEvent* e) const
{
EventSet immediate_conflicts;
- for (const auto event : *this) {
+ for (const auto event : U) {
if (event->immediately_conflicts_with(e)) {
- immediate_conflicts.insert(e);
+ immediate_conflicts.insert(event);
}
}
return immediate_conflicts;
namespace simgrid::mc::udpor {
class Unfolding {
+public:
+ Unfolding() = default;
+ Unfolding& operator=(Unfolding&&) = default;
+ Unfolding(Unfolding&&) = default;
+
+ auto begin() const { return this->event_handles.begin(); }
+ auto end() const { return this->event_handles.end(); }
+ auto cbegin() const { return this->event_handles.cbegin(); }
+ auto cend() const { return this->event_handles.cend(); }
+ size_t size() const { return this->event_handles.size(); }
+ bool empty() const { return this->event_handles.empty(); }
+
+ /**
+ * @brief Moves an event from UDPOR's global set `U` to
+ * the global set `G`
+ */
+ void mark_finished(const UnfoldingEvent* e);
+
+ /**
+ * @brief Moves all events in a set from UDPOR's global
+ * set `U` to the global set `G`
+ */
+ void mark_finished(const EventSet& events);
+
+ /// @brief Adds a new event `e` to the Unfolding if that
+ /// event is not equivalent to any of those already contained
+ /// in the unfolding
+ const UnfoldingEvent* insert(std::unique_ptr<UnfoldingEvent> e);
+
+ /**
+ * @brief Informs the unfolding of a (potentially) new event
+ *
+ * The unfolding of a concurrent program is a well-defined
+ * structure. Given the labeled transition system (LTS) of
+ * a program, the unfolding of that program can be determined
+ * algorithmically. However, UDPOR does not a priori know the structure of the
+ * unfolding as it performs its exploration. Thus, events in the
+ * unfolding are "discovered" as they are encountered, specifically
+ * when computing the extension sets of the configurations that
+ * UDPOR decides to search.
+ *
+ * This lends itself to the following problem: the extension sets
+ * of two different configurations may overlap one another. That
+ * is, for two configurations C and C' explored by UDPOR where C != C',
+ *
+ * ex(C) - ex(C') != empty
+ *
+ * Hence, when extending both `C` and `C'`, any events contained in
+ * the intersection of ex(C) and ex(C') will be attempted to be added
+ * twice. The unfolding will notice that these events have already
+ * been added and simply return the event already added to the unfolding
+ *
+ * @tparam ...Args arguments passed to the `UnfoldingEvent` constructor
+ * @return the handle to either the newly created event OR
+ * to an equivalent event that was already noted by the unfolding
+ * at some point in the past
+ */
+ template <typename... Args> const UnfoldingEvent* discover_event(Args... args)
+ {
+ auto candidate_event = std::make_unique<UnfoldingEvent>(std::forward<Args>(args)...);
+ return insert(std::move(candidate_event));
+ }
+
+ /// @brief Computes "#ⁱ_U(e)" for the given event, where `U` is the set
+ /// of the events in this unfolding
+ EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
+
private:
/**
* @brief All of the events that are currently are a part of the unfolding
*
* @invariant Each unfolding event maps itself to the owner of that event,
- * i.e. the unique pointer that owns the address. The Unfolding owns all
+ * i.e. the unique pointer that manages the data at the address. The Unfolding owns all
* of the addresses that are referenced by EventSet instances and Configuration
* instances. UDPOR guarantees that events are persisted for as long as necessary
*/
*
* @invariant: All of the events in this set are elements of `global_events_`
* and is kept updated at the same time as `global_events_`
+ *
+ * @note: This is for the convenience of iteration over the unfolding
*/
EventSet event_handles;
+ /**
+ * @brief: The collection of events in the unfolding that are "important"
+ */
+ EventSet U;
+
/**
* @brief The "irrelevant" portions of the unfolding that do not need to be kept
* around to ensure that UDPOR functions correctly
*
* The set `G` is another global variable maintained by the UDPOR algorithm which
* is used to keep track of all events which used to be important to UDPOR.
- *
- * @note: The current implementation does not touch the set `G`. Its use is perhaps
- * limited to debugging and/or model-checking acyclic state spaces
*/
EventSet G;
-
-public:
- Unfolding() = default;
- Unfolding& operator=(Unfolding&&) = default;
- Unfolding(Unfolding&&) = default;
-
- void remove(const UnfoldingEvent* e);
- void remove(const EventSet& events);
- void insert(std::unique_ptr<UnfoldingEvent> e);
- bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
-
- auto begin() const { return this->event_handles.begin(); }
- auto end() const { return this->event_handles.end(); }
- auto cbegin() const { return this->event_handles.cbegin(); }
- auto cend() const { return this->event_handles.cend(); }
- size_t size() const { return this->global_events_.size(); }
- bool empty() const { return this->global_events_.empty(); }
-
- /// @brief Computes "#ⁱ_U(e)" for the given event
- EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
};
} // namespace simgrid::mc::udpor
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include <xbt/asserts.h>
+#include <xbt/log.h>
+#include <xbt/string.hpp>
+
namespace simgrid::mc::udpor {
UnfoldingEvent::UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> init_list)
bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
{
+ // Intrinsic identity check
+ if (this == &other) {
+ return true;
+ }
// Two events are equivalent iff:
// 1. they have the same action
// 2. they have the same history
this->immediate_causes == other.immediate_causes;
}
+std::string UnfoldingEvent::to_string() const
+{
+ std::string dependencies_string;
+
+ dependencies_string += "[";
+ for (const auto* e : immediate_causes) {
+ dependencies_string += e->to_string();
+ }
+ dependencies_string += "]";
+
+ return xbt::string_printf("(%p) Actor %ld: %s (%zu dependencies: %s)", this, associated_transition->aid_,
+ associated_transition->to_string().c_str(), immediate_causes.size(),
+ dependencies_string.c_str());
+}
+
EventSet UnfoldingEvent::get_history() const
+{
+ EventSet local_config = get_local_config();
+ local_config.remove(this);
+ return local_config;
+}
+
+EventSet UnfoldingEvent::get_local_config() const
{
return History(this).get_all_events();
}
return false;
}
- const EventSet my_history = get_history();
- const EventSet other_history = other->get_history();
+ const EventSet my_history = get_local_config();
+ const EventSet other_history = other->get_local_config();
const EventSet unique_to_me = my_history.subtracting(other_history);
const EventSet unique_to_other = other_history.subtracting(my_history);
return conflicts_with_me or conflicts_with_other;
}
-bool UnfoldingEvent::conflicts_with(const Configuration& config) const
+bool UnfoldingEvent::conflicts_with_any(const EventSet& events) const
{
- // A configuration is itself already conflict-free. Thus, it is
- // simply a matter of testing whether or not the transition associated
- // with the event is dependent with any already in `config` that are
- // OUTSIDE this event's history (in an unfolding, events only conflict
- // if they are not related)
- const EventSet potential_conflicts = config.get_events().subtracting(get_history());
- return std::any_of(potential_conflicts.cbegin(), potential_conflicts.cend(),
- [&](const UnfoldingEvent* e) { return this->is_dependent_with(e); });
+ return std::any_of(events.begin(), events.end(), [&](const auto e) { return e->conflicts_with(this); });
}
bool UnfoldingEvent::immediately_conflicts_with(const UnfoldingEvent* other) const
UnfoldingEvent(UnfoldingEvent&&) = default;
EventSet get_history() const;
+ EventSet get_local_config() const;
bool in_history_of(const UnfoldingEvent* other) const;
+
+ /**
+ * @brief Whether or not the given event is a decendant
+ * of or an ancestor of the given event
+ */
bool related_to(const UnfoldingEvent* other) const;
/// @brief Whether or not this event is in conflict with
bool conflicts_with(const UnfoldingEvent* other) const;
/// @brief Whether or not this event is in conflict with
- /// any event in the given configuration
- bool conflicts_with(const Configuration& config) const;
+ /// any event in the given set
+ bool conflicts_with_any(const EventSet& events) const;
/// @brief Computes "this #ⁱ other"
bool immediately_conflicts_with(const UnfoldingEvent* other) const;
const EventSet& get_immediate_causes() const { return this->immediate_causes; }
Transition* get_transition() const { return this->associated_transition.get(); }
+ aid_t get_actor() const { return get_transition()->aid_; }
+
+ void set_transition(std::shared_ptr<Transition> t) { this->associated_transition = std::move(t); }
+
+ std::string to_string() const;
bool operator==(const UnfoldingEvent&) const;
bool operator!=(const UnfoldingEvent& other) const { return not(*this == other); }
// e4 e5 e7
//
// e5 and e6 are in conflict, e5 and e7 are in conflict, e2 and e6, and e2 ands e7 are in conflict
- UnfoldingEvent e1(EventSet(), std::make_shared<ConditionallyDependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<DependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<ConditionallyDependentAction>());
- UnfoldingEvent e5(EventSet({&e3}), std::make_shared<DependentAction>());
- UnfoldingEvent e6(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>());
- UnfoldingEvent e7(EventSet({&e6, &e2}), std::make_shared<ConditionallyDependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<ConditionallyDependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<DependentAction>(0));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<ConditionallyDependentAction>(1));
+ UnfoldingEvent e5(EventSet({&e3}), std::make_shared<DependentAction>(1));
+ UnfoldingEvent e6(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>(2));
+ UnfoldingEvent e7(EventSet({&e6, &e2}), std::make_shared<ConditionallyDependentAction>(3));
SECTION("Dependency relation properties")
{
}
}
- SECTION("No conflicts whatsoever")
+ SECTION("Testing with no dependencies whatsoever")
{
// The following tests concern the given event structure:
// e1
// e3 / /
// / / /
// e4 e5 e7
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e7(EventSet({&e6, &e2}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e6(EventSet({&e1}), std::make_shared<IndependentAction>(5));
+ UnfoldingEvent e7(EventSet({&e6, &e2}), std::make_shared<IndependentAction>(6));
// Since everyone's actions are independent of one another, we expect
- // that there are no conflicts between each pair of events
+ // that there are no conflicts between each pair of events (except with
+ // the same event itself)
SECTION("Mutual dependencies")
{
- CHECK_FALSE(e1.is_dependent_with(&e1));
+ CHECK(e1.is_dependent_with(&e1));
CHECK_FALSE(e1.is_dependent_with(&e2));
CHECK_FALSE(e1.is_dependent_with(&e3));
CHECK_FALSE(e1.is_dependent_with(&e4));
CHECK_FALSE(e1.is_dependent_with(&e6));
CHECK_FALSE(e1.is_dependent_with(&e7));
- CHECK_FALSE(e2.is_dependent_with(&e2));
+ CHECK(e2.is_dependent_with(&e2));
CHECK_FALSE(e2.is_dependent_with(&e3));
CHECK_FALSE(e2.is_dependent_with(&e4));
CHECK_FALSE(e2.is_dependent_with(&e5));
CHECK_FALSE(e2.is_dependent_with(&e6));
CHECK_FALSE(e2.is_dependent_with(&e7));
- CHECK_FALSE(e3.is_dependent_with(&e3));
+ CHECK(e3.is_dependent_with(&e3));
CHECK_FALSE(e3.is_dependent_with(&e4));
CHECK_FALSE(e3.is_dependent_with(&e5));
CHECK_FALSE(e3.is_dependent_with(&e6));
CHECK_FALSE(e3.is_dependent_with(&e7));
- CHECK_FALSE(e4.is_dependent_with(&e4));
+ CHECK(e4.is_dependent_with(&e4));
CHECK_FALSE(e4.is_dependent_with(&e5));
CHECK_FALSE(e4.is_dependent_with(&e6));
CHECK_FALSE(e4.is_dependent_with(&e7));
- CHECK_FALSE(e5.is_dependent_with(&e5));
+ CHECK(e5.is_dependent_with(&e5));
CHECK_FALSE(e5.is_dependent_with(&e6));
CHECK_FALSE(e5.is_dependent_with(&e7));
- CHECK_FALSE(e6.is_dependent_with(&e6));
+ CHECK(e6.is_dependent_with(&e6));
CHECK_FALSE(e6.is_dependent_with(&e7));
- CHECK_FALSE(e7.is_dependent_with(&e7));
+ CHECK(e7.is_dependent_with(&e7));
}
SECTION("Mutual conflicts")
}
}
- SECTION("General conflicts")
+ SECTION("Testing with some conflicts")
{
// The following tests concern the given event structure:
// e1
// e3 / /
// / / /
// e4 e5 e7
- UnfoldingEvent e1(EventSet(), std::make_shared<DependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<DependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e1}), std::make_shared<IndependentAction>());
- UnfoldingEvent e7(EventSet({&e6, &e2}), std::make_shared<ConditionallyDependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<DependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<DependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e6(EventSet({&e1}), std::make_shared<IndependentAction>(5));
+ UnfoldingEvent e7(EventSet({&e6, &e2}), std::make_shared<ConditionallyDependentAction>(6));
// Since everyone's actions are independent of one another, we expect
- // that there are no conflicts between each pair of events
+ // that there are no conflicts between each pair of events (except the pair
+ // with the event and itself)
SECTION("Mutual dependencies")
{
CHECK(e1.is_dependent_with(&e1));
CHECK_FALSE(e2.is_dependent_with(&e6));
CHECK(e2.is_dependent_with(&e7));
- CHECK_FALSE(e3.is_dependent_with(&e3));
+ CHECK(e3.is_dependent_with(&e3));
CHECK_FALSE(e3.is_dependent_with(&e4));
CHECK_FALSE(e3.is_dependent_with(&e5));
CHECK_FALSE(e3.is_dependent_with(&e6));
CHECK_FALSE(e3.is_dependent_with(&e7));
- CHECK_FALSE(e4.is_dependent_with(&e4));
+ CHECK(e4.is_dependent_with(&e4));
CHECK_FALSE(e4.is_dependent_with(&e5));
CHECK_FALSE(e4.is_dependent_with(&e6));
CHECK_FALSE(e4.is_dependent_with(&e7));
- CHECK_FALSE(e5.is_dependent_with(&e5));
+ CHECK(e5.is_dependent_with(&e5));
CHECK_FALSE(e5.is_dependent_with(&e6));
CHECK_FALSE(e5.is_dependent_with(&e7));
- CHECK_FALSE(e6.is_dependent_with(&e6));
+ CHECK(e6.is_dependent_with(&e6));
CHECK_FALSE(e6.is_dependent_with(&e7));
- CHECK_FALSE(e7.is_dependent_with(&e7));
+ CHECK(e7.is_dependent_with(&e7));
}
SECTION("Mutual conflicts")
// e3 /
// / / e7
// e4 e5
- UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
- UnfoldingEvent e2(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>());
- UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>());
- UnfoldingEvent e6(EventSet({&e1}), std::make_shared<DependentAction>());
- UnfoldingEvent e7(EventSet({&e6}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>(1));
+ UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(3));
+ UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>(4));
+ UnfoldingEvent e6(EventSet({&e1}), std::make_shared<DependentAction>(5));
+ UnfoldingEvent e7(EventSet({&e6}), std::make_shared<IndependentAction>(6));
CHECK_FALSE(e1.conflicts_with(&e1));
CHECK_FALSE(e1.conflicts_with(&e2));
REQUIRE(unfolding.empty());
}
-TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an unfolding")
+TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and marking events with an unfolding")
{
Unfolding unfolding;
- auto e1 = std::make_unique<UnfoldingEvent>();
- auto e2 = std::make_unique<UnfoldingEvent>();
+ auto e1 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 0));
+ auto e2 =
+ std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1));
const auto e1_handle = e1.get();
const auto e2_handle = e2.get();
REQUIRE(unfolding.size() == 2);
REQUIRE_FALSE(unfolding.empty());
- unfolding.remove(e1_handle);
- REQUIRE(unfolding.size() == 1);
+ unfolding.mark_finished(e1_handle);
+ REQUIRE(unfolding.size() == 2);
REQUIRE_FALSE(unfolding.empty());
- unfolding.remove(e2_handle);
- REQUIRE(unfolding.size() == 0);
- REQUIRE(unfolding.empty());
-}
-
-TEST_CASE("simgrid::mc::udpor::Unfolding: Checking for semantically equivalent events")
-{
- Unfolding unfolding;
- auto e1 = std::make_unique<UnfoldingEvent>(
- EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
- auto e2 = std::make_unique<UnfoldingEvent>(
- EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
-
- // e1 and e2 are equivalent
- REQUIRE(*e1 == *e2);
-
- const auto e1_handle = e1.get();
- const auto e2_handle = e2.get();
- unfolding.insert(std::move(e1));
-
- REQUIRE(unfolding.contains_event_equivalent_to(e1_handle));
- REQUIRE(unfolding.contains_event_equivalent_to(e2_handle));
+ unfolding.mark_finished(e2_handle);
+ REQUIRE(unfolding.size() == 2);
+ REQUIRE_FALSE(unfolding.empty());
}
TEST_CASE("simgrid::mc::udpor::Unfolding: Checking all immediate conflicts restricted to an unfolding") {}
\ No newline at end of file
void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(const UnfoldingEvent* e)
{
- const auto e_history = e->get_history();
- for (const auto e_hist : e_history) {
+ const auto e_local_config = e->get_local_config();
+ for (const auto e_hist : e_local_config) {
event_counts[e_hist]++;
}
}
void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(const UnfoldingEvent* e)
{
- const auto e_history = e->get_history();
- for (const auto e_hist : e_history) {
+ const auto e_local_config = e->get_local_config();
+ for (const auto e_hist : e_local_config) {
xbt_assert(event_counts.find(e_hist) != event_counts.end(),
"Invariant Violation: Attempted to remove an event which was not previously added");
xbt_assert(event_counts[e_hist] > 0, "Invariant Violation: An event `e` had a count of `0` at this point "
using node_filter_function = std::function<bool(const UnfoldingEvent*)>;
using topological_order_position = std::vector<const UnfoldingEvent*>::const_iterator;
- maximal_subsets_iterator() = default;
+ maximal_subsets_iterator() = default;
+ maximal_subsets_iterator(maximal_subsets_iterator&&) noexcept = 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)
public:
using topological_order_position = maximal_subsets_iterator::topological_order_position;
+ bookkeeper() = default;
+ bookkeeper(bookkeeper&&) = default;
+ bookkeeper& operator=(bookkeeper&) = default;
+ bookkeeper& operator=(bookkeeper&&) = default;
+
void mark_included_in_maximal_set(const UnfoldingEvent*);
void mark_removed_from_maximal_set(const UnfoldingEvent*);
topological_order_position find_next_candidate_event(topological_order_position first,
#ifndef SIMGRID_MC_UDPOR_FORWARD_HPP
#define SIMGRID_MC_UDPOR_FORWARD_HPP
+#include "src/mc/mc_forward.hpp"
+#include <simgrid/forward.h>
+
namespace simgrid::mc::udpor {
+class Comb;
+class ExtensionSetCalculator;
class EventSet;
class Configuration;
class History;
struct IndependentAction : public Transition {
IndependentAction() = default;
- IndependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+ IndependentAction(Type type, aid_t issuer, int times_considered = 0) : Transition(type, issuer, times_considered) {}
+ IndependentAction(aid_t issuer, int times_considered = 0)
+ : IndependentAction(simgrid::mc::Transition::Type::UNKNOWN, issuer, times_considered)
+ {
+ }
- // Independent with everyone else
- bool depends(const Transition* other) const override { return false; }
+ // Independent with everyone else (even if run by the same actor). NOTE: This is
+ // only for the convenience of testing: in general, transitions are dependent with
+ // one another if run by the same actor
+ bool depends(const Transition* other) const override
+ {
+ if (aid_ == other->aid_) {
+ return true;
+ }
+ return false;
+ }
};
struct DependentAction : public Transition {
DependentAction() = default;
- DependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+ DependentAction(Type type, aid_t issuer, int times_considered = 0) : Transition(type, issuer, times_considered) {}
+ DependentAction(aid_t issuer, int times_considered = 0)
+ : DependentAction(simgrid::mc::Transition::Type::UNKNOWN, issuer, times_considered)
+ {
+ }
// Dependent with everyone else (except IndependentAction)
bool depends(const Transition* other) const override
{
+ if (aid_ == other->aid_) {
+ return true;
+ }
return dynamic_cast<const IndependentAction*>(other) == nullptr;
}
};
struct ConditionallyDependentAction : public Transition {
ConditionallyDependentAction() = default;
- ConditionallyDependentAction(Type type, aid_t issuer, int times_considered)
+ ConditionallyDependentAction(Type type, aid_t issuer, int times_considered = 0)
: Transition(type, issuer, times_considered)
{
}
+ ConditionallyDependentAction(aid_t issuer, int times_considered = 0)
+ : ConditionallyDependentAction(simgrid::mc::Transition::Type::UNKNOWN, issuer, times_considered)
+ {
+ }
// Dependent only with DependentAction (i.e. not itself)
bool depends(const Transition* other) const override
{
+ if (aid_ == other->aid_) {
+ return true;
+ }
return dynamic_cast<const DependentAction*>(other) != nullptr;
}
};
[](bool) { _mc_cfg_cb_check("value to enable/disable the use of sleep-set in the reduction algorithm"); }};
simgrid::config::Flag<std::string> _sg_mc_strategy{
- "model-check/strategy", "Specify the the kind of heuristic to use for guided model-checking", "none",
- [](std::string_view value) {
- if (value != "none" && value != "nb_wait")
- xbt_die("configuration option 'model-check/guided-mc' can only take 'none' or 'nb_wait' as a 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."},
+ {"nb_wait", "Take any enabled wait transition, to reduce the distance between an async and its wait."}}};
#if SIMGRID_HAVE_STATEFUL_MC
simgrid::config::Flag<int> _sg_mc_checkpoint{
#include "xbt/base.h"
#include <exception>
-constexpr int SIMGRID_MC_EXIT_SUCCESS = 0;
-constexpr int SIMGRID_MC_EXIT_SAFETY = 1;
-constexpr int SIMGRID_MC_EXIT_LIVENESS = 2;
-constexpr int SIMGRID_MC_EXIT_DEADLOCK = 3;
-constexpr int SIMGRID_MC_EXIT_NON_TERMINATION = 4;
-constexpr int SIMGRID_MC_EXIT_NON_DETERMINISM = 5;
-constexpr int SIMGRID_MC_EXIT_PROGRAM_CRASH = 6;
-
-constexpr int SIMGRID_MC_EXIT_ERROR = 63;
-
namespace simgrid::mc {
-class XBT_PUBLIC DeadlockError : public std::exception {
-};
-class XBT_PUBLIC TerminationError : public std::exception {
+
+enum class ExitStatus {
+ SUCCESS = 0,
+ SAFETY = 1,
+ LIVENESS = 2,
+ DEADLOCK = 3,
+ NON_TERMINATION = 4,
+ NON_DETERMINISM = 5,
+ PROGRAM_CRASH = 6,
+ ERROR = 63
};
-class XBT_PUBLIC LivenessError : public std::exception {
+
+struct McError : public std::exception {
+ const ExitStatus value;
+ explicit McError(ExitStatus v = ExitStatus::ERROR) : value(v) {}
};
} // namespace simgrid::mc
{
std::ostringstream stream;
for (auto i = transitions_.begin(); i != transitions_.end(); ++i) {
+ if (*i == nullptr)
+ continue;
if (i != transitions_.begin())
stream << ';';
stream << (*i)->aid_;
s_mc_message_int_t answer = {};
answer.type = MessageType::DEADLOCK_CHECK_REPLY;
answer.value = deadlock;
- xbt_assert(channel_.send(answer) == 0, "Could not send response");
+ xbt_assert(channel_.send(answer) == 0, "Could not send response: %s", strerror(errno));
}
void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const
{
// The client may send some messages to the server while processing the transition
actor->simcall_handle(message->times_considered_);
// Say the server that the transition is over and that it should proceed
- xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker");
+ xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker: %s",
+ strerror(errno));
// Finish the RPC from the server: return a serialized observer, to build a Transition on Checker side
s_mc_message_simcall_execute_answer_t answer = {};
answer.buffer.back() = '\0';
XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> '%s'", actor->get_cname(), str.c_str());
- xbt_assert(channel_.send(answer) == 0, "Could not send response");
+ xbt_assert(channel_.send(answer) == 0, "Could not send response: %s", strerror(errno));
}
void AppSide::handle_finalize(const s_mc_message_int_t* msg) const
#endif
}
coverage_checkpoint();
- xbt_assert(channel_.send(MessageType::FINALIZE_REPLY) == 0, "Could not answer to FINALIZE");
+ xbt_assert(channel_.send(MessageType::FINALIZE_REPLY) == 0, "Could not answer to FINALIZE: %s", strerror(errno));
std::fflush(stdout);
if (terminate_asap)
::_Exit(0);
s_mc_message_need_meminfo_reply_t answer = {};
answer.type = MessageType::NEED_MEMINFO_REPLY;
answer.mmalloc_default_mdp = mmalloc_get_current_heap();
- xbt_assert(channel_.send(answer) == 0, "Could not send response to the request for meminfo.");
+ xbt_assert(channel_.send(answer) == 0, "Could not send response to the request for meminfo: %s", strerror(errno));
#else
xbt_die("SimGrid was compiled without MC suppport, so liveness and similar features are not available.");
#endif
answer.type = MessageType::ACTORS_STATUS_REPLY_COUNT;
answer.count = static_cast<int>(status.size());
- xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg");
+ xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg: %s", strerror(errno));
if (answer.count > 0) {
size_t size = status.size() * sizeof(s_mc_message_actors_status_one_t);
- xbt_assert(channel_.send(status.data(), size) == 0, "Could not send ACTORS_STATUS_REPLY data");
+ xbt_assert(channel_.send(status.data(), size) == 0, "Could not send ACTORS_STATUS_REPLY data: %s", strerror(errno));
}
// Serialize each transition to describe what each actor is doing
XBT_DEBUG("Deliver ACTOR_TRANSITION_PROBE payload");
for (const auto& actor_status : status) {
- if (not actor_status.enabled)
- continue;
const auto& actor = actor_list.at(actor_status.aid);
const int max_considered = actor_status.max_considered;
strncpy(probe.buffer.data(), str.c_str(), probe.buffer.size() - 1);
probe.buffer.back() = '\0';
- xbt_assert(channel_.send(probe) == 0, "Could not send ACTOR_TRANSITION_PROBE payload");
+ xbt_assert(channel_.send(probe) == 0, "Could not send ACTOR_TRANSITION_PROBE payload: %s", strerror(errno));
}
// NOTE: We do NOT need to reset `times_considered` for each actor's
// simcall observer here to the "original" value (i.e. the value BEFORE
s_mc_message_int_t answer = {};
answer.type = MessageType::ACTORS_MAXPID_REPLY;
answer.value = kernel::actor::ActorImpl::get_maxpid();
- xbt_assert(channel_.send(answer) == 0, "Could not send response");
+ xbt_assert(channel_.send(answer) == 0, "Could not send response: %s", strerror(errno));
}
#define assert_msg_size(_name_, _type_) \
XBT_DEBUG("Socket closed on the Checker side, bailing out.");
::_Exit(0); // Nobody's listening to that process anymore => exit as quickly as possible.
}
- xbt_assert(received_size >= 0, "Could not receive commands from the model-checker");
+ xbt_assert(received_size >= 0, "Could not receive commands from the model-checker: %s", strerror(errno));
xbt_assert(static_cast<size_t>(received_size) >= sizeof(s_mc_message_t), "Cannot handle short message (size=%zd)",
received_size);
sthread_enable();
while (true) {
simgrid::mc::execute_actors();
- xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send WAITING message to model-checker");
+ xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send WAITING message to model-checker: %s",
+ strerror(errno));
this->handle_messages();
}
}
void AppSide::report_assertion_failure()
{
- xbt_assert(channel_.send(MessageType::ASSERTION_FAILED) == 0, "Could not send assertion to model-checker");
+ xbt_assert(channel_.send(MessageType::ASSERTION_FAILED) == 0, "Could not send assertion to model-checker: %s",
+ strerror(errno));
this->handle_messages();
}
message.type = MessageType::IGNORE_MEMORY;
message.addr = (std::uintptr_t)addr;
message.size = size;
- xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_MEMORY message to model-checker");
+ xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_MEMORY message to model-checker: %s", strerror(errno));
#else
xbt_die("Cannot really call ignore_heap() in non-SIMGRID_MC mode.");
#endif
heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++;
}
- xbt_assert(channel_.send(message) == 0, "Could not send ignored region to MCer");
+ xbt_assert(channel_.send(message) == 0, "Could not send ignored region to MCer: %s", strerror(errno));
#else
xbt_die("Cannot really call ignore_heap() in non-SIMGRID_MC mode.");
#endif
message.type = MessageType::UNIGNORE_HEAP;
message.addr = (std::uintptr_t)address;
message.size = size;
- xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_HEAP message to model-checker");
+ xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_HEAP message to model-checker: %s", strerror(errno));
#else
xbt_die("Cannot really call unignore_heap() in non-SIMGRID_MC mode.");
#endif
strncpy(message.name.data(), name, message.name.size() - 1);
message.callback = nullptr;
message.data = value;
- xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker");
+ xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker: %s", strerror(errno));
#else
xbt_die("Cannot really call declare_symbol() in non-SIMGRID_MC mode.");
#endif
s_mc_message_stack_region_t message = {};
message.type = MessageType::STACK_REGION;
message.stack_region = region;
- xbt_assert(channel_.send(message) == 0, "Could not send STACK_REGION to model-checker");
+ xbt_assert(channel_.send(message) == 0, "Could not send STACK_REGION to model-checker: %s", strerror(errno));
#else
xbt_die("Cannot really call declare_stack() in non-SIMGRID_MC mode.");
#endif
else if (type == RegionType::Heap)
xbt_assert(not object_info, "Unexpected object info for heap region.");
- auto* region = new Region(page_store_, memory, type, start_addr, size);
+ auto region = std::make_unique<Region>(page_store_, memory, type, start_addr, size);
region->object_info(object_info);
- snapshot_regions_.push_back(std::unique_ptr<Region>(region));
+ snapshot_regions_.push_back(std::move(region));
}
void* Snapshot::read_bytes(void* buffer, std::size_t size, RemotePtr<void> address, ReadOptions options) const
size_t size;
void* src;
void* dstn;
- Region* region0;
- Region* region;
+ std::unique_ptr<Region> region0;
+ std::unique_ptr<Region> region;
};
static prologue_return prologue(int n); // common to the below 5 fxs
static void read_whole_region();
// Init memory and take snapshots:
init_memory(source, byte_size);
- auto* region0 =
- new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
+ auto region0 = std::make_unique<simgrid::mc::Region>(page_store_, *memory_.get(), simgrid::mc::RegionType::Data,
+ source, byte_size);
for (int i = 0; i < n; i += 2) {
init_memory((char*)source + i * xbt_pagesize, xbt_pagesize);
}
- auto* region = new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
+ auto region = std::make_unique<simgrid::mc::Region>(page_store_, *memory_.get(), simgrid::mc::RegionType::Data,
+ source, byte_size);
void* destination = mmap(nullptr, byte_size, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
INFO("Could not allocate destination memory");
REQUIRE(destination != MAP_FAILED);
- return {.size = byte_size, .src = source, .dstn = destination, .region0 = region0, .region = region};
+ return {.size = byte_size,
+ .src = source,
+ .dstn = destination,
+ .region0 = std::move(region0),
+ .region = std::move(region)};
}
void snap_test_helper::read_whole_region()
munmap(ret.dstn, ret.size);
munmap(ret.src, ret.size);
- delete ret.region0;
- delete ret.region;
}
}
}
munmap(ret.dstn, ret.size);
munmap(ret.src, ret.size);
- delete ret.region0;
- delete ret.region;
}
}
prologue_return ret = prologue(n);
INFO("Unexpected match in MC_snapshot_region_memcmp() with previous snapshot");
- REQUIRE(MC_snapshot_region_memcmp(ret.src, ret.region0, ret.src, ret.region, ret.size));
+ REQUIRE(MC_snapshot_region_memcmp(ret.src, ret.region0.get(), ret.src, ret.region.get(), ret.size));
munmap(ret.dstn, ret.size);
munmap(ret.src, ret.size);
- delete ret.region0;
- delete ret.region;
}
}
size_t size = simgrid::xbt::random::uniform_int(0, ret.size - offset - 1);
INFO("Mismatch in MC_snapshot_region_memcmp()");
- REQUIRE(not MC_snapshot_region_memcmp((char*)ret.src + offset, ret.region, (char*)ret.src + offset, ret.region,
- size));
+ REQUIRE(not MC_snapshot_region_memcmp((char*)ret.src + offset, ret.region.get(), (char*)ret.src + offset,
+ ret.region.get(), size));
}
munmap(ret.dstn, ret.size);
munmap(ret.src, ret.size);
- delete ret.region0;
- delete ret.region;
}
}
munmap(ret.dstn, ret.size);
munmap(ret.src, ret.size);
- delete ret.region0;
- delete ret.region;
}
/*************** End: class snap_test_helper *****************************/
[this, profile]() { this->pimpl_->set_write_bandwidth_profile(profile); });
return this;
}
+int Disk::get_concurrency_limit() const
+{
+ return pimpl_->get_concurrency_limit();
+}
+
+Disk* Disk::set_concurrency_limit(int limit)
+{
+ kernel::actor::simcall_object_access(pimpl_, [this, limit] { pimpl_->set_concurrency_limit(limit); });
+ return this;
+}
IoPtr Disk::io_init(sg_size_t size, Io::OpType type) const
{
for (auto* l : linkImpls)
links.push_back(l->get_iface());
}
+std::pair<std::vector<Link*>, double> Host::route_to(const Host* dest) const
+{
+ std::vector<kernel::resource::StandardLinkImpl*> linkImpls;
+ std::vector<Link*> links;
+ double latency = 0;
+ this->route_to(dest, linkImpls, &latency);
+ for (auto* l : linkImpls)
+ links.push_back(l->get_iface());
+ return std::make_pair(links, latency);
+}
/** @brief Just like Host::routeTo, but filling an array of link implementations */
void Host::route_to(const Host* dest, std::vector<kernel::resource::StandardLinkImpl*>& links, double* latency) const
return this;
}
+int Host::get_concurrency_limit() const
+{
+ return pimpl_cpu_->get_concurrency_limit();
+}
+
+Host* Host::set_concurrency_limit(int limit)
+{
+ kernel::actor::simcall_object_access(pimpl_cpu_, [this, limit] { pimpl_cpu_->set_concurrency_limit(limit); });
+ return this;
+}
+
/** Specify a profile turning the host on and off according to an exhaustive list or a stochastic law.
* The profile must contain boolean values. */
Host* Host::set_state_profile(kernel::profile::Profile* p)
friend constexpr iterator_wrapping<IteratorType, Arguments...> make_iterator_wrapping_explicit(Arguments... args);
public:
- iterator_wrapping(Args&&... begin_iteration) : m_args(std::forward<ref_or_value_t<Args>>(begin_iteration)...) {}
+ iterator_wrapping(Args&&... begin_iteration) : m_args(ref_or_value_t<Args>(begin_iteration)...) {}
iterator_wrapping(const iterator_wrapping&) = delete;
iterator_wrapping(iterator_wrapping&&) = delete;
iterator_wrapping& operator=(const iterator_wrapping&) = delete;
template <typename Iterator, typename... Args>
constexpr iterator_wrapping<Iterator, Args...> make_iterator_wrapping_explicit(Args... args)
{
- return iterator_wrapping<Iterator, Args...>(std::forward<Args>(args)...);
+ return iterator_wrapping<Iterator, Args...>(args...);
}
} // namespace simgrid::xbt
template <class Iterator>
struct powerset_iterator : public boost::iterator_facade<powerset_iterator<Iterator>, const std::vector<Iterator>,
boost::forward_traversal_tag> {
- powerset_iterator() = default;
+ powerset_iterator() = default;
+ powerset_iterator(powerset_iterator<Iterator>&) noexcept = default;
+ powerset_iterator(powerset_iterator<Iterator>&&) noexcept = default;
+ powerset_iterator<Iterator>& operator=(powerset_iterator<Iterator>&&) noexcept = default;
+ powerset_iterator<Iterator>& operator=(const powerset_iterator<Iterator>&) noexcept = default;
explicit powerset_iterator(Iterator begin, Iterator end = Iterator());
private:
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 (!current_subset_iter.has_value() || !current_subset_iter_end.has_value() || !current_subset_iter.has_value() ||
+ !iterator_end.has_value()) {
return; // We've traversed all subsets at this point, or we're the "last" iterator
}
add_executable (${x} EXCLUDE_FROM_ALL ${x}/${x}.cpp)
target_link_libraries(${x} simgrid)
set_target_properties(${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${x})
- add_dependencies(tests ${x})
+ add_dependencies(tests-ns3 ${x})
ADD_TESH(tesh-s4u-${x} --setenv srcdir=${CMAKE_HOME_DIRECTORY}/teshsuite/s4u/${x} --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --cd ${CMAKE_BINARY_DIR}/teshsuite/s4u/${x} ${CMAKE_HOME_DIRECTORY}/teshsuite/s4u/${x}/${x}.tesh)
endforeach()
endif()
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/EventSet.cpp
src/mc/explo/udpor/EventSet.hpp
+ src/mc/explo/udpor/ExtensionSetCalculator.cpp
+ src/mc/explo/udpor/ExtensionSetCalculator.hpp
src/mc/explo/udpor/History.cpp
src/mc/explo/udpor/History.hpp
src/mc/explo/udpor/maximal_subsets_iterator.cpp
