Scheduler-facing split callback protocol. The taken closure owns its actual TLS stage; invocation stores its mutated stage only on success, and restoration is checked in the thread selected after the callback.

@[reducible, inline]

abbrev Miri.Interpreter.ThreadLoops.M (U A : Type) : Type

Equations

• Miri.Interpreter.ThreadLoops.M = Miri.Interpreter.ThreadTlsMachine.M

@[reducible, inline]

abbrev Miri.Interpreter.ThreadLoops.State (U : Type) : Type

Equations

• Miri.Interpreter.ThreadLoops.State = Miri.Interpreter.ThreadTlsMachine.State

structure Miri.Interpreter.ThreadLoops.TakenTls : Type

• token : Nat
• stage : TlsDtorsStage Memory.Provenance

def Miri.Interpreter.ThreadLoops.take {U C O X F A Aff : Type} (h : ThreadTlsMachine.Hooks U C O X F A Aff) : M U TakenTls

Origin reset precedes callback take, including on missing callback errors. The registry copy is moved out with the callback, preventing reentry.

Equations

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

def Miri.Interpreter.ThreadLoops.invoke {U C O X F A Aff : Type} (h : ThreadTlsMachine.Hooks U C O X F A Aff) (choice : C) (callback : TakenTls) : M U StackEmptyPoll

No callback take or thread switching occurs here. The source engine may schedule a real destructor frame; errors retain its latest canonical state and do not restore the closure.

Equations

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

def Miri.Interpreter.ThreadLoops.restore {U C O X F A Aff : Type} (h : ThreadTlsMachine.Hooks U C O X F A Aff) (callback : TakenTls) : M U Unit

Source getter selects the thread active after callback execution. Restore assigns Some(callback), matching the unconditional source assignment.

Equations

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

def Miri.Interpreter.ThreadLoops.bind {U C O X F A Aff Payload : Type} (h : ThreadTerminationMachine.Hooks U C O X F A Aff Payload) (base : RunLoopHooks (State U) C TakenTls) : RunLoopHooks (State U) C TakenTls

Scheduler and core-step remain the actual caller dictionaries; TLS taking, invocation, checked restoration, and normal/for_exit termination are closed.

Equations

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

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

Coherent actual scheduler/core-step/stack lifecycle composition. Host I/O, deadline service and permitted scheduling choices remain the scheduler's real required leaves, rather than replacement scheduling tokens.

Equations

• Miri.Interpreter.ThreadLoops.bindActual h base scheduler = Miri.Interpreter.ThreadStacks.bindRunLoop (Miri.Interpreter.ThreadLoops.bind h base) scheduler

def Miri.Interpreter.ThreadLoops.iteration {U C O X F A Aff Payload : Type} (h : ThreadTerminationMachine.Hooks U C O X F A Aff Payload) (base : RunLoopHooks (State U) C TakenTls) (scheduler : C → ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind U) (choice : C) (state : State U) : StepResult (State U) Unit

Execute one real source scheduler iteration with the closed TLS lifecycle.

Equations

• Miri.Interpreter.ThreadLoops.iteration h base scheduler choice state = Miri.Interpreter.RunLoop.iteration (Miri.Interpreter.ThreadLoops.bindActual h base scheduler) choice state