Two-phase locking

InductiveLock mode#✓fully proved

A lock is held in one of two modes: shared (a read lock) or exclusive (a write lock).

inductive LockMode
  /-- A shared (read) lock. -/
  | shared
  /-- An exclusive (write) lock. -/
  | exclusive
deriving DecidableEq

Used by 17

Used byAction of a locked schedule · The two-phase locking theorem · Strict two-phase locking theorem · Lock mode coverage · Holding a lock · Release test · Lock compatibility at a point · Locked items · Lock coverage at a position · Lock mode required by an access · Reads and writes of a locked schedule · Release of the lock requested at a position · Schedules that release every lock · Strictness at a pair of positions · Strict two-phase schedules · Two-phase schedules · Two-phase condition at a pair of positions

DefinitionLock mode coverage#✓fully proved

A lock mode \(m'\) covers a lock mode \(m\) when a lock in mode \(m'\) permits what a lock in mode \(m\) permits: an exclusive lock covers both modes, and a shared lock covers only the shared mode.

def LockMode.Covers : LockMode → LockMode → Prop
  | .exclusive, _ => True
  | .shared, m => m = .shared

Uses 1 · Used by 2

Statement usesLock mode

Used byThe two-phase locking theorem · Holding a lock

DefinitionLock mode required by an access#✓fully proved

The lock mode an access requires: shared for a read, exclusive for a write.

def Access.mode : Access → LockMode
  | .read => .shared
  | .write => .exclusive

Uses 2 · Used by 3

Statement usesRead or write access · Lock mode

Used byThe two-phase locking theorem · Schedules covered by locks · Lock coverage at a position

InductiveAction of a locked schedule#✓fully proved

For \(n\) transactions, numbered \(0, \dots, n-1\), and a type \(X\) of data items, an action of a locked schedule is one of three kinds: a read or write operation; a lock request, in which a transaction \(t\) acquires a lock on an item \(x \in X\) in a lock mode \(m\) (shared or exclusive); or a release, in which a transaction \(t\) releases its lock on an item \(x \in X\).

inductive Action (n : ℕ) (X : Type*)
  /-- A read or a write. -/
  | op (o : Op n X)
  /-- Transaction `t` acquires a lock on `x` in mode `m`. -/
  | lock (t : Fin n) (x : X) (m : LockMode)
  /-- Transaction `t` releases its lock on `x`. -/
  | unlock (t : Fin n) (x : X)
deriving DecidableEq

Uses 2 · Used by 17

Statement usesLock mode · Operation of a schedule

Used byThe two-phase locking theorem · Strict two-phase locking theorem · Holding a lock · Release test · Legal locked schedule · Lock compatibility at a point · Locked items · Schedules covered by locks · Lock coverage at a position · Reads and writes of a locked schedule · Release of the lock requested at a position · Schedules that release every lock · Strictness at a pair of positions · Strict two-phase schedules · Two-phase schedules · Two-phase condition at a pair of positions · Well-formed locked schedules

DefinitionReads and writes of a locked schedule#✓fully proved

For a locked schedule \(s\), the schedule of reads and writes of \(s\): its reads and writes in order, with the lock requests and releases erased.

def ops (s : List (Action n X)) : List (Op n X) :=
  s.filterMap fun
    | .op o => some o
    | _ => none

Uses 3 · Used by 2

Statement usesAction of a locked schedule · Lock mode · Operation of a schedule

Used byThe two-phase locking theorem · Strict two-phase locking theorem

DefinitionHolding a lock#✓fully proved

Let \(s\) be a locked schedule, \(t\) a transaction, \(x\) a data item, \(m\) a lock mode and \(p\) a natural number. Transaction \(t\) holds a lock on \(x\) covering mode \(m\) just before position \(p\) of \(s\) when there is a position \(q < p\) at which \(s\) has a lock request by \(t\) on \(x\) in some mode \(m'\) that covers \(m\), and for no position \(r\) with \(q < r < p\) is the action of \(s\) at \(r\) a release of \(x\) by \(t\).

def HoldsBefore (s : List (Action n X)) (t : Fin n) (x : X) (m : LockMode) (p : ℕ) : Prop :=
  ∃ q < p, (∃ m', s[q]? = some (.lock t x m') ∧ m'.Covers m) ∧
    ∀ r < p, q < r → s[r]? ≠ some (.unlock t x)

Uses 3 · Used by 7

Statement usesAction of a locked schedule · Lock mode · Lock mode coverage

Used byThe two-phase locking theorem · Strict two-phase locking theorem · Lock compatibility at a point · Schedules covered by locks · Lock coverage at a position · Strictness at a pair of positions · Strict two-phase schedules

DefinitionSchedules covered by locks#✓fully proved

A locked schedule \(s\) is covered by locks when every read or write is protected by a lock of its transaction: whenever \(s\) has at position \(p\) a read or write \(o\) by transaction \(t\) on item \(x\), just before position \(p\) transaction \(t\) holds a lock on \(x\) (acquired at an earlier position and not released since) whose mode covers the mode \(o\) requires, namely shared for a read and exclusive for a write; an exclusive lock covers both modes.

def LocksCover (s : List (Action n X)) : Prop :=
  ∀ p o, s[p]? = some (.op o) → HoldsBefore s o.txn o.item o.access.mode p

Uses 5 · Used by 3

Statement usesRead or write access · Lock mode required by an access · Action of a locked schedule · Holding a lock · Operation of a schedule

Used byThe two-phase locking theorem · Strict two-phase locking theorem · Well-formed locked schedules

DefinitionSchedules that release every lock#✓fully proved

A locked schedule \(s\) releases its locks when every lock request is followed by a matching release: whenever \(s\) has at position \(q\) a lock request (in either mode) by transaction \(t\) on item \(x\), there is a position \(r > q\) at which \(s\) has a release by \(t\) of \(x\).

In particular, transactions end holding no locks.

def ReleasesLocks (s : List (Action n X)) : Prop :=
  ∀ (q : ℕ) (t : Fin n) (x : X) (m : LockMode), s[q]? = some (.lock t x m) →
    ∃ r, q < r ∧ s[r]? = some (.unlock t x)

Uses 2 · Used by 1

Statement usesAction of a locked schedule · Lock mode

Used byWell-formed locked schedules

DefinitionWell-formed locked schedules#✓fully proved

A locked schedule \(s\) (a list of reads, writes, lock requests and lock releases of transactions) is well formed when its accesses are covered by locks and it releases its locks: every read or write in \(s\) is preceded by a lock request of its own transaction on its item, in a mode covering the access (shared or exclusive for a read, exclusive for a write), with no release of that item by that transaction in between; and every lock request in \(s\) by a transaction on an item is followed later in \(s\) by a release of that item by the same transaction.

def WellFormed (s : List (Action n X)) : Prop := LocksCover s ∧ ReleasesLocks s

Uses 3

Statement usesAction of a locked schedule · Schedules covered by locks · Schedules that release every lock

DefinitionLock compatibility at a point#✓fully proved

A locked schedule \(s\) is legal just before position \(p\) when, for every data item \(x\), all distinct transactions \(t \ne t'\) and all lock modes \(m\), \(m'\): if \(t\) holds a lock on \(x\) covering \(m\) and \(t'\) holds a lock on \(x\) covering \(m'\) just before position \(p\) of \(s\), then \(m\) and \(m'\) are both the shared mode. In words, two transactions do not both hold locks on the same item unless both locks are shared.

def LegalAt (s : List (Action n X)) (p : ℕ) : Prop :=
  ∀ x t t' m m', t ≠ t' → HoldsBefore s t x m p → HoldsBefore s t' x m' p →
    m = .shared ∧ m' = .shared

Uses 3 · Used by 1

Statement usesAction of a locked schedule · Holding a lock · Lock mode

Used byLegal locked schedule

DefinitionLocked items#✓fully proved

The list of data items locked in a locked schedule \(s\): for each lock request of \(s\), in order, the item it locks, so an item appears once for each lock request on it.

def lockedItems (s : List (Action n X)) : List X :=
  s.filterMap fun
    | .lock _ x _ => some x
    | _ => none

Uses 3

Statement usesAction of a locked schedule · Lock mode · Operation of a schedule

DefinitionLegal locked schedule#✓fully proved

A locked schedule \(s\) of length \(\ell\) is legal when it satisfies lock compatibility at every point \(p \le \ell\): just before position \(p\), no two distinct transactions both hold locks on the same item unless both locks are shared.

After the last action the locks no longer change, so the points \(p \le \ell\) are all the points.

def Legal (s : List (Action n X)) : Prop := ∀ p ≤ s.length, LegalAt s p

Uses 2 · Used by 2

Statement usesAction of a locked schedule · Lock compatibility at a point

Used byThe two-phase locking theorem · Strict two-phase locking theorem

DefinitionTwo-phase schedules#✓fully proved

A locked schedule \(s\) is two-phase when every lock request of a transaction precedes every release of that transaction: whenever \(s\) has at position \(p\) a release by transaction \(t\) and at position \(q\) a lock request by \(t\) (on any items, in any mode), then \(q < p\).

def TwoPhase (s : List (Action n X)) : Prop :=
  ∀ (t : Fin n) (p q : ℕ) (x y : X) (m : LockMode),
    s[p]? = some (.unlock t x) → s[q]? = some (.lock t y m) → q < p

Uses 2 · Used by 3

Statement usesAction of a locked schedule · Lock mode

Used byThe two-phase locking theorem · Strict two-phase locking theorem · Strict two-phase schedules

DefinitionStrict two-phase schedules#✓fully proved

A locked schedule \(s\) is strict two-phase when it is two-phase and every transaction releases its exclusive locks only after its last read or write: whenever \(s\) has at position \(p\) a release by transaction \(t\) of item \(x\) and just before position \(p\) transaction \(t\) holds an exclusive lock on \(x\), every read or write of \(t\) in \(s\) occurs at a position before \(p\).

def StrictTwoPhase (s : List (Action n X)) : Prop :=
  TwoPhase s ∧ ∀ t x p, s[p]? = some (.unlock t x) → HoldsBefore s t x .exclusive p →
    ∀ q o, s[q]? = some (.op o) → o.txn = t → q < p

Uses 5 · Used by 1

Statement usesAction of a locked schedule · Holding a lock · Lock mode · Operation of a schedule · Two-phase schedules

Used byStrict two-phase locking theorem

DefinitionLock coverage at a position#✓fully proved

For a locked schedule \(s\) and a position \(p\): if \(s\) has at position \(p\) a read or write \(o\) by transaction \(t\) on item \(x\), then just before position \(p\) transaction \(t\) holds a lock on \(x\) whose mode covers the mode \(o\) requires (shared for a read, exclusive for a write; an exclusive lock covers both modes). If position \(p\) holds a lock request or a release, or lies beyond the end of \(s\), the condition holds trivially.

def LocksCoverAt (s : List (Action n X)) (p : ℕ) : Prop :=
  match s[p]? with
  | some (.op o) => HoldsBefore s o.txn o.item o.access.mode p
  | _ => True

Uses 6

Statement usesRead or write access · Lock mode required by an access · Action of a locked schedule · Holding a lock · Lock mode · Operation of a schedule

DefinitionRelease of the lock requested at a position#✓fully proved

For a locked schedule \(s\) and a position \(q\): if \(s\) has at position \(q\) a lock request (in either mode) by transaction \(t\) on item \(x\), then there is a position \(r\) with \(q < r\) and \(r\) less than the length of \(s\) at which \(s\) has a release by \(t\) of \(x\). If position \(q\) holds a read, a write or a release, or lies beyond the end of \(s\), the condition holds trivially.

def ReleasedAt (s : List (Action n X)) (q : ℕ) : Prop :=
  match s[q]? with
  | some (.lock t x _) => ∃ r < s.length, q < r ∧ s[r]? = some (.unlock t x)
  | _ => True

Uses 3

Statement usesAction of a locked schedule · Lock mode · Operation of a schedule

DefinitionTwo-phase condition at a pair of positions#✓fully proved

For a locked schedule \(s\) and positions \(p\) and \(q\): if \(s\) has at position \(p\) a release by transaction \(t\) and at position \(q\) a lock request by the same transaction \(t\), then \(q < p\). For every other pair of positions, including positions beyond the end of \(s\), the condition holds trivially.

def TwoPhaseAt (s : List (Action n X)) (p q : ℕ) : Prop :=
  match s[p]?, s[q]? with
  | some (.unlock t _), some (.lock t' _ _) => t' = t → q < p
  | _, _ => True

Uses 3

Statement usesAction of a locked schedule · Lock mode · Operation of a schedule

DefinitionStrictness at a pair of positions#✓fully proved

For a locked schedule \(s\) and positions \(p\) and \(q\): if \(s\) has at position \(p\) a release by transaction \(t\) of item \(x\), just before position \(p\) transaction \(t\) holds an exclusive lock on \(x\), and \(s\) has at position \(q\) a read or write by \(t\), then \(q < p\). For every other pair of positions, including positions beyond the end of \(s\), the condition holds trivially.

def StrictAt (s : List (Action n X)) (p q : ℕ) : Prop :=
  match s[p]?, s[q]? with
  | some (.unlock t x), some (.op o) => o.txn = t → HoldsBefore s t x .exclusive p → q < p
  | _, _ => True

Uses 4

Statement usesAction of a locked schedule · Holding a lock · Lock mode · Operation of a schedule

DefinitionRelease test#✓fully proved

For a transaction \(t\), this Boolean test on the actions of a locked schedule returns true exactly when the action is a release by \(t\) of its lock on some item.

def Action.isUnlockBy (t : Fin n) : Action n X → Bool
  | .unlock t' _ => t' == t
  | _ => false

Uses 3 · Used by 1

Statement usesAction of a locked schedule · Lock mode · Operation of a schedule

Used byThe two-phase locking theorem

TheoremThe two-phase locking theorem#✓fully proved

If the reads and writes of a locked schedule are distinct, are covered by locks, and the schedule is legal and two-phase, then its reads and writes form a conflict-serializable schedule.

theorem TwoPhase.conflictSerializable {s : List (Action n X)}
    (hnd : (ops s).Nodup) (hwf : LocksCover s) (hl : Legal s) (h2 : TwoPhase s) :
    ConflictSerializable (ops s)

Uses 16 · Used by 1

Statement usesAction of a locked schedule · Conflict-serializable schedule · Legal locked schedule · Schedules covered by locks · Operation of a schedule · Two-phase schedules · Reads and writes of a locked schedule

Proof usesRead or write access · Lock mode required by an access · Release test · Holding a lock · Lock mode · Lock mode coverage · Conflicting operations · Edge of the precedence graph · A rank increasing along precedence edges gives conflict serializability

Used byStrict two-phase locking theorem

TheoremStrict two-phase locking theorem#✓fully proved

If the reads and writes of a locked schedule are distinct, are covered by locks, and the schedule is legal and strict two-phase, then its reads and writes form a conflict-serializable schedule.

theorem StrictTwoPhase.conflictSerializable {s : List (Action n X)}
    (hnd : (ops s).Nodup) (hwf : LocksCover s) (hl : Legal s) (h : StrictTwoPhase s) :
    ConflictSerializable (ops s)

Uses 11

Statement usesAction of a locked schedule · Conflict-serializable schedule · Legal locked schedule · Schedules covered by locks · Operation of a schedule · Strict two-phase schedules · Reads and writes of a locked schedule

Proof usesHolding a lock · Lock mode · Two-phase schedules · The two-phase locking theorem

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.