Source thread.rs start_regular_thread / join_thread_exclusive. Thread IDs own actual ThreadStacks, root calls execute Call.initStackFrame, and captured join continuations carry canonical typed destinations rather than completion tokens. TLS closures store the actual source destructor stage.

@[reducible, inline]

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

Equations

• Miri.Interpreter.ThreadMachine.State = Miri.Interpreter.ThreadStacks.State

@[reducible, inline]

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

Equations

• Miri.Interpreter.ThreadMachine.M = Miri.Interpreter.ThreadStacks.M

structure Miri.Interpreter.ThreadMachine.JoinCallback : Type

• token : Nat
• joined : Concurrency.ThreadId
• result : Memory.Scalar Memory.Provenance
• destination : MPlaceTy Memory.Provenance

structure Miri.Interpreter.ThreadMachine.Runtime (Affinity : Type) : Type

• nextCallback : Nat
• tlsCallbacks : Array (Nat × TlsDtorsStage Memory.Provenance)
• joins : Array JoinCallback
• affinity : Option (Array (Concurrency.ThreadId × Affinity))

structure Miri.Interpreter.ThreadMachine.Hooks (K U C Other Extern FnABI ArgABI Affinity : Type) : Type 1

• runtime : U → Runtime Affinity
• putRuntime : U → Runtime Affinity → U
• functions : FunctionCalls.Hooks Memory.Provenance (State K U) C MachineHooks.FrameExtra Other Extern FnABI ArgABI
• allocation : PlaceMachine.AllocationConfig K (ThreadStacks.Storage U)
• machineMemoryKind : K
• writeScalar : C → Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M K U Unit
• spans : AllocationDriver.SpanHooks
• chooseReuseClock : List Concurrency.VectorIdx → M K U (Option Concurrency.VectorIdx)

  Choose only from the source-approved safe vector-clock reuse set. The canonical Miri source connector consumes an execution-tape index here; the default keeps older non-source adapters fail-closed if they reach reuse.

def Miri.Interpreter.ThreadMachine.allocateReturn {K U C O X F A Aff : Type} [DecidableEq K] (h : Hooks K U C O X F A Aff) (layout : LocalLayout) : M K U (MPlaceTy Memory.Provenance)

Real return allocation with source Machine kind visible before root-address assignment; generic stack allocation's hardcoded Stack kind is not substituted.

Equations

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

def Miri.Interpreter.ThreadMachine.functionHooks {K U C O X F A Aff : Type} (h : Hooks K U C O X F A Aff) : FunctionCalls.Hooks Memory.Provenance (State K U) C MachineHooks.FrameExtra O X F A

Bind actual stack/origin operations, retaining compiler ABI and MIR queries. The real call hooks synchronize all pushed frames, including failure prefixes.

Equations

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

def Miri.Interpreter.ThreadMachine.startRegularThread {K U C O X F A Aff : Type} [DecidableEq K] (h : Hooks K U C O X F A Aff) (choice : C) (threadOutput : Option (MPlaceTy Memory.Provenance)) (routine : Memory.Pointer (Option Memory.Provenance)) (abi : X) (argument : RvalueImmTy Memory.Provenance) (returnLayout : LocalLayout) (reuseClock : Option Concurrency.VectorIdx) : M K U Concurrency.ThreadId

Equations

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

def Miri.Interpreter.ThreadMachine.joinExclusive {K U C O X F A Aff : Type} (h : Hooks K U C O X F A Aff) (choice : C) (joined : Concurrency.ThreadId) (value : Memory.Scalar Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M K U Unit

Equations

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

def Miri.Interpreter.ThreadMachine.takeJoin {K U C O X F A Aff : Type} (h : Hooks K U C O X F A Aff) (token : Nat) : M K U JoinCallback

Invoke in ThreadStacks.unblockThread's selected waiter context. The typed continuation is consumed before execution; an error retains that context.

Equations

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

def Miri.Interpreter.ThreadMachine.resumeJoin {K U C O X F A Aff : Type} (h : Hooks K U C O X F A Aff) (choice : C) (token : Nat) (kind : Concurrency.UnblockKind) : M K U Unit

Equations

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

def Miri.Interpreter.ThreadMachine.threadFromUsize {K U : Type} (raw : UInt64) : M K U (Option Concurrency.ThreadId)

Equations

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