Tasks in modular proofs of concurrent algorithms - Assistance à la Certification d’Applications DIstribuées et Embarquées
Article Dans Une Revue Information and Computation Année : 2023

Tasks in modular proofs of concurrent algorithms

Résumé

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.
Fichier principal
Vignette du fichier
journal-final.pdf (900.17 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
licence

Dates et versions

hal-04086420 , version 1 (02-05-2023)

Licence

Identifiants

Citer

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⟩
151 Consultations
92 Téléchargements

Altmetric

Partager

More