Deadlock and circular wait
Deadlock
StructureResource-allocation snapshot#✓fully proved
A resource-allocation snapshot, for a type \(P\) of processes and a type \(R\) of resources, records for each resource the process holding it, if any (so each resource has at most one holder), and for each process \(p\) and resource \(r\) whether \(p\) has an outstanding request for \(r\). A process never requests a resource it holds.
structure AllocState (P Res : Type*) where
/-- The process holding each resource, if any. -/
holder : Res → Option P
/-- Outstanding requests. -/
requests : P → Res → Prop
/-- A process does not request a resource it holds. -/
requests_not_held : ∀ p r, requests p r → holder r ≠ some p requests : P → Res → PropCSLibExt/Algorithms/Concurrency/Deadlock.lean:63
holder : Res → Option PCSLibExt/Algorithms/Concurrency/Deadlock.lean:61
Used by 11
Alloc State
DefinitionWait-for relation#✓fully proved
In a resource-allocation snapshot \(s\), a process \(p\) waits for a process \(q\) when there is a resource \(r\) that \(p\) requests in \(s\) and that \(q\) holds in \(s\).
def WaitsFor (p q : P) : Prop := ∃ r, s.requests p r ∧ s.holder r = some qUses 1 · Used by 7
DefinitionDeadlocked set of processes#✓fully proved
In a resource-allocation snapshot \(s\), a set \(D\) of processes is deadlocked when \(D\) is nonempty and every process \(p \in D\) waits in \(s\) for some process \(q \in D\), that is, \(p\) requests in \(s\) a resource that \(q\) holds in \(s\).
def Deadlocked (D : Set P) : Prop := D.Nonempty ∧ ∀ p ∈ D, ∃ q ∈ D, s.WaitsFor p qUses 2 · Used by 4
DefinitionCircular wait#✓fully proved
A resource-allocation snapshot \(s\) has circular wait when some process \(p\) waits for itself through a chain of one or more wait-for edges in \(s\), that is, there are processes \(p = p_0, p_1, \dots, p_k = p\) with \(k \ge 1\) such that \(p_{i-1}\) waits for \(p_i\) in \(s\) for each \(1 \le i \le k\).
def CircularWait : Prop := ∃ p, Relation.TransGen s.WaitsFor p pUses 2 · Used by 4
TheoremNo process waits for itself directly#✓fully proved
In a resource-allocation snapshot, no process \(p\) waits for itself, that is, there is no resource that \(p\) both requests and holds.
theorem not_waitsFor_self (p : P) : ¬ s.WaitsFor p pUses 2
TheoremA process whose requests are all free waits for no one#✓fully proved
In a resource-allocation snapshot, if no resource requested by a process \(p\) has a holder, then \(p\) waits for no process \(q\).
theorem not_waitsFor_of_free {p q : P} (hfree : ∀ r, s.requests p r → s.holder r = none) :
¬ s.WaitsFor p qUses 2
TheoremCircular wait yields a deadlocked set#✓fully proved
If a resource-allocation snapshot has circular wait, that is, some process \(p\) waits for itself through a chain of one or more wait-for edges, then some set of processes is deadlocked.
One such set consists of the processes on a wait-for cycle through \(p\).
theorem exists_deadlocked_of_circularWait (h : s.CircularWait) : ∃ D, s.Deadlocked DUses 4 · Used by 1
TheoremA deadlocked set forces circular wait#✓fully proved
In a resource-allocation snapshot with finitely many processes, if some set of processes is deadlocked, then the snapshot has circular wait: some process waits for itself through a chain of one or more wait-for edges.
The proof follows wait-for edges inside the deadlocked set; by finiteness it must revisit a process.
Uses 4 · Used by 2
TheoremDeadlock is circular wait#✓fully proved
In a resource-allocation snapshot with finitely many processes, some set of processes is deadlocked if and only if the snapshot has circular wait, that is, some process waits for itself through a chain of one or more wait-for edges.
theorem deadlock_iff_circularWait [Finite P] : (∃ D, s.Deadlocked D) ↔ s.CircularWaitUses 5
DefinitionHavender's resource ordering#✓fully proved
Let \(s\) be a resource-allocation snapshot and let \(\mathrm{rank}\) assign a natural number to each resource. The snapshot \(s\) is ordered by \(\mathrm{rank}\) when, for every process \(p\), every resource \(r\) that \(p\) requests in \(s\) and every resource \(r'\) that \(p\) holds in \(s\), we have \(\mathrm{rank}(r') < \mathrm{rank}(r)\): each process requests only resources ranked strictly above every resource it holds.
def Ordered (rank : Res → ℕ) : Prop :=
∀ p r r', s.requests p r → s.holder r' = some p → rank r' < rank rUses 1 · Used by 2
TheoremResource ordering prevents circular wait#✓fully proved
Let \(\mathrm{rank}\) assign a natural number to each resource. If a resource-allocation snapshot is ordered by \(\mathrm{rank}\) (Havender's discipline), that is, \(\mathrm{rank}(r') < \mathrm{rank}(r)\) whenever some process requests \(r\) and holds \(r'\), then the snapshot has no circular wait: no process waits for itself through a chain of one or more wait-for edges.
theorem not_circularWait_of_ordered {rank : Res → ℕ} (hord : s.Ordered rank) :
¬ s.CircularWaitUses 4 · Used by 1
TheoremResource ordering prevents deadlock#✓fully proved
Let \(\mathrm{rank}\) assign a natural number to each resource. If a resource-allocation snapshot with finitely many processes is ordered by \(\mathrm{rank}\) (Havender's discipline), that is, \(\mathrm{rank}(r') < \mathrm{rank}(r)\) whenever some process requests \(r\) and holds \(r'\), then no set of processes is deadlocked.
theorem not_deadlocked_of_ordered [Finite P] {rank : Res → ℕ} (hord : s.Ordered rank)
(D : Set P) : ¬ s.Deadlocked DUses 5
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.