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.
-
-We 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).
-Many things that were long dreamed of now become technically possible in this code base.
+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 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...
