An Agda Formalization of Üresin and Dubois’ Asynchronous Fixed-Point Theory
View / Open Files
Authors
Zmigrod, R
Daggitt, ML
Griffin, TG
Publication Date
2018Journal Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name
Interactive Theorem Proving
ISSN
0302-9743
ISBN
9783319948201
Publisher
Springer International Publishing
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
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk