20.8 Vector times paired with database values

This section describes a replicated database as a state machine in which the state held at a site is a pair (v,d), where v is a vector time and d is a database value. Vector times record causal progress, while database values are combined by a separate operator.

System state

Let S be a set of site identifiers, let V be the set of vector times over S, and let 𝒟 be the set of database values. A site state is an element of V × 𝒟. The state of the entire system is a mapping

D : S → V × 𝒟.

Let v∅ be the empty vector time and d∅ the initial database value. The initial system state D∅ is defined by

D∅(s) = (v∅,d∅)   for every s ∈ S.

State-machine transitions

A local-generation transition at site s replaces D(s) = (v,d) by (incs(v),d′), where

incs(v)(r) = (r = s ? v(r)+1 : v(r)).

The database value d′ is the complete successor database value produced by the local change. The transition does not produce a delta and does not invoke merge.

A merge transition from site s to site r replaces the state at r by

D(r) := D(r) + D(s),

where + is the merge of site states defined below. All other site states remain unchanged. A configuration is reachable if it is obtained from D∅ by a finite sequence of these two kinds of transition.

Merge of database values

Let ⊕ : 𝒟 × 𝒟 → 𝒟 be a binary operation on database values. It satisfies the following axioms for database values occurring in reachable site states.

Axiom (commutativity):
d1 ⊕ d2 = d2 ⊕ d1.
Axiom (associativity):
(d1 ⊕ d2) ⊕ d3 = d1 ⊕ (d2 ⊕ d3).
Axiom (idempotence):
d ⊕ d = d.
Axiom (initial-value identity):
d ⊕ d∅ = d∅ ⊕ d = d.
Axiom (strict causal absorption):
For reachable site states (v1,d1) and (v2,d2), \(v_1<v_2\Longrightarrow d_1\mathbin{\oplus}d_2=d_2.\)

Strict causal absorption says that a strictly later database value already incorporates the earlier one. It does not prescribe equality of database values associated with equal vector times.

Merge of site states

Definition:
Define + on site states by
(v1,d1) + (v2,d2) = (v1 ↑ v2, d1 ⊕ d2).
Output vector time of merge:
The vector-time component of (v1,d1) + (v2,d2) is v1 ↑ v2.
Proof:
This follows immediately from the definition of +.
Commutativity of site-state merge:
a + b = b + a.
Proof:
Vector-time join and database-value merge are both commutative.
Associativity of site-state merge:
(a + b) + c = a + (b + c).
Proof:
Vector-time join and database-value merge are both associative.
Idempotence of site-state merge:
a + a = a.
Proof:
Vector-time join and database-value merge are both idempotent.
Initial-state identity:
a + (v∅,d∅) = (v∅,d∅) + a = a.
Proof:
The empty vector time is the identity of vector-time join and d∅ is the identity of database-value merge.
Dominated-state merge:
For reachable site states a = (v1,d1) and b = (v2,d2), \(v_1<v_2\Longrightarrow a+b=b.\)
Proof:
If v1 < v2, then v1 ↑ v2 = v2 and strict causal absorption gives d1 ⊕ d2 = d2. Substitution in the definition of + gives the result.

Consequently + can be implemented as

(v1,d1) + (v2,d2) =

(v2,d2) if v1 < v2,

(v1,d1) if v2 < v1,

(v1 ↑ v2,d1 ⊕ d2) otherwise.

The final case includes concurrent vector times and equal vector times. In particular, equal vector times do not give either argument priority.

Join-semilattice and convergence

Commutativity, associativity and idempotence make the reachable site states a join-semilattice under +. The value of a finite merge is therefore independent of the order and grouping of its inputs and of repeated occurrences of an input.

Convergence of merged states:
If two sites have incorporated the same finite collection of site states, allowing different order, grouping and repetition, then the two sites hold the same site state.
Proof:
Commutativity removes dependence on order, associativity removes dependence on grouping, and idempotence removes repeated occurrences. The two merge expressions therefore have the same value.
Convergence at quiescence:
If every generated state is eventually incorporated at every site, all sites converge to the same site state at quiescence.
Proof:
At quiescence each site contains a merge expression over the same generated states. The expressions may differ only in order, grouping and repetition, so convergence of merged states gives equality.