Typed deadlines behind ThreadDeadline's internal tokens, and the stateful source thread.rs::unblock_expired_deadlines. Host readings interleave with thread enabling exactly during the sweep; callbacks execute only afterwards. No precomputed clock observation list is assumed to represent those effects.

structure Miri.Interpreter.DeadlineMachine.Registry (Host System : Type) : Type

• nextToken : Nat
• entries : Std.HashMap Nat (Array (Clock.Deadline Host System))

  Each token retains every associated row so malformed duplicate live metadata remains detectable. The map makes lookup and collision checks independent of the number of deadlines created in earlier waits.

• pruneDepth : Nat

  Nested source operations can temporarily keep expired deadlines alive while callbacks retry with the same token.

def Miri.Interpreter.DeadlineMachine.Registry.empty {Host System : Type} : Registry Host System

Equations

• Miri.Interpreter.DeadlineMachine.Registry.empty = { nextToken := 0, entries := ∅ }

def Miri.Interpreter.DeadlineMachine.Registry.retain {Host System : Type} (registry : Registry Host System) (live : Std.HashSet Nat) : Registry Host System

Keep exactly the token identities still held by blocked threads. Pruning is deferred while a nested deadline/callback transition is in progress; the outermost successful scope supplies the current live set.

Equations

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

def Miri.Interpreter.DeadlineMachine.Registry.enterPruneSuppression {Host System : Type} (registry : Registry Host System) : Registry Host System

Equations

• registry.enterPruneSuppression = { nextToken := registry.nextToken, entries := registry.entries, pruneDepth := registry.pruneDepth + 1 }

def Miri.Interpreter.DeadlineMachine.Registry.leavePruneSuppression {Host System : Type} (registry : Registry Host System) (live : Std.HashSet Nat) : Except StepError (Registry Host System)

Equations

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

def Miri.Interpreter.DeadlineMachine.Registry.leavePruneSuppressionOnError {Host System : Type} (registry : Registry Host System) : Except StepError (Registry Host System)

Equations

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

def Miri.Interpreter.DeadlineMachine.Registry.intern {Host System : Type} (registry : Registry Host System) (deadline : Clock.Deadline Host System) : Except StepError (Registry Host System × Concurrency.ThreadDeadline)

Tokens are representation identities, not times or addresses.

Equations

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

def Miri.Interpreter.DeadlineMachine.Registry.lookup {Host System : Type} (registry : Registry Host System) (deadline : Concurrency.ThreadDeadline) : Except StepError (Clock.Deadline Host System)

Equations

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

structure Miri.Interpreter.DeadlineMachine.Hooks (K User Host System : Type) : Type

• registry : User → Registry Host System
• setRegistry : Registry Host System → User → User
• clock : User → Clock.Monotonic Host
• host : Clock.HostHooks Host System (MachineHooks.State K User)
• communicate : MachineHooks.M K User Bool
• systemDurationSince : System → System → MachineHooks.M K User (Option Clock.Duration)

  SystemTime::duration_since returns Err before zero substitution when the deadline is past. This is a real host operation, not a virtual timestamp.

• selectThread : Concurrency.ThreadId → MachineHooks.M K User Concurrency.ThreadId

  Actual thread view swap, including its complete typed stack.

• invokeCallback : Nat → Concurrency.UnblockKind → MachineHooks.M K User Unit

structure Miri.Interpreter.DeadlineMachine.MonotonicMillisHooks (K User Host System : Type) : Type

The operation needed to create a relative monotonic millisecond deadline. It exposes the actual clock and deadline-token registry, while leaving scheduler callback selection and invocation out of consumers that only create deadlines (for example Unix poll's timeout path).

• registry : User → Registry Host System
• setRegistry : Registry Host System → User → User
• clock : User → Clock.Monotonic Host
• host : Clock.HostHooks Host System (MachineHooks.State K User)

def Miri.Interpreter.DeadlineMachine.intern {K User Host System : Type} (h : Hooks K User Host System) (deadline : Clock.Deadline Host System) : MachineHooks.M K User Concurrency.ThreadDeadline

Equations

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

def Miri.Interpreter.DeadlineMachine.timeout {K User Host System : Type} (h : Hooks K User Host System) (kind : Clock.TimeoutClock) (style : Clock.TimeoutStyle) (duration : Clock.Duration) : MachineHooks.M K User Concurrency.ThreadDeadline

Equations

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

def Miri.Interpreter.DeadlineMachine.monotonicDeadlineMillisFrom {K User Host System : Type} (h : MonotonicMillisHooks K User Host System) (milliseconds : UInt32) : MachineHooks.M K User Concurrency.ThreadDeadline

Intern an actual source monotonic deadline for a relative millisecond timeout. This is the minimal operation required by poll and Windows WaitOnAddress; it shares the source registry, clock, and host arithmetic.

Equations

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

def Miri.Interpreter.DeadlineMachine.monotonicDeadlineMillis {K User Host System : Type} (h : Hooks K User Host System) (milliseconds : UInt32) : MachineHooks.M K User Concurrency.ThreadDeadline

Windows WaitOnAddress uses the same relative monotonic millisecond deadline operation, projected from the complete scheduler hooks.

Equations

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

def Miri.Interpreter.DeadlineMachine.liveTokens (threads : Concurrency.ThreadManager) : Std.HashSet Nat

Equations

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

def Miri.Interpreter.DeadlineMachine.withPruneSuppressed {K User Host System A : Type} (registry : User → Registry Host System) (setRegistry : Registry Host System → User → User) (action : MachineHooks.M K User A) : MachineHooks.M K User A

Defer stale-token pruning across nested source transitions. Success at the outermost scope prunes against the then-current blocked threads; an error only restores the depth, preserving the exact error-state registry prefix.

Equations

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

def Miri.Interpreter.DeadlineMachine.unblockExpiredDeadlines {K User Host System : Type} (h : Hooks K User Host System) : MachineHooks.M K User (Option Nat)

Equations

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

def Miri.Interpreter.DeadlineMachine.bindScheduling {K User C Host System : Type} (base : SchedulingHooks (MachineHooks.State K User) C) (h : Hooks K User Host System) : SchedulingHooks (MachineHooks.State K User) C

Equations

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