Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries

Nathalie Bertrand 1 Igor Konnov 2 Marijana Lazic 3 Josef Widder 4
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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. The combination of these challenges makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized 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 no process enters round r before all other processes finished round r −1. For almost-sure 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 to classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

https://hal.inria.fr/hal-01925533
Contributor : Nathalie Bertrand <>
Submitted on : Friday, April 19, 2019 - 10:37:27 AM
Last modification on : Sunday, April 21, 2019 - 1:17:29 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01925533, version 3

Citation

Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder. Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries. 2019. ⟨hal-01925533v3⟩

Share

Metrics

Record views

70

Files downloads

223