OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Proving a Non-Blocking Algorithm for Process Renaming with TLA+

Hurault, Aurélie and Quéinnec, Philippe Proving a Non-Blocking Algorithm for Process Renaming with TLA+. (2019) In: 13th International Conference on Tests and Proofs (TAP 2019), part of the 3rd World Congress on Formal Methods, 9 October 2019 - 11 October 2019 (Porto, Portugal).

[img]
Preview
(Document in English)

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

Official URL: https://doi.org/10.1007/978-3-030-31157-5_10

Abstract

Shared-memory concurrent algorithms are well-known for being difficult to write, ill-adapted to test, and complex to prove. Wait-free concurrent objects are a subclass where a process is never prevented from progressing, whatever the other processes are doing (or not doing). Algorithms in this subclass are often non intuitive and among the most complex to prove. This paper presents the analysis and the proof of a wait-free concurrent algorithm that is used to rename processes. By its adaptive and non-blocking nature, the renaming algorithm resists to test, because of the cost of covering all its states and transitions even with a small input set. Thus, a proof has been conducted in Open image in new window and verified with TLAPS, the Open image in new window Proof System. This algorithm is itself based on the assembly of wait-free concurrent objects, the splitters, that separate processes. With just two shared variables and three assignments, a splitter seems a simple object but it is not linearizable. To avoid explicitly in-lining it and dealing with its internal state, the proof of the renaming algorithm relies on replacing the splitter with a sequential specification that is proved correct with TLAPS and verified complete by model-checking on finite instances.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in volume 11823 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN: 978-3-030-31156-8 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-030-31157-5_10
HAL Id:hal-02442015
Audience (conference):National conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
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:
Funders:
ANR : Agence nationale de la recherche (France)
Statistics:download
Deposited By: IRIT IRIT
Deposited On:12 Dec 2019 09:40

Repository Staff Only: item control page