Pinned concurrency/thread.rs::terminate_active_thread (756-824) and unblock_thread (849-867). This executes cleanup and callbacks, preserving all prior memory/hook/manager effects on failure. TLS map removal precedes frees; race termination follows all frees; joiners are discovered afterward.

inductive Miri.Interpreter.ThreadExitRace : Type

• none : ThreadExitRace
• vectorClocks (global : Concurrency.GlobalState) : ThreadExitRace

inductive Miri.Interpreter.ThreadExitError (LeafError : Type) : Type

• thread {LeafError : Type} (error : Concurrency.ThreadError) : ThreadExitError LeafError
• tls {LeafError : Type} (error : ThreadLocalError) : ThreadExitError LeafError
• deallocation {LeafError : Type} (error : Memory.MemoryLifecycleError) : ThreadExitError LeafError
• race {LeafError : Type} (error : Concurrency.GlobalStateError) : ThreadExitError LeafError
• leaf {LeafError : Type} (error : LeafError) : ThreadExitError LeafError
• pointerIdentityMismatch {LeafError : Type} : ThreadExitError LeafError

def Miri.Interpreter.instReprThreadExitError.repr {LeafError✝ : Type} [Repr LeafError✝] : ThreadExitError LeafError✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprThreadExitError {LeafError✝ : Type} [Repr LeafError✝] : Repr (ThreadExitError LeafError✝)

Equations

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

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

• tls : ThreadLocalState P E H
• staticRoots : Array Memory.AllocId
• race : ThreadExitRace

@[reducible, inline]

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

Equations

• Miri.Interpreter.ThreadExitM P E H Error A = EStateM (Miri.Interpreter.ThreadExitError Error) (Miri.Interpreter.ThreadExitState P E H) A

structure Miri.Interpreter.ThreadExitQueries (P E H ProvExtra Error : Type) : Type

• deallocation : Memory.MemoryLifecycleHooks P E Memory.MiriMemoryKind H ProvExtra
• unblockCallback : Concurrency.UnblockCallbackObligation → ThreadExitM P E H Error Unit

  Execute the registered callback, including its join-clock and return destination actions, in the already-selected waiter's context.

def Miri.Interpreter.terminateActiveThread {P E H ProvExtra Error : Type} [Memory.PointerProvenance P] (queries : ThreadExitQueries P E H ProvExtra Error) (forExit : Bool) : ThreadExitM P E H Error Unit

Call only after the stack-empty callback actually returned Ready. The callback itself is orchestrated by the TLS destructor state machine.

Equations

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