formalizing multithreading

Stream: general

[Frederick Pu]

I've been procrasinating my operating systems homework so I decided to formalize multithreading

import Std

open Std

/-
  a monad `m` can be collected into a list of atomic instructions
  `β` is the instruction type
-/
class Instruction (m : Type → Type) [Monad m] (β : Type) where
  instructions {α} : m α → m (List β)

/--
`ThreadCollector m β σ`:

Represents a **scheduler** that tracks the evolution of a global scheduling state `σ`
as threads execute atomic instructions of type `β` in monad `m`.
-/
class ThreadCollector (m : Type → Type) (β σ : Type) where
  /--
  Update the scheduler after a thread executes an atomic instruction.

  - `sched` — the current scheduler state.
  - `instr` — the instruction the thread wants to execute.
  - `threadIdx` — index of the thread performing the instruction.

  Returns:
  * `none` if the thread is **denied** (e.g., tries to lock an already-locked mutex
    or is currently asleep).
  * `some mσ` if the thread is allowed to execute, producing a monadic action
    `m σ` that updates the scheduler state after the instruction.
  -/
  step : σ → β → (threadIdx : Nat) → Option (m σ)

/--
`scheduleOf sched instrs` means that `sched` is a **valid interleaving**
of the per-thread instruction lists `instrs`.

Formally:
1. Every instruction in `sched` is tagged by a valid thread index.
2. When we group `sched` by these thread tags, we recover exactly each `instrs[k]`.
3. `sched` and `tags` have the same length.
-/
def scheduleOf {β : Type} (sched : List β) (instrs : List (List β)) : Prop :=
  ∃ (tags : List Nat),
    -- (1) sched and tags have the same length
    sched.length = tags.length ∧
    -- (2) every tag is a valid thread index
    (∀ i, i < tags.length → tags[i]! < instrs.length) ∧
    -- (3) grouping by thread tag recovers the original instrs[k] (List.filterMap perserves order)
    (∀ k < instrs.length,
      let grouped := (sched.zip tags).filterMap (fun (b, t) =>
        if t = k then some b else none);
        grouped = instrs[k]!)

I was wondering if there were similar efforts or if anybody has feedback on my formalisms

[Frederick Pu]

my next goals are to formalize mutexs and show that if you have n threads each of which is locking from a list of m mutexs as long as all threads lock in ascending order of the mutex list then a deadlock can never happen

[Frederick Pu]

here's teh formalizm up to deadlocks

import Std

open Std

/-
  a monad `m` can be collected into a list of atomic instructions
  `β` is the instruction type
-/
class Instruction (m : Type → Type) [Monad m] (β : Type) where
  instructions {α} : m α → m (List β)

/--
`ThreadCollector m β σ`:

Represents a **scheduler** that tracks the evolution of a global scheduling state `σ`
as threads execute atomic instructions of type `β` in monad `m`.
-/
class ThreadCollector (m : Type → Type) (β σ : Type) where
  /--
  Update the scheduler after a thread executes an atomic instruction.

  - `sched` — the current scheduler state.
  - `instr` — the instruction the thread wants to execute.
  - `threadIdx` — index of the thread performing the instruction.

  Returns:
  * `none` if the thread is **denied** (e.g., tries to lock an already-locked mutex
    or is currently asleep).
  * `some mσ` if the thread is allowed to execute, producing a monadic action
    `m σ` that updates the scheduler state after the instruction.
  -/
  step : σ → β → (threadIdx : Nat) → Option (m σ)

/--
`scheduleOf sched instrs` means that `sched` is a **valid interleaving**
of the per-thread instruction lists `instrs`.

- `sched : List (Nat × β)` is a list of `(threadIdx, instruction)` pairs.
- `instrs : List (List β)` is the per-thread list of instructions.

Formally:
1. Every `(threadIdx, _)` in `sched` refers to a valid thread index.
2. For each thread `k`, collecting all instructions in `sched` with `threadIdx = k`
   (in order) recovers exactly `instrs[k]`.
-/
def scheduleOf {β : Type} (sched : List (Nat × β)) (instrs : List (List β)) : Prop :=
  -- (1) every tag is a valid thread index
  (∀ ib ∈ sched, ib.1 < instrs.length) ∧
  -- (2) grouping by thread tag recovers the original instrs[k]
  (∀ k < instrs.length,
    let grouped := sched.filterMap (fun (t, b) =>
      if t = k then some b else none);
    grouped = instrs[k]!)

/--
`partialScheduleOf prefix instrs` means that `prefix` is a **valid partial interleaving**
of the per-thread instruction lists `instrs`.

- `prefix : List (Nat × β)` is a prefix of a schedule.
- `instrs : List (List β)` is the per-thread list of instructions.

Formally:
1. Every `(threadIdx, _)` in `prefix` refers to a valid thread index.
2. For each thread `k`, collecting all instructions in `prefix` with `threadIdx = k`
   (in order) forms a **prefix** of `instrs[k]`.
-/
def partialScheduleOf {β : Type} (pref : List (Nat × β)) (instrs : List (List β)) : Prop :=
  -- (1) every tag is a valid thread index
  (∀ ib ∈ pref, ib.1 < instrs.length) ∧
  -- (2) grouping by thread tag is a prefix of each thread's instructions
  (∀ k < instrs.length,
    let grouped := pref.filterMap (fun (t, b) =>
      if t = k then some b else none);
    grouped.length ≤ instrs[k]!.length ∧
    grouped = instrs[k]!.take grouped.length)

example {β : Type} (pref : List (Nat × β)) (instrs : List (List β)): partialScheduleOf pref instrs → ∃ sched, scheduleOf sched instrs ∧ pref.length ≤ sched.length ∧ pref = sched.take pref.length := sorry

/--
`scheduleValid sched σ0 TC` means that executing `sched` from initial state `σ0`
using the `ThreadCollector` `TC` always produces `some σ` at every step.
-/
def scheduleValid {m : Type → Type}{β σ : Type} [Monad m]
  (TC : ThreadCollector m β σ)
  (sched : List (Nat × β))  -- (threadIdx, instr)
  (σ0 : σ) : Prop :=
  ∃ σFinal : σ,
    sched.foldlM (fun s (ti, instr) =>
      match TC.step s instr ti with
      | some ms => ms  -- bind the monadic action
      | none    => pure s  -- stop counting as valid? (could alternatively fail)
    ) σ0 = pure σFinal

/--
`deadlocks TC σ0 instrs pref` means that after executing the partial schedule `pref`,
the system is in **deadlock** under the `ThreadCollector` `TC` starting from state `σ0`.

Formally:
- `pref : List (Nat × β)` is a valid partial schedule (`partialScheduleOf pref instrs`).
- After `pref`, **any extension** of the remaining instructions cannot produce a
  full valid schedule where every step returns `some`.
-/
def deadlocks {m : Type → Type} {β σ : Type} [Monad m]
  (TC : ThreadCollector m β σ)
  (σ₀ : σ)
  (instrs : List (List β))
  (pref : List (Nat × β)) : Prop :=
  partialScheduleOf pref instrs ∧
  ∀ extension : List (Nat × β),
    -- extension must respect per-thread order of remaining instructions
    scheduleOf (pref ++ extension) instrs →
    ¬ scheduleValid TC (pref ++ extension) σ₀

[Frederick Pu]

a lot of proofs can be done via a starvation invariant which is basically like a loop invariant but you also have to prove it won't starve ie starvationInv threadIdx \sigma -> match step \sigma \beta | x => starvationInv threadIdx x | none => False