Ordinary-lifecycle reuse boundary: thread termination publishes the old release snapshot and then increments its own vector coordinate. Join acquires only the snapshot, so a live caller can remain one tick behind the terminated candidate. A synthetic safe candidate tests the hook/predicate, not reachability through ordinary spawn/join. See MiriTests/DataRace/ThreadClockReuseReachability.lean.

Pinned Miri global vector-clock state

This module models the GlobalState thread/clock bookkeeping and synchronization hooks in src/concurrency/data_race.rs. It preserves the thread-to-vector mapping, re-use set, termination snapshots, all five per-thread clocks, SC fence/write clocks, race-detection flags, and configuration bits. A reusable index is selected through an explicit choice from the exact set of candidates accepted by Miri's predicate; the source uses FxHashSet iteration order, which is an implementation detail, so this relation exposes every safe member instead of inventing a stable order.

The methods here do not implement interpreter callbacks, TLS cleanup, atomic memory-cell validation, allocation metadata, diagnostics, or scheduler actions. threadTerminated is called only after the caller has completed Miri's prior TLS cleanup and marked the active thread terminated. Such cross-subsystem actions remain explicit preconditions at the integration boundary.

structure Miri.Concurrency.ThreadExtraState : Type

Additional source metadata retained for every ever-created ThreadId.

• vectorIndex : Option VectorIdx
• terminationVectorClock : Option VClock

def Miri.Concurrency.instReprThreadExtraState.repr : ThreadExtraState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadExtraState : Repr ThreadExtraState

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedThreadExtraState : Inhabited ThreadExtraState

Equations

• Miri.Concurrency.instInhabitedThreadExtraState = { default := Miri.Concurrency.instInhabitedThreadExtraState.default }

inductive Miri.Concurrency.GlobalStateError : Type

• thread (error : ThreadError) : GlobalStateError
• clock (error : ClockError) : GlobalStateError
• missingThreadMetadata (thread : ThreadId) : GlobalStateError
• missingVectorClock (index : VectorIdx) : GlobalStateError
• missingVectorInfo (index : VectorIdx) : GlobalStateError
• missingTerminationClock (thread : ThreadId) : GlobalStateError
• threadNotTerminated (thread : ThreadId) : GlobalStateError
• childIsActiveThread : GlobalStateError
• invalidReuseChoice : GlobalStateError

@[instance_reducible]

instance Miri.Concurrency.instReprGlobalStateError : Repr GlobalStateError

Equations

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

def Miri.Concurrency.instReprGlobalStateError.repr : GlobalStateError → Nat → Std.Format

Equations

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

structure Miri.Concurrency.SyncOperationBodyResult (External Error Value : Type) : Type

State returned by an operation body executed under Miri's synchronized operation wrapper. The body may update clocks and external memory before returning an error, so those states remain available on the error path.

• clocks : ThreadClockSet
• external : External
• outcome : Except Error (Bool × Value)

structure Miri.Concurrency.GlobalState : Type

Pinned Miri fields needed by concurrency synchronization and reuse.

• multiThreaded : Bool
• ongoingActionDataRaceFree : Bool
• vectorClocks : List ThreadClockSet
• vectorInfo : List ThreadId
• threadInfo : List ThreadExtraState
• reuseCandidates : List VectorIdx
• lastScFence : VClock
• lastScWritePerThread : VClock
• trackOutdatedLoads : Bool
• weakMemory : Bool

@[instance_reducible]

instance Miri.Concurrency.instReprGlobalState : Repr GlobalState

Equations

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

def Miri.Concurrency.instReprGlobalState.repr : GlobalState → Nat → Std.Format

Equations

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

structure Miri.Concurrency.SyncOperationTransition (Error External Value : Type) : Type

Result of maybe_perform_sync_operation. none means Miri's single-threaded fast path skipped the body entirely.

• global : GlobalState
• external : External
• outcome : Except (GlobalStateError ⊕ Error) (Option Value)

def Miri.Concurrency.GlobalState.initial (trackOutdatedLoads weakMemory : Bool) : GlobalState

Equations

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

def Miri.Concurrency.GlobalState.raceDetecting (state : GlobalState) : Bool

Equations

• state.raceDetecting = (state.multiThreaded && !state.ongoingActionDataRaceFree)

def Miri.Concurrency.GlobalState.withDataRaceFreeAction (state : GlobalState) (active : Bool) : GlobalState

Equations

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

def Miri.Concurrency.GlobalState.activeThreadIndex (state : GlobalState) (threads : ThreadManager) : Except GlobalStateError VectorIdx

Equations

• state.activeThreadIndex threads = Miri.Concurrency.GlobalState.threadIndex✝ state threads.activeThread

def Miri.Concurrency.GlobalState.activeThreadState (state : GlobalState) (threads : ThreadManager) : Except GlobalStateError (VectorIdx × ThreadClockSet)

Equations

• state.activeThreadState threads = do let index ← state.activeThreadIndex threads let clocks ← Miri.Concurrency.GlobalState.clocksAt✝ state index pure (index, clocks)

def Miri.Concurrency.GlobalState.maybePerformSyncOperation {External Error Value : Type} (state : GlobalState) (threads : ThreadManager) (external : External) (body : VectorIdx → ThreadClockSet → External → SyncOperationBodyResult External Error Value) : SyncOperationTransition Error External Value

Run the same callback boundary as Miri's maybe_perform_sync_operation. The callback is skipped when multithreaded tracking is off. Otherwise its clock and external-state mutations survive failure, and a normal true result causes one clock increment after the callback.

Equations

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

def Miri.Concurrency.GlobalState.reusableCandidates (state : GlobalState) : List VectorIdx

Every candidate accepted by the source's all-clocks predicate, in the existing collection's order. Selection remains explicit because the original FxHashSet traversal order is not a language-level semantic guarantee.

Equations

• state.reusableCandidates = List.filter (Miri.Concurrency.GlobalState.safeReuseCandidate✝ state) state.reuseCandidates

def Miri.Concurrency.GlobalState.threadCreated (state : GlobalState) (threads : ThreadManager) (child : ThreadId) (reuseChoice : Option VectorIdx) : Except GlobalStateError GlobalState

Apply Miri's thread-created hook after the ThreadManager has created the child. reuseChoice must be a safe candidate when any exist, and must be none when none exist. This preserves Miri's join-before-increment ordering.

Equations

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

def Miri.Concurrency.GlobalState.acquireClock (state : GlobalState) (threads : ThreadManager) (clock : VClock) : Except GlobalStateError GlobalState

Acquire a clock into the active thread without incrementing its timestamp.

Equations

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

def Miri.Concurrency.GlobalState.releaseClock (state : GlobalState) (threads : ThreadManager) : Except GlobalStateError (GlobalState × VClock)

Release snapshot: return the old clock and increment the active clock.

Equations

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

def Miri.Concurrency.GlobalState.threadTerminated (state : GlobalState) (threads : ThreadManager) : Except GlobalStateError GlobalState

Thread termination hook. The manager must already have marked the active thread Terminated and completed the preceding TLS cleanup effects.

Equations

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

def Miri.Concurrency.GlobalState.threadJoined (state : GlobalState) (threadsAfterJoin : ThreadManager) (joinee : ThreadId) : Except GlobalStateError GlobalState

Join a terminated thread. The caller supplies the post-join ThreadManager, whose live-thread count controls Miri's multi-threaded fast-path disabling.

Equations

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

def Miri.Concurrency.GlobalState.scWrite (state : GlobalState) (threads : ThreadManager) : Except GlobalStateError GlobalState

SC atomic store hook: save the active thread's clock at its own coordinate.

Equations

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

def Miri.Concurrency.GlobalState.scRead (state : GlobalState) (threads : ThreadManager) : Except GlobalStateError GlobalState

SC atomic load hook: remember the global last-SC-fence clock in this thread.

Equations

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

def Miri.Concurrency.GlobalState.atomicFence (state : GlobalState) (threads : ThreadManager) (ordering : AtomicFenceOrd) : Except GlobalStateError GlobalState

Apply the exact GlobalState fence ordering: acquire fence, SeqCst global RMW-style join, last-SC-write metadata, then release fence. If the source's multi-threaded flag is false, maybe_perform_sync_operation is a no-op.

Equations

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