- Rework the internals, for simpler and modern code. This shall unlock many future improvements.
- You can now define plugins onto SafetyChecker (a simple DFS explorer), using the declared signals.
See CommunicationDeterminism for an example.
- - Support mutex in DPOR reduction
+ - Support mutex and semaphore in DPOR reduction
- Seems to work on Arm64 architectures too.
- Display a nice error message when ptrace is not usable.
S4U:
- New signal: Engine::on_simulation_start_cb()
+New plugin: the Chaos Monkey (killing actors at any time)
+ - Along with the new simgrid-monkey script, it tests whether your simulation
+ resists resource failures at any possible timestamp in your simulation.
+ - It is mostly intended to test the simgrid core in extreme conditions,
+ but users may find it interesting too.
+
XBT:
- Drop xbt_dynar_shrink().
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.
-Future work on the model checker include: support for mutexes (that are still not handled), implementation of another exploration algorithm based on UDPOR
+This cleaned design allowed us to finally implement the support for mutexes and semaphores in the model-checker.
+
+Future work on the model checker include: support for condition variables and barriers (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.
