Deadlock detection
Deadlock Detection
StructureResource-allocation state#✓fully proved
For a type \(P\) of processes and a type \(R\) of resource types, a state consists of two functions \(\mathrm{alloc}, \mathrm{request} : P \to R \to \mathbb{N}\): \(\mathrm{alloc}(p)(r)\) is the number of instances of resource type \(r\) that process \(p\) holds, and \(\mathrm{request}(p)(r)\) is the number of instances of \(r\) that \(p\) is waiting for.
structure State (P R : Type*) where
/-- The resources each process holds. -/
alloc : P → R → ℕ
/-- The resources each process is waiting for. -/
request : P → R → ℕUsed by 11
State
DefinitionReduction sequences#✓fully proved
Let \(P\) be a type of processes and \(R\) a type of resource types, and let \(S\) be a state that gives each process \(p\) an allocation \(\mathrm{alloc}(p)\) and a request \(\mathrm{request}(p)\), both functions \(R \to \mathbb{N}\) ordered componentwise. A list of processes \(p_1, \dots, p_k\) is a reduction sequence of \(S\) from the free vector \(w : R \to \mathbb{N}\) when, for every \(1 \le i \le k\), we have \(\mathrm{request}(p_i) \le w + \mathrm{alloc}(p_1) + \dots + \mathrm{alloc}(p_{i-1})\). In particular the empty list is a reduction sequence from every \(w\).
Informally: starting with \(w\) free, each process in turn gets its request, finishes, and releases its allocation.
def Reduces : (R → ℕ) → List P → Prop
| _, [] => True
| work, p :: rest => S.request p ≤ work ∧ Reduces (work + S.alloc p) restUses 1 · Used by 6
TheoremLetting a process that fits finish first preserves reduction sequences#✓fully proved
Let \(w\) be a resource vector and \(p\) a process whose request is at most \(w\). If \(\sigma\) is a reduction sequence from \(w\), then the list obtained from \(\sigma\) by removing the first occurrence of \(p\), if any, is a reduction sequence from \(w\) plus the allocation of \(p\).
theorem Reduces.erase [DecidableEq P] {work : R → ℕ} {σ : List P} {p : P}
(h : S.Reduces work σ) (hfit : S.request p ≤ work) :
S.Reduces (work + S.alloc p) (σ.erase p)Uses 2 · Used by 1
TheoremA reduction sequence in which no process fits is empty#✓fully proved
Let \(w\) be a resource vector. If \(\sigma\) is a reduction sequence from \(w\) and no process of \(\sigma\) has a request at most \(w\), then \(\sigma\) is empty.
theorem Reduces.eq_nil {work : R → ℕ} {σ : List P} (h : S.Reduces work σ)
(hstuck : ∀ q ∈ σ, ¬ S.request q ≤ work) : σ = []Uses 2 · Used by 1
DefinitionThe detection algorithm with fuel#✓fully proved
Given the fuel, a number of steps, together with the free resource vector \(w\) and a list of pending processes, the algorithm returns two lists: the processes that finished, in order, and the processes left over. With fuel \(0\), or when no pending process has a request at most \(w\), no process finishes and all the pending processes are left over. Otherwise the fuel is \(n + 1\) for some \(n\); take the first pending process \(p\) whose request is at most \(w\) and run the algorithm with fuel \(n\), free vector \(w\) plus the allocation of \(p\), and the list with that entry of \(p\) removed. The result is \(p\) followed by the processes that finished there, together with the processes left over there.
def reduceAux : ℕ → (R → ℕ) → List P → List P × List P
| 0, _, pending => ([], pending)
| fuel + 1, work, pending =>
match pending.find? (fun p => decide (S.request p ≤ work)) with
| none => ([], pending)
| some p =>
let r := reduceAux fuel (work + S.alloc p) (pending.erase p)
(p :: r.1, r.2)Uses 1 · Used by 7
DefinitionThe processes the detection algorithm lets finish#✓fully proved
Given the free resource vector \(w\) and a list of pending processes, run the detection algorithm: repeatedly take the first pending process whose request is at most what is free, let it finish, remove that entry from the list and add its allocation to what is free, until no pending process has a request at most what is free. This is the list of the processes taken, in the order they were taken.
def finished (work : R → ℕ) (pending : List P) : List P :=
(S.reduceAux pending.length work pending).1Uses 2 · Used by 4
DefinitionThe detection algorithm#✓fully proved
Given the free resource vector \(w\) and a list of pending processes, repeatedly take the first pending process whose request is at most what is free, let it finish, remove that entry from the list and add its allocation to what is free, until no pending process has a request at most what is free. The processes still pending then are the ones reported as deadlocked.
def detect (work : R → ℕ) (pending : List P) : List P :=
(S.reduceAux pending.length work pending).2Uses 2 · Used by 3
TheoremThe algorithm with fuel leaves over no process of a reduction sequence#✓fully proved
Let \(w\) be the free resource vector, let the list of pending processes contain no duplicates, and let the fuel be at least the number of pending processes. If \(\sigma\) is a duplicate-free reduction sequence from \(w\) all of whose processes are pending, then no process of \(\sigma\) is among the processes that the detection algorithm with that fuel leaves over.
theorem reduceAux_disjoint (fuel : ℕ) (work : R → ℕ) (pending : List P)
(hlen : pending.length ≤ fuel) (hnd : pending.Nodup) {σ : List P}
(hσ : S.Reduces work σ) (hσnd : σ.Nodup) (hsub : σ ⊆ pending) :
∀ x ∈ σ, x ∉ (S.reduceAux fuel work pending).2Uses 5 · Used by 1
TheoremEvery reported process is stuck#✓fully proved
Let \(w\) be the free resource vector. For every process \(q\) that the detection algorithm reports, the request of \(q\) is not at most \(w\) plus the sum of the allocations of the processes that the algorithm lets finish: for at least one resource type, \(q\) requests more than is free even after all those processes have released their allocations.
theorem detect_stuck (work : R → ℕ) (pending : List P) :
∀ q ∈ S.detect work pending,
¬ S.request q ≤ work + ((S.finished work pending).map S.alloc).sumUses 4
TheoremThe processes the algorithm lets finish form a reduction sequence#✓fully proved
For every free resource vector \(w\) and every list of pending processes, the processes that the detection algorithm lets finish, in the order it lets them finish, form a reduction sequence from \(w\).
theorem finished_reduces (work : R → ℕ) (pending : List P) :
S.Reduces work (S.finished work pending)Uses 4 · Used by 2
TheoremCorrectness of deadlock detection#✓fully proved
Let \(w\) be the free resource vector and let the list of pending processes contain no duplicates. A process \(p\) is reported by the detection algorithm if and only if \(p\) is pending and no duplicate-free reduction sequence \(\sigma\) from \(w\) made of pending processes contains \(p\).
theorem mem_detect_iff {work : R → ℕ} {pending : List P} (hnd : pending.Nodup) {p : P} :
p ∈ S.detect work pending ↔
p ∈ pending ∧ ¬ ∃ σ, S.Reduces work σ ∧ σ.Nodup ∧ σ ⊆ pending ∧ p ∈ σUses 7 · Used by 1
TheoremNo deadlock is reported exactly when all the processes can finish#✓fully proved
Let \(w\) be the free resource vector and let the list of pending processes contain no duplicates. The detection algorithm, started with \(w\) free, reports no process if and only if some reordering of the pending processes is a reduction sequence from \(w\).
theorem detect_eq_nil_iff {work : R → ℕ} {pending : List P} (hnd : pending.Nodup) :
S.detect work pending = [] ↔ ∃ σ, σ.Perm pending ∧ S.Reduces work σLoading dependency explorer…
The dependency explorer needs JavaScript and its graph data.