Pinned concurrency/scheduler.rs::run_on_stack_empty (31-41), step_current_thread (174-186), and thread.rs new-thread captured TlsDtorsState. The closure registry supplies real mutable destructor state for opaque callback tokens. Taking a closure removes it before invocation; errors do not restore it. Callbacks for main/program exit remain distinct mandatory orchestration.

structure Miri.Interpreter.TlsCallback (P : Type) : Type

• token : Nat
• stage : TlsDtorsStage P

structure Miri.Interpreter.TlsCallbacksState (P E H : Type) : Type

• execution : TlsExecutionState P E H
• callbacks : Array (TlsCallback P)

inductive Miri.Interpreter.TlsCallbackError (Error : Type) : Type

• thread {Error : Type} (error : Concurrency.ThreadError) : TlsCallbackError Error
• missingCallback {Error : Type} : TlsCallbackError Error
• duplicateCallbackToken {Error : Type} (token : Nat) : TlsCallbackError Error
• unknownCallbackToken {Error : Type} (token : Nat) : TlsCallbackError Error
• callback {Error : Type} (error : TlsExecutionError Error) : TlsCallbackError Error
• termination {Error : Type} (error : ThreadExitError Error) : TlsCallbackError Error

def Miri.Interpreter.instReprTlsCallbackError.repr {Error✝ : Type} [Repr Error✝] : TlsCallbackError Error✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprTlsCallbackError {Error✝ : Type} [Repr Error✝] : Repr (TlsCallbackError Error✝)

Equations

• Miri.Interpreter.instReprTlsCallbackError = { reprPrec := Miri.Interpreter.instReprTlsCallbackError.repr }

@[reducible, inline]

abbrev Miri.Interpreter.TlsCallbackM (P E H Error A : Type) : Type

Equations

• Miri.Interpreter.TlsCallbackM P E H Error A = EStateM (Miri.Interpreter.TlsCallbackError Error) (Miri.Interpreter.TlsCallbacksState P E H) A

def Miri.Interpreter.registerTlsCallback {P E H Error : Type} (state : TlsCallbacksState P E H) (token : Nat) : Except (TlsCallbackError Error) (TlsCallbacksState P E H)

Register the closure captured for a new ordinary thread. Allocation of the opaque callback token belongs to the caller; duplicate tokens are rejected.

Equations

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

def Miri.Interpreter.runTlsOnStackEmpty {P E H Error : Type} [Memory.PointerProvenance P] (dummySpanToken : Nat) (platform : TlsPlatform) (target : ABI.RuntimeTargetDataLayout) (queries : TlsDestructorQueries P E H Error) : TlsCallbackM P E H Error Concurrency.StackEmptyCallbackResult

The explicit dummy-span token must name the source DUMMY_SP in the caller's span-token representation. It is not a fabricated span for an actual MIR site.

Equations

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

def Miri.Interpreter.stepEmptyTlsThread {P E H Error ProvExtra : Type} [Memory.PointerProvenance P] (dummySpanToken : Nat) (platform : TlsPlatform) (target : ABI.RuntimeTargetDataLayout) (queries : TlsDestructorQueries P E H Error) (exit : ThreadExitQueries P E H ProvExtra Error) : TlsCallbackM P E H Error Unit

Invoke only after the actual interpreter step reports an empty stack. Ready means normal thread termination; main/program-exit callbacks use their separate handler and must not be routed through this TLS-only entrypoint.

Equations

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