Execute the existing source TLS destructor state machine against canonical machine memory, actual frames, and thread manager. The legacy engine view is transient: every compiler/root-call query restores the latest full state and recaptures it on both outcomes. No persistent memory/clock copy is stored.

@[reducible, inline]

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

Equations

• Miri.Interpreter.ThreadTlsMachine.State U = Miri.Interpreter.ThreadStacks.State Miri.Memory.MiriMemoryKind U

@[reducible, inline]

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

Equations

• Miri.Interpreter.ThreadTlsMachine.M U A = Miri.Interpreter.ThreadStacks.M Miri.Memory.MiriMemoryKind U A

@[reducible, inline]

abbrev Miri.Interpreter.ThreadTlsMachine.Scratch (U : Type) : Type

Equations

• Miri.Interpreter.ThreadTlsMachine.Scratch U = Miri.Interpreter.TlsExecutionState Miri.Memory.Provenance Miri.TreeBorrows.BorrowTree (Miri.Interpreter.ThreadTlsMachine.State U)

@[reducible, inline]

abbrev Miri.Interpreter.ThreadTlsMachine.SM (U A : Type) : Type

Equations

• Miri.Interpreter.ThreadTlsMachine.SM U A = Miri.Interpreter.TlsM Miri.Memory.Provenance Miri.TreeBorrows.BorrowTree (Miri.Interpreter.ThreadTlsMachine.State U) Miri.Interpreter.StepError A

structure Miri.Interpreter.ThreadTlsMachine.Data : Type

• values : ThreadTlsData Memory.Provenance
• statics : Array (ThreadLocalEntry Memory.Provenance)
• staticRoots : Array Memory.AllocId

structure Miri.Interpreter.ThreadTlsMachine.Hooks (U C O X F A Aff : Type) : Type 1

• thread : ThreadMachine.Hooks Memory.MiriMemoryKind U C O X F A Aff
• data : U → Data
• putData : U → Data → U
• target : ABI.RuntimeTargetDataLayout
• platform : TlsPlatform
• unitPtrMut : LocalLayout
• unitPtrConst : LocalLayout
• u32Layout : LocalLayout
• lookupLinkSection : String → M U (Array (TlsImmediate Memory.Provenance × MIR.SpanRef))
• evalWindows : String → String → M U (Memory.Scalar Memory.Provenance)
• abi : TlsCallAbi → X
• error : TlsExecutionError StepError → StepError

def Miri.Interpreter.ThreadTlsMachine.queries {U C O X F A Aff : Type} (h : Hooks U C O X F A Aff) (choice : C) : TlsDestructorQueries Memory.Provenance TreeBorrows.BorrowTree (State U) StepError

Equations

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

def Miri.Interpreter.ThreadTlsMachine.onStackEmpty {U C O X F A Aff : Type} (h : Hooks U C O X F A Aff) (choice : C) : M U Concurrency.StackEmptyCallbackResult

scheduler.rs run_on_stack_empty: reset origin, take the callback, run its real captured stage, restore it only on success. Errors retain the callback's consumption and all earlier destructor state/frame/memory effects.

Equations

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