Dining philosophers problem

AbbreviationDining-philosophers state#✓fully proved

A state of the three dining philosophers is a triple \((s_0, s_1, s_2)\) with each \(s_i \in \{0, 1, 2\}\) the phase of philosopher \(i\): \(0\) thinking, \(1\) holding the first fork, \(2\) eating (holding both forks).

abbrev State := Fin 3 × Fin 3 × Fin 3

Used by 26

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Dining philosophers with atomic fork acquisition · Mutual exclusion under atomic acquisition · Under a butler every philosopher can always still eat · A butler prevents deadlock · Dining philosophers with a butler · Mutual exclusion under a butler · When a philosopher can move · Enabled moves under atomic acquisition · Enabled moves under a butler · The eating valuation · Held forks · Initial state of the dining philosophers · Transition system of a dining-philosophers protocol · Move of a philosopher · Move of a philosopher under atomic acquisition · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering · Phase of a philosopher · Number of seated philosophers · Updating the phase of a philosopher

DefinitionPhase of a philosopher#✓fully proved

For a state \(s = (s_0, s_1, s_2)\) of the three dining philosophers and a philosopher \(i \in \{0, 1, 2\}\), the phase of philosopher \(i\) in \(s\) is the component \(s_i\).

def phase (s : State) : Fin 3 → Fin 3
  | 0 => s.1
  | 1 => s.2.1
  | 2 => s.2.2

Uses 1 · Used by 20

Statement usesDining-philosophers state

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Mutual exclusion under atomic acquisition · Under a butler every philosopher can always still eat · A butler prevents deadlock · Mutual exclusion under a butler · When a philosopher can move · Enabled moves under atomic acquisition · Enabled moves under a butler · The eating valuation · Held forks · Move of a philosopher · Move of a philosopher under atomic acquisition · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering · Number of seated philosophers

DefinitionUpdating the phase of a philosopher#✓fully proved

For a state \(s = (s_0, s_1, s_2)\) of the three dining philosophers, a philosopher \(i \in \{0, 1, 2\}\) and a phase \(p \in \{0, 1, 2\}\), setting the phase of philosopher \(i\) to \(p\) gives the state obtained from \(s\) by replacing the component \(s_i\) by \(p\) and keeping the other two components.

def setPhase (s : State) (i : Fin 3) (p : Fin 3) : State :=
  match i with
  | 0 => (p, s.2.1, s.2.2)
  | 1 => (s.1, p, s.2.2)
  | 2 => (s.1, s.2.1, p)

Uses 1 · Used by 2

Statement usesDining-philosophers state

Used byMove of a philosopher · Move of a philosopher under atomic acquisition

StructureDining-philosophers protocol#✓fully proved

A protocol for three philosophers \(i \in \{0, 1, 2\}\) sitting between forks \(0, 1, 2\) consists of two maps \(\mathrm{first}, \mathrm{second}\) from \(\{0, 1, 2\}\) to itself, the fork philosopher \(i\) picks up first and the one it picks up second, such that for every \(i\) these are its two neighbouring forks \(i\) and \(i + 1\) (modulo \(3\)) in some order: either \(\mathrm{first}(i) = i\) and \(\mathrm{second}(i) = i + 1\), or \(\mathrm{first}(i) = i + 1\) and \(\mathrm{second}(i) = i\).

structure Protocol where
  /-- The fork picked up first. -/
  first : Fin 3 → Fin 3
  /-- The fork picked up second. -/
  second : Fin 3 → Fin 3
  /-- The two forks are the two neighbouring forks, in some order. -/
  neighbours : ∀ i, (first i = i ∧ second i = i + 1) ∨
    (first i = i + 1 ∧ second i = i)

Used by 11

Used byWhen a philosopher can move · Held forks · Transition system of a dining-philosophers protocol · Naive dining-philosophers protocol · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Resource-ordered dining-philosophers protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionHeld forks#✓fully proved

Given a protocol and a state, fork \(f\) is held exactly when some philosopher \(i\) either has \(f\) as its first fork and is in phase \(1\) or \(2\), or has \(f\) as its second fork and is in phase \(2\) (eating).

def held (P : Protocol) (s : State) (f : Fin 3) : Bool :=
  [0, 1, 2].any fun (i : Fin 3) =>
    (P.first i == f && decide (1 ≤ (phase s i).val)) || (P.second i == f && phase s i == 2)

Uses 3 · Used by 2

Statement usesDining-philosophers protocol · Dining-philosophers state · Phase of a philosopher

Used byWhen a philosopher can move · Enabled moves under atomic acquisition

DefinitionWhen a philosopher can move#✓fully proved

Given a protocol and a state, philosopher \(i\) can move exactly when it is thinking (phase \(0\)) and its first fork is not held by any philosopher, or it holds its first fork (phase \(1\)) and its second fork is not held by any philosopher, or it is eating (phase \(2\)), in which case its move puts both forks down.

def canMove (P : Protocol) (s : State) (i : Fin 3) : Bool :=
  match (phase s i).val with
  | 0 => !held P s (P.first i)
  | 1 => !held P s (P.second i)
  | _ => true

Uses 4 · Used by 8

Statement usesDining-philosophers protocol · Dining-philosophers state · Held forks · Phase of a philosopher

Used byEnabled moves under a butler · Transition system of a dining-philosophers protocol · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionMove of a philosopher#✓fully proved

The state obtained from \(s\) when philosopher \(i\) moves: the phase of \(i\) advances from thinking (\(0\)) to holding its first fork (\(1\)), from \(1\) to eating (\(2\)), and from eating back to thinking; the phases of the other philosophers are unchanged. Whether the move is allowed is not checked here.

def move (s : State) (i : Fin 3) : State :=
  setPhase s i (match (phase s i).val with | 0 => 1 | 1 => 2 | _ => 0)

Uses 3 · Used by 11

Statement usesDining-philosophers state · Phase of a philosopher · Updating the phase of a philosopher

Used byUnder a butler every philosopher can always still eat · A butler prevents deadlock · Dining philosophers with a butler · Mutual exclusion under a butler · Transition system of a dining-philosophers protocol · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionTransition system of a dining-philosophers protocol#✓fully proved

For a protocol \(P\), the labelled transition system on the states whose labels are the philosophers: there is a transition from \(s\) to \(t\) labelled \(i\) exactly when philosopher \(i\) can move in \(s\) under \(P\) and \(t\) is the state obtained from \(s\) by the move of philosopher \(i\).

def lts (P : Protocol) : LTS State (Fin 3) where
  Tr s i t := canMove P s i = true ∧ t = move s i

Uses 4 · Used by 6

Statement usesDining-philosophers protocol · Dining-philosophers state · When a philosopher can move · Move of a philosopher

Used byThe naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionThe eating valuation#✓fully proved

The valuation of the atoms \(i \in \{0, 1, 2\}\) on the states of the dining philosophers: atom \(i\) holds at a state exactly when philosopher \(i\) is eating there, that is, when its phase is \(2\).

def eating : State → Fin 3 → Prop := fun s i => phase s i = 2

Uses 2 · Used by 12

Statement usesDining-philosophers state · Phase of a philosopher

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Mutual exclusion under atomic acquisition · Under a butler every philosopher can always still eat · A butler prevents deadlock · Mutual exclusion under a butler · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionInitial state of the dining philosophers#✓fully proved

The state in which all three philosophers are thinking, that is, every phase is \(0\).

def initial : State := (0, 0, 0)

Uses 1 · Used by 11

Statement usesDining-philosophers state

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Mutual exclusion under atomic acquisition · Under a butler every philosopher can always still eat · A butler prevents deadlock · Mutual exclusion under a butler · The naive protocol can deadlock · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionNaive dining-philosophers protocol#✓fully proved

The protocol in which every philosopher \(i \in \{0, 1, 2\}\) picks up fork \(i\) (its left fork) first and fork \(i + 1\) (modulo \(3\)) second.

def naive : Protocol := ⟨fun i => i, fun i => i + 1, fun _ => Or.inl ⟨rfl, rfl⟩⟩

Uses 1 · Used by 5

Statement usesDining-philosophers protocol

Used byEnabled moves under atomic acquisition · Enabled moves under a butler · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol

DefinitionResource-ordered dining-philosophers protocol#✓fully proved

The protocol in which every philosopher \(i \in \{0, 1, 2\}\) picks up the lower-numbered of its two forks \(i\) and \(i + 1\) (modulo \(3\)) first and the higher-numbered one second: philosophers \(0\) and \(1\) take fork \(i\) first, and philosopher \(2\) takes fork \(0\) first and fork \(2\) second.

def ordered : Protocol :=
  ⟨fun i => min i (i + 1), fun i => max i (i + 1), by decide⟩

Uses 1 · Used by 3

Statement usesDining-philosophers protocol

Used byEvery philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionThe deadlock formula#✓fully proved

The CTL formula \(\neg\,\mathsf{EX}\,\top\) over the philosophers as atoms. It holds at a state exactly when the state has no successor; in the transition system of a protocol, exactly when no philosopher can move.

def deadlock : Formula (Fin 3) := .not (.existsNext .top)

Uses 1 · Used by 2

Statement usesCTL formulas

Used byThe naive protocol can deadlock · A deadlock state of the naive protocol

DefinitionNeighbours-apart formula#✓fully proved

For a philosopher \(i \in \{0, 1, 2\}\), the CTL formula \(\neg(p_i \wedge p_{i+1})\) over the atoms \(p_0, p_1, p_2\) (one per philosopher), with indices modulo \(3\). Under the valuation in which \(p_j\) holds when philosopher \(j\) eats, it says that the neighbouring philosophers \(i\) and \(i + 1\) do not eat at the same time.

def neighboursApart (i : Fin 3) : Formula (Fin 3) :=
  .not (.and (.atom i) (.atom (i + 1)))

Uses 1 · Used by 4

Statement usesCTL formulas

Used byMutual exclusion under atomic acquisition · Mutual exclusion under a butler · Mutual exclusion under the naive protocol · Neighbours never eat together under resource ordering

TheoremThe naive protocol can deadlock#✓fully proved

Consider the transition system of the naive protocol, in which every philosopher \(i\) picks up fork \(i\) first and fork \(i + 1\) second (indices modulo \(3\)), with atom \(i\) read as "philosopher \(i\) is eating". Its initial state, where all philosophers are thinking, satisfies the CTL formula \(\mathsf{EF}\) applied to the deadlock formula: from it, a state in which no philosopher can move is reachable.

theorem naive_deadlock_reachable :
    Satisfies (lts naive) eating initial (Formula.existsFinally deadlock)

Uses 16

Statement usesDining-philosophers state · The deadlock formula · The eating valuation · Initial state of the dining philosophers · Transition system of a dining-philosophers protocol · Naive dining-philosophers protocol · Exists finally · Satisfaction of CTL formulas

Proof usesDining-philosophers protocol · When a philosopher can move · Move of a philosopher · Phase of a philosopher · CTL formulas · The CTL model checker as a Boolean decision procedure · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremA deadlock state of the naive protocol#✓fully proved

In the transition system of the naive protocol, with atom \(i\) read as "philosopher \(i\) is eating", the state in which every philosopher holds its first fork (every phase is \(1\)) satisfies the deadlock formula: no philosopher can move there.

theorem naive_deadlock_state : Satisfies (lts naive) eating (1, 1, 1) deadlock

Uses 14

Statement usesDining-philosophers state · The deadlock formula · The eating valuation · Transition system of a dining-philosophers protocol · Naive dining-philosophers protocol · Satisfaction of CTL formulas

Proof usesDining-philosophers protocol · When a philosopher can move · Move of a philosopher · Phase of a philosopher · CTL formulas · The CTL model checker as a Boolean decision procedure · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremResource ordering prevents deadlock for the dining philosophers#✓fully proved

In the transition system of the three dining philosophers under the resource-ordered protocol, the initial state, in which everybody thinks, satisfies the CTL formula \(\mathrm{AG}\,\mathrm{EX}\,\top\): every state reachable from it has a successor, that is, some philosopher can move.

theorem ordered_deadlock_free :
    Satisfies (lts ordered) eating initial (Formula.forallGlobally (.existsNext .top))

Uses 15

Statement usesDining-philosophers state · The eating valuation · Initial state of the dining philosophers · Transition system of a dining-philosophers protocol · Resource-ordered dining-philosophers protocol · CTL formulas · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesDining-philosophers protocol · When a philosopher can move · Move of a philosopher · Phase of a philosopher · The CTL model checker as a Boolean decision procedure · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremEvery philosopher can still eat under resource ordering#✓fully proved

In the transition system of the three dining philosophers under the resource-ordered protocol, with the atom \(p_j\) holding when philosopher \(j\) eats, the initial state, in which everybody thinks, satisfies the CTL formula \(\mathrm{AG}\,\mathrm{EF}\,p_i\) for every philosopher \(i \in \{0, 1, 2\}\): from every state reachable from the initial state, some state in which philosopher \(i\) eats is reachable.

theorem ordered_can_eat (i : Fin 3) :
    Satisfies (lts ordered) eating initial
      (Formula.forallGlobally (Formula.existsFinally (.atom i)))

Uses 15

Statement usesDining-philosophers state · The eating valuation · Initial state of the dining philosophers · Transition system of a dining-philosophers protocol · Resource-ordered dining-philosophers protocol · CTL formulas · Exists finally · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesDining-philosophers protocol · When a philosopher can move · Move of a philosopher · Phase of a philosopher · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremMutual exclusion under the naive protocol#✓fully proved

For every philosopher \(i\), in the transition system of the naive protocol, with atom \(j\) read as "philosopher \(j\) is eating", the initial state satisfies \(\mathsf{AG}\) applied to the formula that philosophers \(i\) and \(i + 1\) (indices modulo \(3\)) do not both eat: in no state reachable from the initial state, where all philosophers are thinking, are philosophers \(i\) and \(i + 1\) both eating.

theorem naive_mutex (i : Fin 3) :
    Satisfies (lts naive) eating initial (Formula.forallGlobally (neighboursApart i))

Uses 15

Statement usesDining-philosophers state · The eating valuation · Initial state of the dining philosophers · Transition system of a dining-philosophers protocol · Naive dining-philosophers protocol · Neighbours-apart formula · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesDining-philosophers protocol · When a philosopher can move · Move of a philosopher · Phase of a philosopher · CTL formulas · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremNeighbours never eat together under resource ordering#✓fully proved

In the transition system of the three dining philosophers under the resource-ordered protocol, with the atom \(p_j\) holding when philosopher \(j\) eats, the initial state, in which everybody thinks, satisfies the CTL formula \(\mathrm{AG}\,\neg(p_i \wedge p_{i+1})\) for every philosopher \(i \in \{0, 1, 2\}\), with indices modulo \(3\): in no state reachable from the initial state do philosophers \(i\) and \(i + 1\) both eat.

theorem ordered_mutex (i : Fin 3) :
    Satisfies (lts ordered) eating initial (Formula.forallGlobally (neighboursApart i))

Uses 15

Statement usesDining-philosophers state · The eating valuation · Initial state of the dining philosophers · Transition system of a dining-philosophers protocol · Neighbours-apart formula · Resource-ordered dining-philosophers protocol · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesDining-philosophers protocol · When a philosopher can move · Move of a philosopher · Phase of a philosopher · CTL formulas · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

DefinitionEnabled moves under atomic acquisition#✓fully proved

Philosopher \(i\) can move in state \(s\) when it thinks and neither of its forks \(i\) and \(i + 1\) (modulo \(3\)) is held in \(s\), or when it eats (it then puts both forks down); a philosopher holding only its first fork cannot move. A fork is held as in the naive protocol: philosopher \(j\) holds fork \(j\) when it holds its first fork or eats, and holds fork \(j + 1\) when it eats.

def canMoveAtomic (s : State) (i : Fin 3) : Bool :=
  match (phase s i).val with
  | 0 => !held naive s i && !held naive s (i + 1)
  | 1 => false
  | _ => true

Uses 4 · Used by 4

Statement usesDining-philosophers state · Held forks · Naive dining-philosophers protocol · Phase of a philosopher

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Dining philosophers with atomic fork acquisition · Mutual exclusion under atomic acquisition

DefinitionMove of a philosopher under atomic acquisition#✓fully proved

In a state \(s\) (the phases of the three philosophers), the move of philosopher \(i\) changes only the phase of \(i\): if \(i\) is thinking, it starts eating, picking up both forks at once; otherwise it goes back to thinking. The phases of the other two philosophers are unchanged.

def moveAtomic (s : State) (i : Fin 3) : State :=
  setPhase s i (if (phase s i).val = 0 then 2 else 0)

Uses 3 · Used by 4

Statement usesDining-philosophers state · Phase of a philosopher · Updating the phase of a philosopher

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Dining philosophers with atomic fork acquisition · Mutual exclusion under atomic acquisition

DefinitionDining philosophers with atomic fork acquisition#✓fully proved

The labelled transition system on the states of the three philosophers, labelled by the philosopher that moves: there is a step labelled \(i\) from \(s\) to \(t\) exactly when either philosopher \(i\) thinks in \(s\), neither of its forks \(i\) and \(i + 1\) (modulo \(3\)) is held in \(s\), and \(t\) is \(s\) with philosopher \(i\) eating; or philosopher \(i\) eats in \(s\) and \(t\) is \(s\) with philosopher \(i\) thinking. A fork is held as in the naive protocol: philosopher \(j\) holds fork \(j\) when it holds its first fork or eats, and holds fork \(j + 1\) when it eats.

def atomicLts : LTS State (Fin 3) where
  Tr s i t := canMoveAtomic s i = true ∧ t = moveAtomic s i

Uses 3 · Used by 3

Statement usesDining-philosophers state · Enabled moves under atomic acquisition · Move of a philosopher under atomic acquisition

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Mutual exclusion under atomic acquisition

DefinitionNumber of seated philosophers#✓fully proved

The number of seated philosophers in a state \(s\) is the number of philosophers that hold at least one fork in \(s\), that is, whose phase is either holding the first fork or eating.

def seated (s : State) : ℕ :=
  ([0, 1, 2] : List (Fin 3)).countP fun i => decide (1 ≤ (phase s i).val)

Uses 2 · Used by 1

Statement usesDining-philosophers state · Phase of a philosopher

Used byEnabled moves under a butler

DefinitionEnabled moves under a butler#✓fully proved

Philosopher \(i\) can move in state \(s\) when it can move in \(s\) under the naive protocol and, if it is thinking, fewer than two philosophers hold at least one fork in \(s\). Under the naive protocol each philosopher \(i\) picks up the left fork \(i\) first and then the right fork \(i + 1\) (modulo \(3\)), each only when no philosopher holds it, and an eating philosopher can always put both forks down.

def canMoveButler (s : State) (i : Fin 3) : Bool :=
  canMove naive s i && ((phase s i).val != 0 || decide (seated s < 2))

Uses 5 · Used by 4

Statement usesDining-philosophers state · When a philosopher can move · Naive dining-philosophers protocol · Phase of a philosopher · Number of seated philosophers

Used byUnder a butler every philosopher can always still eat · A butler prevents deadlock · Dining philosophers with a butler · Mutual exclusion under a butler

DefinitionDining philosophers with a butler#✓fully proved

The labelled transition system on the states of the three philosophers, labelled by the philosopher that moves: there is a step labelled \(i\) from \(s\) to \(t\) exactly when philosopher \(i\) can move in \(s\) under the naive protocol, if philosopher \(i\) is thinking then fewer than two philosophers hold a fork in \(s\), and \(t\) is \(s\) with philosopher \(i\) advanced one phase (thinking to holding its first fork, to eating, to thinking). Under the naive protocol each philosopher \(i\) picks up the left fork \(i\) first and then the right fork \(i + 1\) (modulo \(3\)), each only when no philosopher holds it, and an eating philosopher can always put both forks down.

def butlerLts : LTS State (Fin 3) where
  Tr s i t := canMoveButler s i = true ∧ t = move s i

Uses 3 · Used by 3

Statement usesDining-philosophers state · Enabled moves under a butler · Move of a philosopher

Used byUnder a butler every philosopher can always still eat · A butler prevents deadlock · Mutual exclusion under a butler

TheoremAtomic acquisition prevents deadlock#✓fully proved

In the dining philosophers transition system with atomic acquisition of both forks, every state reachable from the initial state (all three philosophers thinking) has a successor: some philosopher can move.

theorem atomic_deadlock_free :
    Satisfies atomicLts eating initial (Formula.forallGlobally (.existsNext .top))

Uses 13

Statement usesDining-philosophers state · Dining philosophers with atomic fork acquisition · The eating valuation · Initial state of the dining philosophers · CTL formulas · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesEnabled moves under atomic acquisition · Move of a philosopher under atomic acquisition · Phase of a philosopher · The CTL model checker as a Boolean decision procedure · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremUnder atomic acquisition every philosopher can always still eat#✓fully proved

In the dining philosophers transition system with atomic acquisition of both forks, for each philosopher \(i \in \{0, 1, 2\}\), from every state reachable from the initial state (all three philosophers thinking) a state in which philosopher \(i\) eats is reachable, in zero or more steps.

theorem atomic_can_eat (i : Fin 3) :
    Satisfies atomicLts eating initial
      (Formula.forallGlobally (Formula.existsFinally (.atom i)))

Uses 13

Statement usesDining-philosophers state · Dining philosophers with atomic fork acquisition · The eating valuation · Initial state of the dining philosophers · CTL formulas · Exists finally · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesEnabled moves under atomic acquisition · Move of a philosopher under atomic acquisition · Phase of a philosopher · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremMutual exclusion under atomic acquisition#✓fully proved

In the dining philosophers transition system with atomic acquisition of both forks, for each philosopher \(i \in \{0, 1, 2\}\), in no state reachable from the initial state (all three philosophers thinking) do philosopher \(i\) and its neighbour \(i + 1\) (modulo \(3\)) both eat.

theorem atomic_mutex (i : Fin 3) :
    Satisfies atomicLts eating initial (Formula.forallGlobally (neighboursApart i))

Uses 13

Statement usesDining-philosophers state · Dining philosophers with atomic fork acquisition · The eating valuation · Initial state of the dining philosophers · Neighbours-apart formula · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesEnabled moves under atomic acquisition · Move of a philosopher under atomic acquisition · Phase of a philosopher · CTL formulas · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremA butler prevents deadlock#✓fully proved

In the dining philosophers transition system of the naive protocol under a butler, every state reachable from the initial state (all three philosophers thinking) has a successor: some philosopher can move.

theorem butler_deadlock_free :
    Satisfies butlerLts eating initial (Formula.forallGlobally (.existsNext .top))

Uses 13

Statement usesDining-philosophers state · Dining philosophers with a butler · The eating valuation · Initial state of the dining philosophers · CTL formulas · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesEnabled moves under a butler · Move of a philosopher · Phase of a philosopher · The CTL model checker as a Boolean decision procedure · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremUnder a butler every philosopher can always still eat#✓fully proved

In the dining philosophers transition system of the naive protocol under a butler, for each philosopher \(i \in \{0, 1, 2\}\), from every state reachable from the initial state (all three philosophers thinking) a state in which philosopher \(i\) eats is reachable, in zero or more steps.

theorem butler_can_eat (i : Fin 3) :
    Satisfies butlerLts eating initial
      (Formula.forallGlobally (Formula.existsFinally (.atom i)))

Uses 13

Statement usesDining-philosophers state · Dining philosophers with a butler · The eating valuation · Initial state of the dining philosophers · CTL formulas · Exists finally · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesEnabled moves under a butler · Move of a philosopher · Phase of a philosopher · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremMutual exclusion under a butler#✓fully proved

In the dining philosophers transition system of the naive protocol under a butler, for each philosopher \(i \in \{0, 1, 2\}\), in no state reachable from the initial state (all three philosophers thinking) do philosopher \(i\) and its neighbour \(i + 1\) (modulo \(3\)) both eat.

theorem butler_mutex (i : Fin 3) :
    Satisfies butlerLts eating initial (Formula.forallGlobally (neighboursApart i))

Uses 13

Statement usesDining-philosophers state · Dining philosophers with a butler · The eating valuation · Initial state of the dining philosophers · Neighbours-apart formula · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesEnabled moves under a butler · Move of a philosopher · Phase of a philosopher · CTL formulas · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

32 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.