Contacts: Erwan.JahierATuniv-grenoble-alpes.fr, Karine.AltisenATuniv-grenoble-alpes.fr, Stephane.DevismesATu-picardie.fr
Keywords: distributed algorithms, self-stabilization, simulation.
The design of distributed algorithms usually involves high-level models to describe the system and its semantics. The model abstracts away most of the very precise behavior of the system to rather focus on the main nature of distributed computations, that is: processes have local programs and memory and can only share information using message exchanges.
Distributed algorithms are developed and analyzed in such a (theoretical) model: usually their specification as well as their complexity are proven. Now, the distributed nature of the computation involves many situations and particular cases; furthermore, the design of distributed algorithms becomes harsher when in one hand the requirements are reinforced and in the other hand the environment becomes more intricate (how to obtain a fault-tolerant solution in a very highly dynamic environment?). This is why tools helping the design are mandatory.
We propose here a simulator, called SASA, that can be used as a debugging tool to interactively test the solution (i.e. the distributed algorithm) under development. The SASA simulator focuses on a family of fault-tolerant solutions called self-stabilizing algorithms.
Recently, we enhanced SASA with simulation campaign support: the tool allows to compute benchmarks where simulations can be launched as many times as necessary on various inputs - for example, a family of randomly generated networks - in order to obtain performance evaluations and in particular average time complexity. The goal of the internship would be to perform a broad simulation campaign on a given family of distributed fault-tolerant algorithms in order to measure fault-containment (how far and long can a fault disturb and break down the behavior of the system?).
Further developments of SASA (written in OCAML) would include:
- support for other input algorithm languages;
- connection to verification tools such as a model-checkers or a proof assistant;
- design of search heuristics to find worst-case scenarios
SASA Webpage: https://verimag.gricad-pages.univ-g...
Working context: The internship is part of ANR project ESTATE. The student will be integrated in the lab Verimag.
Possible extension into a PhD thesis.