The TAU Programming Languages and Systems Seminar - Synthesis of Distributed Algorithms with Parameterized Thresholds Guards

Abstract:

In threshold-based distributed algorithms, a process has to wait until the number of messages it receives reaches a certain threshold, in order to perform an action. Examples of such distributed algorithms include fault-tolerant broadcast, non-blocking atomic commitment, and consensus. I will present an automated method for synthesizing these thresholds, given a sketch of a distributed algorithm and specifications. In this way we synthesize distributed algorithms that are correct for every number n of processes and every number t of faults, provided some resilience condition holds, e.g. n > 3t. This approach combines recent progress in parameterized model checking of distributed algorithms, which I will also address in this talk, with counterexample-guided synthesis.

This is joint work with Igor Konnov, Josef Widder and Roderick Bloem.