2021-03558 - PhD Position F/M Verification of distributed algorithms with fair schedulers

Contract type : Fixed-term contract

Level of qualifications required : Graduate degree or equivalent

Fonction : PhD Position

About the research centre or Inria department

The Inria Rennes - Bretagne Atlantique Centre is one of Inria's eight centres and has more than thirty research teams. The Inria Center is a major and recognized player in the field of digital sciences. It is at the heart of a rich R&D and innovation ecosystem: highly innovative PMEs, large industrial groups, competitiveness clusters, research and higher education players, laboratories of excellence, technological research institute, etc.

Assignment

Context

Distributed algorithms are algorithms executed asynchronously by several identical components that interact and communicate e.g. by rendez-vous, message broadcast, or shared variables. They are heavily used in numerous applications such as telecommunications, cloud computing or blockchain technologies. Such algorithms usually have simple objectives, such as selecting a leader among the participants or agreeing on a proposed value. Still, in the area of distributed algorithms, proving correctness properties of such algorithms usually relies on ad hoc manual proofs. One of the main difficulties lies in the fact that the number of components is seen as a parameter, and that the aim is to prove correctness for any value of this parameter.

In the area of model checking, parameterized verification has been a very active field over the last few years [BJK+15, BMR+16, LR16, BKL+19, BEH+20]: it precisely aims at developing model-checking techniques to verify properties of parameterized systems, made of an arbitrary number of copies of one component (usually represented as a finite transition system). Automated verification techniques would avoid errors in the highly non-trivial task analyzing of distributed algorithms. However, modelling real-life distributed algorithms and proving their correctness is still mostly out-of-reach of formal verification techniques, either because the models considered are not expressive enough, or because the techniques are not adapted (e.g., they do not take fairness into account), or because they are not efficient enough.

Objectives

Our aim is to develop automated parameterized-verification techniques to formally prove properties of distributed algorithms. A possible target is to be able to automatically prove correctness of Aspnes' consensus algorithm [Asp02], in which a network of components have to reach a consensus using shared variables.

A model-checking technique has recently been developed to verify termination of consensus algorithms for a bounded number of shared registers [BMR+16]. It addresses fairness issues by considering a randomized scheduler. However, this technique does not apply to Aspnes' algorithm, which requires two registers per round (hence arbitrarily many registers). Our aim is to build on such existing work to develop and analyze (complexity-wise) novel verification techniques that would apply to distributed algorithms such as Aspnes'.

 

Bibliographie

[BMR+16] Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, Daniel Stan: Reachability in Networks of Register Protocols under Stochastic Schedulers. ICALP 2016, pages 106:1-106:14.

[Asp02] James Aspnes: Fast deterministic consensus in a noisy environment. J. Algorithms 45(1):16-39 (2002).

[BEH+20] Michael Blondin, Javier Esparza, Martin Helfrich, Antonin Kucera, Philipp J. Meyer: Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. CAV 2020 (2), pages 372-397.

[BKL+19] Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder: Verification of randomized Consensus Algorithms Under Round-Rigid Adversaries. CONCUR 2019, pages 33:1-33:15.

[BJK+15] Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers 2015.

[LR16] Anthony W. Lin, Philipp Ruemmer: Liveness of Randomised Parameterised Systems under Arbitrary Schedulers. CAV 2016 (2), pages 112-133.

 

 

Main activities

Working on bibliography, writing papers, giving talks, writing thesis manuscript.

 

Benefits package

  • Subsidized meals
  • Partial reimbursement of public transport costs

Remuneration

monthly gross salary amounting to 1982 euros for the first and second years and 2085 euros for the third year