Vector clocks

DefinitionVector clock stamp of an event#✓fully proved

Let \(P\) be the set of processes. Given the current vectors \(V_q \in \mathbb{N}^P\) of the processes \(q\) and the timestamps \(T_0, T_1, \dots\) assigned so far, the vector clock algorithm stamps an event \(e\) of process \(p\) as follows. Let \(m = T_i\) if \(e\) receives the message sent by the event at position \(i\) and \(T_i\) has been assigned, and \(m = 0\) otherwise. The stamp of \(e\) is the pointwise maximum of \(V_p\) and \(m\), with its \(p\)-entry increased by \(1\).

def stamp (st : (P → P → ℕ) × Array (P → ℕ)) (e : Event P) : P → ℕ :=
  let base : P → ℕ := fun q =>
    max (st.1 e.proc q) ((e.recvFrom.map fun i => (st.2[i]?.getD 0) q).getD 0)
  Function.update base e.proc (base e.proc + 1)

Uses 1 · Used by 7

Statement usesEvent

Used byOne step of the vector clock algorithm · Own-entry comparison detects happened-before · An event's own entry is positive · Each process's vector dominates its events' timestamps · Timestamps are stamps from the preceding state · Vector timestamps are monotone along one step of happened-before · A process's final vector is zero or one of its timestamps

DefinitionOne step of the vector clock algorithm#✓fully proved

The state of the algorithm holds a vector \(V_q \in \mathbb{N}^P\) for each process \(q\), where \(P\) is the set of processes, and the timestamps assigned so far, kept in an array for constant-time append and lookup. On an event \(e\) of process \(p\), the step replaces \(V_p\) by the stamp \(s\) of \(e\) computed from the current state, leaves the other vectors unchanged, and appends \(s\) to the timestamps.

def clockStep (st : (P → P → ℕ) × Array (P → ℕ)) (e : Event P) :
    (P → P → ℕ) × Array (P → ℕ) :=
  (Function.update st.1 e.proc (stamp st e), st.2.push (stamp st e))

Uses 2 · Used by 6

Statement usesEvent · Vector clock stamp of an event

Used byOwn-entry comparison detects happened-before · Running the vector clock algorithm · Each process's vector dominates its events' timestamps · Timestamps are stamps from the preceding state · Vector timestamps are monotone along one step of happened-before · A process's final vector is zero or one of its timestamps

DefinitionRunning the vector clock algorithm#✓fully proved

The state of the vector clock algorithm after an execution is obtained by starting from the state in which every process's vector is \(0\) and no timestamps have been assigned, and applying one step of the algorithm to each event of the execution in order.

def run (tr : List (Event P)) : (P → P → ℕ) × Array (P → ℕ) :=
  tr.foldl clockStep (fun _ => 0, #[])

Uses 2 · Used by 8

Statement usesEvent · One step of the vector clock algorithm

Used byOwn-entry comparison detects happened-before · An event's own entry is positive · Array lookup agrees with the timestamp list · Each process's vector dominates its events' timestamps · Vector timestamps of an execution · Timestamps are stamps from the preceding state · Vector timestamps are monotone along one step of happened-before · A process's final vector is zero or one of its timestamps

DefinitionVector timestamps of an execution#✓fully proved

The vector timestamps of an execution are the list of vectors that the vector clock algorithm, run over the execution, assigns to its events, in order.

def timestamps (tr : List (Event P)) : List (P → ℕ) := (run tr).2.toList

Uses 2 · Used by 9

Statement usesEvent · Running the vector clock algorithm

Used byOwn-entry comparison detects happened-before · Vector clocks characterize happened-before · An event's own entry is positive · Array lookup agrees with the timestamp list · Each process's vector dominates its events' timestamps · Timestamps are stamps from the preceding state · Vector timestamps are monotone along happened-before · Vector timestamps are monotone along one step of happened-before · A process's final vector is zero or one of its timestamps

TheoremArray lookup agrees with the timestamp list#✓fully proved

For every execution and every natural number \(i\), the entry at index \(i\) of the array of timestamps built by the vector clock algorithm on the execution equals the \(i\)-th vector timestamp of the execution, where an index out of range gives the zero vector in both lookups.

theorem run_getD (tr : List (Event P)) (i : ℕ) :
    (run tr).2[i]?.getD 0 = (timestamps tr).getD i 0

Uses 3 · Used by 2

Statement usesEvent · Running the vector clock algorithm · Vector timestamps of an execution

Used byOwn-entry comparison detects happened-before · Vector timestamps are monotone along one step of happened-before

TheoremTimestamps are stamps from the preceding state#✓fully proved

For every execution and every position \(j\) of an event \(e\) of it, the vector timestamp of \(j\) equals the stamp of \(e\) computed from the state of the vector clock algorithm after the first \(j\) events of the execution.

theorem timestamps_getD_eq_stamp {tr : List (Event P)} {j : ℕ} {ej : Event P}
    (hj : tr[j]? = some ej) :
    (timestamps tr).getD j 0 = stamp (run (tr.take j)) ej

Uses 5 · Used by 3

Statement usesEvent · Running the vector clock algorithm · Vector clock stamp of an event · Vector timestamps of an execution

Proof usesOne step of the vector clock algorithm

Used byOwn-entry comparison detects happened-before · An event's own entry is positive · Vector timestamps are monotone along one step of happened-before

TheoremEach process's vector dominates its events' timestamps#✓fully proved

For every execution and every position \(i\) of an event of it, the vector timestamp of \(i\) is pointwise at most the vector of that event's process in the state of the vector clock algorithm after the whole execution.

theorem timestamp_le_vector (tr : List (Event P)) {i : ℕ} {ei : Event P}
    (hi : tr[i]? = some ei) : (timestamps tr).getD i 0 ≤ (run tr).1 ei.proc

Uses 5 · Used by 2

Statement usesEvent · Running the vector clock algorithm · Vector timestamps of an execution

Proof usesOne step of the vector clock algorithm · Vector clock stamp of an event

Used byOwn-entry comparison detects happened-before · Vector timestamps are monotone along one step of happened-before

TheoremA process's final vector is zero or one of its timestamps#✓fully proved

Run the vector clock algorithm over an execution, starting from all vectors \(0\). For every process \(p\), the vector held by \(p\) at the end is either the zero vector or the vector timestamp of some event of \(p\) in the execution.

theorem vector_eq (tr : List (Event P)) (p : P) :
    (run tr).1 p = 0 ∨ ∃ j ej, tr[j]? = some ej ∧ ej.proc = p ∧
      (run tr).1 p = (timestamps tr).getD j 0

Uses 5 · Used by 1

Statement usesEvent · Running the vector clock algorithm · Vector timestamps of an execution

Proof usesOne step of the vector clock algorithm · Vector clock stamp of an event

Used byOwn-entry comparison detects happened-before

TheoremAn event's own entry is positive#✓fully proved

For every position \(j\) of an event of an execution, if \(p\) is the process of that event, then the \(p\)-entry of the vector timestamp of \(j\) is at least \(1\).

theorem one_le_own {tr : List (Event P)} {j : ℕ} {ej : Event P} (hj : tr[j]? = some ej) :
    1 ≤ (timestamps tr).getD j 0 ej.proc

Uses 5 · Used by 1

Statement usesEvent · Vector timestamps of an execution

Proof usesRunning the vector clock algorithm · Vector clock stamp of an event · Timestamps are stamps from the preceding state

Used byOwn-entry comparison detects happened-before

TheoremVector timestamps are monotone along one step of happened-before#✓fully proved

In an execution, write \(V_i\) for the vector timestamp that the vector clock algorithm gives to the event at position \(i\). If the event at position \(j\) follows the event at position \(i\) by one step of happened-before, then \(V_i(q) \le V_j(q)\) for every process \(q\).

theorem vectorClock_le_of_step {tr : List (Event P)} {i j : ℕ} (h : Step tr i j) :
    (timestamps tr).getD i 0 ≤ (timestamps tr).getD j 0

Uses 9 · Used by 1

Statement usesEvent · One step of happened-before · Vector timestamps of an execution

Proof usesOne step of the vector clock algorithm · Running the vector clock algorithm · Array lookup agrees with the timestamp list · Vector clock stamp of an event · Each process's vector dominates its events' timestamps · Timestamps are stamps from the preceding state

Used byVector timestamps are monotone along happened-before

TheoremVector timestamps are monotone along happened-before#✓fully proved

In an execution, write \(V_i\) for the vector timestamp that the vector clock algorithm gives to the event at position \(i\). If the event at position \(a\) happened before the event at position \(b\), then \(V_a(q) \le V_b(q)\) for every process \(q\).

theorem vectorClock_le_of_happensBefore {tr : List (Event P)} {a b : ℕ}
    (h : HappensBefore tr a b) : (timestamps tr).getD a 0 ≤ (timestamps tr).getD b 0

Uses 5 · Used by 1

Statement usesEvent · Happened-before · Vector timestamps of an execution

Proof usesOne step of happened-before · Vector timestamps are monotone along one step of happened-before

Used byVector clocks characterize happened-before

TheoremOwn-entry comparison detects happened-before#✓fully proved

Let \(a\) and \(b\) be positions of events of an execution, and let \(p\) be the process of the event at \(a\). If the \(p\)-entry of the vector timestamp of \(a\) is at most the \(p\)-entry of the vector timestamp of \(b\), then \(a = b\) or \(a\) happened before \(b\).

theorem eq_or_happensBefore_of_le {tr : List (Event P)} :
    ∀ (b : ℕ) {a : ℕ} {ea eb : Event P}, tr[a]? = some ea → tr[b]? = some eb →
      (timestamps tr).getD a 0 ea.proc ≤ (timestamps tr).getD b 0 ea.proc →
      a = b ∨ HappensBefore tr a b

Uses 12 · Used by 1

Statement usesEvent · Happened-before · Vector timestamps of an execution

Proof usesOne step of happened-before · One step of the vector clock algorithm · An event's own entry is positive · Running the vector clock algorithm · Array lookup agrees with the timestamp list · Vector clock stamp of an event · Each process's vector dominates its events' timestamps · Timestamps are stamps from the preceding state · A process's final vector is zero or one of its timestamps

Used byVector clocks characterize happened-before

TheoremVector clocks characterize happened-before#✓fully proved

For two events of an execution, a happened before b exactly when a's timestamp is smaller than b's in the pointwise order.

theorem happensBefore_iff_lt {tr : List (Event P)} {a b : ℕ} (ha : a < tr.length)
    (hb : b < tr.length) :
    HappensBefore tr a b ↔ (timestamps tr).getD a 0 < (timestamps tr).getD b 0

Uses 6

Statement usesEvent · Happened-before · Vector timestamps of an execution

Proof usesHappened-before goes forward in the execution · Own-entry comparison detects happened-before · Vector timestamps are monotone along happened-before

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.