20.11 State machine based on interval operations

This section takes the interval operation ∑[v₁,v₂) as the primitive semantic object. Full database states, factorisation, merge and the transitions of a distributed database are derived from it. The interval notation specifies no concrete representation of a composite operation.

Interval operations

Let S be a set of site identifiers. A vector time is a mapping v : S → ℕ. Let v_∅ be the empty vector time. Vector times are ordered pointwise; their meet and join are denoted by ↓ and ↑ respectively.

Axiom (existence and uniqueness of interval operations):

For causally valid vector times v₁,v₂ satisfying v₁ ≤ v₂, there exists a unique abstract composite operation \[ \sum[v_1,v_2). \] It represents exactly the generated operations in \[ \chi[v_1,v_2)=\chi(v_2)\setminus\chi(v_1). \]

Uniqueness is semantic. Different concrete data structures may represent the same abstract interval operation.

Definition:

For \(O=\sum[v_1,v_2)\), define \[ v_{\mathrm{in}}(O)=v_1, \qquad v_{\mathrm{out}}(O)=v_2, \qquad \Psi(O)=\chi(v_2)\setminus\chi(v_1). \]

Uniqueness from contexts:

For interval operations O₁ and O₂, \[ v_{\mathrm{in}}(O_1)=v_{\mathrm{in}}(O_2) \ \land\ v_{\mathrm{out}}(O_1)=v_{\mathrm{out}}(O_2) \Longrightarrow O_1=O_2. \]

Proof:

Both operations are the unique interval operation with those endpoints.

Factorisation

Definition:

Let \(O=\sum[v_1,v_2)\) and let v be a causally valid vector time satisfying v₁ ≤ v ≤ v₂. Define \[ Lf(O,v)=\sum[v_1,v), \qquad Rf(O,v)=\sum[v,v_2). \]

Contexts of factors:

\[ \begin{aligned} v_{\mathrm{in}}(Lf(O,v))&=v_{\mathrm{in}}(O), & v_{\mathrm{out}}(Lf(O,v))&=v,\\ v_{\mathrm{in}}(Rf(O,v))&=v, & v_{\mathrm{out}}(Rf(O,v))&=v_{\mathrm{out}}(O). \end{aligned} \]

Proof:

These equations follow directly from the endpoints of the two intervals.

Nested factors:

If \[ v_{\mathrm{in}}(O)\le v_1\le v_2\le v_{\mathrm{out}}(O), \] then \[ \begin{aligned} Lf(Lf(O,v_2),v_1)&=Lf(O,v_1),\\ Rf(Rf(O,v_1),v_2)&=Rf(O,v_2),\\ Rf(Lf(O,v_2),v_1)&=Lf(Rf(O,v_1),v_2)=\sum[v_1,v_2). \end{aligned} \]

Proof:

On each line, the operations on both sides have the same interval endpoints. Existence and uniqueness of interval operations gives equality.

Merge

Let \[ O_1=\sum[v_1,v_2), \qquad O_2=\sum[v_3,v_4), \qquad m=v_2\mathbin{\downarrow}v_4. \] The operations have sufficient history when \[ v_1\le m \qquad\text{and}\qquad v_3\le m. \]

Definition:

For interval operations with sufficient history, define \[ \sum[v_1,v_2)\mathbin{\oplus}\sum[v_3,v_4) = \sum[v_1\mathbin{\downarrow}v_3,\ v_2\mathbin{\uparrow}v_4). \]

The sufficient-history condition ensures that the result represents exactly the union of the input extents rather than introducing operations absent from both inputs.

Contexts and extent of merge:

For every defined merge, \[ \begin{aligned} v_{\mathrm{in}}(O_1\mathbin{\oplus}O_2) &=v_{\mathrm{in}}(O_1)\mathbin{\downarrow}v_{\mathrm{in}}(O_2),\\ v_{\mathrm{out}}(O_1\mathbin{\oplus}O_2) &=v_{\mathrm{out}}(O_1)\mathbin{\uparrow}v_{\mathrm{out}}(O_2),\\ \Psi(O_1\mathbin{\oplus}O_2) &=\Psi(O_1)\mathbin{\cup}\Psi(O_2). \end{aligned} \]

Proof:

The context equations follow from the definition. The extent equation follows from the set identity \[ (A\mathbin{\cup}B)\setminus(C\mathbin{\cap}D) = (A\setminus C)\mathbin{\cup}(B\setminus D) \] under the containments supplied by sufficient history.

Merge laws:

Whenever the displayed merges are defined, \[ \begin{aligned} O_1\mathbin{\oplus}O_2&=O_2\mathbin{\oplus}O_1,\\ (O_1\mathbin{\oplus}O_2)\mathbin{\oplus}O_3 &=O_1\mathbin{\oplus}(O_2\mathbin{\oplus}O_3),\\ O\mathbin{\oplus}O&=O. \end{aligned} \]

Proof:

Meet and join of vector times are commutative, associative and idempotent. The operations on the two sides of each equation therefore have the same interval endpoints. Uniqueness of interval operations gives equality.

Reconstruction from factors:

For every defined factorisation, \[ Lf(O,v)\mathbin{\oplus}Rf(O,v)=O. \]

Proof:

If \(O=\sum[v_1,v_2)\), then \[ \sum[v_1,v)\mathbin{\oplus}\sum[v,v_2) = \sum[v_1\mathbin{\downarrow}v,\ v\mathbin{\uparrow}v_2) = \sum[v_1,v_2). \]

Full database states

Definition:

For every causally valid vector time v, define the full database state \[ State(v)=\sum[v_{\emptyset},v). \]

The initial database state is \[ State(v_{\emptyset})=\sum[v_{\emptyset},v_{\emptyset}). \]

Merge of full states:

\[ State(v_1)\mathbin{\oplus}State(v_2)=State(v_1\mathbin{\uparrow}v_2). \]

Proof:

The two input contexts are both v_∅, so their meet is v_∅. Their output context is v₁ ↑ v₂.

Thus full database states form a join-semilattice under merge. No meet of full states is required.

Distributed state machine

Let S also index the sites of the distributed system. A system configuration is a mapping D that assigns a full state to every site. Initially, \[ D(s)=State(v_{\emptyset})=\sum[v_{\emptyset},v_{\emptyset}) \qquad\text{for every }s\in S. \]

There are two kinds of transition.

Generate a local operation

Suppose \[ D(s)=State(v) \] and site s generates its next atomic operation. Let \[ v'=inc_s(v), \] where only the s component is incremented. The generated atomic interval is \[ O=\sum[v,v'), \] and the new site state is \[ D(s):=State(v')=\sum[v_{\emptyset},v'). \] Every other site retains its existing state.

Equivalently, \[ State(v)\mathbin{\oplus}O=State(v'), \] although local generation is a primitive state-machine transition and need not be implemented by calling merge.

Merge an R-factor from another site

Suppose source site s holds State(v_s) and receiver site r holds State(v_r). Their common vector time is \[ c=v_s\mathbin{\downarrow}v_r. \] The source contribution not already in their common history is \[ \Delta=Rf(State(v_s),c)=\sum[c,v_s). \] The transition at the receiver is \[ \begin{aligned} D(r) &:=D(r)\mathbin{\oplus}\Delta\\ &=\sum[v_{\emptyset},v_r)\mathbin{\oplus}\sum[c,v_s)\\ &=\sum[v_{\emptyset},v_r\mathbin{\uparrow}v_s)\\ &=State(v_r\mathbin{\uparrow}v_s). \end{aligned} \] Every other site retains its existing state.

This transition is a generalised merge rather than contextual serialisation: the input context c of Δ need not equal the receiver's output vector time v_r.

Convergence

Uniqueness of a full state:

For causally valid vector time v, State(v) is unique.

Proof:

It is the unique interval operation \(\sum[v_{\emptyset},v)\).

Convergence at equal vector times:

If two sites have the same output vector time v, they hold the same full database state State(v).

Proof:

Both site states are the unique interval operation \(\sum[v_{\emptyset},v)\).

Convergence at quiescence:

If every generated atomic operation is eventually incorporated at every site, all sites converge to the same full database state at quiescence.

Proof:

At quiescence every site has the same output vector time v, containing every generated atomic operation. Convergence at equal vector times gives State(v) at every site.

Obligation on concrete representations

A concrete database-operation type need not use temporal lists or store every op(s,t) explicitly. It may use sets, maps, intervals, accumulated values, dominance summaries or another type-specific representation. It must nevertheless implement the observable interval semantics: input and output contexts, factorisation, merge and application effect. Any discarded information must be irrelevant to all of those observations.

Previous20.10 Scratch pad Next20.12 Control algorithm using interval operations