Skip to content

Banker's algorithm

16 fully proved

Banker

StructureClaims and allocations of processes#✓fully proved

A system with processes \(P\) and resource types \(R\) consists of two maps \(\mathrm{claim}, \mathrm{alloc} : P \to (R \to \mathbb{N})\), where \(\mathrm{claim}(p)\) is the maximum demand of process \(p\) for each resource type and \(\mathrm{alloc}(p)\) is the amount of each resource type currently allocated to \(p\). No inequality between the two is required.

@[ext]
structure System (P R : Type*) where
  /-- The maximum demand of each process. -/
  claim : P → R → ℕ
  /-- The resources currently allocated to each process. -/
  alloc : P → R → ℕ
Used by 15
Used byRemoving a process from a safe sequence · A safe state is not deadlocked · Granting a request · Safe sequences are monotone in the free resources · Remaining need · Remaining need after a grant · Resource-request algorithm · The request algorithm grants exactly the safe requests within the claim and the free resources · Granted requests lead to safe states · Safe state · Letting a process that fits finish preserves safety · Safe sequence · Banker's safety algorithm · Banker's safety algorithm with fuel · Correctness of the safety algorithm

System

DefinitionRemaining need#✓fully proved

The remaining need of a process \(p\) in a system \(S\) is the resource vector \(\mathrm{claim}(p) - \mathrm{alloc}(p)\): the maximum claim of \(p\) minus its current allocation, computed for each resource type by truncated subtraction of natural numbers, so it is \(0\) for every resource type where the allocation exceeds the claim.

def need (p : P) : R → ℕ := S.claim p - S.alloc p
Uses 1 · Used by 11
Statement usesClaims and allocations of processes
Used byRemoving a process from a safe sequence · A safe state is not deadlocked · Safe sequences are monotone in the free resources · Remaining need after a grant · Resource-request algorithm · The request algorithm grants exactly the safe requests within the claim and the free resources · Granted requests lead to safe states · Letting a process that fits finish preserves safety · Safe sequence · Banker's safety algorithm with fuel · Correctness of the safety algorithm

DefinitionSafe sequence#✓fully proved

Let \(S\) be a system with processes \(P\) and resource types \(R\), where process \(p\) has maximum claim \(\mathrm{claim}(p)\) and allocation \(\mathrm{alloc}(p)\) in \(R \to \mathbb{N}\). A list \(p_1, \dots, p_k\) of processes is a safe sequence from the free resource vector \(w : R \to \mathbb{N}\) when, for each \(i\), the remaining need \(\mathrm{claim}(p_i) - \mathrm{alloc}(p_i)\) (truncated at zero) is at most \(w + \mathrm{alloc}(p_1) + \cdots + \mathrm{alloc}(p_{i-1})\) componentwise. In particular the empty list is a safe sequence from every \(w\).

Thus each process in turn can be given its remaining need from what is free, finish, and release its allocation.

def SafeSeq : (R → ℕ) → List P → Prop
  | _, [] => True
  | work, p :: rest => S.need p ≤ work ∧ SafeSeq (work + S.alloc p) rest
Uses 2 · Used by 6
Statement usesClaims and allocations of processes · Remaining need
Used byRemoving a process from a safe sequence · A safe state is not deadlocked · Safe sequences are monotone in the free resources · Safe state · Letting a process that fits finish preserves safety · Correctness of the safety algorithm

DefinitionSafe state#✓fully proved

Let \(S\) be a system of claims and allocations with processes \(P\) and resource types \(R\). A list of pending processes is safe from the free resource vector \(w : R \to \mathbb{N}\) when it has no repetitions and some permutation of it is a safe sequence from \(w\): the pending processes can all finish, one after another, in some order.

def Safe (work : R → ℕ) (pending : List P) : Prop :=
  pending.Nodup ∧ ∃ σ, σ.Perm pending ∧ S.SafeSeq work σ
Uses 2 · Used by 5
Statement usesClaims and allocations of processes · Safe sequence
Used byA safe state is not deadlocked · The request algorithm grants exactly the safe requests within the claim and the free resources · Granted requests lead to safe states · Letting a process that fits finish preserves safety · Correctness of the safety algorithm

TheoremSafe sequences are monotone in the free resources#✓fully proved

Let \(S\) be a system of processes with maximum claims and current allocations, and let \(\sigma\) be a list of processes. If \(\sigma\) is a safe sequence for \(S\) from a vector \(w\) of free resources (a natural number for each resource type), and \(w \le w'\) componentwise, then \(\sigma\) is also a safe sequence for \(S\) from \(w'\).

theorem SafeSeq.mono {work work' : R → ℕ} (hle : work ≤ work') {σ : List P}
    (h : S.SafeSeq work σ) : S.SafeSeq work' σ
Uses 3
Statement usesClaims and allocations of processes · Safe sequence
Proof usesRemaining need

TheoremRemoving a process from a safe sequence#✓fully proved

Let \(S\) be a system of processes with maximum claims and current allocations, let \(w\) be a vector of free resources (a natural number for each resource type), and let \(\sigma\) be a list of processes that is a safe sequence for \(S\) from \(w\). If \(p\) occurs in \(\sigma\), then the list obtained from \(\sigma\) by deleting the first occurrence of \(p\) is a safe sequence for \(S\) from \(w + \mathrm{alloc}(p)\), where \(\mathrm{alloc}(p)\) is the current allocation of \(p\) and the sum is taken componentwise.

In other words, letting a member of a safe sequence finish first and release its allocation leaves the rest of the sequence safe. This is why the greedy safety check is complete.

theorem SafeSeq.erase {work : R → ℕ} {σ : List P} {p : P} (h : S.SafeSeq work σ)
    (hp : p ∈ σ) : S.SafeSeq (work + S.alloc p) (σ.erase p)
Uses 3 · Used by 1
Statement usesClaims and allocations of processes · Safe sequence
Proof usesRemaining need
Used byLetting a process that fits finish preserves safety

TheoremA safe state is not deadlocked#✓fully proved

Let \(S\) be a system of processes with maximum claims and current allocations, let \(w\) be a vector of free resources (a natural number for each resource type), and let \(L\) be a nonempty list of pending processes. If \(S\) is safe from \(w\) for \(L\), then some process \(p\) in \(L\) has remaining need \(\mathrm{need}(p) \le w\) componentwise, so it can be given its whole remaining need.

theorem Safe.exists_runnable {work : R → ℕ} {pending : List P} (h : S.Safe work pending)
    (hne : pending ≠ []) : ∃ p ∈ pending, S.need p ≤ work
Uses 4 · Used by 1
Statement usesClaims and allocations of processes · Safe state · Remaining need
Proof usesSafe sequence
Used byCorrectness of the safety algorithm

TheoremLetting a process that fits finish preserves safety#✓fully proved

Let \(S\) be a system of processes with maximum claims and current allocations, \(w\) a vector of free resources (a natural number for each resource type) and \(L\) a list of pending processes without repetitions. If \(p\) occurs in \(L\) and its remaining need \(\mathrm{need}(p)\) in \(S\) satisfies \(\mathrm{need}(p) \le w\) componentwise, then \(S\) is safe from \(w\) for \(L\) if and only if \(S\) is safe from \(w + \mathrm{alloc}(p)\) for the list obtained from \(L\) by removing \(p\), where \(\mathrm{alloc}(p)\) is the current allocation of \(p\) and the sum is taken componentwise.

theorem safe_iff_safe_erase {work : R → ℕ} {pending : List P} {p : P} (hnd : pending.Nodup)
    (hp : p ∈ pending) (hfit : S.need p ≤ work) :
    S.Safe work pending ↔ S.Safe (work + S.alloc p) (pending.erase p)
Uses 5 · Used by 1
Statement usesClaims and allocations of processes · Safe state · Remaining need
Proof usesSafe sequence · Removing a process from a safe sequence
Used byCorrectness of the safety algorithm

DefinitionBanker's safety algorithm with fuel#✓fully proved

Let \(S\) be a system with processes \(P\) and a finite set \(R\) of resource types, where process \(p\) has maximum claim \(\mathrm{claim}(p)\) and allocation \(\mathrm{alloc}(p)\) in \(R \to \mathbb{N}\). Given a fuel \(n \in \mathbb{N}\), a free resource vector \(w : R \to \mathbb{N}\) and a list of pending processes, the algorithm succeeds if the list is empty. Otherwise, if \(n > 0\) and some pending process \(q\) has remaining need \(\mathrm{claim}(q) - \mathrm{alloc}(q)\) (truncated at zero) at most \(w\) componentwise, it takes the first such process \(p\) in the list, removes that occurrence of \(p\) from the list, adds \(\mathrm{alloc}(p)\) to \(w\) and continues with fuel \(n - 1\); if \(n = 0\) or no pending process fits, it fails.

def safetyCheckAux : ℕ → (R → ℕ) → List P → Bool
  | 0, _, pending => pending.isEmpty
  | fuel + 1, work, pending =>
      match pending.find? (fun p => decide (S.need p ≤ work)) with
      | none => pending.isEmpty
      | some p => safetyCheckAux fuel (work + S.alloc p) (pending.erase p)
Uses 2 · Used by 2
Statement usesClaims and allocations of processes · Remaining need
Used byBanker's safety algorithm · Correctness of the safety algorithm

DefinitionBanker's safety algorithm#✓fully proved

Let \(S\) be a system of claims and allocations with processes \(P\) and a finite set \(R\) of resource types. Given a free resource vector \(w : R \to \mathbb{N}\) and a list of pending processes, the algorithm fails if the list has a repetition. Otherwise it runs the safety algorithm with fuel equal to the length of the list: it repeatedly lets the first pending process whose remaining need (claim minus allocation, truncated at zero) is at most the free resources componentwise finish and adds its allocation to the free resources, for at most one round per pending process, and it succeeds exactly when no pending process is left at the end.

def safetyCheck (work : R → ℕ) (pending : List P) : Bool :=
  decide pending.Nodup && S.safetyCheckAux pending.length work pending
Uses 2 · Used by 3
Statement usesClaims and allocations of processes · Banker's safety algorithm with fuel
Used byResource-request algorithm · The request algorithm grants exactly the safe requests within the claim and the free resources · Correctness of the safety algorithm

TheoremCorrectness of the safety algorithm#✓fully proved

For every system \(S\) of claims and allocations over a finite set \(R\) of resource types, every free resource vector \(w : R \to \mathbb{N}\) and every list of pending processes, the banker's safety algorithm succeeds on \(w\) and the list if and only if the list is a safe state from \(w\).

theorem safetyCheck_iff (work : R → ℕ) (pending : List P) :
    S.safetyCheck work pending = true ↔ S.Safe work pending
Uses 8 · Used by 1
Statement usesClaims and allocations of processes · Safe state · Banker's safety algorithm
Proof usesA safe state is not deadlocked · Safe sequence · Remaining need · Letting a process that fits finish preserves safety · Banker's safety algorithm with fuel
Used byThe request algorithm grants exactly the safe requests within the claim and the free resources

DefinitionGranting a request#✓fully proved

For a system \(S\) of processes with maximum claims and current allocations, a process \(p\) and a resource vector \(r\) (a natural number for each resource type), the system obtained by granting \(r\) to \(p\) has the same maximum claims as \(S\), gives \(p\) the allocation \(\mathrm{alloc}(p) + r\) (componentwise sum, where \(\mathrm{alloc}(p)\) is the current allocation of \(p\) in \(S\)), and leaves the allocation of every other process unchanged.

def grant (S : System P R) (p : P) (req : R → ℕ) : System P R :=
  ⟨S.claim, Function.update S.alloc p (S.alloc p + req)⟩
Uses 1 · Used by 4
Statement usesClaims and allocations of processes
Used byRemaining need after a grant · Resource-request algorithm · The request algorithm grants exactly the safe requests within the claim and the free resources · Granted requests lead to safe states

TheoremRemaining need after a grant#✓fully proved

For a system \(S\) of processes with maximum claims and current allocations, a process \(p\) and a resource vector \(r\) (a natural number for each resource type), the remaining need of \(p\) in the system obtained by granting \(r\) to \(p\) equals \(\mathrm{need}(p) - r\), where \(\mathrm{need}(p)\) is the remaining need of \(p\) in \(S\) and the subtraction is truncated subtraction of natural numbers, taken componentwise.

@[simp] theorem need_grant_self (S : System P R) (p : P) (req : R → ℕ) :
    (S.grant p req).need p = S.need p - req
Uses 3
Statement usesClaims and allocations of processes · Granting a request · Remaining need

DefinitionResource-request algorithm#✓fully proved

Let \(S\) be a system of claims and allocations with processes \(P\) and a finite set \(R\) of resource types, let \(a : R \to \mathbb{N}\) be the vector of free resources, \(L\) a list of pending processes, \(p\) a process and \(r : R \to \mathbb{N}\) the resources that \(p\) requests. The request is granted when \(p\) occurs in \(L\), \(L\) has no repetitions, \(r \le \mathrm{need}(p)\) and \(r \le a\) componentwise, where \(\mathrm{need}(p)\) is the remaining need of \(p\) in \(S\), and the banker's safety algorithm succeeds for the system obtained from \(S\) by granting \(r\) to \(p\), from the free vector \(a - r\) (componentwise truncated subtraction) and the list \(L\). A granted request returns the free vector \(a - r\) and that system; otherwise the algorithm returns no result.

No result covers the error case of the textbook algorithm (a request beyond the remaining claim), the cases where the process must wait, and malformed input (a requester that is not pending, or a pending list with repetitions).

def request (S : System P R) (available : R → ℕ) (pending : List P) (p : P)
    (req : R → ℕ) : Option ((R → ℕ) × System P R) :=
  if p ∈ pending ∧ pending.Nodup ∧ req ≤ S.need p ∧ req ≤ available ∧
      (S.grant p req).safetyCheck (available - req) pending
  then some (available - req, S.grant p req)
  else none
Uses 4 · Used by 2
Statement usesClaims and allocations of processes · Granting a request · Remaining need · Banker's safety algorithm
Used byThe request algorithm grants exactly the safe requests within the claim and the free resources · Granted requests lead to safe states

TheoremThe request algorithm grants exactly the safe requests within the claim and the free resources#✓fully proved

The request algorithm grants exactly the safe requests within the claim and the free resources. Let \(S\) be a system of claims and allocations with processes \(P\) and a finite set \(R\) of resource types, let \(a : R \to \mathbb{N}\) be the vector of free resources, \(L\) a list of pending processes, \(p\) a process and \(r : R \to \mathbb{N}\) the resources that \(p\) requests. Write \(\mathrm{need}(p)\) for the remaining need of \(p\) in \(S\), \(T\) for the system obtained from \(S\) by granting \(r\) to \(p\), and \(a - r\) for componentwise truncated subtraction. The resource-request algorithm grants the request and returns the free vector \(a'\) and the system \(S'\) if and only if \(p\) occurs in \(L\), \(L\) has no repetitions, both \(r \le \mathrm{need}(p)\) and \(r \le a\) hold componentwise, \(T\) is safe from \(a - r\) for \(L\), \(a' = a - r\), and \(S' = T\).

theorem request_eq_some_iff {available : R → ℕ} {pending : List P} {p : P} {req : R → ℕ}
    {available' : R → ℕ} {S' : System P R} :
    request S available pending p req = some (available', S') ↔
      p ∈ pending ∧ pending.Nodup ∧ req ≤ S.need p ∧ req ≤ available ∧
        (S.grant p req).Safe (available - req) pending ∧
        available' = available - req ∧ S' = S.grant p req
Uses 7 · Used by 1
Statement usesClaims and allocations of processes · Safe state · Granting a request · Remaining need · Resource-request algorithm
Proof usesBanker's safety algorithm · Correctness of the safety algorithm
Used byGranted requests lead to safe states

TheoremGranted requests lead to safe states#✓fully proved

Let \(S\) be a system of processes with maximum claims and current allocations, \(a\) the vector of free resources, \(L\) the list of pending processes, \(p\) a process and \(r\) a resource vector. If the resource-request algorithm grants the request of \(r\) by \(p\), returning the free vector \(a'\) and the system \(S'\), then \(S'\) is safe from \(a'\) for \(L\).

theorem request_safe {available : R → ℕ} {pending : List P} {p : P} {req : R → ℕ}
    {available' : R → ℕ} {S' : System P R}
    (h : request S available pending p req = some (available', S')) :
    S'.Safe available' pending
Uses 6
Statement usesClaims and allocations of processes · Safe state · Resource-request algorithm
Proof usesGranting a request · Remaining need · The request algorithm grants exactly the safe requests within the claim and the free resources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.