An Agda Formalization of Üresin and Dubois’ Asynchronous Fixed-Point Theory
View / Open Files
Publication Date
2018-01-01Journal Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN
0302-9743
ISBN
9783319948201
Volume
10895 LNCS
Pages
623-639
Type
Conference Object
Metadata
Show full item recordCitation
Zmigrod, R., Daggitt, M., & Griffin, T. (2018). An Agda Formalization of Üresin and Dubois’ Asynchronous Fixed-Point Theory. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10895 LNCS 623-639. https://doi.org/10.1007/978-3-319-94821-8_37
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.
Sponsorship
EPSRC (1642042)
Identifiers
External DOI: https://doi.org/10.1007/978-3-319-94821-8_37
This record's URL: https://www.repository.cam.ac.uk/handle/1810/280227