Tasks in modular proofs of concurrent algorithms - Assistance à la Certification d’Applications DIstribuées et Embarquées Access content directly
Journal Articles Information and Computation Year : 2023

Tasks in modular proofs of concurrent algorithms

Abstract

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
Origin : Files produced by the author(s)
licence : CC BY NC ND - Attribution - NonCommercial - NoDerivatives

Dates and versions

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

Identifiers

Cite

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⟩
56 View
21 Download

Altmetric

Share

Gmail Facebook X LinkedIn More