Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries - Archive ouverte HAL Access content directly
Journal Articles International Journal on Software Tools for Technology Transfer Year : 2021

Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries

(1) , (2) , (3) , (2)
1
2
3

Abstract

Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r − 1. For almostsure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine This is an extended version of [7], which appeared in the proceedings of CONCUR 2019. In the conference version, we did not provide proofs. As a result, also the definitions where just sketched and we omitted preliminary lemmas. In this paper we completely develop our theory. Moreover, we give more detailed discussions and explanation with new figures and diagrams, we add and extend examples.
Fichier principal
Vignette du fichier
main.pdf (618.12 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03480268 , version 1 (14-12-2021)

Identifiers

Cite

Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder. Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries. International Journal on Software Tools for Technology Transfer, 2021, 23, pp.797-821. ⟨10.1007/s10009-020-00603-x⟩. ⟨hal-03480268⟩
79 View
48 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More