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

Many applications work with an iterative algorithm \(\mathbf F \) and an initial state \(\mathbf x (0)\) where successive states are computed asuntil a fixed point \(\xi \) is reached at some time \(t'\) when \(\mathbf x (t') = \xi = \mathbf F (\xi )\). Here we assume that \(\mathbf x (t)\) represents an n-dimensional vector in some state space. If we rewrite \(\mathbf F \) asthen we can imagine that it may be possible to assign the computation of each \(\mathbf F _i\) to a distinct processor. This might be performed in parallel with shared memory or in a completely distributed manner. However, enforcing correctness using global synchronization mechanisms may incur performance penalties that negate the gains from the parallelization. Furthermore, global synchronization is infeasible for applications such as network routing.

This leads to the question: When can we use the \(\mathbf F _i\) to correctly implement an asynchronous version of \(\mathbf F \)-iteration? There are many answers to this question that depend on properties of the state space and the function \(\mathbf F \) – see the survey paper by Frommer & Syzld [9].

Many of the approaches discussed in [9] rely on the rich structure of vector spaces over continuous domains. However, our motivation arises from network routing protocols where the state space is comprised of discrete data. Happily, Üresin and Dubois [21] have developed a theory of asynchronous iterations over discrete state spaces. They prove that if \(\mathbf F \) is an Asynchronously Contracting Operator (ACO, see Sect. 3), then the associated asynchronous iteration will always converge to the correct fixed point. Their proof uses very weak assumptions about inter-process communication (indeed, in the case that the state space is finite they show that ACO is a necessary condition as well). These weak assumptions are a good model for the case of distributed routing protocols where messages can be delayed, lost, duplicated or reordered. Henceforth we will refer to Üresin and Dubois [21] as UD.

Proving that a given \(\mathbf F \) is an ACO can be dramatically simpler than reasoning directly about an asynchronous implementation. However, in many cases it still remains non-trivial and so UD also derive several sufficient conditions that imply the ACO condition. These conditions are typically easier to prove for many common iterative algorithms. For example, they provide sufficient conditions for special cases where the state space is a partial order and \(\mathbf F \) is order preserving.

In this paper we describe an Agda [3] formalization of the sufficient conditions and associated proofs from UD. This represents one part of a larger project in which we are developing formalized proofs of the asynchronous convergence for policy-rich distributed Bellman-Ford routing protocols (see [5]). This work required formalizing a new sufficient condition not found in UD, based on the ultrametric theory of Gurney [11]. During formalization it also became apparent that two of the other sufficient conditions in the original paper are incorrect. We provide a counter-example. In addition we suggest how to strengthen one of the sufficient conditions so that correctness is still guaranteed.

Many other applications of the results of UD can be found in the literature (for example, [4, 6, 7, 16]). The proofs in UD are mathematically rigorous in the traditional sense, but their definitions are somewhat informal and they occasionally claim the existence of objects without providing an explicit construction. In our opinion a formal verification of the results is therefore a useful exercise.

There have been other efforts to formalize asynchronous computation such as Meseguer and Ölveczky [17] for real-time systems and Henrio, Khan, and Kammüller [13, 14] for distributed languages. However, as far as we know our work is the first attempt to formalize the results of UD.

Our Agda development can be found on Github [1]. We hope that this will be a valuable resource for others interested in asynchronous iterations.

We begin by formalizing the product state space \(S = S_1 \times \cdots \times S_n\). This is encoded by a -indexed family of s. The type is a function that takes i and returns the type of the i-th setoid. We can now formalize the iterative algorithm as follows:

Routing Example. We briefly outline how this work can be applied to reasoning about convergence of a very general class of internet routing protocols. Full details can be found in Daggitt et al. [5].

Routing problems can be formalized as a tuple \((R,\ \oplus ,\ E,\ \bar{0},\ \infty )\), where:

A network configuration is represented as an \(n \times n\) adjacency matrix \(\mathbf A \) over E. The state space is made up of \(n \times n\) matrices \(\mathbf X \) over R. Matrix addition, \(\mathbf X \oplus \mathbf X '\), is just the pointwise application of \(\oplus \). The application of \(\mathbf A \) to state \(\mathbf X \) is defined asThat is, each node i choose the best extensions of the routes to j advertised by its neighbors. Finally, the iterative algorithm \(\mathbf F \) is defined aswhere \(\mathbf I \) is the matrix defined as \(\mathbf I _{ii} = \bar{0}\), and \(\mathbf I _{ij} = \infty \) for \(i\not = j\). As explained in [5], an asynchronous version of \(\mathbf F \) provides a good model of Distributed Bellman-Ford (DBF) routing protocols. At each asynchronous iteration in the distributed setting, each node i will compute only the i-th row of \(\mathbf F (\mathbf X )\) from the rows communicated by its adjacent neighbors.

Shortest paths routing is probably the simplest example where \(\oplus = \min \) and E is the set of all \(f_w\) with \(f_w(r) = w + r\).

UD define a class of \(\mathbf F \)s called Asynchronously Contracting Operators (ACOs). They then prove that if an operator is an ACO, then it will converge to the correct fixed point for all possible schedules.

The sequence D(K) can be seen as a form of approximation for the process with each iteration providing a higher accuracy. Each set contains the possible states at a moment in time. D(0) contains many possible states as the algorithm has just begun, and each set in the sequence removes some incorrect states. This occurs until \(D(T)=\{ \mathbf {\xi }\}\) when the converged state has been found.

The definition of an ACO is captured in the following record type:

The variable represents the universe level of the family of sets , while the universe level of is inferred automatically ( ). The sets themselves are implemented as a double-indexed family of predicates over .

In order to prove this theorem, UD consider the concept of a pseudo-periodic schedule. It is then proved that every schedule (Definition 2) is in fact pseudo-periodic, which greatly simplifies reasoning about schedules. This is perhaps the least rigorous aspect of the work of UD, as they state this without proof.

The intuition behind \(\varphi \) is that by time \(\varphi (K+1)\) every node is guaranteed to be using data generated at least as recently as \(\varphi (K)\). Hence the interval \((\varphi (K),\varphi (K+1)]\) is known as the \(k^{th}\) pseudo-period.

We formalize the pseudo-periodic property in Agda as follows:

Note that this represents a simplification of UD’s definition. We worked backwards from the proof of Theorem 1 and identified only those properties required. This simplification may have to change if we extend our library to include UD’s proof that the ACO condition is also necessary (in the case of finite state spaces).

UD assert that for any schedule there exist an infinite number of possible functions \(\varphi \), but they do not provide any explicit constructions. This is one area where we had initial concerns when planning our proof strategy in Agda.

We start by defining , which takes a time t and a node index i and returns the first time after t for which that i is active.

We then define , which returns the first time after t such that all nodes have activated since t.

We then need to define three auxiliary functions: returns a time after which i does not use the data generated by j at time t.

returns a time after which i only uses data generated by j after time t.

returns a time after which i only uses data generated after time t.

Using these we can define the function that returns a time after which all nodes only use data generated after time t.

Finally, we construct \(\varphi \) as follows:

Therefore we find a time t such that all nodes have been activated after \(\varphi (K)\) and then \(\varphi (K+1)\) is defined as the time after which all data used was generated after t. The function \(\tau \) (as defined in property (iii) of pseudo-periodic schedules) is simply a special call to .

We now prove that and satisfy the properties required to be pseudo-periodic as given in Definition 5. The property is relatively simple, given that proofs that the various functions are increasing:

The second property says that is always active and it can be satisfied by using properties of :

The third property can be easily proved using the fact that is increasing:

The final property states that at all points during a pseudo-period, no nodes use information generated in a previous pseudo-period. This is the most complex of the four properties to prove.

As previously mentioned the construction of \(\varphi \) is not discussed in UD. Nevertheless, filling this gap required significant effort in our Agda development.

The proof of Theorem 1 requires an additional fact about the functions \(\tau _i\): for each K, once all i have been updated after some time t, then \(\mathbf x (t) \in D(K)\).

In UD Lemma 1 is proved by a fairly easy induction on K. However, in Agda the construction, called , turned out to be more difficult. Several smaller lemmas were required, the biggest of which is that the asynchronous iteration remains within D(0), the proof of which is called .

We now construct the final proof of convergence. To do this we must construct a time after which the result of the asynchronous iteration is always equal to the fixed point. UD prove that \(\varphi (T+1)\), where T is from the ACO, is the convergence time. This is because each pseudo-period, every node is updated at least once and a total of T updates must occur before convergence. In the Agda, we first extract and from . We then prove Theorem 1 as follows.

UD show that being an ACO is a sufficient (and sometimes a necessary) condition for convergence. However in practice, constructing the sets D(K) can still be a non-trivial exercise. Therefore, an extensive array of sufficient (but often not necessary) conditions have been constructed that in practice can be simpler and more intuitive to apply. These conditions are nearly always a reduction back to ACOs.

In this section we discuss three different proposed sufficient conditions. The first two are from UD and the third is a modified version of a new sufficient condition found in a recent paper by Gurney [11] (which was essential for the results described in Daggitt et al. [5]). During the formalization process, we discovered counterexamples to the two conditions from UD.

In this paper we have taken the mathematically rigorous yet informal proof of Üresin and Dubois’ theory regarding the convergence of asynchronous iterations [21] and formalized it constructively in Agda. After explicitly constructing the previously unspecified pseudo-periodic sequences and mildly weakening some assumptions, we have succeeded in formalizing the core theorem of the paper. However some of the auxiliary propositions proposed in the original paper turned out to be false. In our opinion this alone justifies the formalization process.

Furthermore, we have described our library of proofs and sufficient conditions for asynchronous convergence, including a recent, new ultrametric condition. We hope that the library of sufficient conditions will be a valuable resource for those wanting to formally verify the convergence of a wide range of asynchronous iterations. The library is available on Github [1].

We are primarily interested in proving convergence and therefore we have thus far only formalized the sufficient conditions from Üresin and Dubois and not their proof that the ACO condition is also necessary in the case of finite state spaces. This would be an interesting extension to our development. In addition it would be interesting to see if other related work such as [15, 22, 23], using different models, could be integrated into our formalization.