OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Tasks in Modular Proofs of Concurrent Algorithms

Castañeda, Armando and Hurault, Aurélie and Quéinnec, Philippe and Roy, Matthieu Tasks in Modular Proofs of Concurrent Algorithms. (2019) In: 21st International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2019), 22 October 2019 - 25 October 2019 (Pisa, Italy).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
360kB

Official URL: https://doi.org/10.1007/978-3-030-34992-9_6

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. The Moir&Anderson implementation of renaming using splitters is an iconic example of such algorithms designed by composition.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-02903005
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Other partners > Consejo Nacional de Ciencia y Tecnología - CONACYT (MEXICO)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Other partners > Universidad Nacional Autónoma de México - UNAM (MEXICO)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited On:20 Jul 2020 13:27

Repository Staff Only: item control page