Deadline sweep and timeout callback protocol

This follows ThreadManager::unblock_expired_deadlines in thread.rs. Host-clock reads are supplied as exact per-thread remaining durations; this module does not invent a clock or unit. It performs the source's full sweep before invoking timeout callbacks, keeps the minimum positive wait, and then exposes callback execution in thread-index order. A callback failure retains the mutated manager and stops the remaining callbacks, matching ? before active-thread restoration.

structure Miri.Concurrency.DeadlineObservation : Type

Exact result of Miri's host clock subtraction for one blocked thread. A zero duration means the deadline has expired.

• thread : ThreadId
• remaining : Nat

def Miri.Concurrency.instReprDeadlineObservation.repr : DeadlineObservation → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Concurrency.instReprDeadlineObservation : Repr DeadlineObservation

Equations

• Miri.Concurrency.instReprDeadlineObservation = { reprPrec := Miri.Concurrency.instReprDeadlineObservation.repr }

inductive Miri.Concurrency.DeadlineSweepError : Type

• realTimeTimeoutInIsolation (thread : ThreadId) : DeadlineSweepError
• missingObservation (thread : ThreadId) : DeadlineSweepError
• duplicateObservations (thread : ThreadId) : DeadlineSweepError
• threadIdOverflow (index : Nat) : DeadlineSweepError

def Miri.Concurrency.instReprDeadlineSweepError.repr : DeadlineSweepError → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Concurrency.instReprDeadlineSweepError : Repr DeadlineSweepError

Equations

• Miri.Concurrency.instReprDeadlineSweepError = { reprPrec := Miri.Concurrency.instReprDeadlineSweepError.repr }

structure Miri.Concurrency.DeadlineCallback : Type

• thread : ThreadId
• reason : BlockReason
• callbackToken : Nat

def Miri.Concurrency.instReprDeadlineCallback.repr : DeadlineCallback → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Concurrency.instReprDeadlineCallback : Repr DeadlineCallback

Equations

• Miri.Concurrency.instReprDeadlineCallback = { reprPrec := Miri.Concurrency.instReprDeadlineCallback.repr }

structure Miri.Concurrency.DeadlineSweep : Type

The source mutates expired thread states during the sweep, before it starts calling any callbacks. outcome retains a source assertion or missing environment fact together with those prior mutations.

• manager : ThreadManager
• callbacks : List DeadlineCallback
• minimumWait : Option Nat
• outcome : Option DeadlineSweepError

@[instance_reducible]

instance Miri.Concurrency.instReprDeadlineSweep : Repr DeadlineSweep

Equations

• Miri.Concurrency.instReprDeadlineSweep = { reprPrec := Miri.Concurrency.instReprDeadlineSweep.repr }

def Miri.Concurrency.instReprDeadlineSweep.repr : DeadlineSweep → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.DeadlineSweep.initial (manager : ThreadManager) : DeadlineSweep

Equations

• Miri.Concurrency.DeadlineSweep.initial manager = { manager := manager, callbacks := [], minimumWait := none, outcome := none }

def Miri.Concurrency.DeadlineSweep.sweep (manager : ThreadManager) (observations : List DeadlineObservation) (communicate : Bool) : DeadlineSweep

Run the source's thread-index-ordered sweep. The observation list must contain the actual clock subtraction for each blocked deadline.

Equations

• One or more equations did not get rendered due to their size.

inductive Miri.Concurrency.DeadlineCallbackError : Type

• sweepFailed (error : DeadlineSweepError) : DeadlineCallbackError
• thread (error : ThreadError) : DeadlineCallbackError
• wrongCallbackKind (expected actual : UnblockKind) : DeadlineCallbackError

def Miri.Concurrency.instReprDeadlineCallbackError.repr : DeadlineCallbackError → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Concurrency.instReprDeadlineCallbackError : Repr DeadlineCallbackError

Equations

• Miri.Concurrency.instReprDeadlineCallbackError = { reprPrec := Miri.Concurrency.instReprDeadlineCallbackError.repr }

inductive Miri.Concurrency.DeadlineCallbackStep : Type

• complete (manager : ThreadManager) (minimumWait : Option Nat) : DeadlineCallbackStep
• invoke (manager : ThreadManager) (obligation : UnblockCallbackObligation) (remaining : List DeadlineCallback) (minimumWait : Option Nat) : DeadlineCallbackStep
• callbackFailed (managerAfterFailure : ThreadManager) (obligation : UnblockCallbackObligation) (remaining : List DeadlineCallback) (minimumWait : Option Nat) : DeadlineCallbackStep

def Miri.Concurrency.instReprDeadlineCallbackStep.repr : DeadlineCallbackStep → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Concurrency.instReprDeadlineCallbackStep : Repr DeadlineCallbackStep

Equations

• Miri.Concurrency.instReprDeadlineCallbackStep = { reprPrec := Miri.Concurrency.instReprDeadlineCallbackStep.repr }

def Miri.Concurrency.ThreadManager.beginDeadlineCallbacks (sweep : DeadlineSweep) : Except DeadlineCallbackError DeadlineCallbackStep

Start callbacks only after a successful complete sweep. Every expired thread has already been set to Enabled.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.ThreadManager.continueDeadlineCallbacks (managerAfterCallback : ThreadManager) (obligation : UnblockCallbackObligation) (remaining : List DeadlineCallback) (minimumWait : Option Nat) (returnedNormally : Bool) : Except DeadlineCallbackError DeadlineCallbackStep

Continue after one actual callback. A failed callback leaves its active thread selected and prevents later callbacks from running.

Equations

• One or more equations did not get rendered due to their size.