ABSTRACT. It is well known that reasoning about asynchronous processes is far harder than their synchronous counterparts. Motivated by this, sig- nificant work has been put into developing theorems that allow one to reason about asynchronous processes as if they were synchronous. These theorems drastically simplify the burden of proof required for guarantee- ing desirable asynchronous behaviour. Naturally this shifts the complex- ity from the user to these theorems. Hence, a formal verification of their correctness is a worthwhile exercise.

In this paper we describe an Agda-based formalisation of the results from Üresin & Dubois’s "Parallel Asynchronous Algorithms for Discrete Data". Their paper provides sufficient conditions for the convergence of asynchronous processes to unique fixed points, and their results are used extensively in later literature as the basis of further sufficient conditions. Our development provides a usable library with a selection of sufficient conditions, including a new condition based on ultrametrics that can be applied to inter-domain routing in the internet. We also manage to mildly relax the assumptions made in the original paper.