Repository logo
 

An Agda Formalization of Üresin and Dubois’ Asynchronous Fixed-Point Theory

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Zmigrod, R 
Daggitt, ML 
Griffin, TG 

Abstract

In this paper we describe an Agda-based formalization of results from "{U}resin & Dubois' ``Parallel Asynchronous Algorithms for Discrete Data.'' That paper investigates a large class of iterative algorithms that can be transformed into asynchronous processes. In their model each node asynchronously performs partial computations and communicates results to other nodes using unreliable channels. "{U}resin & Dubois provide sufficient conditions on iterative algorithms that guarantee convergence to unique fixed points for the associated asynchronous iterations. Proving such sufficient conditions for an iterative algorithm is often dramatically simpler than reasoning directly about an asynchronous implementation. These results are used extensively in the literature of distributed computation, making formal verification worthwhile.

Our Agda library provides users with a collection of sufficient conditions, some of which mildly relax assumptions made in the original paper. Our primary application has been in reasoning about the correctness of network routing protocols. To do so we have derived a new sufficient condition based on the ultrametric theory of Alexander Gurney. This was needed to model the complex policy-rich routing protocol that maintains global connectivity in the internet.

Description

Keywords

4606 Distributed Computing and Systems Software, 46 Information and Computing Sciences

Journal Title

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Conference Name

Interactive Theorem Proving

Journal ISSN

0302-9743
1611-3349

Volume Title

10895 LNCS

Publisher

Springer International Publishing
Sponsorship
EPSRC (1642042)