Lamport clocks

StructureEvent#✓fully proved

An event of an execution, for a type \(P\) of processes, consists of the process in \(P\) it belongs to and, if it is a receipt, a natural number: the position in the execution of the event whose message it receives. The structure does not require that position to be earlier than the event itself.

structure Event (P : Type*) where
  /-- The process the event belongs to. -/
  proc : P
  /-- The position of the sending event, for a receipt. -/
  recvFrom : Option ℕ

Used by 31

Used byThe clock condition · One step of the Lamport clock algorithm · Happened-before relates positions of the execution · Happened-before · Happened-before goes forward in the execution · Running the Lamport clock algorithm · One step of happened-before · One step of happened-before raises the timestamp · Process counters dominate their timestamps · Lamport timestamps increase along each process · A receipt is stamped later than its send · Lamport timestamps · Appending events does not change earlier timestamps · A timestamp depends only on a prefix containing its event · Lamport's total order · Lamport's total order extends happened-before · Lamport's order is total · Well-formed executions · One step of the vector clock algorithm · Own-entry comparison detects happened-before · Vector clocks characterize happened-before · 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 · Vector timestamps of an execution · 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

DefinitionWell-formed executions#✓fully proved

An execution \(e_0, \dots, e_{n-1}\) is well formed when every receipt names an earlier event: whenever \(e_j\) receives the message sent by the event at position \(i\), then \(i < j\).

def WellFormed (tr : List (Event P)) : Prop :=
  ∀ j (ej : Event P) i, tr[j]? = some ej → ej.recvFrom = some i → i < j

Uses 1 · Used by 1

Statement usesEvent

Used byA receipt is stamped later than its send

DefinitionOne step of happened-before#✓fully proved

In an execution, position \(i\) precedes position \(j\) by one step when \(i < j\), both positions hold events, and either the two events belong to the same process or the event at \(j\) receives the message of the event at \(i\).

def Step (tr : List (Event P)) (i j : ℕ) : Prop :=
  i < j ∧ ∃ ei ej, tr[i]? = some ei ∧ tr[j]? = some ej ∧
    (ei.proc = ej.proc ∨ ej.recvFrom = some i)

Uses 1 · Used by 8

Statement usesEvent

Used byThe clock condition · Happened-before relates positions of the execution · Happened-before · Happened-before goes forward in the execution · One step of happened-before raises the timestamp · Own-entry comparison detects happened-before · Vector timestamps are monotone along happened-before · Vector timestamps are monotone along one step of happened-before

DefinitionHappened-before#✓fully proved

Lamport's happened-before relation on the positions of an execution is the transitive closure of one step of happened-before: \(a\) happened before \(b\) when there is a chain \(a = i_0, i_1, \dots, i_k = b\) with \(k \ge 1\) in which each \(i_m\) precedes \(i_{m+1}\) by one step.

def HappensBefore (tr : List (Event P)) : ℕ → ℕ → Prop :=
  Relation.TransGen (Step tr)

Uses 2 · Used by 7

Statement usesEvent · One step of happened-before

Used byThe clock condition · Happened-before relates positions of the execution · Happened-before goes forward in the execution · Lamport's total order extends happened-before · Own-entry comparison detects happened-before · Vector clocks characterize happened-before · Vector timestamps are monotone along happened-before

TheoremHappened-before goes forward in the execution#✓fully proved

If position \(a\) happened before position \(b\) in an execution, then \(a < b\).

theorem HappensBefore.lt {tr : List (Event P)} {a b : ℕ} (h : HappensBefore tr a b) : a < b

Uses 3 · Used by 1

Statement usesEvent · Happened-before

Proof usesOne step of happened-before

Used byVector clocks characterize happened-before

DefinitionOne step of the Lamport clock algorithm#✓fully proved

The state is a counter \(c(p) \in \mathbb{N}\) for each process \(p\) together with the timestamps assigned so far. An event \(e\) of process \(p\) gets the timestamp \(t = \max(c(p), s) + 1\), where \(s\) is the timestamp already assigned at the position that \(e\) receives from; \(s = 0\) if \(e\) is not a receipt or if no timestamp has been assigned at that position. The step sets \(c(p)\) to \(t\) and appends \(t\) to the timestamps.

The timestamps are kept in an array, for constant-time append and lookup.

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

Uses 1 · Used by 4

Statement usesEvent

Used byRunning the Lamport clock algorithm · One step of happened-before raises the timestamp · Process counters dominate their timestamps · Appending events does not change earlier timestamps

DefinitionRunning the Lamport clock algorithm#✓fully proved

The clock algorithm over an execution applies one step of the algorithm to each event in order, starting from all process counters \(0\) and no timestamps. The result is the final counters together with the timestamps assigned to the events, in order.

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

Uses 2 · Used by 4

Statement usesEvent · One step of the Lamport clock algorithm

Used byOne step of happened-before raises the timestamp · Process counters dominate their timestamps · Lamport timestamps · Appending events does not change earlier timestamps

DefinitionLamport timestamps#✓fully proved

The Lamport timestamps \(t_0, \dots, t_{n-1}\) of an execution \(e_0, \dots, e_{n-1}\) are computed by Lamport's clock algorithm. Every process keeps a counter, initially \(0\). For \(k = 0, \dots, n-1\) in turn, let \(c\) be the current counter of the process of \(e_k\), and let \(m = t_i\) if \(e_k\) receives the message sent by the event at position \(i\) with \(i < k\), and \(m = 0\) otherwise. Then \(t_k = \max(c, m) + 1\), and the counter of the process of \(e_k\) is set to \(t_k\).

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

Uses 2 · Used by 10

Statement usesEvent · Running the Lamport clock algorithm

Used byThe clock condition · One step of happened-before raises the timestamp · Process counters dominate their timestamps · Lamport timestamps increase along each process · A receipt is stamped later than its send · Appending events does not change earlier timestamps · A timestamp depends only on a prefix containing its event · Lamport's total order · Lamport's total order extends happened-before · Lamport's order is total

TheoremAppending events does not change earlier timestamps#✓fully proved

Let \(e_0, \dots, e_{n-1}\) be an execution, and extend it by appending further events. For every \(i < n\), the Lamport timestamp of the event at position \(i\) is the same in the extended execution as in the original one.

theorem timestamps_append (tr rest : List (Event P)) {i : ℕ} (hi : i < tr.length) :
    (timestamps (tr ++ rest)).getD i 0 = (timestamps tr).getD i 0

Uses 4 · Used by 1

Statement usesEvent · Lamport timestamps

Proof usesOne step of the Lamport clock algorithm · Running the Lamport clock algorithm

Used byA timestamp depends only on a prefix containing its event

TheoremProcess counters dominate their timestamps#✓fully proved

After the Lamport clock algorithm has run over an execution, the counter of each process is at least the timestamp of every event of that process in the execution.

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

Uses 4 · Used by 1

Statement usesEvent · Running the Lamport clock algorithm · Lamport timestamps

Proof usesOne step of the Lamport clock algorithm

Used byOne step of happened-before raises the timestamp

TheoremA timestamp depends only on a prefix containing its event#✓fully proved

Let \(e_0, \dots, e_{n-1}\) be an execution and let \(i < k \le n\). The Lamport timestamp of \(e_i\) in the whole execution equals its Lamport timestamp in the prefix \(e_0, \dots, e_{k-1}\).

theorem timestamps_getD_take (tr : List (Event P)) {i k : ℕ} (hik : i < k) (hk : k ≤ tr.length) :
    (timestamps tr).getD i 0 = (timestamps (tr.take k)).getD i 0

Uses 3 · Used by 1

Statement usesEvent · Lamport timestamps

Proof usesAppending events does not change earlier timestamps

Used byOne step of happened-before raises the timestamp

TheoremOne step of happened-before raises the timestamp#✓fully proved

If position \(i\) precedes position \(j\) by one step of happened-before in an execution, then the Lamport timestamp of \(i\) is smaller than the Lamport timestamp of \(j\).

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

Uses 7 · Used by 3

Statement usesEvent · One step of happened-before · Lamport timestamps

Proof usesOne step of the Lamport clock algorithm · Running the Lamport clock algorithm · Process counters dominate their timestamps · A timestamp depends only on a prefix containing its event

Used byThe clock condition · Lamport timestamps increase along each process · A receipt is stamped later than its send

TheoremA receipt is stamped later than its send#✓fully proved

Let \(e_0, \dots, e_{n-1}\) be a well-formed execution and let \(t_k\) be the Lamport timestamp of \(e_k\). If \(j < n\) and \(e_j\) receives the message sent by the event at position \(i\), then \(t_i < t_j\).

This is Lamport's clock condition C2, which his implementation rule IR2 guarantees.

theorem timestamp_lt_of_recv {tr : List (Event P)} (hwf : WellFormed tr) {i j : ℕ}
    {ej : Event P} (hj : tr[j]? = some ej) (hr : ej.recvFrom = some i) :
    (timestamps tr).getD i 0 < (timestamps tr).getD j 0

Uses 4

Statement usesEvent · Well-formed executions · Lamport timestamps

Proof usesOne step of happened-before raises the timestamp

TheoremLamport timestamps increase along each process#✓fully proved

Let \(e_0, \dots, e_{n-1}\) be an execution and let \(t_k\) be the Lamport timestamp of \(e_k\). If \(i < j < n\) and \(e_i\) and \(e_j\) belong to the same process, then \(t_i < t_j\).

This is Lamport's clock condition C1, which his implementation rule IR1 guarantees.

theorem timestamp_lt_of_proc {tr : List (Event P)} {i j : ℕ} {ei ej : Event P}
    (hij : i < j) (hi : tr[i]? = some ei) (hj : tr[j]? = some ej) (hp : ei.proc = ej.proc) :
    (timestamps tr).getD i 0 < (timestamps tr).getD j 0

Uses 3 · Used by 1

Statement usesEvent · Lamport timestamps

Proof usesOne step of happened-before raises the timestamp

Used byLamport's order is total

TheoremThe clock condition#✓fully proved

In every execution, if the event at position \(a\) happened before the event at position \(b\), then the Lamport timestamp of \(a\) is smaller than the Lamport timestamp of \(b\) (Lamport 1978).

theorem clock_condition {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 · Lamport timestamps

Proof usesOne step of happened-before · One step of happened-before raises the timestamp

Used byLamport's total order extends happened-before

TheoremHappened-before relates positions of the execution#✓fully proved

If position \(a\) happened before position \(b\) in an execution, then the execution has an event at position \(a\) and an event at position \(b\).

theorem HappensBefore.exists_events {tr : List (Event P)} {a b : ℕ} (h : HappensBefore tr a b) :
    (∃ ea, tr[a]? = some ea) ∧ ∃ eb, tr[b]? = some eb

Uses 3 · Used by 1

Statement usesEvent · Happened-before

Proof usesOne step of happened-before

Used byLamport's total order extends happened-before

DefinitionLamport's total order#✓fully proved

Fix a linear order on the processes. In an execution \(e_0, \dots, e_{n-1}\) with Lamport timestamps \(t_0, \dots, t_{n-1}\), position \(a\) precedes position \(b\) when \(a < n\), \(b < n\), and either \(t_a < t_b\), or \(t_a = t_b\) and the process of \(e_a\) is smaller than the process of \(e_b\).

def TotalBefore (tr : List (Event P)) (a b : ℕ) : Prop :=
  ∃ ea eb, tr[a]? = some ea ∧ tr[b]? = some eb ∧
    toLex ((timestamps tr).getD a 0, ea.proc) < toLex ((timestamps tr).getD b 0, eb.proc)

Uses 2 · Used by 2

Statement usesEvent · Lamport timestamps

Used byLamport's total order extends happened-before · Lamport's order is total

TheoremLamport's total order extends happened-before#✓fully proved

In every execution, if the event at position \(a\) happened before the event at position \(b\), then position \(a\) precedes position \(b\) in Lamport's total order.

theorem totalBefore_of_happensBefore {tr : List (Event P)} {a b : ℕ}
    (h : HappensBefore tr a b) : TotalBefore tr a b

Uses 6

Statement usesEvent · Happened-before · Lamport's total order

Proof usesHappened-before relates positions of the execution · The clock condition · Lamport timestamps

TheoremLamport's order is total#✓fully proved

In every execution, for any two distinct positions \(a \ne b\) that both hold events, \(a\) precedes \(b\) or \(b\) precedes \(a\) in Lamport's total order.

Two events of the same process have different timestamps (an earlier event of a process has a smaller timestamp), so ties only occur between different processes, which the order on processes breaks.

theorem totalBefore_total {tr : List (Event P)} {a b : ℕ} {ea eb : Event P}
    (ha : tr[a]? = some ea) (hb : tr[b]? = some eb) (hab : a ≠ b) :
    TotalBefore tr a b ∨ TotalBefore tr b a

Uses 4

Statement usesEvent · Lamport's total order

Proof usesLamport timestamps increase along each process · Lamport timestamps

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.