A Relaxation of Üresin and Dubois’ Asynchronous Fixed-Point Theory in Agda

Let \(S\) be a set. Iterative algorithms attempt to find a fixed point \(x^*\in S\) for a function \(\mathbf{F }: S\rightarrow S\) by repeatedly applying the function to some initial starting point \(x \in S\). The state after k such iterations, \(\sigma ^k(x)\), is defined as follows:The algorithm terminates when it reaches an iteration \(k^*\) such that \({\sigma ^{k^*+1}(x) = \sigma ^{k^*}(x)}\) and so \(x^*= \sigma ^{k^*}(x)\) is the desired fixed point.

Many iterative algorithms can be performed in parallel. Assume that the state space \(S\) and the function \(\mathbf{F }\) are decomposable into n parts:where \(\mathbf{F }_i : S\rightarrow S_i\) takes in a state and calculates the ith component of the new state. It is now possible to assign the computation of each \(\mathbf{F }_i\) to a separate processor. The processors may be part of a single computer with shared memory or distributed across many networked computers. We would prefer our model to be agnostic to this choice, and so this paper will simply refer to the processors as nodes. Each node i continues to apply \(\mathbf{F }_i\) locally and propagate its updated state to the other nodes who incorporate it into their own computations. We will refer to an asynchronous implementation of this scheme as \(\delta \). A rigorous mathematical definition of \(\delta \) will be presented in Sect. 2.2.

If the nodes’ applications of \(\mathbf{F }_i\) are synchronised then the parallel computation \(\delta \) will be identical to \(\sigma \). However in many cases enforcing synchronisation may not be practical or even possible. For example in distributed routing, the overhead of synchronisation on a continental scale would be prohibitive to the operation of the protocol. However, when updates are performed asynchronously, the behaviour of \(\delta \) depends on the exact sequence of node activations and the timings of update messages between nodes. Furthermore, \(\delta \) may enter states unreachable by \(\sigma \) and hence \(\delta \) may not converge even when \(\sigma \) is guaranteed to do so. This motivates the question: what properties of \(\mathbf{F }\) are required to guarantee that the asynchronous computation \(\delta \) always converges to a unique fixed point?

Depending on the properties of the state space \(S\) and the function \(\mathbf{F }\), there are multiple answers to this question—see the survey paper by Frommer and Szyld [12]. For example many of the approaches discussed in [12] rely on the rich structure of vector spaces over continuous domains. Üresin and Dubois [20] were the first to develop a theory that applied to both discrete and continuous domains. They prove that if \(\mathbf{F }\) is an asynchronously contracting operator (ACO), then \(\delta \) will always converge to a unique fixed point. Their model makes only very weak assumptions about inter-node communication and allows messages to be delayed, lost, duplicated and reordered. Henceforth we will refer to Üresin and Dubois [20] as UD.

Proving that \(\mathbf{F }\) is an ACO is dramatically simpler than directly reasoning about the asynchronous behaviour of \(\delta \). However, in many cases it remains non-trivial and so UD also derive several alternative conditions that are easier to prove in special cases and that imply the ACO conditions. For example, they provide sufficient conditions when \(S\) is partially ordered and \(\mathbf{F }\) is order preserving.

Many applications of these results can be found in the literature including in routing [6, 9], programming language design [10], peer-to-peer protocols [16] and numerical simulation [7].

This paper makes several contributions to UD’s existing theory. The original intention was to formalise the work of UD in the proof assistant Agda [4] as part of a larger project to develop formal proofs of correctness for distributed routing protocols [8]. 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. Given this and the breadth of fields these results have been applied to, in our opinion a formal verification of the results is a useful exercise.

During the process of formalisation, we discovered various relaxations of the theory. This includes: (i) enlarging the set of schedules for which it is possible to prove \(\delta \) converges over, (ii) relaxing the ACO conditions and (iii) generalising the model to include fully distributed algorithms rather than just shared-memory models. Furthermore, it was found that two of UD’s auxiliary sufficient conditions were incorrect, and we demonstrate a counter-example: an iteration which satisfies the conditions yet does not converge to a unique fixed point. Finally, we also formalise (and relax) a recently proposed alternative sufficient condition based on metric spaces by Gurney [13].

We have made the resulting library publicly available [1]. Its modular design should make it easy to apply the results to specific algorithms without understanding the technical details and we hope that it will be of use to others who are interested in developing formal proofs of correctness for asynchronous iterative algorithms. In this paper we have also included key definitions and proofs from the library alongside the standard mathematics. We do not provide an introduction to Agda, but have tried to mirror the mathematical notation as closely as possible to ensure that it is readable. Interested readers may find several excellent introductions to Agda online [3]. Any Agda types that are used but not explicitly referenced can be found in version 0.17 of the Agda standard library [2].

There have been efforts to formalise other asynchronous models and algorithms such as real-time systems [18] and distributed languages [14, 15]. However, as far as we know our work is the first attempt to formalize the results of UD.

This paper is a revised version of our ITP 2018 conference paper [23]. In particular, the following contributions are new: (i) showing that it is possible to enlarge the set of schedules that the iteration converges over, (ii) relaxing the ACO conditions. As a result, the main proof has been simplified sufficiently to include its Agda formalisation within this paper.

Schedules determine the non-deterministic behaviour of the asynchronous environment in which the iteration takes place; they describe when nodes update their values and the timings of the messages to other nodes. Let \(V\) be the finite set of nodes participating in the asynchronous process. Time \(T\) is assumed to be a discrete, linearly ordered set (i.e. \({\mathbb {N}}\)).

We formalise schedules in Agda as a dependent record. The number of nodes in the computation is passed as a parameter and the nodes themselves are represented by the type , the type of finite sets with n elements.

It would be possible to implicitly capture by changing the return type of to instead of . However, this would require converting the result of to type almost every time it wanted to be used. The simplification of the definition of is therefore not worth complicating the resulting proofs.

We should explicitly highlight that one of the advantages of UD’s theory is that there is no requirement for the data flow function to be monotonic, i.e. that messages arrive in the order they were sent:Although this assumption is natural in many settings, it does not hold for example if the nodes are communicating over a network and different messages take different routes through the network. Figure 1 demonstrates this and other artefacts of asynchronous communication that can be captured by \(\beta \).

We now define the asynchronous state function \(\delta \). We formalise the state space \(S = S_1 \times \cdots \times S_n\) in Agda using a ( )-indexed from the Agda standard library, i.e. n sets each equipped with some suitable notion of equality.

Initially node i adopts \(x_i\), the ith component of the initial state. At a subsequent point in time then if node i is inactive then it simply carries over its state from the previous time step. However if node i is in the set of active nodes then it applies \(\mathbf{F }_i\) to the state of the computation from node i’s local perspective, e.g. the term \(\delta ^{\beta (t,i,1)}_1(x)\) is the contents of the most recent message node i received from node 1 at time t. This definition is formalised in Agda as follows:

Those unfamiliar with Agda may wonder why the additional argument is necessary. Agda requires that every program terminates, and its termination checker ensures this by verifying that the function’s arguments get structurally smaller with each recursive call. While we can see that \(\delta \) will terminate, in the case where i activates at time t, the time index of the recursive call \(\beta (t+1,i,j)\) is only smaller than \(t+1\) because of , and so a naive implementation fails to pass the Agda termination checker. The type helps the termination checker see that the function terminates by providing an argument that always becomes structurally smaller with each recursive call. The argument for the second case has the type: . Therefore in order to generate the next one must prove the time really does strictly decrease. For the second recursive case this is proved by , where proves \(\beta (t+1,i,j) \leqslant t\) and is a proof that if \(x \leqslant y\) then \(x + 1 \leqslant y + 1\) and hence that \(\beta (t+1,i,j)+1 \leqslant t+1 \Leftrightarrow \beta (t+1,i,j) < t+1\). This additional complexity can be hidden from the users of the library by defining a second function of the expected type:

by using the proof which shows the natural numbers are well-founded with respect to < and which has type

Note that our revised definition of a schedule contains only what is necessary to define the asynchronous state function \(\delta \) and nothing more. This provides circumstantial evidence that the decision to remove assumptions (S2) and (S3) from the definition was a reasonable one, as they are extraneous when defining the core iteration.

Before exploring UD’s conditions for the asynchronous iteration \(\delta \) to behave correctly, we must first establish what “behave correctly” means. An intuitive and informal definition might be as follows:

The asynchronous iteration, \(\delta \), behaves correctly if for a given starting state x and all well-behaved schedules \((\alpha , \beta )\) there exists a time after which the iteration will have converged to the fixed point \(x^*\).

What is a “well-behaved” schedule? As in many cases, it is initially easier to describe when a schedule is not well-behaved. For example, if a node i never activates then the iteration cannot be expected to converge to a fixed point. Equally, if node i never succeeds in sending a message to node j then a fixed point is unlikely to be reached.

UD incorporated their notion of well-behavedness into the definition of the schedule itself in the form of assumptions (S2) and (S3). These state that nodes continue to activate indefinitely and links will never fail entirely. As discussed previously in Sect. 2.1, this guarantees that the schedule is well-behaved forever. However, intuitively they are unnecessarily strong assumptions as both the definition of correctness above and the definition used by UD require that \(\delta \) converges in a finite amount of time.

We now explore how to relax (S2) and (S3), so that the schedule is only required to be well-behaved for a finite amount of time. Unfortunately this is not as simple as requiring “every node must activate at least n times” and “every pair of nodes must exchange at least m messages”, because the interleaving of node activations and message arrivals is important. For example node 1 activating n times followed by node 2 activating n times is unlikely to allow convergence as there is no opportunity for feedback from node 2 to node 1.

The right notion of a suitable interleaving of messages and activations turns out to be that of a pseudoperiodic schedule, as used by UD in their proof of convergence.

Note that UD refer to such schedules simply as pseudoperiodic. We have renamed it infinitely pseudoperiodic for reasons that will hopefully become apparent as we unpick the components of the definition.

First of all we define a period of time as a pair of times:

We do not include that \(\leqslant \) as in turns out that it will always be inferrable from the context and hence including the proof in the record only leads to duplication.

Assumption (P1) for an infinitely pseudoperiodic schedule simply says that the initial time of interest is time 0. This turns out to be unnecessary and any starting point will do and hence we leave it unformalised. Assumptions (P2) and (P3) guarantee that every node activates at least once between times \(\varphi (k)\) and \(\varphi (k+1)\). We will call such a period an activation period.

Assumption (P4) says that any message that arrives after \(\varphi (k+1)\) must have been sent after \(\tau _i(k)\), i.e. \(\varphi (k+1)\) is long enough in the future that all messages sent before node i activated have either arrived or been lost. This motivates the following definition:

UD call the period of time between \(\varphi (k)\) and \(\varphi (k+1)\) a pseudocycle. In such a period of time every node activates and subsequently all the messages sent before its activation time expire. The sequence \(\varphi (k)\) therefore forms an infinite sequence of pseudocycles.

We argue that a pseudocycle is more naturally defined the other way round, i.e. all messages sent to node i before the start of the pseudoperiod should expire and then the node should activate. As shown in Fig. 2 and proved in Sect. 3.1, this alteration aligns the end of the pseudocycle with the moment the iteration converges. This has the consequence of simplifying the definition of what it means for the asynchronous iteration to converge in a finite time as well as the subsequent proofs that the iteration converges.

The notion of a pseudocycle is related to the iteration converging, as during a pseudocycle the asynchronous iteration will make at least as much progress as that of a single synchronous iteration. This will be shown rigorously in Sect. 3.1.

We define a schedule to be k-pseudoperiodic if it contains k pseudocycles. UD show that a schedule satisfies (S2) and (S3) if and only if the schedule is \(\infty \)-pseudoperiodic. Therefore UD’s definition of convergence implicitly assumes that all schedules are \(\infty \)-pseudoperiodic. By removing (S2) and (S3) from the definition of a schedule we can relax our definition to say that the schedule only needs to be \(k^*\)-pseudoperiodic for some finite \(k^*\). Our definition of what it means for \(\delta \) to converge therefore runs as follows:

Note that prior to this, the definitions of \(\delta \) and pseudocycles etc. have been implicitly parameterised by some schedule \(\psi \) (omitted in the Agda via module parameters). As the definition of quantifies over all schedules, this dependency must now be made explicit. Another point that Agda forces us to make explicit, and which is perhaps not immediately obvious in the mathematical definition above due to the overloading of \(\in \), is that when we write \(x \in X_0\) we really mean \(\forall i : x_i \in (X_0)_i\). The latter is represented in the Agda code by the indexed membership relation .

What are the practical advantages of this new definition of convergence?The next section discusses under what conditions \(\delta \) can be proved to fulfil this definition of convergence.

UD define a class of functions called Asynchronously Contracting Operators (ACO). They then prove that if the function \(\mathbf{F }\) is an ACO, then \(\delta \) will converge to a unique fixed point for all possible \(\infty \)-pseudoperiodic schedules.

The ACO conditions state that the space S can be divided into a series of boxes \(D(k)\). Every application of \(\mathbf{F }\) moves the state into the next box, and eventually a box containing only a single element is reached. Intuitively, the reason why it is possible to show that these conditions guarantee asynchronous convergence, instead of just synchronous convergence, is that each box is to be decomposable over each of the n nodes. Therefore, \(\mathbf{F }\) remains contracting even if every node has not activated the same number of times. The definition of an ACO is formalised in Agda as follows:

The variable is necessary to keep track of the universe level the family of sets reside in. The sets themselves are implemented as a ( )-indexed family of predicates. The code can be read as “there exists two objects \(k^*\) and \(x^*\) such that”.

Even after relaxing (A1*) to (A1), the ACO sets \(D(k)\) are not always intuitive or simple to construct. UD recognised this and provided several alternative sufficient conditions which are applicable in special cases. They then claim that these new conditions are sufficient for convergence by showing that they imply that \(\mathbf{F }\) is an ACO.

The first set of sufficient conditions apply when there exists a partial order \(\leqslant _i\) over each \(S_i\). These are then lifted to form the order \(\leqslant \) over \(S\) where \(x \leqslant y\) means \(\forall i : x_i \leqslant y_i\). UD then make the following claim, where \(\sigma \) is the synchronous state function:

UD attempt to prove this by first showing a reduction from these conditions to an ACO and then applying Theorem 1 to obtain the required result. However this claim is not true. While the asynchronous iteration does converge from every starting state in \(D\) under these assumptions, it does not necessarily converge to the same fixed point. The flaw in the original proof is that UD tacitly assume that the set \(D(0)\) for the ACO they construct is the same as the original \(D\) specified in the conditions above. However the only elements that are provably in the ACO’s \(D(0)\) is the set \(\{\sigma ^k(x) \mid k \in {\mathbb {N}}\}\). We now present a counter-example to the claim.

It is possible to “fix” this claim by strengthening (iv) to “the synchronous iteration always converges to the same fixed point”. Additionally it also turns out that the reduction to the ACO requires \(D\) to be non-empty so that there exists an initial state from which to begin iterating. The modified conditions are formalised in Agda as follows:

One point of interest is that the sets defined above depend on the initial state \(x_0\), and that \(D(0)\) as defined only contains the synchronous iterates from \(x_0\), and hence D(0) is only a subset of \(D\). It is still possible to show convergence for all states in \(D\) by constructing an ACO for each initial element and proving that \(D(k^*)\) contains the same final element (which is possible due to the modification that \(\sigma \) now converges to a unique fixed point). However, even with our updated assumptions we have been unable to construct a single “unified” ACO for which \(D(0) = D\). Whether or not it is possible to do so is an interesting open question.

UD also provide a set of sufficient conditions that are applicable for convergence over a finite set of values. Like Claim 1, they require that \(S\) is equipped with some indexed order.

UD’s attempted proof for Claim 2 is a reduction to the conditions for Claim 1. Therefore like Claim 1, the conditions guarantee convergence but not to a unique solution. Similarly, the counterexample for Claim 1 is also a counterexample for Claim 2.

Unlike Claim 1, we do not have a proposed strengthening of Claim 2 which guarantees the uniqueness of the fixed point. This is because the finiteness of \(D\) does not help to ensure the uniqueness of the fixed point. Instead much stronger assumptions would be required to guarantee uniqueness (for example the existence of a metric space over the computation as discussed in the next section) and any such stronger conditions have the tendency to make the finiteness assumption redundant.

Many classical convergence results for synchronous iterations rely on the notion of distance, and in suitable metric spaces the iteration can be proved to converge by showing that every application of the operator \(\mathbf{F }\) moves the state closer (in non-negligible steps) to some fixed point \(x^*\). There already exist several results of this type for asynchronous iterations. El Tarazi [11] shows that \(\delta \) converges if each \(S_i\) is a normed linear space and there exists a fixed point \(x^*\) and a \(\gamma \in (0, 1]\) such that for all \(x \in S\):However, this is a strong requirement as the use of the norm implies the existence of an additive operator over \(S\) and in many applications such an operator may not exist.

Recently Gurney [13] proposed a new, more general set of conditions based on ultrametrics [19]. Gurney does not name these conditions himself but for convenience we will call an \(\mathbf{F }\) that satisfies them an asynchronously metrically contracting operator (AMCO). He then proves that \(\mathbf{F }\) being an AMCO is equivalent to \(\mathbf{F }\) being an ACO. We are primarily concerned with applying the results to prove correctness and so we only formalise the forwards direction of the proof here. Before doing so, we define some terminology for different types of metrics.

It should be noted that in these definitions the image of d is \({\mathbb {N}}\) rather than \(\mathbb {R^+}\). This is important as it later allows us to prove that the distance between consecutive states in the iteration must reduce to 0 by the well-foundedness of the natural numbers over <.

Assumption (M1) is not listed in Gurney [13] but was found to be required during formalisation as proofs in Agda are constructive. It should be noted that if (M1) does not hold (i.e. there are no states) then convergence is trivial to prove. Assumption (M2) says that two states are equal if and only if they occupy the same point in space. Assumption (M3) says that there exists a maximum distance between pairs of states. Assumption (M4) says that the distance between consecutive iterations must strictly decrease, and assumption (M5) says that for any fixed point \(x^*\) then applying \(\mathbf{F }\) must move any state closer to that fixed point. These conditions are formalised in Agda as follows:

In this paper we have formalised the asynchronous fixed point theory of Üresin and Dubois’ in Agda. Along the way we have proposed various relaxations by:We have also described how an accordingly relaxed version of UD’s main theorem was successfully formalised. However our efforts to formalise Propositions 3 and 4 as stated in UD’s paper revealed that they are false. We hope that this finding alone justifies the formalisation process. We have proposed a fix for Proposition 3 but have been unable to come up with a similar practical alteration for Proposition 4. Finally, we have also relaxed and formalised the set of AMCO conditions based on the work by Gurney.

Our formalisation efforts have resulted in a library of proofs for general asynchronous iterations. The library is publicly available [1] and we hope that it will be a valuable resource for those wanting to formally verify the correctness of a wide range of asynchronous iterations. We ourselves have used the library to verify a proof about the largest possible set of distributed vector-based routing protocols that are always guaranteed to converge over any network [8].

We are primarily interested in proving correctness and therefore we have only formalised that the \(\mathbf{F }\) being an ACO is sufficient to guarantee that the asynchronous iteration converges. However Üresin and Dubois also show that if \(\mathbf{F }\) converges then \(\mathbf{F }\) is necessarily an ACO whenever the state space S is finite. The accompanying proof is significantly more complex and technical than the forwards direction and so would be an interesting extension to our formalisation.

Additionally it would be instructive to see if other related work such as [17, 21, 22], using different models, could be integrated into our formalisation.