Actual per-thread interpreter stacks behind Miri's active_thread_stack view. The StepState stack is the active view, and every inactive thread owns its complete saved Stack. No token-only stack is used to resume execution.

@[reducible, inline]

abbrev Miri.Interpreter.ThreadStacks.ActualStack : Type

Equations

• Miri.Interpreter.ThreadStacks.ActualStack = Miri.Interpreter.Stack Miri.Memory.Provenance Miri.Interpreter.LocalLayout Miri.Interpreter.MachineHooks.FrameExtra

structure Miri.Interpreter.ThreadStacks.SavedStack : Type

• thread : Concurrency.ThreadId
• stack : ActualStack

structure Miri.Interpreter.ThreadStacks.Registry : Type

The active stack lives in StepState.stack, never duplicated here. Thread IDs are never reused by the source ThreadManager.

• activeThread : Concurrency.ThreadId
• inactive : Array SavedStack

structure Miri.Interpreter.ThreadStacks.Storage (User : Type) : Type

Canonical machine User embedding. All existing MachineHooks/Place/Call adapters remain polymorphic in this payload and operate on the active stack.

• registry : Registry
• identitySupply : LocalsIdentitySupply
• user : User

@[reducible, inline]

abbrev Miri.Interpreter.ThreadStacks.State (K User : Type) : Type

Equations

• Miri.Interpreter.ThreadStacks.State K User = Miri.Interpreter.MachineHooks.State K (Miri.Interpreter.ThreadStacks.Storage User)

@[reducible, inline]

abbrev Miri.Interpreter.ThreadStacks.M (K User A : Type) : Type

Equations

• Miri.Interpreter.ThreadStacks.M K User A = EStateM Miri.Interpreter.StepError (Miri.Interpreter.ThreadStacks.State K User) A

def Miri.Interpreter.ThreadStacks.validate (registry : Registry) (manager : Concurrency.ThreadManager) : Except StepError Unit

Check coverage and uniqueness instead of inventing missing stacks. The manager's old opaque stackFrames field is not an interpreter frame source.

Equations

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

def Miri.Interpreter.ThreadStacks.freshLocalsIdentity {K User : Type} (machine : MachineHooks.MachineState K (Storage User)) : MachineHooks.MachineState K (Storage User) × LocalsIdentity

Total locals-buffer ghost allocation adapter for StackLifecycleHooks. The supply must start above all identities assigned with the lifetime-label policy. Explicit host-buffer-token embeddings may instead provide their own allocator.

Equations

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

def Miri.Interpreter.ThreadStacks.bindLifecycle {K User : Type} (base : StackLifecycleHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (Storage User))) : StackLifecycleHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (Storage User))

Equations

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

def Miri.Interpreter.ThreadStacks.attach {K User : Type} (state : MachineHooks.State K User) (inactive : Array SavedStack) (identitySupply : LocalsIdentitySupply) : Except StepError (State K User)

Attach a preexisting active view and explicit inactive stacks. This does not create any interpreter frame, local, layout, continuation or identity.

Equations

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

def Miri.Interpreter.ThreadStacks.installManager {K User : Type} (manager : Concurrency.ThreadManager) : M K User Unit

Install a source manager transition and its active stack together. All unrelated machine fields and actual frame contents remain unchanged. Any missing target is an invariant failure before mutation, never an empty stack. Existing manager updates (including callback state) come from the caller's source transition; stack restoration adds no compiler or machine callbacks.

Equations

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

def Miri.Interpreter.ThreadStacks.synchronize {K User : Type} : M K User Unit

Refresh compatibility lifecycle tokens after pushes/pops or callbacks, including failed callbacks that have already changed the current stack.

Equations

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

def Miri.Interpreter.ThreadStacks.synchronized {K User A : Type} (action : M K User A) : M K User A

Keep successful and failing active-frame mutation prefixes, then refresh the derived manager view. No source callback is invoked during reflection.

Equations

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

def Miri.Interpreter.ThreadStacks.bindCall {K User C Other Extern FnABI ArgABI : Type} (base : CallHooks Memory.Provenance (State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI) : CallHooks Memory.Provenance (State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI

Keep ThreadRecord's lifecycle projection coherent after both successful and partially failing call-stack operations. Use with the actual source call binding; no frame or local state is reconstructed from compatibility tokens.

Equations

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

def Miri.Interpreter.ThreadStacks.bindControl {K User C Op : Type} (base : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (Storage User)) C Op) : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (Storage User)) C Op

ControlFlow also pops directly on return/unwind. Refresh the derived thread lifecycle view even if protector release or cleanup fails midway.

Equations

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

def Miri.Interpreter.ThreadStacks.setActiveThread {K User : Type} (id : Concurrency.ThreadId) : M K User Concurrency.ThreadId

thread.rs set_active_thread returns the previous ID and accepts any existing thread; scheduler enabled-state checks belong to the source caller.

Equations

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

def Miri.Interpreter.ThreadStacks.withActiveThread {K User A : Type} (id : Concurrency.ThreadId) (action : M K User A) : M K User A

Source callbacks restore only on normal return. A callback error keeps its actual selected stack and all previous local/memory/machine mutations.

Equations

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

def Miri.Interpreter.ThreadStacks.createThread {K User : Type} (onStackEmpty : Nat) : M K User Concurrency.ThreadId

Thread::new owns an actually empty stack. This is the sole implicit empty stack here, created only after source create_thread allocates a new ID.

Equations

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

def Miri.Interpreter.ThreadStacks.unblockThread {K User : Type} (id : Concurrency.ThreadId) (reason : Concurrency.BlockReason) (invoke : Nat → Concurrency.UnblockKind → M K User Unit) : M K User Unit

unblock_thread changes the target to Enabled and selects it before the callback. Success restores the previous thread; errors retain the callback's current thread (which may itself have changed) and its actual stack.

Equations

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

def Miri.Interpreter.ThreadStacks.finishLocal {K User : Type} (potentialSleepTime : Option Nat) (anyThreadBlockedOnHost : Bool) (rank : Nat) : M K User RunSchedulingAction

Apply finishLocal's source scheduling policy to actual saved frames. The service-environment callbacks must already have run in their source order.

Equations

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

structure Miri.Interpreter.ThreadStacks.LocalSchedulerHooks (K User : Type) : Type

Required leaves for the complete local (local) scheduler branch. Host readiness/deadlines and nondeterministic choices remain genuine effects.

• processDelayedReadiness : M K User Unit
• communicate : M K User Bool
• pollHostIoNonBlocking : M K User Unit
• unblockExpiredDeadlines : M K User (Option Nat)
• choose : List Concurrency.ThreadId → M K User (Option Concurrency.ThreadId)
• anyThreadBlockedOnHost : M K User Bool

def Miri.Interpreter.ThreadStacks.scheduleLocal {K User : Type} (h : LocalSchedulerHooks K User) : M K User RunSchedulingAction

scheduler.rs schedule, local branch. Candidate selection precedes clearing yield; host-blocked queries run only after the enabled/all-terminated and finite-sleep branches have failed. Every callback operates on real stacks. The nondeterministic leaf must choose only a source-eligible candidate.

Equations

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

def Miri.Interpreter.ThreadStacks.bindRunLoop {K User C Callback : Type} (base : RunLoopHooks (State K User) C Callback) (h : C → LocalSchedulerHooks K User) : RunLoopHooks (State K User) C Callback

Bind the actual-stack scheduler to the outer run loop. All other lifecycle and environment callbacks remain the supplied source implementations.

Equations

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

def Miri.Interpreter.ThreadStacks.stackFor {K User : Type} (id : Concurrency.ThreadId) : M K User ActualStack

Observe any thread's actual stack. The active view includes all mutations since the last switch; inactive snapshots never come from opaque frame tokens.

Equations

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