* Introducing v4 of the XML platform format (many long-due cleanups)
* MSG examples fully reorganized (in C and Java)
- * The S4U interface is rising, toward SimGrid 4:|br| All host manipulations now done in S4U,
+ * The S4U interface is rising, toward SimGrid 4:|br| All host manipulations now done in S4U,
SimDag was mostly rewritten on top of S4U but MSG & SimDag interfaces mostly unchanged.
Version 3.14 (Dec 25. 2016)
Once the S4U interface stabilizes, we will provide C bindings on top of it, along with Java and Python ones. Maybe in 3.21 or 3.22.
All this is not contradictory with the fact that MSG as a whole is deprecated, because this deprecation only means that new projects
-should go for S4U instead of MSG to benefit of the future. Despite this deprecation, old MSG projects should still be usable with no
+should go for S4U instead of MSG to benefit of the future. Despite this deprecation, old MSG projects should still be usable with no
change, if we manage to. This is a matter of scientific reproducibility to us.
Version 3.20 (June 25 2018)
The plan is to completely remove MSG by 2020Q4 or 2021Q1.
* SimDAG++: Automatic dependencies on S4U activities (experimental). |br|
- This implements some features of SimDAG within S4U, but not all of them: you cannot block an activity until it's scheduled on a resource
+ This implements some features of SimDAG within S4U, but not all of them: you cannot block an activity until it's scheduled on a resource
and there is no heterogeneous wait_any() that would mix Exec/Comm/Io activities. See ``examples/s4u/{io,exec,comm}-dependent`` for what's already there.
Since last fall, we continued to push toward the future SimGrid4 release. This requires to remove MSG and SimDAG once all users have
of years.
* The removal of SimDag led us to also remove the export to Jedule files that was tightly coupled to SimDag. The instrumentation of DAG simulation
is still possible through the regular instrumentation API based on the Paje format.
-
-On the bindings front, we dropped the Lua bindings to create new platforms, as the C++ and Python interfaces are much better to that extend.
-Also, the algorithm tutorial can now be taken in Python, for those of you allergic to C++.
-Finally, on the SMPI front, we introduced a new documentation section on calibrating the SMPI models from your measurements and fixed some issues
-with the replay mechanism.
+On the bindings front, we dropped the Lua bindings to create new platforms, as the C++ and Python interfaces are much better to that extend.
+Also, the algorithm tutorial can now be taken in Python, for those of you allergic to C++.
-Version 3.31 (not released yet)
--------------------------------
+Finally, on the SMPI front, we introduced a :ref:`new documentation section <models_calibration>` on calibrating the SMPI models from your
+measurements and fixed some issues with the replay mechanism.
-Expected: spring 2022
+Version 3.31 (March 22. 2022)
+-----------------------------
**On the model checking front**, the long awaited big bang finally occurred, greatly simplifying future evolution.
A formal verification with Mc SimGrid implies two processes: a verified application that is an almost regular SimGrid simulation, and a checker that
is an external process guiding the verified application to ensure that it explores every possible execution scenario. When formal verification was
initially introduced in SimGrid 15 years ago, both processes were intertwined in the same system process, but the mandated system tricks made it
-impossible to use gdb or valgrind on that Frankenstein process. Having more than one heap in your process is not usually supported.
+impossible to use gdb or valgrind on that Frankenstein process. Having two heaps in one process is not usually supported.
The design was simplified in v3.12 (2015) by splitting the application and the checker in separate system processes. But both processes remained tightly
-coupled: when the checker needed some information (for example the mailbox implied in a send operation to compute whether this operation `commutes
+coupled: when the checker needed some information (such as the mailbox implied in a send operation, to compute whether this operation `commutes
with another one <https://en.wikipedia.org/wiki/Partial_order_reduction>`_), the checker was directly reading the memory of the other system process.
This was efficient and nice in C, but it prevented us from using C++ features such as opaque ``std::function`` data types. As such, it hindered the
ongoing SimDAG++ code reorganization toward SimGrid4, where all activity classes should be homogeneously written in modern C++.
-This release introduces a new design, where the simcalls are given object-oriented Observers that can serialize the relevant information over the wire.
-This information is used on the checker side to build Transition objects, representing the application simcalls. This explanation may not be crystal
-clear, but the checker code is now much easier to work with as the formal logic is not spoiled with system-level tricks to retrieve the needed information.
+This release introduces a new design, where the simcalls are given object-oriented ``Observers`` that can serialize the relevant information over the wire.
+This information is used on the checker side to build ``Transition`` objects that the application simcalls. The checker code is now much simpler, as the
+formal logic is not spoiled with system-level tricks to retrieve the needed information.
+
+This cleaned design allowed us to finally implement the support for mutexes, semaphores and barriers in the model-checker (condition variables are still
+missing). This enables in particular the verification of RMA primitives with Mc SimGrid, as their implementation in SMPI is based on mutexes and barriers.
+Simix, a central element of the SimGrid 3 design, was also finally removed: the last bits are deprecated and will be removed in 3.35. We also replaced the
+old, non-free ISP test suite by the one from the `MPI Bug Initiative <https://hal.archives-ouvertes.fr/hal-03474762>`_ (not all tests are activated yet).
+This will eventually help improving the robustness of Mc SimGrid.
+
+These changes unlock the future of Mc SimGrid. For the next releases, we plan to implement another exploration algorithm based on event unfoldings (using
+`The Anh Pham's thesis <https://tel.archives-ouvertes.fr/tel-02462074>`_), the exploration of scenarios where the actors get killed and/or where
+communications timeout, and the addition of a `wrapper to pthreads <https://hal.inria.fr/hal-02449080>`_, opening the path to the verification classical
+multithreaded applications.
+
+
+**On the model front,** we continued our quest for the modeling of parallel tasks (ptasks for short). Parallel tasks are intended to be an extension
+of the max-min fairness model (that computes the sharing of communication flows or computation tasks) to tasks mixing resource kinds (e.g., a MPI
+computationnal kernel with computations and communications, or a video stream with IO read, network transfer and decompression on the CPU). Just
+specify the amount of computation for each involved host, the amount of data to transfer between each host pair, and you're set. The model will
+identify bottleneck resources and fairly share them across activities within a ptask. From a user-level perspective, SimGrid handles ptasks just like
+every other activity except that the usual SimGrid models (LV08 or SMPI) rely on an optimized algorithm that cannot handle ptasks. You must
+activate :ref:`the L07 model <s4u_ex_ptasks>` on :ref:`the command line <options_model_select>`. This "model" remains a sort of hack since its introduction 15 years ago, as
+it has never been well defined. We never succeded to unify L07 and max-min based models: Fairness is still to be defined in this context that mixes
+flops and communicated bytes. The resulting activity rates are then specific to ptasks. Furthermore, unlike our network models, this model were not
+thoroughly validated with respect to real experiments before `the thesis of Adrien Faure <https://tel.archives-ouvertes.fr/tel-03155702>`_ (and the
+outcome was quite disappointing). Recent articles by Bonald and Roberts `properly define <https://hal.inria.fr/hal-01243985>`_ the allocation
+objective we had in mind (under the name Bounded MaxMin Fairness -- BMF) and `study the convergence <https://hal.archives-ouvertes.fr/hal-01552739>`_
+of the microscopic dynamic model to a macroscopic equilibrium, but this convergence could only be proved in rather simple cases. Even worse, there is
+no known algorithm to efficiently compute a BMF!
+
+L07 should still be avoided as we have exhibited simple scenarios where its solution is irrelevant to the BMF one (that is mathematically sound). This
+release thus introduces a new BMF model to finally unify both classical and parallel tasks, but this is still ongoing work. The implemented
+heuristic works very well for most SimGrid tests, but we have found some (not so prevalent) corner cases where our code fails to solve the sharing
+problem in over 10 minutes... So this all should still be considered an ongoing research effort. We expect to have a better understanding of this issue
+by the next release.
+
+On a related topic, this release introduces :cpp:func:`simgrid::s4u::this_actor::thread_execute`, which allows creating a computation that comprises
+several threads, and thus capable of utilizing more cores than a classical :cpp:func:`simgrid::s4u::this_actor::execute` action. The goal is to make
+it straightforward to model multithreaded computational kernels, and it comes with an illustrating example. It can be seen as a simplified ptask, but
+since it does not mix bytes and flops and has a homogeneous consumption over a single CPU, it perfectly fits with the classical SimGrid model.
+
+This release also introduces steadily progress **on the bindings front**, introducing in particular the Mutex, Barrier and Semaphore to your python scripts.
+
+Version 3.32 (October 3. 2022)
+------------------------------
+
+The Wiedervereinigung release. Germany was reunited 32 years ago.
+
+This release introduces tons of bugs fixes overall, and many small usability improvements contributed by the community.
+
+**On the bindings front**, we further completed the Python bindings: the whole C++ API of Comms is now accessible (and exemplified) in Python, while a
+few missing functions have been added to Engine and Mailboxes. It is also possible to manipulate ptasks from Python.
-This cleaned design allowed us to finally implement the support for mutexes, semaphores and barriers in the model-checker. In particular, this should
-enable the verification of RMA primitives with Mc SimGrid, as their implementation in SMPI is based on mutexes and barriers. Simix, a central element of
-the SimGrid 3 design, was also finally removed: the last bits are deprecated and will be removed in 3.35. We also replaced the old, non-free ISP test suite
-by the one from the `MPI Bug Initiative <https://hal.archives-ouvertes.fr/hal-03474762>`_, but not all tests are activated yet. This should eventually
-help improving the robustness of Mc SimGrid.
+The Python platform generation has also been improved. In particular, user's errors should now raise an exception instead of killing the interpreter.
+Various small improvements have been done to the graphicator tool so that you can now use jupyter to generate your platforms semi-interactively.
-Future work on the model checker include: support for condition variables (that are still not handled), implementation of another exploration algorithm
-based on event unfoldings (`The Anh Pham's thesis <https://tel.archives-ouvertes.fr/tel-02462074/document>`_ was defended in 2019), and the exploration
-of scenarios where the actors get killed and communications timeout. Many things that were long dreamed of now become technically possible in this code base.
+**On the model checking front**, we did many refactoring operations behind the scene (the deprecated ``mc::api`` namespace was for example emptied and removed),
+but there are almost no user-level changes. The internal work is twofold.
+First, we'd like to make optional all the complexity that liveness properties require to explore the application state (dwarf, libunwind, mmalloc,
+etc) and instead only rely on fork to explore all the executions when liveness is not used. This would allow us to run the verified application under valgrind to
+ease its debugging. Some progress was made towards that goal, but we are still rather far from this goal.
+Second, we'd like to simplify the protocol between the model-checker and the application, to make it more robust and hopefully simplify the
+model-checker code. After release v3.31, the model-checker can properly observe the simcall of a given actor through the protocol instead of reading
+the application memory directly, but retrieving the list of actors still requires to read the remote memory, which in turn requires the aforementioned tricks on state
+introspection that we are trying to remove. This goal is much harder to achieve than it may sound in the current code base, but we
+note steady improvements in that direction.
-**On the model front,** we continued our quest for the modeling of parallel tasks (ptasks for short). Parallel tasks are intended to be an extension of the max-min fairness model (for communication flows or computation tasks) to tasks using both network and CPU resources at the same time (e.g., a [p]dgemm or a video stream with IO read, network transfer and decompression on the CPU). Just specify the amount of computation for each involved host, the amount of data to transfer between each host pair, and you're set. The model will identify bottleneck resources and fairly share them across activities within a ptask. From a user-level perspective, SimGrid handles ptasks just like every other activity except that the usual SimGrid models (LV08 or SMPI) rely on an optimized algorithm that cannot handle ptasks. Only the L07 model can handle them and it should be specified on the command line. The L07 "model", proposed 15 years ago (its name is the shorthand for Legrand 2007 although there is no corresponding publication), has never been well defined and was considered as sort of a hack for which we only had an efficient algorithm. We have striven to unify L07 and max-min based models since their introduction, but we never succeeded. One of the underlying reasons is that when mixing flops and communicated bytes, rates become ptask specific and we did not manage to properly define fairness in this context. Furthermore, unlike our network models, this model had never been thoroughly validated with respect to real experiments until recently (in the thesis of Adrien Faure `<https://tel.archives-ouvertes.fr/tel-03155702>`_ and the outcome was quite disappointing). It turns out that a 2015 article by Bonald and Roberts (`<https://hal.inria.fr/hal-01243985>`_) properly defines exactly the allocation objective we had in mind. In a later article (`<https://hal.archives-ouvertes.fr/hal-01552739>`), they proved several properties (existence, non-uniqueness) and studied the convergence of the microscopic dynamic model to a macroscopic equilibrium, but it turned out to be surprisingly difficulty and could only be proved in rather simple cases. Even worse, how to efficiently compute a BMF remains an open question! BMF appears quite sound while we have exhibited very simple scenarios where the solution returned by L07 is irrelevant.
+In addition to these refactoring, this version introduces ``sthread``, a tool to intercept pthread operations at run time. The goal is to use it
+together with the model-checker, but it's not working yet: we get a segfault during the initialization phase, and we failed to debug it so far. If
+only we could use valgrind on the verified application, this would probably be much easier.
-L07 should thus be avoided as much as possible. Instead, a new model called Bounded MaxMin Fairness (BMF) was introduced in this release (thereby allowing to have a fully unified model for both classical tasks and parallel tasks) but this is still ongoing work. We have implemented a heuristic similar to what was suggested in the 2017 article. It works very well for most SimGrid tests, but we have found some (not so prevalent) corner cases where the algorithm fails to find any solution to the sharing problem in a reasonable amount of time (e.g., over 10 minutes). So all this should still be considered highly experimental and we expect to have a better understanding of this issue by the next release.
+But we feel that it's probably better to not delay this release any further, as this tangled web will probably take time to get solved. So ``sthread``
+is included in the source even if it's not usable in MC mode yet.
+
+**On the interface front**, small API fixes and improvements have been done in S4U (in particular about virtual machines), while the support for MPI
+IO has been improved in SMPI. We also hope that ``sthread`` will help simulating OpenMP applications at some point, but it's not usable for that either.
+Hopefully in the next release.
+
+Finally, this release mostly entails maintenance work **on the model front**: a bug was fixed when using ptasks on multicore hosts, and the legacy
+stochastic generator of external load has been reintroduced.
+
+Version 3.33 (never released)
+-----------------------------
+
+This version was overdue for more than 6 months, so it was skipped to not hinder our process of deprecating old code.
+
+Version 3.34 (June 26. 2023)
+----------------------------
-On a related topic, this release introduces ``this_actor::thread_execute()``, which allows creating a computation that comprises several threads, and thus capable of utilizing more cores than a classical ``this_actor::execute()`` action. The goal is to make it straightforward to model multithreaded computational kernels, and it comes with an illustrating example. It can be seen as a simplified ptask, but since it does not mix bytes and flops and has a homogeneous consumption over a single CPU, it perfectly fits with the classical SimGrid model.
+**On the maintenance front,** we removed the ancient MSG interface which end-of-life was scheduled for 2020, the Java bindings
+that was MSG-only, support for native builds on Windows (WSL is now required) and support for 32 bits platforms. Keeping SimGrid
+alive while adding new features require to remove old, unused stuff. The very rare users impacted by these removals are urged to
+move to the new API and systems.
+
+We also conducted many internal refactorings to remove any occurrence of "surf" and "simix". SimGrid v3.12 used a layered design
+where simix was providing synchronizations to actors, on top of surf which was computing the models. These features are now
+provided in modules, not layers. Surf became the kernel::{lmm, resource, routing, timer, xml} modules while simix became
+the kernel::{activity, actor, context} modules.
+
+**On the model front,** we realized an idea that has been on the back of our minds for quite some time. The question
+was: could we use something in the line of the ptask model, that mixes computations and network transfers in a single
+fluid activity, to simulate a *fluid I/O stream activity* that would consume both disk and network resources? This
+remained an open question for years, mainly because the implementation of the ptask does not rely on the LMM solver as
+the other models do. The *fair bottleneck* solver is convenient, but with less solid theoretical bases and the
+development of its replacement (the *bmf solver*) is still ongoing. However, this combination of I/Os and
+communications seemed easier as these activities share the same unit (bytes).
+
+After a few tentatives, we opted for a simple, slightly imperfect, yet convenient way to implement such I/O streams at the
+kernel level. It doesn't require a new model, just that the default HostModels implements a new function which creates a
+classical NetworkAction, but add some I/O-related constraints to it. A couple little hacks here and there, and done! A single
+activity mixing I/Os and communications can be created whose progress is limited by the resource (Disk or Link) of least
+bandwidth value. As a result, a new :cpp:func:`Io::streamto()` function has been added to send data between arbitrary disks or
+hosts. The user can specify a ``src_disk`` on a ``src_host`` and a ``dst_disk`` on a ``dst_host`` to stream data of a
+given ``size``. Note that disks are optional, allowing users to simulate some kind of "disk-to-memory" or "memory-to-disk" I/O
+streams. It's highly inspired by the existing :cpp:func:`Comm::sendto` that can be used to send data between arbitrary hosts.
+
+We also modified the Wi-Fi model so that the total capacity of a link depends on the amount of flows on that link, accordingly to
+the result of some ns-3 experiments. This model can be more accurate for congestioned Wi-Fi links, but its calibration is more
+demanding, as shown in the `example
+<https://framagit.org/simgrid/simgrid/tree/master/teshsuite/models/wifi_usage_decay/wifi_usage_decay.cpp>`_ and in the `research
+paper <https://hal.archives-ouvertes.fr/hal-03777726>`_.
+
+We also worked on the usability of our models, by actually writing the long overdue documentation of our TCP models and by renaming
+some options for clarity (old names are still accepted as aliases). A new function ``s4u::Engine::flatify_platform()`` dumps an
+XML representation that is inefficient (all zones are flatified) but easier to read (routes are explicitly defined). You should
+not use the output as a regular input file, but it will prove useful to double-check the your platform.
+
+**On the interface front**, some functions were deprecated and will be removed in 4 versions, while some old deprecated functions
+were removed in this version, as usual.
+
+Expressing your application as a DAG or a workflow is even more integrated than before. We added a new tutorial on simulating
+DAGs and a DAG loader for workflows using the `wfcommons formalism <https://wfcommons.org/>`_. Starting an activity is now
+properly delayed until after all its dependencies are fulfilled. We also added a notion of :ref:`Task <API_s4u_Tasks>`, a sort
+of activity that can be fired several time. It's very useful to represent complex workflows. We added a ``on_this`` variant of
+:ref:`every signal <s4u_API_signals>`, to react to the signals emitted by one object instance only. This is sometimes easier than
+reacting to every signals of a class, and then filtering on the object you want. Activity signals (veto, suspend, resume,
+completion) are now specialized by activity class. That is, callbacks registered in Exec::on_suspend_cb will not be fired for
+Comms nor Ios
+
+Three new useful plugins were added: The :ref:`battery plugin<plugin_battery>` can be used to create batteries that get discharged
+by the energy consumption of a given host, the :ref:`solar panel plugin <plugin_solar_panel>` can be used to create
+solar panels which energy production depends on the solar irradiance and the :ref:`chiller plugin <plugin_chiller>` can be used to
+create chillers and compensate the heat generated by hosts. These plugins could probably be better integrated
+in the framework, but our goal is to include in SimGrid the building blocks upon which everybody would agree, while the model
+elements that are more arguable are provided as plugins, in the hope that the users will carefully assess the plugins and adapt
+them to their specific needs before usage. Here for example, there is several models of batteries (the one provided does not
+take the aging into account), and would not be adapted to every studies.
+
+It is now easy to mix S4U actors and SMPI applications, or even to start more than one MPI application in a given simulation
+with the :ref:`SMPI_app_instance_start() <SMPI_mix_s4u>` function.
+
+**On the model checking front**, this release brings a huge load of good improvements. First, we finished the long refactoring
+so that the model-checker only reads the memory of the application for state equality (used for liveness checking) and for
+:ref:`stateful checking <cfg=model-check/checkpoint>`. Instead, the network protocol is used to retrieve the information and the
+application is simply forked to explore new execution branches. The code is now easier to read and to understand. Even better,
+the verification of safety properties is now enabled by default on every platforms since it does not depend on advanced OS
+mechanisms anymore. You can even run the verified application in valgrind in that case. On the other hand, liveness checking
+still needs to be enabled at compile time if you need it. Tbh, this part of the framework is not very well maintained nowadays.
+We should introduce more testing of the liveness verification at some point to fix this situation.
+
+Back on to safety verification, we fixed a bug in the DPOR reduction which resulted in some failures to be missed by the
+exploration, but this somewhat hinders the reduction quality (as we don't miss branches anymore). Some scenarios which could be
+exhaustively explored earlier (with our buggy algorithm) are now too large for our (correct) exploration algorithm. But that's
+not a problem because we implemented several mechanism to improve the performance of the verification. First, we implemented
+source sets in DPOR, to blacklist transitions that are redundant with previously explored ones. Then, we implemented several new
+DPOR variants. SDPOR and ODPOR are very efficient algorithms described in the paper "Source Sets: A Foundation for Optimal
+Dynamic Partial Order Reduction" by Abdulla et al in 2017. We also have an experimental implementation of UPDOR, described in
+the paper "Unfolding-based Partial Order Reduction" by Rodriguez et al in 2015, but it's not completely functional yet. We hope
+to finish it for the next release. And finally, we implemented a guiding mechanism trying to converge faster toward the bugs in
+the reduced state space. We have some naive heuristics, and we hope to provide better ones in the next release.
+
+We also extended the sthread module, which allows to intercept simple code that use pthread mutex and semaphores to simulate and
+verify it. You do not even need to recompile your code, as it uses LD_PRELOAD to intercept on the target functions. This module
+is still rather young, but it could probably be useful already, e.g. to verify the code written by students in a class on UNIX
+IPC and synchronization. Check `the examples <https://framagit.org/simgrid/simgrid/tree/master/examples/sthread>`_. 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 future.
+
+Version 3.35 (November 23. 2023)
+--------------------------------
+
+**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 heap 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.
+
+Version 3.36 (TBD)
+------------------
.. |br| raw:: html
