The Free Termination Property of Queries over Time

A common CRDT is the “grow-only set” CRDT: this is a replicated distributed set where each machine propagates its local set to other machines in the system. Upon receiving a message containing the local set at another machine, the local machine will apply its “merge” operation, modifying its local state to be the union of its current state and the incoming set. This process of propagation over an asynchronous network introduces non-determinism as messages might be delivered in a different order than they are sent and messages may arrive multiple times. The fact that set union forms a semi-lattice ensures that, regardless of these sources of network nondeterminism, the state at each machine will eventually converge to the same value. That eventual value is the union of all of the initial states at each machine and the time at which it is reached is called the quiescence point.

Grow-only sets illustrate the point that CRDTs provide coordination-free consistency, but do not support free termination. In the absence of coordination, we do not have a mechanism for determining locally whether we have received all the elements in the network – i.e. whether we have reached a quiescence point. Without a guarantee of quiescence, what should we do to answer a query from a user? CRDTs allow arbitrary queries at any time and make no guarantee on the relationship between the query result at time $t$ and the query result at the quiescence point. For example, consider the query $Q(x)=R(x)-T(x)$. A value $(a)$ may be returned at time $t$, but eventually be excluded from the final output via subsequent “merges” into $T(a)$. This is not a particularly satisfactory contract between the system and the user: what good is distributed state if you do not know when you can query it reliably?

Threshold queries characterize a class of queries over CRDTs in which a machine is able to unilaterally detect that the output will never change regardless of future applications of the merge operation (set union in our example). For example, consider the query $Q()=|R(x)|>10$. This boolean query is monotone with respect to the partial order of our semilattice (which is ordered by subset containment). Since the merge operation can only increase the position in the partial order, once the local state contains more than ten tuples in $R$, the result of the query is guaranteed to be the same at the quiescence time. By contrast, if the quiescence-time answer to this query is false – i.e. $\neg (|R(x)|>10)$ – then no machine will ever return an answer to this query. From a local perspective, a machine cannot know if there is some additional element out there that it has not heard about and will someday need to union into its local state. Threshold queries, while useful, only offer free termination for database instances where the answer is true!

The CALM Theorem [5] uses relational transducer networks [1] to prove the relationship between queries expressed in monotonic logic and coordination-freeness. This formalism allows for the expression of distributed programs in terms of logical formulas that are evaluated iteratively on each machine and communicate state between machines. Similar models have been used by developers to implement distributed programs (e.g., Webdamlog [1], Bloom [3]). While both the CALM theorem and CRDTs use proofs based on notions of monotonicity, there remains a gap between the logic formalism of the CALM theorem and the state-based formalisms of other work on coordination-freeness. In this paper, we are not interested in the programmability differences between these approaches but exclusively in reasoning about guarantees on query results without coordination. In departing from the realm of logic programming, we want to reason naturally about programs beyond the boolean or relational setting. For example, consider a system that takes on integer values and supports the multiplication operation by a user-specified input integer. Now consider the query “is the running product divisible by two?”. This query is not monotone with respect to the traditional ordering of the integers, but it can be computed coordination-free on input instances that contain any even number under the free-termination framework we introduce throughout this paper. Once we have multiplied by an even number, all possible future states will return True on this query.

As mentioned above, transducers were used to prove coordination-free consistency guarantees, but they do not directly address termination. As an example, consider a network of transducers supporting the Datalog language, and a simple program like transitive closure. Transducers accumulate knowledge about the set of paths in the global input, and once they learn about a path they can output it with certainty, but they will never conclude that they have finished finding new paths. Indeed, this depends on the database instance! We will return to this point in Section 5.

In the first instantiation, we consider $D$ to be the set of all instances over a fixed relational schema $𝐑$. The update function $U$ allows modification only by inserting a tuple to the instance; in other words, the set $L$ is the set of all tuples over $𝐑$ and $U(I,t)=I\cup \{t\}$. We will refer to this semiautomaton as ${𝕊}_{\cup }$. A trace in ${𝕊}_{\cup }$ is a sequence of single-tuple insertions to the initial database. Let us consider a query $Q$ that is a Boolean Conjunctive Query, hence it maps the database instance (state) to its range $R=\{𝖳,𝖥\}$.

The characterization of free termination states for $Q$ is fairly straightforward. Indeed, take any instance $I$ in the state space such that $Q(I)$ is true; then, because $Q$ is a monotone query and the updates are only tuple insertions, any $I^{\prime }$ reachable from $I$ will also have $Q(I^{\prime })=𝖳$. Thus, such an $I$ will be a free termination state. On the other hand, if $Q(I)=𝖥$, free termination is not possible since we can always insert a sequence of tuples to make $Q$ true. As we will see later on, this is a special case of a more general characterization of free termination.

A state-based CRDT defines three functions over its state $D$: an update operation that allows state to be mutated from outside the system ($\text{update}:D\times L\to D$), a merge operation that determines how the states of two replicas can combine to converge to the same state ($\text{merge}:D\times D\to D$), and a query operation that defines what is visible to the user from the internal state ($Q:D\to R$). The basic idea is that updates from users can modify the state of any replica in the distributed system and asynchronous gossip of replica states in the background will ensure each replica eventually converges to the same state regardless of duplicated or out-of-order message delivery. To guarantee this convergence (formally known as strong eventual consistency), the merge operation must be associative, commutative, and idempotent and the update operation must be inflationary with respect to the partial ordering induced by the merge operation. In Appendix B, we give four popular examples of state-based CRDTs.

To capture a state-based CRDT in our model, we define it as a semiautomaton ${𝕊}_{\mathrm{\square }}=(D,L,U)$, where $D$ is the set of states, and the update $U$ captures both the update and merge operation of the CRDT. Specifically, $U(s,⟨\text{u},\mathrm{\ell }⟩)=\text{update}(s,\mathrm{\ell })$ and $U(s,⟨\text{m},s^{\prime }⟩)=\text{merge}(s,s^{\prime })$. A crucial property of a state-based CRDT is that the partial order induced by the merge operation forms a join-semilattice. Observe that because of this, the state transition system for a state-based CRDT will always be acyclic - a property that we will explore in detail in Section 4.1.

Consider a partial order $⊑$ over a domain $D$, and take $f:D\to D$ to be a monotone function w.r.t. $⊑$. Further consider a (parameter-independent) semiautomaton and assume that it captures a fixpoint computation from a starting state $s_0\to f(s_0)\to f(f(s_0))\to \mathrm{\dots }$ that eventually reaches a state $s$ with $f(s)=s$ after finitely many steps. For any query $Q$ over $D$, the fixpoint state $s$ is a free termination state (no other state is reachable from it). However, the structure of $Q$ may allow us to find an earlier free termination state before we even reach the fixpoint.

As an example, consider the case where the fixpoint computation is an iterative (naive or semi-naive) evaluation of a Datalog program $P$ on an instance $I$. Here, the starting state is the set of EDBs and each iteration during evaluation is an update that adds to the current state the newly produced IDB facts via the rules of the program. Our query $Q$ is a view over the IDBs of the program $P$, which can be thought of as the “target” of $P$. Concretely, consider the following Datalog program that determines whether there exists a path between vertices $s$ and $t$ in a graph.

For this program, we can freely terminate as long as the state contains the IDB fact $P(s,t)$, even before we have reached a fixpoint. This is because the fixpoint computation is monotone w.r.t. set containment (so the update $U$ is inflationary) and $Q$ is a monotone query as well w.r.t. the partial order $𝖥⊑𝖳$. If we replaced $Q$ with another query $Q^{\prime }()\leftarrow P(x,x)$ which detects the presence of a cycle in the graph, we also can freely terminate earlier as long as the state contains a cycle. As we will see in the next section, both of these are examples of Boolean threshold queries.

Datalog^o [2] is an extension of Datalog to support recursive queries over partially ordered pre-semirings (POPS). This can also be viewed as a parameter-independent fixpoint computation. Datalog^o requires that both semiring operations be monotone w.r.t. the partial order of the POPS. This tells us that the update transition for any Datalog^o graph is inflationary, which we show in Proposition 13 implies any Boolean monotone query will have a free termination state. For instance, the query $Q$ below that computes whether the distance between vertices $s,t$ in a graph is at most 10.

Intuitively, if the input state will only increase in the partial order because $U$ is inflationary, and $Q$ is monotone, then over time the output of $Q$ will always stay the same or increase. However, free termination is concerned specifically with when the output of $Q$ will stay the same. We identify two general conditions that guarantee free termination in this case.

Consider any state $s^{\prime }\in D$ such that $s^{\prime }\in U^{\mathrm{\infty }}(s)$. Then, because $𝕊$ is inflationary and ${⊑}_D$ is transitive, we must have that $s{⊑}_D{s}^{\prime }$. But $s$ is a maximal element of ${⊑}_D$, hence $s=s^{\prime }$. Thus, $Q(s)=Q(s^{\prime })$. The proof for when $U$ is deflationary and $s$ a minimal element is symmetrical. $◀$

In some cases, we will consider partial orders ${⊑}_D$ with a bottom element $\perp$ or a top element $\top$: then, we have that for every $s\in D$, $\perp {⊑}_{D}s$ or $s{⊑}_D\top$ respectively. Note that if a top element exists, then $\top$ is a free termination state by the above proposition.

Consider any state $s^{\prime }\in D$ such that $s^{\prime }\in U^{\mathrm{\infty }}(s)$. Then, because $𝕊$ is inflationary and ${⊑}_D$ is transitive, we must have that $s{⊑}_D{s}^{\prime }$. From the monotonicity of $Q$, this implies that $Q(s){⊑}_{R}Q(s^{\prime })$. But because $Q(s)$ is maximal, we must have that $Q(s^{\prime })=Q(s)$. The case where $Q$ is antitone and $Q(s)$ is a minimal element is symmetric. $◀$

In this part, we ask the following question: what classes of queries have free termination states? We will restrict our attention to settings where the behavior of $𝕊$ is inflationary as threshold queries are naturally valuable in this setting. Further, all state-based CRDTs are examples of $𝕊$ that are inflationary. We define first an important class of queries, inspired by the LVars [21] work on coordination-free programming languages, called Threshold Queries. Recall that an antichain in a partial order $⊑$ with domain $D$ is a subset $C\subseteq D$ such that no two distinct elements of $C$ are comparable under $⊑$.

Boolean threshold queries are monotone and this allows us to obtain the free termination states in this case.

We first show that $Q_C$ must be monotone. Indeed, let $s{⊑}_D{s}^{\prime }$ and assume $Q_C(s)$ is true. Then, there exists $c\in C$ such that $s{⊒}_{D}c$. But since $s{⊑}_D{s}^{\prime }$, $s^{\prime }{⊒}_{D}c$ and $Q_C(s^{\prime })$ must also be true. Since $𝖳$ is the maximal element of $𝔹$, all states $s$ such that $Q_C(s)$ is true are free termination states. Note that any element of $D$ that is at or above the threshold line $C$ has this property. $◀$

We should note here that any monotone Boolean query must be a Boolean threshold query (excluding the trivial query that is always false). In this work, we do not wish to limit ourselves to threshold queries that return only true, or even to thresholds where each $c$ returns the same value $Q(c)$. We can generalize the concept of Boolean threshold queries with the following result.

Let $F\subseteq D$ be the set of free termination states. $F$ cannot be empty. Let $F_{\tau }$ be the minimal states in $F$ w.r.t. ${⊑}_U$. By construction, $F_{\tau }$ forms an antichain and will be our set $C$. Take now any state $s\in D$ such that $c{⊑}_{U}s$ for some $c\in C$. Since $c$ is a free termination state and $c$ reaches $s$, it must be that $Q(c)=Q(s)$. $◀$

In other words, there exists a threshold (formed by the antichain $C$) such that at or above the threshold the behavior of $Q$ is governed completely by the threshold states. However, the behavior of $Q$ outside of this threshold space has no restriction (unlike in the case of Boolean monotone queries).

When the partial order has further algebraic structure, we can characterize the behavior of free termination states more precisely. Here, we consider the case where $𝕊$ has a natural partial order ${⊑}_U$ and this order is a join-semilattice (this means that there is a least upper bound for any nonempty finite subset of $D$).

Indeed, take any two free termination states $s_1,s_2$. Since ${⊑}_U$ is a join-semilattice, there exists a least upper bound $s$ such that $s_1{⊑}_{U}s$ and $s_2{⊑}_{U}s$. Since ${⊑}_U$ is the natural partial order, $s_1\twoheadrightarrow s$ and $s_2\twoheadrightarrow s$. But $s_1,s_2$ are free termination states, so it must be that $Q(s_1)=Q(s)$ and $Q(s_2)=Q(s)$. Thus, $Q(s_1)=Q(s_2)$. $◀$

As a corollary of the above proposition, any free termination state in a state-based CRDT must have the same value. A special case is when the natural partial order has a top element $\top$; in this case, all free termination states must take the value of $Q(\top )$.

In other words, if there exists a free termination state, it is possible to reach a free termination state from whichever state we currently are in (with an appropriate set of updates).

Let $s$ be the current state and $s_t$ be a free termination state. Since ${⊑}_U$ is a join-semilattice, there exists a least upper bound $s^{\prime }$ such that $s{⊑}_U{s}^{\prime }$ and $s_t{⊑}_U{s}^{\prime }$. Since ${⊑}_U$ is the natural partial order, $s\to s^{\prime }$ and $s_t\to s^{\prime }$. But then $s^{\prime }$ must also be a free termination state. $◀$

One would be tempted to think that monotone (or antitone) queries are the only ones that have free termination states in a join-semilattice, but this is not true even for Boolean queries. Take for example the semiautomaton ${𝕊}_{\cup }$ with the Boolean query $Q()=R(c)\wedge \neg S(c)$ for some constant $c$. This query is neither monotone nor antitone, since, for example, it returns false on $\{R(a)\}$, true on $\{R(a),R(c)\}$, and false on $\{R(a),R(c),S(c)\}$. However, it has free termination states: these are the states in which the tuple $S(c)$ is in the instance.

Suppose that some state $s\in D$ freely terminates. Since $Q$ is not constant, there exists some state $s^{\prime }\in D$ such that $Q(s)\ne Q(s^{\prime })$. Since $s$ is invertible, we have that $s\twoheadrightarrow \mathrm{𝗂𝖽}$, where $\mathrm{𝗂𝖽}$ is an identity element. By the definition of an identity element, $\mathrm{𝗂𝖽}\twoheadrightarrow s^{\prime }$. Hence, $s\twoheadrightarrow s^{\prime }$, which contradicts the fact that $s$ is a free termination state. $◀$

When $U:D\times D\to D$ and $(D,U)$ forms a group ($U$ has identity element and every element has an inverse), then we obtain the following corollary:

This corollary tells us that an update function that forms a group precludes the possibility of free termination. It also tells us that in view maintenance, which often studies rings rather than semirings, free termination is impossible. This is consistent with the monotonicity lens on threshold queries from CRDTs [22] where an inverse corresponds to moving backward in the partial order, which prevents the possibility of threshold queries with free termination states. The practical benefits of having inverses in CRDTs to allow “undo” operations have been discussed in [13] and [25]. This is an interesting dichotomy. Two parallel lines of work have shown the value of invertibility in data systems (DBSP [9], DBToaster [20]) and the value of coordination-free monotone queries (CALM theorem, CRDTs), but the benefits of these properties appear mutually exclusive.

Suppose $I$ is a free termination state. Consider the following algorithm: it will set $ready(v)$ to true exactly when $state(v)$ is a free termination state for $Q$ in ${𝕊}_{\cup }$. This algorithm is correct, since at the instance $I^{\prime }$ where $ready$ becomes true, all reachable states maintain the result of $Q$. Since $I$ is reachable from $I^{\prime }$ (from the network flooding construction), $Q(I)=Q(I^{\prime })$. Further, every fair and complete run reaches the quiescence point, when $state(v)=I$, and thus the algorithm will set $ready$ to true.

In the other direction, suppose $(Q,I)$ is coordination-free correct and consider an algorithm that computes the output correctly. At the quiescence point, when $state(v)=I$, this algorithm must set $ready$ to true (since the state will remain unchanged from that point on). But now consider a fair and complete run for another input $I^{\prime }\supseteq I$ (which is a reachable state in ${𝕊}_{\cup }$) such that some node $v$ receives first all of $I$. At this point, the algorithm would need to do the ready transition. But because of correctness, it must be that $Q(I)=Q(I^{\prime })$. Hence, $I$ is a free termination state. $◀$

If the input is not a free termination state, the system will often need to perform some coordination to get the user a concrete answer. We thus avoid coordination for a given query on some inputs, but not all inputs! In practice, the distribution of inputs to a given system is what determines how helpful free termination is.

We next discuss how we could define a notion of coordination-free correctness for the entire query $Q$. As a first attempt, we could define $Q$ to be coordination-free correct if $(Q,I)$ is coordination-free correct for every input $I$. From Theorem 22, this is equivalent to saying that every input is free terminating, which happens only when $Q$ is a constant query. Hence, we need to slightly relax this notion, by requiring that $(Q,I)$ is coordination-free correct for some inputs.

The notion of positive coordination-freeness is exactly the notion of query coordination-freeness used for transducer networks in [5]. Indeed, a transducer can only write true in its output tape, so if nothing is written, we assume a false output.

From Theorem 22, $Q$ is positively coordination-free if and only if every state $I$ with $Q(I)=𝖳$ is a free termination state. Say $I\subseteq I^{\prime }$ and suppose $Q(I)$ is true. Then, $I$ is a free termination state and thus $I^{\prime }$ is as well, which implies $Q(I^{\prime })=Q(I)=𝖳$. Hence, $Q$ is monotone. The antitone case is symmetric. $◀$

For instance, consider the Boolean query $\forall x:R(x)>0$. This query freely terminates on all false instances, and hence it can be considered negatively coordination-free. Observe that Ameloot et al. [5] categorizes antitone Boolean queries as not being computable by oblivious transducer networks. This is because of the definition of the output of a transducer network being the union of outputs and the encoding of the boolean values True and False being the presence of an empty tuple and the absence of a tuple respectively. In addition to antitone queries, some queries are neither monotone nor antitone, but still have coordination-free correct inputs such as our example from Section 4.1, $Q()=R(c)\wedge \neg S(c)$.

Consider now a non-Boolean query $Q$ that outputs a set. In this case, we will introduce a ready variable $ready(v,t)$ for every node $v$ and every potential tuple $t$. Note that this introduces another layer of granularity since we can now compute some tuples in a coordination-free correct manner, while others we cannot. We can similarly lift coordination-free correctness to the entire query $Q$ by saying that $Q$ is positively (resp. negatively) coordination-free if every Boolean query $(t\in Q(I))$ is positively (resp. negatively) coordination-free. Positive coordination-freeness captures exactly how oblivious relational transducers work: they can write only correct facts to the output tape, which they can never retract. The following result is immediate.

We complete this section by an example that shows the benefits of a fine-grained coordination-free definition. Consider the following query $Q$, which is neither monotone nor antitone: $Q(x)=(R(x)\wedge x>10)\vee (S(x)\wedge \neg T(x))$. In this case, any instance that contains a tuple $R(20)$ freely terminates (with true) for the output tuple $(20)$. Also, any instance that contains $(T(5))$ freely terminates (with false) for the output tuple $(5)$. Thus, we can correctly output the existence/non-existence of the two tuples in a coordination-free manner.

To achieve this result, we first need the following observation on the behavior of free terminating states: if $s$ is a free terminating state, then all states in the Strongly Connected Component (SCC) of $s$ in $G[𝕊]$ are also free terminating. Thus if two states $s,s^{\prime }$ are in the same SCC and $Q(s)\ne Q(s^{\prime })$, then none of the states in the SCC are free terminating.

The first step of the algorithm is to convert $G[𝕊]$ to a Directed Acyclic Graph (DAG) $G^{\prime }$, where each node represents an SCC. This is standard and can be done in linear time. As a second step, we iterate over all SCCs and label them as a candidate if $Q$ is the same across all states in that SCC; otherwise, we remove from $G^{\prime }$ the SCC and all other nodes that can reach it. This step can also be implemented in linear time.

We are now left with a DAG $G^{\prime \prime }$ where each SCC has the same value for $Q$. In our final step, we perform a traversal of the SCCs in reverse topological order. Any SCC with no outgoing edge in $G^{\prime \prime }$ is free terminating (meaning all the states in the SCC are free terminating). At any step, if an SCC $C$ has outgoing edges only to free terminating SCCs and $Q$ is the same for $C$ and its outgoing SCCs, we mark $C$ as free terminating; otherwise, it is not free terminating. This final step also requires linear time. $◀$

Recall that a finite semiautomaton $𝕊$ is a DFA without a start or accept states. If we denote a state of $𝕊$ to be the start state, and take $Q$ to be a Boolean query that returns true for accept states and false for the other states, we have exactly a DFA. In this case, free termination of a state means essentially that we can stop the computation of the DFA without the need to read any more symbols from the input. From Proposition 26, we obtain as a corollary:

DFAs are an interesting example of converting an infinite state space (all strings over the alphabet) to a finite state space. We now explore connections between free termination and this notion of equivalent state representations.

Assume for the sake of contradiction that we have a minimal DFA and a free termination state $s$ that participates in a cycle in that DFA. Each state in the cycle is reachable from $s$, so they must all return the same query result as $s$ (accept/reject) and also be free-termination states. The DFA in which each state in the cycle is collapsed into a single state is equivalent and has strictly fewer states, thus the original DFA cannot have been minimal. $◀$

For a general pair $(𝕊,Q)$, we can follow the same idea as state minimization in DFAs. We define the collapsing of a set of states $S\subseteq D$ that take the same value for $Q$ as the modification of the semiautomaton that $(i)$ replaces $D$ with $(D\setminus S)\cup \{s_0\}$, where $s_0$ is a new state, and $(ii)$ any update that transitions to a state in $S$ goes to $s_0$, and any update that transitions from a state in $S$ starts in $s_0$. We also set $Q(s_0)$ to be the value of a state in $S$.

Because $s$ is a free termination state, we know every state in $U^{\mathrm{\infty }}(s)$ returns the same query result as $Q(s)$. We can collapse all states in $U^{\mathrm{\infty }}(s)$ with all transitions being self-loops. The collapsed state $s_0$ is a free termination state and cannot be part of a cycle. Any sequence of updates that ends up in $U^{\mathrm{\infty }}(s)$ in $𝕊$ will end up in $s_0$ in $𝕊$, and hence we have the desired equivalence. $◀$

Given $(𝕊,Q)$ with finite state space, consider now the equivalent pair $({𝕊}_{\mathrm{\square }},Q_{\mathrm{\square }})$ obtained by repeatedly applying the above proposition to free termination states until there is no more change; we call $({𝕊}_{\mathrm{\square }},Q_{\mathrm{\square }})$ collapsed. This is analogous to a minimal state representation. Note that we need finiteness to guarantee that the process of collapsing states will terminate at some point. We can now show the following characterization of free termination in this case.

From Proposition 30, we know that a free termination state that has any reachable states other than itself can be collapsed into a single state in which there are no outgoing edges except self-loops. The other direction is also clear as a state $s$ that has no outgoing transitions satisfies the definition of a free termination state as $U^{\mathrm{\infty }}(s)=\{s\}$. $◀$

State minimization offers an interesting perspective on distributed systems techniques like CRDTs. While CRDTs appear to only describe inflationary state mutations, it is common to convert non-inflationary updates into inflationary ones using metadata. We see this in both the two-phase set CRDT and the positive-negative counter CRDT (appendix B). While the state transition graphs for these CRDTs are acyclic, they have equivalent representations that are cyclic. By looking at these structures from the perspective of user-visible state (query-layer equivalence), the separation between free termination of query results and eventual consistency of state becomes clear.