Ordered thread-finish and join-wakeup protocol

This composes the source order in thread.rs::terminate_active_thread: beginTerminateActive marks the thread terminated and removes its TLS entries; the caller performs each TLS cleanup; this module then runs the selected termination hook; only then are joiners unblocked one at a time, with each callback executed in that joiner's active-thread context. Callback execution remains an external obligation.

inductive Miri.Concurrency.ThreadFinishHandler : Type

• none : ThreadFinishHandler
• vectorClocks : ThreadFinishHandler

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqThreadFinishHandler : DecidableEq ThreadFinishHandler

Equations

• Miri.Concurrency.instDecidableEqThreadFinishHandler x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Concurrency.instReprThreadFinishHandler.repr : ThreadFinishHandler → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadFinishHandler : Repr ThreadFinishHandler

Equations

• Miri.Concurrency.instReprThreadFinishHandler = { reprPrec := Miri.Concurrency.instReprThreadFinishHandler.repr }

inductive Miri.Concurrency.ThreadFinishError : Type

• globalState (error : GlobalStateError) : ThreadFinishError
• globalStateRequired : ThreadFinishError

def Miri.Concurrency.instReprThreadFinishError.repr : ThreadFinishError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadFinishError : Repr ThreadFinishError

Equations

• Miri.Concurrency.instReprThreadFinishError = { reprPrec := Miri.Concurrency.instReprThreadFinishError.repr }

inductive Miri.Concurrency.PostTlsFinish : Type

• wakeJoiners (manager : ThreadManager) (terminated : ThreadId) (waiters : List ThreadId) : PostTlsFinish
• wakeJoinersWithClocks (global : GlobalState) (manager : ThreadManager) (terminated : ThreadId) (waiters : List ThreadId) : PostTlsFinish

def Miri.Concurrency.instReprPostTlsFinish.repr : PostTlsFinish → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprPostTlsFinish : Repr PostTlsFinish

Equations

• Miri.Concurrency.instReprPostTlsFinish = { reprPrec := Miri.Concurrency.instReprPostTlsFinish.repr }

def Miri.Concurrency.afterTlsCleanup (handler : ThreadFinishHandler) (continuation : ThreadTerminationContinuation) (global : Option GlobalState := none) : Except ThreadFinishError PostTlsFinish

The source's chosen termination handler runs only after completeTlsCleanup has returned its continuation.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.afterTlsCleanup Miri.Concurrency.ThreadFinishHandler.vectorClocks continuation global = throw Miri.Concurrency.ThreadFinishError.globalStateRequired

def Miri.Concurrency.afterTlsCleanupWithGlobal (global : GlobalState) (continuation : ThreadTerminationContinuation) : Except ThreadFinishError PostTlsFinish

Execute the vector-clock termination hook against an explicitly supplied global state. The production state is not replaced by a fresh initial state.

Equations

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

inductive Miri.Concurrency.JoinWakeStep : Type

One wakeup iteration. Miri's unblock_thread invokes the callback synchronously; Lean exposes the exact callback action and leaves its effects to the interpreter.

• complete (manager : ThreadManager) : JoinWakeStep
• invokeCallback (manager : ThreadManager) (terminated : ThreadId) (unblock : UnblockCallbackObligation) (remaining : List ThreadId) : JoinWakeStep
• callbackFailed (managerAfterFailure : ThreadManager) (terminated : ThreadId) (unblock : UnblockCallbackObligation) (remaining : List ThreadId) : JoinWakeStep

@[instance_reducible]

instance Miri.Concurrency.instReprJoinWakeStep : Repr JoinWakeStep

Equations

• Miri.Concurrency.instReprJoinWakeStep = { reprPrec := Miri.Concurrency.instReprJoinWakeStep.repr }

def Miri.Concurrency.instReprJoinWakeStep.repr : JoinWakeStep → Nat → Std.Format

Equations

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

def Miri.Concurrency.ThreadManager.beginJoinerWakeups (manager : ThreadManager) (terminated : ThreadId) (waiters : List ThreadId) : Except ThreadError JoinWakeStep

Start ordered joiner wakeups after TLS and the selected termination hook have both completed.

Equations

• One or more equations did not get rendered due to their size.
• manager.beginJoinerWakeups terminated [] = pure (Miri.Concurrency.JoinWakeStep.complete manager)

def Miri.Concurrency.ThreadManager.continueJoinerWakeups (managerAfterCallback : ThreadManager) (terminated : ThreadId) (callback : UnblockCallbackObligation) (remaining : List ThreadId) (returnedNormally : Bool) : Except ThreadError JoinWakeStep

Continue after actually invoking one callback. On callback failure the source returns immediately, preserving the post-failure machine state and leaving later joiners blocked. On success the scheduler restores the previous active thread before issuing the next callback.

Equations

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