The behavior of a MessageQueue is similar to that of a Mailbox, but intended for
control messages that do not incur any simulated cost. Information is automagically
transported over thin air between producer and consumer. See examples/cpp/mess-wait
+ - New function: Mutex::get_owner()
New S4U plugins:
- Add a JBOD (just a bunch of disks) concept. It's a sort of host with many disks.
- Revamp the battery plugin: rewrite completely the API, for a better usability.
The examples were updated accordingly.
The battery can now act as a simple connector (see battery-connector example).
- - Revamp of the Photovoltaic plugin: now called SolarPanel and complete rewrite of the API
+ - Revamp of the photovoltaic plugin: now called SolarPanel and complete rewrite of the API
- Add chiller plugin: enable the management of chillers consuming electrical energy
to compensate heat generated by hosts.
- Add a battery-chiller-solar example combining several plugins to evaluate the amount
- Memory usage due to SMPI for non-MPI actors greatly reduced.
sthread:
- - Allow to use on valgrind-observed processes
+ - Allow to use on valgrind-observed or gdb-observed processes.
- Install sthread on user's disk.
- Implement recursive pthreads.
- - Implement pthread_barrier and pthread_cond.
+ - Implement pthread_barrier and pthread_cond (but conditional are not supported by the MC yet).
- Add some McMini codes to test sthread further (controlled with enable_testsuite_McMini).
Model checking:
- Comm::waitall/waitany/testany() are gone. Please use ActivitySet() instead.
- Comm::waitallfor() is gone too. Its semantic was unclear on timeout anyway.
- Io::waitany() and waitanyfor() are gone. Please use ActivitySet() instead.
- - Add the bindings of the host load plugin
C API:
- Introduce sg_activity_set_t and deprecate wait_all/wait_any/test_any for
include teshsuite/mc/mcmini/simple_semaphores_with_threads_deadlock.tesh
include teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.c
include teshsuite/mc/mcmini/simple_semaphores_with_threads_ok.tesh
+include teshsuite/mc/mcmini/simple_threads_ok.c
+include teshsuite/mc/mcmini/simple_threads_ok.tesh
include teshsuite/mc/mutex-handling/mutex-handling.cpp
include teshsuite/mc/mutex-handling/mutex-handling.tesh
include teshsuite/mc/mutex-handling/without-mutex-handling.tesh
include src/mc/explo/odpor/Execution.cpp
include src/mc/explo/odpor/Execution.hpp
include src/mc/explo/odpor/Execution_test.cpp
-include src/mc/explo/odpor/ReversibleRaceCalculator.cpp
-include src/mc/explo/odpor/ReversibleRaceCalculator.hpp
include src/mc/explo/odpor/WakeupTree.cpp
include src/mc/explo/odpor/WakeupTree.hpp
include src/mc/explo/odpor/WakeupTreeIterator.cpp
\_/ \___|_| |___/_|\___/|_| |_| |____(_)____/____/
(not released yet)
+ * Maint: liveness checking is gone. It was fragile and buggy.
+ * API: ActivitySet make it easier to manage sets of activities.
+ * Plugins chiller, photovoltaic and battery revamped and improved.
+ * Performance improvements, both in time and memory.
+ * (+ internal refactoring, usability improvements and bug fixes)
_ _____ _____ _ _
__ _____ _ __ ___(_) ___ _ __ |___ / |___ /| || |
\ \ / / _ \ '__/ __| |/ _ \| '_ \ |_ \ |_ \| || |_
IPC and synchronization. Check `the examples <https://framagit.org/simgrid/simgrid/tree/master/examples/sthread>`_. In addition,
sthread can now also check concurrent accesses to a given collection, loosely inspired from `this paper
<https://www.microsoft.com/en-us/research/publication/efficient-and-scalable-thread-safety-violation-detection-finding-thousands-of-concurrency-bugs-during-testing>`_.
-This feature is not very usable yet, as you have to manually annotate your code, but we hope to improve it in the near future.
+This feature is not very usable yet, as you have to manually annotate your code, but we hope to improve it in the future.
Version 3.35 (TBD)
------------------
-**On the interface front**, we introduced a new MessageQueue abstraction and associated Mess simulated object. The behavior of a
-MessageQueue is similar to that of a Mailbox, but intended for control messages that do not incur any simulated cost.
-Information is automagically transported over thin air between producer and consumer. Internally, the implementation is very
-similar to Mailboxes and Comms, only simpler. The motivation for this new abstraction came from a scalability issue observed in
-the WRENCH framework, which is heavily based on control messages. When the simulated size of these messages is set to 0, it creates
-very short lived network actions (i.e., lasting for only the route latency) that tend to overwhelm the LMM. Switching from Mailbox
-to MessageQueue for such information exchange avoid this problem and greatly improves the scalability of WRENCH-based simulators.
+
+**On the performance front**, we did some profiling and optimisation for this release. We saved some memory in simulation
+mixing MPI applications and S4U actors, and we greatly improved the performance of simulation exchanging many messages. We even
+introduced a new abstraction called MessageQueue and associated Mess simulated object to represent control messages in a very
+efficient way. When using MessageQueue and Mess instead of Mailboxes and Comms, information is automagically transported over
+thin air between producer and consumer in no simulated time. The implementation is much simpler, yielding much better
+performance. Indeed, this abstraction solves a scalability issue observed in the WRENCH framework, which is heavily based on
+control messages.
+
+
+**On the interface front**, we introduced a new abstraction called ActivitySets. It makes it easy to interact with a bag of
+mixed activities, waiting for the next occurring one, or for the completion of the whole set. This feature already existed in
+SimGrid, but was implemented in a crude way with vectors of activities and static functions. It is also much easier than earlier
+to mix several kinds of activities in activity sets.
+
+We introduced a new plugin called JBOD (just a bunch of disks), that proves useful to represent a sort of hosts gathering many
+disks. We also revamped the battery, photovoltaic and chiller plugins introduced in previous release to make it even easier to
+study green computing scenarios. On a similar topic, we eased the expression of vertical scaling with the :ref:`Task
+<API_s4u_Tasks>`, the repeatable activities introduced in the previous release that can be used to represent microservices
+applications.
+
+We not only added new abstractions and plugins, but also polished the existing interfaces. For example, the declaration of
+multi-zoned platforms was greatly simplified by adding methods with fewer parameters to cover the common cases, leaving the
+complete methods for the more advanced use cases (see the ChangeLog for details). Another difficulty in the earlier interface
+was related to :ref:`Mailbox::get_async()` which used to require the user to store the payload somewhere on her side. Instead,
+it is now possible to retrieve the payload from the communication object once it's over with :ref:`Comm::get_payload()`.
+
+Finally on the SMPI front, we introduced :ref:`SMPI_app_instance_join()` to wait for the completion of a started MPI instance.
+This enables further mixture of MPI codes and controlled by S4U applications and plugins. We are currently considering
+implementing some MPI4 calls, but nothing happened so far.
+
+**On the model-checking front**, the first big news is that we completely removed the liveness checker from the code base. This
+is unfortunate, but the truth is that this code was very fragile and not really tested.
+
+For the context, liveness checking is the part of model checking that can determine whether the studied system always terminates
+(absence of infinite loops, called non-progression loops in this context), or whether the system can reach a desirable state in
+a finite time (for example, when you press the button, you want the elevator to come eventually). This relies on the ability to
+detect loops in the execution, most often through the detection that this system state was already explored earlier. SimGrid
+relied on tricks and heuristics to detect such state equality by leveraging debug information meant for gdb or valgrind. It
+kinda worked, but was very fragile because neither this information nor the compilation process are meant for state equality
+evaluation. Not zeroing the memory induces many crufty bits, for example in the padding bytes of the data structures or on the
+stack. This can be solved by only comparing the relevant bits (as instructed by the debug information), but this process was
+rather slow. Detecting equality in the stack was even more hackish, as we usually don't have any debug information about the
+memory blocks retrieved from malloc(). This prevents any introspection into these blocks, which is problematic because the order
+of malloc calls will create states that are syntactically different (the blocks are not in the same location in memory) but
+semantically equivalent (the data meaning rarely depends on the block location itself). The heuristics we used here were so
+crude that I don't want to detail them here.
+
+If liveness checking were to be re-implemented nowadays, I would go for a compiler-aided approach. I would maybe use a compiler
+plugin to save the type of malloced blocks as in `Compiler-aided type tracking for correctness checking of MPI applications
+<https://scholar.google.com/citations?view_op=view_citation&citation_for_view=dRhZFBsAAAAJ:9yKSN-GCB0IC>`_ and zero the stack on
+call returns to ease introspection. We could even rely on a complete introspection mechanism such as `MetaCPP
+<https://github.com/mlomb/MetaCPP>`_ or similar. We had a great piece of code to checkpoint millions of states in a
+memory-efficient way. It was able to detect the common memory pages between states, and only save the modified ones. I guess
+that this would need to be exhumed from the git when reimplementing liveness checking in SimGrid. But I doubt that we will
+happen anytime soon, as we concentrate our scarce manpower on other parts. In particular, safety checking is about searching for
+failed assertions by inspecting each state. A counter example to a safety property is simply a state where the assertion failed
+/ the property is violated. A counter example to a liveness property is an infinite execution path that violates the property.
+In some sense, safety checking is much easier than liveness checking, but it's already very powerful to exhaustively test an
+application.
+
+In this release, we made several interesting progress on the safety side of model checking. First, we ironed out many bugs in
+the ODPOR exploration algorithm (and dependency and reversible race theorems on which it relies). ODPOR should now be usable,
+and it's much faster than our previous DPOR reduction. We also extended sthread a bit, by adding many tests from the McMini tool
+and by implementing pthread barriers and conditionals. It seems to work rather well with C codes using pthreads and with C++
+codes using the standard library. You can even use sthread on a process running in valgrind or gdb.
+
+Unfortunately, conditionals cannot be verified so far by the model checker, because our implementation of condition variables is
+still synchronous. Our reduction algorithms are optimized because we know that all transitions of our computation model are
+persistent: once a transition gets enabled, it remains so until it's actually fired. This enables to build upon previous
+computations, while everything must be recomputed in each state when previously enabled transitions can get disabled by an
+external event. Unfortunately, this requires that every activity is written in an asynchronous way. You first declare your
+intent to lock that mutex in an asynchronous manner, and then wait for the ongoing_acquisition object. Once a given acquisition
+is granted, it will always remain so even if another actor creates another acquisition on the same mutex. This is the equivalent
+of asynchronous communications that are common in MPI, but for mutex locks, barriers and semaphores. The thing that is missing
+to verify pthread_cond in sthread is that I didn't manage to write an asynchronous version of the condition variables. We have an
+almost working code lying around, but it fails for timed waits on condition variables. This will probably be part of the next
+release.
.. |br| raw:: html
XBT_INFO("Completed a Comm");
if (sg_exec_isinstance(completed_one))
XBT_INFO("Completed an Exec");
+ sg_activity_unref(completed_one);
} else {
XBT_INFO("Nothing matches, test again in 0.5s");
sg_actor_sleep_for(.5);
XBT_INFO("Wait for asynchronous activities to complete, all in one shot.");
sg_activity_set_wait_all(pending_activities);
+ sg_activity_unref((sg_activity_t)exec);
+ sg_activity_unref((sg_activity_t)comm);
XBT_INFO("All activities are completed.");
free(payload);
XBT_INFO("Completed a Comm");
if (sg_exec_isinstance(completed_one))
XBT_INFO("Completed an Exec");
+ sg_activity_unref(completed_one);
completed_one = sg_activity_set_test_any(pending_activities);
}
}
XBT_INFO("Completed an Exec");
else
xbt_die("This activity set is supposed to only contain Comm or Exec");
+ sg_activity_unref(completed_one);
}
XBT_INFO("Last activity is complete");
free(payload);
XBT_LOG_NEW_DEFAULT_CATEGORY(jbod_test, "Messages specific for this simulation");
namespace sg4 = simgrid::s4u;
-static void write_then_read(simgrid::plugin::Jbod* jbod)
+static void write_then_read(simgrid::plugin::JbodPtr jbod)
{
simgrid::plugin::JbodIoPtr io = jbod->write_async(1e7);
XBT_INFO("asynchronous write posted, wait for it");
// set up link so that data transfer from host to JBOD takes exactly 1 second (without crosstraffic)
auto* link = zone->create_link("link", 1e7/0.97)->set_latency(0);
- auto* jbod_raid0 =
- simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid0", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID0, 1e7, 5e6);
- zone->add_route(host, jbod_raid0, {link});
+ auto jbod_raid0 =
+ simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid0", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID0, 1e7, 5e6);
+ zone->add_route(host, jbod_raid0->get_controller(), {link});
- auto* jbod_raid1 =
- simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid1", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID1, 1e7, 5e6);
- zone->add_route(host, jbod_raid1, {link});
+ auto jbod_raid1 =
+ simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid1", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID1, 1e7, 5e6);
+ zone->add_route(host, jbod_raid1->get_controller(), {link});
- auto* jbod_raid4 =
- simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid4", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID4, 1e7, 5e6);
- zone->add_route(host, jbod_raid4, {link});
+ auto jbod_raid4 =
+ simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid4", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID4, 1e7, 5e6);
+ zone->add_route(host, jbod_raid4->get_controller(), {link});
- auto* jbod_raid5 =
- simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid5", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID5, 1e7, 5e6);
- zone->add_route(host, jbod_raid5, {link});
+ auto jbod_raid5 =
+ simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid5", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID5, 1e7, 5e6);
+ zone->add_route(host, jbod_raid5->get_controller(), {link});
- auto* jbod_raid6 =
- simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid6", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID6, 1e7, 5e6);
- zone->add_route(host, jbod_raid6, {link});
+ auto jbod_raid6 =
+ simgrid::plugin::Jbod::create_jbod(zone, "jbod_raid6", 1e9, 4, simgrid::plugin::Jbod::RAID::RAID6, 1e7, 5e6);
+ zone->add_route(host, jbod_raid6->get_controller(), {link});
zone->seal();
XBT_PUBLIC sg_activity_t sg_activity_set_wait_any_for(sg_activity_set_t as, double timeout);
XBT_PUBLIC void sg_activity_set_delete(sg_activity_set_t as);
+/** You must call this function manually on activities extracted from an activity_set with waitany and friends */
+XBT_PUBLIC void sg_activity_unref(sg_activity_t acti);
+
SG_END_DECL
#endif /* INCLUDE_SIMGRID_ACTIVITY_SET_H */
class Simcall;
class SimcallObserver;
class MutexObserver;
+class ConditionVariableObserver;
class ObjectAccessSimcallObserver;
class ObjectAccessSimcallItem;
} // namespace actor
using ConditionVariableImplPtr = boost::intrusive_ptr<ConditionVariableImpl>;
XBT_PUBLIC void intrusive_ptr_add_ref(ConditionVariableImpl* cond);
XBT_PUBLIC void intrusive_ptr_release(ConditionVariableImpl* cond);
+ class ConditionVariableAcquisitionImpl;
+ using ConditionVariableAcquisitionImplPtr = boost::intrusive_ptr<ConditionVariableAcquisitionImpl>;
class CommImpl;
using CommImplPtr = boost::intrusive_ptr<CommImpl>;
friend void intrusive_ptr_add_ref(Chiller* o) { o->refcount_.fetch_add(1, std::memory_order_relaxed); }
#endif
- inline static xbt::signal<void(Chiller*)> on_power_change;
+ static xbt::signal<void(Chiller*)> on_power_change;
xbt::signal<void(Chiller*)> on_this_power_change;
public:
namespace simgrid::plugin {
+class Jbod;
+using JbodPtr = boost::intrusive_ptr<Jbod>;
class JbodIo;
-/** Smart pointer to a simgrid::s4u::Activity */
using JbodIoPtr = boost::intrusive_ptr<JbodIo>;
-XBT_PUBLIC void intrusive_ptr_release(const JbodIo* io);
-XBT_PUBLIC void intrusive_ptr_add_ref(const JbodIo* io);
-class Jbod : public s4u::Host {
+class Jbod {
public:
enum class RAID {RAID0 = 0, RAID1 = 1, RAID4 = 4 , RAID5 = 5, RAID6 = 6};
+ s4u::Host* get_controller() const { return controller_; }
int get_parity_disk_idx() { return parity_disk_idx_; }
void update_parity_disk_idx() { parity_disk_idx_ = (parity_disk_idx_- 1) % num_disks_; }
JbodIoPtr write_async(sg_size_t size);
sg_size_t write(sg_size_t size);
- static Jbod* create_jbod(s4u::NetZone* zone, const std::string& name, double speed, unsigned int num_disks,
- RAID raid_level, double read_bandwidth, double write_bandwidth);
+ static JbodPtr create_jbod(s4u::NetZone* zone, const std::string& name, double speed, unsigned int num_disks,
+ RAID raid_level, double read_bandwidth, double write_bandwidth);
protected:
+ void set_controller(s4u::Host* host) { controller_ = host; }
void set_num_disks(unsigned int num_disks) { num_disks_ = num_disks; }
void set_parity_disk_idx(unsigned int index) { parity_disk_idx_ = index; }
void set_read_disk_idx(int index) { read_disk_idx_ = index; }
void set_raid_level(RAID raid_level) { raid_level_ = raid_level; }
private:
+ s4u::Host* controller_;
unsigned int num_disks_;
RAID raid_level_;
unsigned int parity_disk_idx_;
int read_disk_idx_;
+ std::atomic_int_fast32_t refcount_{1};
+#ifndef DOXYGEN
+ friend void intrusive_ptr_release(Jbod* jbod)
+ {
+ if (jbod->refcount_.fetch_sub(1, std::memory_order_release) == 1) {
+ std::atomic_thread_fence(std::memory_order_acquire);
+ delete jbod;
+ }
+ }
+ friend void intrusive_ptr_add_ref(Jbod* jbod) { jbod->refcount_.fetch_add(1, std::memory_order_relaxed); }
+#endif
};
class JbodIo {
#endif
};
+/* Refcounting functions */
+XBT_PUBLIC void intrusive_ptr_release(const Jbod* io);
+XBT_PUBLIC void intrusive_ptr_add_ref(const Jbod* io);
+XBT_PUBLIC void intrusive_ptr_release(const JbodIo* io);
+XBT_PUBLIC void intrusive_ptr_add_ref(const JbodIo* io);
+
} // namespace simgrid::plugin
-#endif
\ No newline at end of file
+#endif
#ifndef SIMGRID_S4U_MUTEX_HPP
#define SIMGRID_S4U_MUTEX_HPP
+#include "simgrid/s4u/Actor.hpp"
#include <simgrid/forward.h>
#include <xbt/asserts.h>
void lock();
void unlock();
bool try_lock();
+
+ Actor* get_owner();
};
} // namespace simgrid::s4u
#include "src/kernel/activity/ConditionVariableImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/kernel/activity/Synchro.hpp"
-#include "src/kernel/actor/SimcallObserver.hpp"
+#include "src/kernel/actor/SynchroObserver.hpp"
#include <cmath> // std::isfinite
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(ker_condition, ker_synchro, "Condition variables kernel-space implementation");
/* Now transform the cond wait simcall into a mutex lock one */
actor::Simcall* simcall = &proc.simcall_;
- const auto* observer = dynamic_cast<kernel::actor::ConditionWaitSimcall*>(simcall->observer_);
+ const auto* observer = dynamic_cast<kernel::actor::ConditionVariableObserver*>(simcall->observer_);
xbt_assert(observer != nullptr);
observer->get_mutex()->lock_async(simcall->issuer_)->wait_for(simcall->issuer_, -1);
}
XBT_DEBUG("Wait condition %p", this);
xbt_assert(std::isfinite(timeout), "timeout is not finite!");
- /* If there is a mutex unlock it */
- if (mutex != nullptr) {
- xbt_assert(mutex->get_owner() == issuer,
- "Actor %s cannot wait on ConditionVariable %p since it does not own the provided mutex %p",
- issuer->get_cname(), this, mutex);
- mutex_ = mutex;
- mutex->unlock(issuer);
- }
+ /* Unlock the provided mutex (the simcall observer ensures that one is provided, no need to check) */
+ auto* owner = mutex->get_owner();
+ xbt_assert(owner == issuer,
+ "Actor %s cannot wait on ConditionVariable %p since it does not own the provided mutex %p (which is "
+ "owned by %s).",
+ issuer->get_cname(), this, mutex, (owner == nullptr ? "nobody" : owner->get_cname()));
+ mutex_ = mutex;
+ mutex->unlock(issuer);
SynchroImplPtr synchro(new SynchroImpl([this, issuer]() {
this->remove_sleeping_actor(*issuer);
- auto* observer = dynamic_cast<kernel::actor::ConditionWaitSimcall*>(issuer->simcall_.observer_);
+ auto* observer = dynamic_cast<kernel::actor::ConditionVariableObserver*>(issuer->simcall_.observer_);
xbt_assert(observer != nullptr);
observer->set_result(true);
}));
#define SIMGRID_KERNEL_ACTIVITY_CONDITIONVARIABLE_HPP
#include "simgrid/s4u/ConditionVariable.hpp"
+#include "src/kernel/activity/ActivityImpl.hpp"
#include "src/kernel/actor/ActorImpl.hpp"
+
#include <boost/intrusive/list.hpp>
namespace simgrid::kernel::activity {
return res;
}
- // None-recursive mutex
+ // Non-recursive mutex
auto res = MutexAcquisitionImplPtr(new kernel::activity::MutexAcquisitionImpl(issuer, this), true);
if (owner_ == nullptr) { // Lock is free, take it
owner_ = issuer;
#include "simgrid/s4u/Mutex.hpp"
#include "src/kernel/activity/ActivityImpl.hpp"
#include "src/kernel/actor/ActorImpl.hpp"
+#include "xbt/asserts.h"
#include <boost/intrusive/list.hpp>
namespace simgrid::kernel::activity {
MutexImplPtr get_mutex() { return mutex_; }
actor::ActorImpl* get_issuer() { return issuer_; }
void grant() { granted_ = true; }
+ bool is_granted() { return granted_; }
bool test(actor::ActorImpl* issuer = nullptr) override;
void wait_for(actor::ActorImpl* issuer, double timeout) override;
friend void intrusive_ptr_release(MutexImpl* mutex)
{
- if (mutex->refcount_.fetch_sub(1) == 1)
+ if (mutex->refcount_.fetch_sub(1) == 1) {
+ xbt_assert(mutex->ongoing_acquisitions_.empty(), "The destroyed mutex still had ongoing acquisitions");
+ xbt_assert(mutex->owner_ == nullptr, "The destroyed mutex is still owned by actor %s",
+ mutex->owner_->get_cname());
delete mutex;
+ }
}
- s4u::Mutex& mutex() { return piface_; }
+ s4u::Mutex& get_iface() { return piface_; }
};
} // namespace simgrid::kernel::activity
#endif
return max_ - min_ + 1;
}
-bool ConditionWaitSimcall::is_enabled()
-{
- if (static bool warned = false; not warned) {
- XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
- warned = true;
- }
- return true;
-}
-void ConditionWaitSimcall::serialize(std::stringstream& stream) const
-{
- THROW_UNIMPLEMENTED;
-}
-std::string ConditionWaitSimcall::to_string() const
-{
- return "ConditionWait(cond_id:" + ptr_to_id<activity::ConditionVariableImpl const>(get_cond()) +
- " mutex_id:" + std::to_string(get_mutex()->get_id()) + ")";
-}
-
ActorJoinSimcall::ActorJoinSimcall(ActorImpl* actor, ActorImpl* other, double timeout)
: SimcallObserver(actor), other_(s4u::ActorPtr(other->get_iface())), timeout_(timeout)
{
int get_value() const { return next_value_; }
};
-class ConditionWaitSimcall final : public ResultingSimcall<bool> {
- activity::ConditionVariableImpl* const cond_;
- activity::MutexImpl* const mutex_;
- const double timeout_;
-
-public:
- ConditionWaitSimcall(ActorImpl* actor, activity::ConditionVariableImpl* cond, activity::MutexImpl* mutex,
- double timeout = -1.0)
- : ResultingSimcall(actor, false), cond_(cond), mutex_(mutex), timeout_(timeout)
- {
- }
- void serialize(std::stringstream& stream) const override;
- std::string to_string() const override;
- bool is_enabled() override;
- activity::ConditionVariableImpl* get_cond() const { return cond_; }
- activity::MutexImpl* get_mutex() const { return mutex_; }
- double get_timeout() const { return timeout_; }
-};
-
class ActorJoinSimcall final : public SimcallObserver {
s4u::ActorPtr const other_; // We need a Ptr to ensure access to the actor after its end, but Ptr requires s4u
const double timeout_;
(type_ == mc::Transition::Type::BARRIER_WAIT && acquisition_ != nullptr && acquisition_->granted_);
}
+bool ConditionVariableObserver::is_enabled()
+{
+ if (static bool warned = false; not warned) {
+ XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
+ warned = true;
+ }
+ return true;
+}
+void ConditionVariableObserver::serialize(std::stringstream& stream) const
+{
+ THROW_UNIMPLEMENTED;
+}
+std::string ConditionVariableObserver::to_string() const
+{
+ return "ConditionWait(cond_id:" + ptr_to_id<activity::ConditionVariableImpl const>(get_cond()) +
+ " mutex_id:" + std::to_string(get_mutex()->get_id()) + ")";
+}
+
} // namespace simgrid::kernel::actor
#define SIMGRID_MC_MUTEX_OBSERVER_HPP
#include "simgrid/forward.h"
+#include "src/kernel/activity/ConditionVariableImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/kernel/actor/ActorImpl.hpp"
#include "src/kernel/actor/SimcallObserver.hpp"
double get_timeout() const { return timeout_; }
};
+class ConditionVariableObserver final : public ResultingSimcall<bool> {
+ //mc::Transition::Type type_; Will be used when we implement CV on the MC side
+ activity::ConditionVariableImpl* const cond_;
+ activity::MutexImpl* const mutex_;
+ const double timeout_;
+
+public:
+ ConditionVariableObserver(ActorImpl* actor, activity::ConditionVariableImpl* cond, activity::MutexImpl* mutex,
+ double timeout = -1.0)
+ : ResultingSimcall(actor, false), cond_(cond), mutex_(mutex), timeout_(timeout)
+ {
+ xbt_assert(mutex != nullptr, "Cannot wait on a condition variable without a valid mutex");
+ }
+ void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
+ bool is_enabled() override;
+ activity::ConditionVariableImpl* get_cond() const { return cond_; }
+ activity::MutexImpl* get_mutex() const { return mutex_; }
+ double get_timeout() const { return timeout_; }
+};
+
} // namespace simgrid::kernel::actor
#endif
#include "src/mc/explo/odpor/Execution.hpp"
#include "src/mc/api/State.hpp"
-#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
#include "xbt/asserts.h"
#include "xbt/string.hpp"
#include <algorithm>
std::unordered_set<Execution::EventHandle> Execution::get_reversible_races_of(EventHandle handle) const
{
std::unordered_set<EventHandle> reversible_races;
+ const auto* this_transition = get_transition_for_handle(handle);
for (EventHandle race : get_racing_events_of(handle)) {
- if (ReversibleRaceCalculator::is_race_reversible(*this, race, handle)) {
+ const auto* other_transition = get_transition_for_handle(race);
+
+ if (this_transition->reversible_race(other_transition)) {
reversible_races.insert(race);
}
}
+++ /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/odpor/ReversibleRaceCalculator.hpp"
-#include "src/mc/explo/odpor/Execution.hpp"
-#include "src/mc/transition/Transition.hpp"
-#include "src/mc/transition/TransitionSynchro.hpp"
-
-#include <functional>
-#include <unordered_map>
-#include <xbt/asserts.h>
-#include <xbt/ex.h>
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker");
-
-namespace simgrid::mc::odpor {
-
-/**
- The reversible race detector should only be used if we already have the assumption
- e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that :
- - e1 -->_E e2
- - proc(e1) != proc(e2)
- - there is no event e3 s.t. e1 --> e3 --> e2
-*/
-
-bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
- Execution::EventHandle e2)
-{
- using Action = Transition::Type;
- using Handler = std::function<bool(const Execution&, const Transition*, const Transition*)>;
- using HandlerMap = std::unordered_map<Action, Handler>;
-
- const static HandlerMap handlers = {
- {Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
- {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
- {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
- {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
- {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
- {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
- {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
- {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
- {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
- {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
- {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
- {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
- {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
- {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
- {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
- {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
- {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
- {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
- {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
-
- const auto* other_transition = E.get_transition_for_handle(e1);
- const auto* t2 = E.get_transition_for_handle(e2);
- if (const auto handler = handlers.find(t2->type_); handler != handlers.end()) {
- return handler->second(E, other_transition, t2);
- } else {
- xbt_die("There is currently no specialized computation for the transition "
- "'%s' for computing reversible races in ODPOR, so the model checker cannot "
- "determine how to proceed. Please submit a bug report requesting "
- "that the transition be supported in SimGrid using ODPPR and consider "
- "using the other model-checking algorithms supported by SimGrid instead "
- "in the meantime",
- t2->to_string().c_str());
- }
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // ActorJoin races with another event iff its target `T` is the same as
- // the actor executing the other transition. Clearly, then, we could not join
- // on that actor `T` and then run a transition by `T`, so no race is reversible
- return false;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&,
- const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // BarrierAsyncLock is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, const Transition* other_transition,
- const Transition* /*t2*/)
-{
- // If the other event is a barrier lock event, then we
- // are not reversible; otherwise we are reversible.
- const auto other_action = other_transition->type_;
- return other_action != Transition::Type::BARRIER_ASYNC_LOCK;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // CommRecv is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // CommSend is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, const Transition* other_transition,
- const Transition* /*t2*/)
-{
- // If the other event is a communication event, then we
- // are not reversible; otherwise we are reversible.
- const auto other_action = other_transition->type_;
- return other_action != Transition::Type::COMM_ASYNC_SEND && other_action != Transition::Type::COMM_ASYNC_RECV;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // CommTest is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&,
- const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // MutexAsyncLock is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // MutexTest is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // MutexTrylock is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // MutexUnlock is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // Only an Unlock can be dependent with a Wait
- // and in this case, that Unlock enabled the wait
- // Not reversible
- return false;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // SemAsyncLock is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // SemUnlock is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, const Transition* other_transition,
- const Transition* /*t2*/)
-{
-
- if (other_transition->type_ == Transition::Type::SEM_UNLOCK &&
- static_cast<const SemaphoreTransition*>(other_transition)->get_capacity() <= 1) {
- return false;
- }
- xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // Object access is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // Random is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // TestAny is always enabled
- return true;
-}
-
-bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, const Transition* /*other_transition*/,
- const Transition* /*t2*/)
-{
- // TODO: We need to check if any of the transitions
- // waited on occurred before `e1`
- return true; // Let's overapproximate to not miss branches
-}
-
-} // namespace simgrid::mc::odpor
+++ /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_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
-#define SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
-
-#include "src/mc/explo/odpor/Execution.hpp"
-#include "src/mc/explo/odpor/odpor_forward.hpp"
-#include "src/mc/transition/Transition.hpp"
-#include "src/mc/transition/TransitionActor.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::odpor {
-
-/**
- * @brief Computes whether a race between two events
- * in a given execution is a reversible race.
- *
- * @note: All of the methods assume that there is
- * indeed a race between the two events in the
- * execution; indeed, the question the method answers
- * is only sensible in the context of a race
- */
-class ReversibleRaceCalculator final {
- static bool is_race_reversible_ActorJoin(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_BarrierAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_BarrierWait(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_CommRecv(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_CommSend(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_CommWait(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_CommTest(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_MutexAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_MutexTest(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_MutexTrylock(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_MutexUnlock(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_MutexWait(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_SemAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_SemUnlock(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_SemWait(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_ObjectAccess(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_Random(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_TestAny(const Execution&, const Transition* t1, const Transition* t2);
- static bool is_race_reversible_WaitAny(const Execution&, const Transition* t1, const Transition* t2);
-
-public:
- static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2);
-};
-
-} // namespace simgrid::mc::odpor
-#endif
#define SIMGRID_MC_TRANSITION_HPP
#include "simgrid/forward.h" // aid_t
+#include "xbt/ex.h"
#include "xbt/utility.hpp" // XBT_DECLARE_ENUM_CLASS
#include <sstream>
* calls.
*/
class Transition {
- /* Textual representation of the transition, to display backtraces */
+ /* Global statistics */
static unsigned long executed_transitions_;
static unsigned long replayed_transitions_;
virtual bool depends(const Transition* other) const { return true; }
+ /**
+ The reversible race detector should only be used if we already have the assumption
+ this <* other (see Source set: a foundation for ODPOR). In particular this means that :
+ - this -->_E other
+ - proc(this) != proc(other)
+ - there is no event e s.t. this --> e --> other
+
+ @note: It is safe to assume that there is indeed a race between the two events in the execution;
+ indeed, the question the method answers is only sensible in the context of a race
+ */
+ virtual bool reversible_race(const Transition* other) const
+ {
+ xbt_die("%s unimplemented for %s", __func__, to_c_str(type_));
+ }
+
/* Returns the total amount of transitions executed so far (for statistics) */
static unsigned long get_executed_transitions() { return executed_transitions_; }
/* Returns the total amount of transitions replayed so far while backtracing (for statistics) */
return false;
}
+bool ActorJoinTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::ACTOR_JOIN:
+ // ActorJoin races with another event iff its target `T` is the same as
+ // the actor executing the other transition. Clearly, then, we could not join
+ // on that actor `T` and then run a transition by `T`, so no race is reversible
+ return false;
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
ActorSleepTransition::ActorSleepTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::ACTOR_SLEEP, issuer, times_considered)
{
return false;
}
+bool ActorSleepTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::ACTOR_SLEEP:
+ return true; // Always enabled
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
} // namespace simgrid::mc
ActorJoinTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
bool get_timeout() const { return timeout_; }
/** Target ID */
ActorSleepTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
};
} // namespace simgrid::mc
return transitions_[times_considered_]->depends(other);
}
+bool TestAnyTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::TESTANY:
+ return true; // TestAny is always enabled
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::WAITANY, issuer, times_considered)
{
return true;
return transitions_[times_considered_]->depends(other);
}
+bool WaitAnyTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::WAITANY:
+ // TODO: We need to check if any of the transitions waited on occurred before `e1`
+ return true; // Let's overapproximate to not miss branches
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
} // namespace simgrid::mc
TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
Transition* get_current_transition() const { return transitions_.at(times_considered_); }
bool result() const
WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
Transition* get_current_transition() const { return transitions_.at(times_considered_); }
};
return false; // Comm transitions are INDEP with non-comm transitions
}
+
+bool CommWaitTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::COMM_WAIT:
+ // If the other event is a communication event, then we are not reversible; otherwise we are reversible.
+ return other->type_ != Transition::Type::COMM_ASYNC_SEND && other->type_ != Transition::Type::COMM_ASYNC_RECV;
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_,
aid_t receiver_, unsigned mbox_)
: Transition(Type::COMM_TEST, issuer, times_considered)
{
return xbt::string_printf("TestComm(from %ld to %ld, mbox=%u)", sender_, receiver_, mbox_);
}
+
bool CommTestTransition::depends(const Transition* other) const
{
if (other->type_ < type_)
return false; // Comm transitions are INDEP with non-comm transitions
}
+bool CommTestTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::COMM_TEST:
+ return true; // CommTest is always enabled
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_)
: Transition(Type::COMM_ASYNC_RECV, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_)
{
return false; // Comm transitions are INDEP with non-comm transitions
}
+bool CommRecvTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::COMM_ASYNC_RECV:
+ return true; // CommRecv is always enabled
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_)
{
return false; // Comm transitions are INDEP with non-comm transitions
}
+bool CommSendTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::COMM_ASYNC_SEND:
+ return true; // CommSend is always enabled
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
} // namespace simgrid::mc
CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
bool get_timeout() const { return timeout_; }
/** ID of the corresponding Communication object in the application, or 0 if unknown */
CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
/** ID of the corresponding Communication object in the application, or 0 if unknown */
unsigned get_comm() const { return comm_; }
CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
/** ID of the corresponding Communication object in the application (or 0 if unknown)*/
unsigned get_comm() const { return comm_; }
CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
/** ID of the corresponding Communication object in the application, or 0 if unknown */
unsigned get_comm() const { return comm_; }
return false;
}
+bool ObjectAccessTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::OBJECT_ACCESS:
+ return true; // Object access is always enabled
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
} // namespace simgrid::mc
ObjectAccessTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
};
} // namespace simgrid::mc
xbt_assert(stream >> min_ >> max_);
}
+bool RandomTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::RANDOM:
+ return true; // Random is always enabled
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
} // namespace simgrid::mc
return aid_ == other->aid_;
} // Independent with any other transition
+ bool reversible_race(const Transition* other) const override;
};
} // namespace simgrid::mc
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/transition/TransitionSynchro.hpp"
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/transition/TransitionObjectAccess.hpp"
#include "xbt/asserts.h"
#include "xbt/ex.h"
#include "xbt/string.hpp"
return false; // barriers are INDEP with non-barrier transitions
}
+bool BarrierTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::BARRIER_ASYNC_LOCK:
+ return true; // BarrierAsyncLock is always enabled
+ case Type::BARRIER_WAIT:
+ // If the other event is a barrier lock event, then we are not reversible;
+ // otherwise we are reversible.
+ return other->type_ != Transition::Type::BARRIER_ASYNC_LOCK;
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
std::string MutexTransition::to_string(bool verbose) const
{
return false; // mutexes are INDEP with non-mutex transitions
}
+bool SemaphoreTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::SEM_ASYNC_LOCK:
+ return true; // SemAsyncLock is always enabled
+ case Type::SEM_UNLOCK:
+ return true; // SemUnlock is always enabled
+ case Type::SEM_WAIT:
+ if (other->type_ == Transition::Type::SEM_UNLOCK &&
+ static_cast<const SemaphoreTransition*>(other)->get_capacity() <= 1) {
+ return false;
+ }
+ xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
+ return true;
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
std::string SemaphoreTransition::to_string(bool verbose) const
{
if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
return false; // semaphores are INDEP with non-semaphore transitions
}
+bool MutexTransition::reversible_race(const Transition* other) const
+{
+ switch (type_) {
+ case Type::MUTEX_ASYNC_LOCK:
+ return true; // MutexAsyncLock is always enabled
+ case Type::MUTEX_TEST:
+ return true; // MutexTest is always enabled
+ case Type::MUTEX_TRYLOCK:
+ return true; // MutexTrylock is always enabled
+ case Type::MUTEX_UNLOCK:
+ return true; // MutexUnlock is always enabled
+
+ case Type::MUTEX_WAIT:
+ // Only an Unlock can be dependent with a Wait
+ // and in this case, that Unlock enabled the wait
+ // Not reversible
+ return false;
+ default:
+ xbt_die("Unexpected transition type %s", to_c_str(type_));
+ }
+}
+
} // namespace simgrid::mc
std::string to_string(bool verbose) const override;
BarrierTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
};
class MutexTransition : public Transition {
std::string to_string(bool verbose) const override;
MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
uintptr_t get_mutex() const { return this->mutex_; }
aid_t get_owner() const { return this->owner_; }
std::string to_string(bool verbose) const override;
SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
bool depends(const Transition* other) const override;
+ bool reversible_race(const Transition* other) const override;
+
int get_capacity() const { return capacity_; }
};
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(Chiller, kernel, "Logging specific to the solar panel plugin");
namespace simgrid::plugins {
+xbt::signal<void(Chiller*)> Chiller::on_power_change; // initialisation of static field
/* ChillerModel */
namespace simgrid::plugin {
-Jbod* Jbod::create_jbod(s4u::NetZone* zone, const std::string& name, double speed, unsigned int num_disks,
- RAID raid_level, double read_bandwidth, double write_bandwidth)
+JbodPtr Jbod::create_jbod(s4u::NetZone* zone, const std::string& name, double speed, unsigned int num_disks,
+ RAID raid_level, double read_bandwidth, double write_bandwidth)
{
xbt_assert(not ((raid_level == RAID::RAID4 || raid_level == RAID::RAID5) && num_disks < 3),
"RAID%d requires at least 3 disks", (int) raid_level);
xbt_assert(not (raid_level == RAID::RAID6 && num_disks < 4), "RAID6 requires at least 4 disks");
- auto* jbod = static_cast<Jbod*>(zone->create_host(name, speed));
+ auto* jbod = new Jbod();
+ jbod->set_controller(zone->create_host(name, speed));
jbod->set_num_disks(num_disks);
jbod->set_parity_disk_idx(num_disks -1 );
jbod->set_read_disk_idx(-1);
jbod->set_raid_level(raid_level);
for (unsigned int i = 0; i < num_disks; i++)
- jbod->create_disk(name + "_disk_" + std::to_string(i), read_bandwidth, write_bandwidth);
+ jbod->get_controller()->create_disk(name + "_disk_" + std::to_string(i), read_bandwidth, write_bandwidth);
- return jbod;
+ return JbodPtr(jbod);
}
JbodIoPtr Jbod::read_async(sg_size_t size)
{
- auto comm = s4u::Comm::sendto_init()->set_source(const_cast<Jbod*>(this))->set_payload_size(size);
+ auto comm = s4u::Comm::sendto_init()->set_source(this->controller_)->set_payload_size(size);
std::vector<s4u::IoPtr> pending_ios;
sg_size_t read_size = 0;
std::vector<s4u::Disk*> targets;
switch(raid_level_) {
case RAID::RAID0:
read_size = size / num_disks_;
- targets = get_disks();
+ targets = controller_->get_disks();
break;
case RAID::RAID1:
read_size = size;
- targets.push_back(get_disks().at(get_next_read_disk_idx()));
+ targets.push_back(controller_->get_disks().at(get_next_read_disk_idx()));
break;
case RAID::RAID4:
read_size = size / (num_disks_ - 1);
- targets = get_disks();
+ targets = controller_->get_disks();
targets.pop_back();
break;
case RAID::RAID5:
read_size = size / (num_disks_ - 1);
- targets = get_disks();
+ targets = controller_->get_disks();
targets.erase(targets.begin() + (get_parity_disk_idx() + 1 % num_disks_));
break;
case RAID::RAID6:
read_size = size / (num_disks_ - 2);
- targets = get_disks();
+ targets = controller_->get_disks();
if ( (get_parity_disk_idx() + 2 % num_disks_) == 0 ) {
targets.pop_back();
targets.erase(targets.begin());
JbodIoPtr Jbod::write_async(sg_size_t size)
{
- auto comm = s4u::Comm::sendto_init(s4u::Host::current(), const_cast<Jbod*>(this));
+ auto comm = s4u::Comm::sendto_init(s4u::Host::current(), this->get_controller());
std::vector<s4u::IoPtr> pending_ios;
sg_size_t write_size = 0;
switch(raid_level_) {
default:
xbt_die("Unsupported RAID level. Supported level are: 0, 1, 4, 5, and 6");
}
- for (const auto* disk : get_disks()) {
+ for (const auto* disk : get_controller()->get_disks()) {
auto io = s4u::IoPtr(disk->io_init(write_size, s4u::Io::OpType::WRITE));
io->set_name(disk->get_name());
pending_ios.push_back(io);
transfer_->wait();
XBT_DEBUG("Data received on JBOD");
if (parity_block_comp_) {
- parity_block_comp_->set_host(const_cast<Jbod*>(jbod_))->wait();
+ parity_block_comp_->set_host(jbod_->get_controller())->wait();
XBT_DEBUG("Parity block computed");
}
XBT_DEBUG("Start writing");
{
delete as;
}
+void sg_activity_unref(sg_activity_t acti)
+{
+ acti->unref();
+}
SG_END_DECL
#include "src/kernel/activity/ActivityImpl.hpp"
#include "src/kernel/activity/ConditionVariableImpl.hpp"
-#include "src/kernel/actor/SimcallObserver.hpp"
+#include "src/kernel/actor/SynchroObserver.hpp"
#include <mutex>
void ConditionVariable::wait(MutexPtr lock)
{
kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
- kernel::actor::ConditionWaitSimcall observer{issuer, pimpl_, lock->pimpl_};
+ kernel::actor::ConditionVariableObserver observer{issuer, pimpl_, lock->pimpl_};
kernel::actor::simcall_blocking(
[&observer] { observer.get_cond()->wait(observer.get_mutex(), -1.0, observer.get_issuer()); }, &observer);
}
void ConditionVariable::wait(const std::unique_lock<Mutex>& lock)
{
kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
- kernel::actor::ConditionWaitSimcall observer{issuer, pimpl_, lock.mutex()->pimpl_};
+ kernel::actor::ConditionVariableObserver observer{issuer, pimpl_, lock.mutex()->pimpl_};
kernel::actor::simcall_blocking(
[&observer] { observer.get_cond()->wait(observer.get_mutex(), -1.0, observer.get_issuer()); }, &observer);
}
timeout = 0.0;
kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
- kernel::actor::ConditionWaitSimcall observer{issuer, pimpl_, lock.mutex()->pimpl_, timeout};
+ kernel::actor::ConditionVariableObserver observer{issuer, pimpl_, lock.mutex()->pimpl_, timeout};
bool timed_out = kernel::actor::simcall_blocking(
[&observer] { observer.get_cond()->wait(observer.get_mutex(), observer.get_timeout(), observer.get_issuer()); },
&observer);
MutexPtr Mutex::create(bool recursive)
{
auto* mutex = new kernel::activity::MutexImpl(recursive);
- return MutexPtr(&mutex->mutex(), false);
+ return MutexPtr(&mutex->get_iface(), false);
+}
+
+Actor* Mutex::get_owner()
+{
+ auto* owner = pimpl_->get_owner();
+ if (owner == nullptr)
+ return nullptr;
+ return owner->get_ciface();
}
/* refcounting of the intrusive_ptr is delegated to the implementation object */
}
if (win->allocated_)
xbt_free(win->base_);
+ for (auto m : {win->mut_, win->lock_mut_, win->atomic_mut_})
+ if (m->get_owner() != nullptr)
+ m->unlock();
F2C::free_f(win->f2c_id());
win->cleanup_attr<Win>();
static int (*raw_pthread_cond_signal)(pthread_cond_t*);
static int (*raw_pthread_cond_broadcast)(pthread_cond_t*);
static int (*raw_pthread_cond_wait)(pthread_cond_t*, pthread_mutex_t*);
+static int (*raw_pthread_cond_timedwait)(pthread_cond_t*, pthread_mutex_t*, const struct timespec* abstime);
static int (*raw_pthread_cond_destroy)(pthread_cond_t*);
static unsigned int (*raw_sleep)(unsigned int);
raw_pthread_cond_signal = dlsym(RTLD_NEXT, "raw_pthread_cond_signal");
raw_pthread_cond_broadcast = dlsym(RTLD_NEXT, "raw_pthread_cond_broadcast");
raw_pthread_cond_wait = dlsym(RTLD_NEXT, "raw_pthread_cond_wait");
+ raw_pthread_cond_timedwait = dlsym(RTLD_NEXT, "raw_pthread_cond_timedwait");
raw_pthread_cond_destroy = dlsym(RTLD_NEXT, "raw_pthread_cond_destroy");
raw_sleep = dlsym(RTLD_NEXT, "sleep");
intercepted_pthcall(cond_broadcast, (pthread_cond_t * cond), (cond), ((sthread_cond_t*)cond));
intercepted_pthcall(cond_wait, (pthread_cond_t * cond, pthread_mutex_t* mutex), (cond, mutex),
((sthread_cond_t*)cond, (sthread_mutex_t*)mutex));
+intercepted_pthcall(cond_timedwait, (pthread_cond_t * cond, pthread_mutex_t* mutex, const struct timespec* abstime),
+ (cond, mutex, abstime), ((sthread_cond_t*)cond, (sthread_mutex_t*)mutex, abstime));
intercepted_pthcall(cond_destroy, (pthread_cond_t * cond), (cond), ((sthread_cond_t*)cond));
#define intercepted_call(rettype, name, raw_params, call_params, sim_params) \
typedef struct {
void* cond;
+ void* mutex;
} sthread_cond_t;
int sthread_cond_init(sthread_cond_t* cond, sthread_condattr_t* attr);
int sthread_cond_signal(sthread_cond_t* cond);
int sthread_cond_broadcast(sthread_cond_t* cond);
int sthread_cond_wait(sthread_cond_t* cond, sthread_mutex_t* mutex);
+int sthread_cond_timedwait(sthread_cond_t* cond, sthread_mutex_t* mutex, const struct timespec* abs_timeout);
int sthread_cond_destroy(sthread_cond_t* cond);
typedef struct {
intrusive_ptr_add_ref(cv.get());
cond->cond = cv.get();
+ cond->mutex = nullptr;
return 0;
}
int sthread_cond_signal(sthread_cond_t* cond)
{
XBT_DEBUG("%s(%p)", __func__, cond);
+
+ if (cond->mutex == nullptr)
+ XBT_WARN("No mutex was associated so far with condition variable %p. Safety checks skipped.", cond);
+ else {
+ auto* owner = static_cast<sg4::Mutex*>(cond->mutex)->get_owner();
+ if (owner == nullptr)
+ XBT_WARN("The mutex associated to condition %p is not currently owned by anyone when calling "
+ "pthread_cond_signal(). The signal could get lost.",
+ cond);
+ else if (owner != simgrid::s4u::Actor::self())
+ XBT_WARN("The mutex associated to condition %p is currently owned by %s, not by the thread currently calling "
+ "calling pthread_cond_signal(). The signal could get lost.",
+ cond, owner->get_cname());
+ }
+
static_cast<sg4::ConditionVariable*>(cond->cond)->notify_one();
return 0;
}
int sthread_cond_broadcast(sthread_cond_t* cond)
{
XBT_DEBUG("%s(%p)", __func__, cond);
+
+ if (cond->mutex == nullptr)
+ XBT_WARN("No mutex was associated so far with condition variable %p. Safety checks skipped.", cond);
+ else {
+ auto* owner = static_cast<sg4::Mutex*>(cond->mutex)->get_owner();
+ if (owner == nullptr)
+ XBT_WARN("The mutex associated to condition %p is not currently owned by anyone when calling "
+ "pthread_cond_broadcast(). The signal could get lost.",
+ cond);
+ else if (owner != simgrid::s4u::Actor::self())
+ XBT_WARN("The mutex associated to condition %p is currently owned by %s, not by the thread currently calling "
+ "calling pthread_cond_broadcast(). The signal could get lost.",
+ cond, owner->get_cname());
+ }
+
static_cast<sg4::ConditionVariable*>(cond->cond)->notify_all();
return 0;
}
int sthread_cond_wait(sthread_cond_t* cond, sthread_mutex_t* mutex)
{
XBT_DEBUG("%s(%p)", __func__, cond);
+
+ if (cond->mutex == nullptr)
+ cond->mutex = mutex->mutex;
+ else if (cond->mutex != mutex->mutex)
+ XBT_WARN("The condition %p is now waited with mutex %p while it was previoulsy waited with mutex %p. sthread may "
+ "not work with such a dangerous code.",
+ cond, cond->mutex, mutex->mutex);
+
static_cast<sg4::ConditionVariable*>(cond->cond)->wait(static_cast<sg4::Mutex*>(mutex->mutex));
return 0;
}
+int sthread_cond_timedwait(sthread_cond_t* cond, sthread_mutex_t* mutex, const struct timespec* abs_timeout)
+{
+ XBT_DEBUG("%s(%p)", __func__, cond);
+
+ if (cond->mutex == nullptr)
+ cond->mutex = mutex->mutex;
+ else if (cond->mutex != mutex->mutex)
+ XBT_WARN("The condition %p is now waited with mutex %p while it was previoulsy waited with mutex %p. sthread may "
+ "not work with such a dangerous code.",
+ cond, cond->mutex, mutex->mutex);
+
+ THROW_UNIMPLEMENTED;
+}
int sthread_cond_destroy(sthread_cond_t* cond)
{
XBT_DEBUG("%s(%p)", __func__, cond);
simgrid::s4u::this_actor::sleep_for(seconds);
return 0;
}
-
-#if 0
-int pthread_cond_init(pthread_cond_t *cond, pthread_condattr_t *cond_attr) {
- *cond = sg_cond_init();
- return 0;
-}
-
-int pthread_cond_signal(pthread_cond_t *cond) {
- sg_cond_notify_one(*cond);
- return 0;
-}
-
-int pthread_cond_broadcast(pthread_cond_t *cond) {
- sg_cond_notify_all(*cond);
- return 0;
-}
-
-int pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex) {
- sg_cond_wait(*cond, *mutex);
- return 0;
-}
-
-int pthread_cond_destroy(pthread_cond_t *cond) {
- sg_cond_destroy(*cond);
- return 0;
-}
-#endif
# simple_cond_broadcast_ok simple_cond_broadcast_deadlock
# simple_cond_broadcast_with_semaphore_ok
# simple_cond_broadcast_with_semaphore_deadlock1 simple_cond_broadcast_with_semaphore_deadlock2
-# simple_threads_ok
# simple_cond_deadlock
simple_mutex_ok simple_mutex_deadlock
simple_semaphore_deadlock simple_semaphores_deadlock
simple_semaphores_ok
simple_semaphores_with_threads_ok simple_semaphores_with_threads_deadlock
-#
-# philosophers_spurious_deadlock
+ simple_threads_ok
+
barber_shop_ok barber_shop_deadlock
philosophers_semaphores_ok philosophers_semaphores_deadlock
philosophers_mutex_ok philosophers_mutex_deadlock
producer_consumer_ok producer_consumer_deadlock
-
+ # philosophers_spurious_deadlock # infinite no-op loop
# producer_consumer_spurious_nok # infinite no-op loop
)
--- /dev/null
+#include <pthread.h>
+#include <stdlib.h>
+#include <unistd.h>
+#include <stdio.h>
+
+static void * thread_doit(void *unused) {
+ int len = (int) ((drand48() * 5) + 1);
+ sleep(len);
+ return NULL;
+}
+
+int main(int argc, char* argv[]) {
+ if(argc < 2) {
+ printf("Expected usage: %s THREAD_NUM\n", argv[0]);
+ return -1;
+ }
+
+ int thread_num = atoi(argv[1]);
+
+ pthread_t *threads = malloc(sizeof(pthread_t) * thread_num);
+
+ for(int i = 0; i < thread_num; i++) {
+ pthread_create(&threads[i], NULL, &thread_doit, NULL);
+ }
+
+ for(int i = 0; i < thread_num; i++) {
+ pthread_join(threads[i], NULL);
+ }
+
+ free(threads);
+
+ return 0;
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-simple_threads_ok 3
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor'
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor.
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 7 unique states visited; 0 backtracks (0 transition replays, 7 states visited overall)
\ No newline at end of file
src/mc/explo/odpor/Execution.cpp
src/mc/explo/odpor/Execution.hpp
- src/mc/explo/odpor/ReversibleRaceCalculator.cpp
- src/mc/explo/odpor/ReversibleRaceCalculator.hpp
src/mc/explo/odpor/WakeupTree.cpp
src/mc/explo/odpor/WakeupTree.hpp
src/mc/explo/odpor/WakeupTreeIterator.cpp
# workaround for https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81767
set(warnCXXFLAGS "${warnCXXFLAGS} -Wno-error=unused-variable")
endif()
+ if (CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL "13.2.0")
+ # workaround for https://gcc.gnu.org/bugzilla/show_bug.cgi?id=101361
+ set(warnCXXFLAGS "${warnCXXFLAGS} -Wno-error=stringop-overread")
+ endif()
endif()
if (CMAKE_CXX_COMPILER_ID MATCHES "Clang")
