Conflict serializability

16 fully proved

Databases

InductiveRead or write access#✓fully proved

The kind of access an operation makes to its data item is one of two values: a read or a write.

inductive Access
  /-- A read. -/
  | read
  /-- A write. -/
  | write
deriving DecidableEq

Used by 10

Used bySerializing along a topological order preserves conflict equivalence · A rank increasing along precedence edges gives conflict serializability · Conflicting operations · A conflict-serializable schedule has an acyclic precedence graph · Operation of a schedule · Precedence graph · The two-phase locking theorem · Schedules covered by locks · Lock coverage at a position · Lock mode required by an access

StructureOperation of a schedule#✓fully proved

For \(n\) transactions, numbered \(0, \dots, n - 1\), and data items of type \(X\), an operation consists of a transaction \(t \in \{0, \dots, n - 1\}\), an occurrence identifier \(k \in \mathbb{N}\), an access, which is a read or a write, and a data item \(x \in X\): transaction \(t\) reads or writes \(x\), and \(k\) makes repeated accesses of \(t\) to an item distinct operations.

structure Op (n : ℕ) (X : Type*) where
  /-- The transaction performing the operation. -/
  txn : Fin n
  /-- An identifier of the occurrence (for instance its position in the transaction), which makes
  repeated accesses of a transaction to an item distinct operations. -/
  step : ℕ
  /-- Read or write. -/
  access : Access
  /-- The data item accessed. -/
  item : X
deriving DecidableEq

Uses 1 · Used by 26

Statement usesRead or write access

Used byConflict equivalence · Serializing along a topological order preserves conflict equivalence · Conflict-serializable schedule · The serializability theorem · A rank increasing along precedence edges gives conflict serializability · Conflicting operations · A conflict-serializable schedule has an acyclic precedence graph · Serial schedule · Serializing along a complete transaction order gives a serial schedule · Operations whose relative order matters · Edge of the precedence graph · Precedence graph · Serialization of a schedule along a transaction order · One transaction before another in a schedule · Action of a locked schedule · The two-phase locking theorem · Strict two-phase locking theorem · Release test · 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 · Strictness at a pair of positions · Strict two-phase schedules · Two-phase condition at a pair of positions

Conflicting operations

DefinitionConflicting operations#✓fully proved

Two operations of a schedule conflict when they belong to different transactions, access the same data item, and at least one of the two accesses is a write.

def Conflicts (a b : Op n X) : Prop :=
  a.txn ≠ b.txn ∧ a.item = b.item ∧ (a.access = .write ∨ b.access = .write)

Uses 2 · Used by 7

Statement usesRead or write access · Operation of a schedule

Used bySerializing along a topological order preserves conflict equivalence · A rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · Operations whose relative order matters · Edge of the precedence graph · Precedence graph · The two-phase locking theorem

DefinitionOperations whose relative order matters#✓fully proved

Two operations \(a\) and \(b\) are order-relevant when they belong to the same transaction or they conflict. These are the pairs whose relative order a conflict-equivalent schedule must keep.

def OrderMatters (a b : Op n X) : Prop := a.txn = b.txn ∨ a.Conflicts b

Uses 2 · Used by 3

Statement usesOperation of a schedule · Conflicting operations

Used byConflict equivalence · Serializing along a topological order preserves conflict equivalence · A conflict-serializable schedule has an acyclic precedence graph

Databases

DefinitionConflict equivalence#✓fully proved

A schedule \(s'\) is conflict-equivalent to a schedule \(s\) when \(s'\) is a permutation of \(s\) and, for any two operations \(a\) and \(b\) that belong to the same transaction or conflict, an occurrence of \(a\) comes before an occurrence of \(b\) in \(s\) if and only if the same holds in \(s'\).

def ConflictEquiv (s s' : List (Op n X)) : Prop :=
  s.Perm s' ∧ ∀ a b, a.OrderMatters b → ([a, b] <+ s ↔ [a, b] <+ s')

Uses 2 · Used by 4

Statement usesOperation of a schedule · Operations whose relative order matters

Used bySerializing along a topological order preserves conflict equivalence · Conflict-serializable schedule · The serializability theorem · A conflict-serializable schedule has an acyclic precedence graph

DefinitionOne transaction before another in a schedule#✓fully proved

For a schedule \(s\) and transactions \(i\) and \(j\), transaction \(i\) precedes transaction \(j\) in \(s\) when every operation of \(i\) in \(s\) occurs in \(s\) before every operation of \(j\) in \(s\).

def TxnBefore (s : List (Op n X)) (i j : Fin n) : Prop :=
  ∀ a ∈ s, ∀ b ∈ s, a.txn = i → b.txn = j → [a, b] <+ s

Uses 1 · Used by 3

Statement usesOperation of a schedule

Used byA conflict-serializable schedule has an acyclic precedence graph · Serial schedule · Serializing along a complete transaction order gives a serial schedule

DefinitionSerial schedule#✓fully proved

A schedule \(s\) is serial when, for any two distinct transactions \(i\) and \(j\), either every operation of \(i\) in \(s\) occurs before every operation of \(j\) in \(s\), or every operation of \(j\) in \(s\) occurs before every operation of \(i\) in \(s\).

def IsSerial (s : List (Op n X)) : Prop := ∀ i j, i ≠ j → TxnBefore s i j ∨ TxnBefore s j i

Uses 2 · Used by 4

Statement usesOperation of a schedule · One transaction before another in a schedule

Used byConflict-serializable schedule · The serializability theorem · A conflict-serializable schedule has an acyclic precedence graph · Serializing along a complete transaction order gives a serial schedule

DefinitionConflict-serializable schedule#✓fully proved

A schedule \(s\) is conflict-serializable when some serial schedule is conflict-equivalent to \(s\).

def ConflictSerializable (s : List (Op n X)) : Prop := ∃ s', IsSerial s' ∧ ConflictEquiv s s'

Uses 3 · Used by 5

Statement usesConflict equivalence · Serial schedule · Operation of a schedule

Used byThe serializability theorem · A rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · The two-phase locking theorem · Strict two-phase locking theorem

DefinitionEdge of the precedence graph#✓fully proved

For a schedule \(s\) and transactions \(i\) and \(j\), there is a precedence edge from \(i\) to \(j\) in \(s\) when some operation of \(i\) occurs in \(s\) before some operation of \(j\) in \(s\) that conflicts with it.

def PrecedenceEdge (s : List (Op n X)) (i j : Fin n) : Prop :=
  ∃ a ∈ s, ∃ b ∈ s, a.txn = i ∧ b.txn = j ∧ a.Conflicts b ∧ [a, b] <+ s

Uses 2 · Used by 5

Statement usesOperation of a schedule · Conflicting operations

Used bySerializing along a topological order preserves conflict equivalence · A rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · Precedence graph · The two-phase locking theorem

DefinitionPrecedence graph#✓fully proved

The precedence (serialization) graph of a schedule \(s\) of \(n\) transactions is the directed adjacency graph whose vertices are the transactions \(0, \dots, n - 1\), listed in increasing order, and whose adjacency list at a transaction \(i\) lists, in increasing order, the transactions \(j\) such that there is a precedence edge from \(i\) to \(j\) in \(s\).

def precedenceGraph (s : List (Op n X)) : DirectedAdjacency (Fin n) where
  vertices := List.finRange n
  vertices_nodup := List.nodup_finRange n
  vertices_complete := List.mem_finRange
  adjacency i := (List.finRange n).filter fun j => decide (PrecedenceEdge s i j)

Uses 5 · Used by 4

Statement usesDirected adjacency graph · Read or write access · Operation of a schedule · Conflicting operations · Edge of the precedence graph

Used bySerializing along a topological order preserves conflict equivalence · The serializability theorem · A rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph

DefinitionSerialization of a schedule along a transaction order#✓fully proved

For a list \(\sigma\) of transactions and a schedule \(s\), the serialization of \(s\) along \(\sigma\) sorts the operations of \(s\) by the position of the first occurrence of their transaction in \(\sigma\), where a transaction that does not occur in \(\sigma\) gets the length of \(\sigma\) as its position. The sort is stable: operations with the same position keep their relative order in \(s\).

def serialize (order : List (Fin n)) (s : List (Op n X)) : List (Op n X) :=
  s.insertionSort fun a b => order.idxOf a.txn ≤ order.idxOf b.txn

Uses 1 · Used by 3

Statement usesOperation of a schedule

Used bySerializing along a topological order preserves conflict equivalence · The serializability theorem · Serializing along a complete transaction order gives a serial schedule

TheoremA conflict-serializable schedule has an acyclic precedence graph#✓fully proved

If a schedule \(s\) in which no operation occurs twice is conflict-serializable, then the precedence graph of \(s\) is acyclic.

In a conflict-equivalent serial schedule, the position of the first operation of each transaction increases along every edge of the precedence graph.

theorem ConflictSerializable.isAcyclic {s : List (Op n X)} (hs : s.Nodup)
    (h : ConflictSerializable s) : TopologicalSort.IsAcyclic (precedenceGraph s)

Uses 15 · Used by 1

Statement usesAcyclic directed graph · Conflict-serializable schedule · Operation of a schedule · Precedence graph

Proof usesDirected adjacency graph · Edge of a directed adjacency graph · Directed cycle within a vertex list · Characterization of directed cycles within a vertex list · Read or write access · Conflict equivalence · Serial schedule · Conflicting operations · Operations whose relative order matters · Edge of the precedence graph · One transaction before another in a schedule

Used byThe serializability theorem

TheoremSerializing along a complete transaction order gives a serial schedule#✓fully proved

Let \(s\) be a schedule and \(L\) a list in which every transaction occurs. Then the schedule obtained from \(s\) by stably sorting its operations by the first position of their transaction in \(L\) is serial.

theorem isSerial_serialize (s : List (Op n X)) {order : List (Fin n)}
    (hocomp : ∀ i, i ∈ order) : IsSerial (serialize order s)

Uses 4 · Used by 1

Statement usesSerial schedule · Operation of a schedule · Serialization of a schedule along a transaction order

Proof usesOne transaction before another in a schedule

Used byThe serializability theorem

TheoremSerializing along a topological order preserves conflict equivalence#✓fully proved

Let \(s\) be a schedule in which no operation occurs twice, and let \(L\) be a topological order of the precedence graph of \(s\). Then the schedule obtained from \(s\) by stably sorting its operations by the first position of their transaction in \(L\) is conflict-equivalent to \(s\).

theorem conflictEquiv_serialize {s : List (Op n X)} (hs : s.Nodup) {order : List (Fin n)}
    (horder : TopologicalSort.IsTopologicalOrder (precedenceGraph s) order) :
    ConflictEquiv s (serialize order s)

Uses 11 · Used by 1

Statement usesTopological order · Conflict equivalence · Operation of a schedule · Precedence graph · Serialization of a schedule along a transaction order

Proof usesDirected adjacency graph · Edge of a directed adjacency graph · Read or write access · Conflicting operations · Operations whose relative order matters · Edge of the precedence graph

Used byThe serializability theorem

TheoremThe serializability theorem#✓fully proved

A schedule without duplicate operations is conflict-serializable exactly when its precedence graph is acyclic.

theorem conflictSerializable_iff_isAcyclic {s : List (Op n X)} (hs : s.Nodup) :
    ConflictSerializable s ↔ TopologicalSort.IsAcyclic (precedenceGraph s)

Uses 17 · Used by 1

Statement usesAcyclic directed graph · Conflict-serializable schedule · Operation of a schedule · Precedence graph

Proof usesDirected adjacency graph · Edge of a directed adjacency graph · Topological order · Outcome of Kahn's topological sort · Kahn's algorithm succeeds on acyclic graphs · Kahn's topological sort · A successful topological sort is a topological order · Conflict equivalence · A conflict-serializable schedule has an acyclic precedence graph · Serial schedule · Serializing along a topological order preserves conflict equivalence · Serializing along a complete transaction order gives a serial schedule · Serialization of a schedule along a transaction order

Used byA rank increasing along precedence edges gives conflict serializability

TheoremA rank increasing along precedence edges gives conflict serializability#✓fully proved

Let \(s\) be a schedule in which no operation occurs twice. If \(r\) is a function from the transactions to the natural numbers with \(r(i) < r(j)\) whenever the precedence graph of \(s\) has an edge from \(i\) to \(j\), then \(s\) is conflict-serializable.

theorem conflictSerializable_of_rank {s : List (Op n X)} (hs : s.Nodup) (rank : Fin n → ℕ)
    (h : ∀ i j, PrecedenceEdge s i j → rank i < rank j) : ConflictSerializable s

Uses 12 · Used by 1

Statement usesConflict-serializable schedule · Operation of a schedule · Edge of the precedence graph

Proof usesDirected adjacency graph · Edge of a directed adjacency graph · Directed cycle within a vertex list · Acyclic directed graph · Characterization of directed cycles within a vertex list · Read or write access · Conflicting operations · The serializability theorem · Precedence graph

Used byThe two-phase locking theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.