Tasks in modular proofs of concurrent algorithms

Armando Castañeda (1) , Aurélie Hurault (2, 3) , Philippe Quéinnec (3) , Matthieu Roy (4)

1 UNAM - Universidad Nacional Autónoma de México = National Autonomous University of Mexico
2 Toulouse INP - Institut National Polytechnique (Toulouse)
3 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
4 LAAS-TSF - Équipe Tolérance aux fautes et Sûreté de Fonctionnement informatique

Proving correctness of distributed or concurrent algorithms is a mind-challenging and complex process. Slight errors in the reasoning are difficult to find, calling for computer-checked proof systems. In order to build computer-checked proofs with usual tools, such as Coq or TLA + , having sequential specifications of all base objects that are used as building blocks in a given algorithm is a requisite to provide a modular proof built by composition. Alas, many concurrent objects do not have a sequential specification. This article describes a systematic method to transform any task, a specification method that captures concurrent one-shot distributed problems, into a sequential specification involving two calls, set and get. This transformation allows system designers to compose proofs, thus providing a framework for modular computer-checked proofs of algorithms designed using tasks and sequential objects as building blocks. Moir & Anderson implementation of renaming using splitters is an iconic example of such algorithms designed by composition, although the actual algorithm is not modular. Moir & Anderson algorithm is adaptive and non-blocking, and, being the assembly of wait-free concurrent objects, the splitters, it resists testing, because of the cost of covering all its states and transitions even with a small input set. Using the get/set transformation, a modular description of the algorithm can be obtained. A proof of the modular algorithm has been conducted in TLA + and verified with TLAPS, the TLA + Proof System. As far as we know, this is the first time this algorithm is mechanically verified.

Mots clés: Formal methods; Verification; Concurrent algorithms; Renaming; Splitter; Linearizability; Distributed tasks; TLA +

Domaines: Calcul parallèle, distribué et partagé [cs.DC]

Armando Castañeda, Aurélie Hurault, Philippe Quéinnec, Matthieu Roy. Tasks in modular proofs of concurrent algorithms. Information and Computation, 2023, 292 (Selected papers from SSS’2019, the 21st International Symposium on Stabilization, Safety, and Security of Distributed Systems), pp.105040. ⟨10.1016/j.ic.2023.105040⟩. ⟨hal-04086420⟩