Source thread.rs:756–824, canonical Ready→termination integration. TLS metadata is removed before frees, race finish follows successful cleanup, then each typed join continuation executes in the waiter's actual frame context.

@[reducible, inline]

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

Equations

• Miri.Interpreter.ThreadTerminationMachine.M = Miri.Interpreter.ThreadTlsMachine.M

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

• tls : ThreadTlsMachine.Hooks U C O X F A Aff
• deallocationError : Memory.MemoryLifecycleError → StepError
• deallocate : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind Memory.MiriMemoryKind → M U Unit

  Full-state deallocation operation, which owns active stack/address context instead of retaining it in a startup-time hook record.

def Miri.Interpreter.ThreadTerminationMachine.terminate {U C O X F A Aff Payload : Type} (h : Hooks U C O X F A Aff Payload) (choice : C) (forExit : Bool) : M U Unit

No token-only compatibility stack controls termination: the canonical actual frame array determines the source empty-stack assertion.

Equations

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

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

Bind this to the scheduler's normal-thread callback. Program exit has a separate exit handler and its explicit for_exit cleanup policy.

Equations

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