Coherent threaded runtime assembly. Spawned MIR root frames, ordinary calls, TLS roots, scalar results and allocation extras share the same actual machine dictionaries. Compiler ABI/body facts and host effects remain required inputs; this is not a second executable MIR representation.

structure Miri.Interpreter.ThreadRuntime.Configuration (K U C O X F A Aff Payload : Type) : Type 1

• thread : ThreadMachine.Hooks K U C O X F A Aff
• access : PlaceMachine.AccessConfig K (ThreadStacks.Storage U)
• compiler : PlaceMachine.CompilerHooks K (ThreadStacks.Storage U) C
• lifecycle : CallMachine.Lifecycle K (ThreadStacks.Storage U) C
• unwind : Unwind.Hooks K (ThreadStacks.Storage U) C O
• retag : TypedRetag.Hooks K (ThreadStacks.Storage U)
• retagBudget : Nat
• copy : PlaceCopyHooks Memory.Provenance (ThreadStacks.State K U) C
• evaluatePlace : C → MIR.Place → Bool → ThreadStacks.M K U (RuntimePlace Memory.Provenance)
• extras : MemoryExtras.Hooks K (ThreadStacks.Storage U) Payload
• weakMemory : Bool

def Miri.Interpreter.ThreadRuntime.thread {K U C O X F A Aff Payload : Type} [DecidableEq K] (config : Configuration K U C O X F A Aff Payload) : ThreadMachine.Hooks K U C O X F A Aff

Every constructed root frame uses canonical LoadedBody, compiler frame relevance, global locals identity supply, FnEntry retag/argument protection, real local storage/copy and actual after-pop unwind/cache behavior.

Equations

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

def Miri.Interpreter.ThreadRuntime.control {K U C O X F A Aff Payload : Type} [DecidableEq K] (config : Configuration K U C O X F A Aff Payload) (base : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (ThreadStacks.Storage U)) C (OpTy Memory.Provenance)) : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (ThreadStacks.Storage U)) C (OpTy Memory.Provenance)

Return/unwind terminators share the exact frame cleanup/protector/cache pipeline used by root calls and ordinary calls.

Equations

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

def Miri.Interpreter.ThreadRuntime.miriThread {U C O X F A Aff Payload : Type} (config : Configuration Memory.MiriMemoryKind U C O X F A Aff Payload) : ThreadMachine.Hooks Memory.MiriMemoryKind U C O X F A Aff

Miri's ignored thread return slot has the fixed source Machine kind.

Equations

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

def Miri.Interpreter.ThreadRuntime.termination {U C O X F A Aff Payload : Type} (config : Configuration Memory.MiriMemoryKind U C O X F A Aff Payload) (base : ThreadTerminationMachine.Hooks U C O X F A Aff Payload) : ThreadTerminationMachine.Hooks U C O X F A Aff Payload

TLS and normal-thread termination receive exactly the spawn/call dictionaries above, including the same extras registry used for allocation and memory access.

Equations

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

def Miri.Interpreter.ThreadRuntime.loop {U C O X F A Aff Payload : Type} (config : Configuration Memory.MiriMemoryKind U C O X F A Aff Payload) (terminate : ThreadTerminationMachine.Hooks U C O X F A Aff Payload) (base : RunLoopHooks (ThreadStacks.State Memory.MiriMemoryKind U) C ThreadLoops.TakenTls) (scheduler : C → ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind U) : RunLoopHooks (ThreadStacks.State Memory.MiriMemoryKind U) C ThreadLoops.TakenTls

Scheduler iteration and callback/termination protocol are a single binding; all callback take/restore actions are the checked source implementation.

Equations

• Miri.Interpreter.ThreadRuntime.loop config terminate base scheduler = Miri.Interpreter.ThreadLoops.bindActual (Miri.Interpreter.ThreadRuntime.termination config terminate) base scheduler

def Miri.Interpreter.ThreadRuntime.shims {U C O X F A Aff Payload D B I HostPath : Type} (config : Configuration Memory.MiriMemoryKind U C O X F A Aff Payload) (choice : C) (reuseClock : Option Concurrency.VectorIdx) (base : MiriShims.Hooks Memory.Provenance (ThreadStacks.State Memory.MiriMemoryKind U) D (MPlaceTy Memory.Provenance) B I HostPath) : MiriShims.Hooks Memory.Provenance (ThreadStacks.State Memory.MiriMemoryKind U) D (MPlaceTy Memory.Provenance) B I HostPath

The foreign Miri spawn/join arms share the same calls/allocations/retags as the scheduler's TLS and root-frame cleanup. Reuse is a permitted choice input.

Equations

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