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 classical debugging tools such as gdb or valgrind on that Frankenstein process. Having more than one heap in your process is not
-usually supported.
+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.
-The design was simplified in v3.12 (2015) by splitting the application and the checker in separate system process. But both processes remained tightly
+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
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
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 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.
+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.
-Future work on the model checker include: support for condition variables (that are still not handled), implementation of another exploration algorithm based on UDPOR
-(`The Anh Pham's thesis <https://tel.archives-ouvertes.fr/tel-02462074/document>`_ was defended in 2019), and robustness improvement using the `MPI Bug
-Initiative <https://hal.archives-ouvertes.fr/hal-03474762>`_ tests. Many things that were long dreamed of now become technically possible in this code base.
+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 front, we added BMF...
.. |br| raw:: html