20.7 Full database states

This section describes a replicated database as a state machine whose sites hold full database states. A locally generated change produces a new full state. A state received from another site is combined with the local state by a merge operator. There are no delta operations in this model.

Sites, vector times and database states

Let S be a set of site identifiers. A vector time is a mapping v : S → ℕ. The empty vector time v∅ is defined by v∅(s) = 0 for every s ∈ S. Vector times are ordered pointwise. Their pointwise least upper bound is denoted by ↑.

Let 𝒟 be the set of full database states. Every d ∈ 𝒟 has an output vector time vout(d). Let d∅ be the initial database state, satisfying

vout(d∅) = v∅.

A state of the entire system, also called a configuration, is a mapping D : S → 𝒟. Thus D(s) is the full database state held at site s. The initial configuration D∅ is defined by

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

State-machine transitions

There are two kinds of transition. A local-generation transition at site s replaces D(s) = d by a new full database state d′ such that

vout(d′)(s) = vout(d)(s) + 1, and

vout(d′)(r) = vout(d)(r) for every r ≠ s.

The transition directly produces the successor state d′; it does not produce a delta and does not invoke merge. Every other site retains its existing state.

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

D(r) := D(r) ⊕ D(s).

Every other site retains its existing state. This single transition is sufficient to model communication. A cached state can be held at an additional site and merged into another site later; the mathematical model does not need separate send and receive events.

A configuration is reachable if it is the initial configuration or is obtained from the initial configuration by a finite sequence of local-generation and merge transitions. Properties of reachable configurations are proved by induction on the length of this transition sequence.

Happened-before relation

The transition rules induce a happened-before relation on occurrences of database states. If d′ is locally generated from d, then d precedes d′. If c = a ⊕ b is produced by a merge, then both a and b precede c. The reflexive transitive closure of these relations is denoted by ≼. On reachable states, ≼ is a partial order; d∅ is its least element.

The strict happened-before relation is defined by a ≺ b if a ≼ b and a ≠ b. A redundant merge that leaves a state unchanged therefore does not introduce a strict happened-before edge.

Definition:
A vector time v is causally valid if v = vout(d) for some reachable database state d.

The output-vector-time mapping preserves the causal order:

a ≼ b   ⇒   vout(a) ≤ vout(b).

Merge axioms

The merge operator ⊕ combines two full database states. It satisfies the following axioms on reachable states.

Axiom (output vector time of merge):
vout(a ⊕ b) = vout(a) ↑ vout(b).
Axiom (commutativity):
a ⊕ b = b ⊕ a.
Axiom (causal absorption):
If vout(b) ≤ vout(a), then a ⊕ b = a.

Causal absorption says that merging a state whose complete history is already incorporated has no effect. It is stronger than idempotence.

The state join-semilattice

Idempotence:
For every reachable state a, a ⊕ a = a.
Proof:
Since vout(a) ≤ vout(a), the result follows from causal absorption.
Initial-state identity:
For every reachable state a, a ⊕ d∅ = d∅ ⊕ a = a.
Proof:
The empty vector time is no greater than any vector time, so causal absorption gives a ⊕ d∅ = a. Commutativity gives the other equality.
Uniqueness at a vector time:
For reachable states a,b, \(v_{\mathrm{out}}(a)=v_{\mathrm{out}}(b)\Longrightarrow a=b.\)
Proof:
Equality of the vector times gives vout(b) ≤ vout(a), so causal absorption gives a ⊕ b = a. It also gives vout(a) ≤ vout(b), so causal absorption gives b ⊕ a = b. Commutativity therefore gives a = b.
Associativity:
(a ⊕ b) ⊕ c = a ⊕ (b ⊕ c).
Proof:
The output-vector-time axiom and associativity of vector-time join give
vout((a ⊕ b) ⊕ c) = (vout(a) ↑ vout(b)) ↑ vout(c) = vout(a) ↑ (vout(b) ↑ vout(c)) = vout(a ⊕ (b ⊕ c)).
Uniqueness at a vector time gives the result.

Consequently each causally valid vector time v determines a unique full database state, denoted by State(v), satisfying vout(State(v)) = v.

Merge is least upper bound:
For reachable states a and b, a ⊕ b is their least upper bound in the happened-before order.
Proof:
The merge transition makes both a and b precede a ⊕ b. Its output vector time is the least upper bound of their output vector times. If c is any common causal successor, both output vector times are no greater than vout(c), so vout(a ⊕ b) ≤ vout(c). Causal absorption and uniqueness at a vector time identify the corresponding reachable state below c. Hence a ⊕ b is the least common successor.

Thus reachable full database states form a join-semilattice under ⊕. Merge is the join. A meet has not been defined and is not required by this model, so the states are not assumed to form a lattice. No delta operation is needed to state or prove these properties.

Convergence

Convergence of full database states:
If two sites have the same output vector time, they have the same full database state.
Proof:
The states at both sites are reachable. The result follows immediately from uniqueness at a vector time.
Convergence at quiescence:
If every generated change is eventually incorporated at every site, all sites converge to the same full database state at quiescence.
Proof:
At quiescence every site has incorporated the same generated changes, so every site has the same output vector time. Convergence of full database states then gives equality of their database states.