Thread lifecycle state used by Miri's concurrency hooks

This is a source-shaped state model of src/concurrency/thread.rs at the pinned revision. It keeps the manager's contiguous, never-reused thread IDs, active ID, every thread's Enabled/Blocked/Terminated state, join status, blocked callback token and deadline, names, stacks, origin span, stack-empty callback, frame-cache index, unwind payloads, last-error location, TLS map, and scheduler flags. Interpreter frames, pointers, spans, and machine callbacks are opaque tokens here: their concrete Miri behavior is outside Lean's concurrency state model, and callback-dependent operations return explicit obligations rather than assuming callback success.

This module does not implement MIR execution, TLS allocation/deallocation, stack unwinding, callback code, or Miri's scheduler.

structure Miri.Concurrency.ThreadId : Type

A Rust ThreadId, represented with the exact unsigned 32-bit bound.

• value : Fin 4294967296

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqThreadId : DecidableEq ThreadId

Equations

• Miri.Concurrency.instDecidableEqThreadId = Miri.Concurrency.instDecidableEqThreadId.decEq

def Miri.Concurrency.instDecidableEqThreadId.decEq (x✝ x✝¹ : ThreadId) : Decidable (x✝ = x✝¹)

Equations

• Miri.Concurrency.instDecidableEqThreadId.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.Concurrency.instReprThreadId.repr : ThreadId → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadId : Repr ThreadId

Equations

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

def Miri.Concurrency.ThreadId.MAIN_THREAD : ThreadId

Equations

• Miri.Concurrency.ThreadId.MAIN_THREAD = { value := ⟨0, Miri.Concurrency.ThreadId.MAIN_THREAD._proof_1⟩ }

def Miri.Concurrency.ThreadId.ofU32 (value : Nat) (bound : value < 4294967296) : ThreadId

Equations

• Miri.Concurrency.ThreadId.ofU32 value bound = { value := ⟨value, bound⟩ }

def Miri.Concurrency.ThreadId.toNat (id : ThreadId) : Nat

Checked counterpart of rustc-index Idx::new for host vector indices.

Equations

• id.toNat = ↑id.value

inductive Miri.Concurrency.BlockReason : Type

Reasons retained verbatim by ThreadState::Blocked.

• Join (thread : ThreadId) : BlockReason
• Sleep : BlockReason
• Mutex : BlockReason
• Condvar : BlockReason
• RwLock : BlockReason
• Semaphore : BlockReason
• Futex : BlockReason
• InitOnce : BlockReason
• Readiness : BlockReason
• Eventfd : BlockReason
• VirtualSocket : BlockReason
• IO : BlockReason

def Miri.Concurrency.instDecidableEqBlockReason.decEq (x✝ x✝¹ : BlockReason) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqBlockReason : DecidableEq BlockReason

Equations

• Miri.Concurrency.instDecidableEqBlockReason = Miri.Concurrency.instDecidableEqBlockReason.decEq

def Miri.Concurrency.instReprBlockReason.repr : BlockReason → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprBlockReason : Repr BlockReason

Equations

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

inductive Miri.Concurrency.ThreadDeadline : Type

Deadline kind and opaque clock value. Clock arithmetic is owned by Miri's clock subsystem and is not silently approximated here.

• Monotonic (opaqueInstant : Nat) : ThreadDeadline
• RealTime (opaqueSystemTime : Nat) : ThreadDeadline

def Miri.Concurrency.instDecidableEqThreadDeadline.decEq (x✝ x✝¹ : ThreadDeadline) : Decidable (x✝ = x✝¹)

Equations

• Miri.Concurrency.instDecidableEqThreadDeadline.decEq (Miri.Concurrency.ThreadDeadline.Monotonic a) (Miri.Concurrency.ThreadDeadline.Monotonic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Concurrency.instDecidableEqThreadDeadline.decEq (Miri.Concurrency.ThreadDeadline.Monotonic opaqueInstant) (Miri.Concurrency.ThreadDeadline.RealTime opaqueSystemTime) = isFalse ⋯
• Miri.Concurrency.instDecidableEqThreadDeadline.decEq (Miri.Concurrency.ThreadDeadline.RealTime opaqueSystemTime) (Miri.Concurrency.ThreadDeadline.Monotonic opaqueInstant) = isFalse ⋯
• Miri.Concurrency.instDecidableEqThreadDeadline.decEq (Miri.Concurrency.ThreadDeadline.RealTime a) (Miri.Concurrency.ThreadDeadline.RealTime b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqThreadDeadline : DecidableEq ThreadDeadline

Equations

• Miri.Concurrency.instDecidableEqThreadDeadline = Miri.Concurrency.instDecidableEqThreadDeadline.decEq

@[instance_reducible]

instance Miri.Concurrency.instReprThreadDeadline : Repr ThreadDeadline

Equations

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

def Miri.Concurrency.instReprThreadDeadline.repr : ThreadDeadline → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.UnblockKind : Type

• Ready : UnblockKind
• TimedOut : UnblockKind

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqUnblockKind : DecidableEq UnblockKind

Equations

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

def Miri.Concurrency.instReprUnblockKind.repr : UnblockKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprUnblockKind : Repr UnblockKind

Equations

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

inductive Miri.Concurrency.ThreadJoinStatus : Type

• Joinable : ThreadJoinStatus
• Detached : ThreadJoinStatus
• Joined : ThreadJoinStatus

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqThreadJoinStatus : DecidableEq ThreadJoinStatus

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadJoinStatus : Repr ThreadJoinStatus

Equations

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

def Miri.Concurrency.instReprThreadJoinStatus.repr : ThreadJoinStatus → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.ThreadState : Type

Callback-free view of the thread state tag and blocked payload.

• Enabled : ThreadState
• Blocked (reason : BlockReason) (deadline : Option ThreadDeadline) (callbackToken : Nat) : ThreadState
• Terminated : ThreadState

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqThreadState : DecidableEq ThreadState

Equations

• Miri.Concurrency.instDecidableEqThreadState = Miri.Concurrency.instDecidableEqThreadState.decEq

def Miri.Concurrency.instDecidableEqThreadState.decEq (x✝ x✝¹ : ThreadState) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqThreadState.decEq Miri.Concurrency.ThreadState.Enabled Miri.Concurrency.ThreadState.Enabled = isTrue ⋯
• Miri.Concurrency.instDecidableEqThreadState.decEq Miri.Concurrency.ThreadState.Enabled (Miri.Concurrency.ThreadState.Blocked reason deadline callbackToken) = isFalse ⋯
• Miri.Concurrency.instDecidableEqThreadState.decEq (Miri.Concurrency.ThreadState.Blocked reason deadline callbackToken) Miri.Concurrency.ThreadState.Enabled = isFalse ⋯
• Miri.Concurrency.instDecidableEqThreadState.decEq (Miri.Concurrency.ThreadState.Blocked reason deadline callbackToken) Miri.Concurrency.ThreadState.Terminated = isFalse ⋯
• Miri.Concurrency.instDecidableEqThreadState.decEq Miri.Concurrency.ThreadState.Terminated (Miri.Concurrency.ThreadState.Blocked reason deadline callbackToken) = isFalse ⋯
• Miri.Concurrency.instDecidableEqThreadState.decEq Miri.Concurrency.ThreadState.Terminated Miri.Concurrency.ThreadState.Terminated = isTrue ⋯

@[instance_reducible]

instance Miri.Concurrency.instReprThreadState : Repr ThreadState

Equations

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

def Miri.Concurrency.instReprThreadState.repr : ThreadState → Nat → Std.Format

Equations

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

structure Miri.Concurrency.ThreadRecord : Type

Opaque per-thread interpreter fields, preserved by lifecycle updates. Each field corresponds to an actual Thread field in pinned Miri.

• state : ThreadState
• threadName : Option (List UInt8)
• stackFrames : List Nat
• originSpanToken : Nat
• onStackEmptyCallback : Option Nat
• topUserRelevantFrame : Option Nat
• joinStatus : ThreadJoinStatus
• unwindPayloads : List Nat
• lastErrorLocation : Option Nat

@[instance_reducible]

instance Miri.Concurrency.instReprThreadRecord : Repr ThreadRecord

Equations

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

def Miri.Concurrency.instReprThreadRecord.repr : ThreadRecord → Nat → Std.Format

Equations

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

def Miri.Concurrency.ThreadRecord.initial (name : Option (List UInt8)) (onStackEmpty : Option Nat) : ThreadRecord

Equations

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

def Miri.Concurrency.ThreadRecord.isEnabled (thread : ThreadRecord) : Bool

Equations

• thread.isEnabled = match thread.state with | Miri.Concurrency.ThreadState.Enabled => true | x => false

def Miri.Concurrency.ThreadRecord.isTerminated (thread : ThreadRecord) : Bool

Equations

• thread.isTerminated = match thread.state with | Miri.Concurrency.ThreadState.Terminated => true | x => false

def Miri.Concurrency.ThreadRecord.isBlockedOn (thread : ThreadRecord) (reason : BlockReason) : Bool

Equations

• thread.isBlockedOn reason = match thread.state with | Miri.Concurrency.ThreadState.Blocked actual deadline callbackToken => actual == reason | x => false

structure Miri.Concurrency.ThreadLocalAllocation : Type

Thread-local allocation identity; the pointer token is preserved but not interpreted as a Rust pointer by this module.

• definitionToken : Nat
• thread : ThreadId
• pointerToken : Nat

def Miri.Concurrency.instDecidableEqThreadLocalAllocation.decEq (x✝ x✝¹ : ThreadLocalAllocation) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqThreadLocalAllocation : DecidableEq ThreadLocalAllocation

Equations

• Miri.Concurrency.instDecidableEqThreadLocalAllocation = Miri.Concurrency.instDecidableEqThreadLocalAllocation.decEq

@[instance_reducible]

instance Miri.Concurrency.instReprThreadLocalAllocation : Repr ThreadLocalAllocation

Equations

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

def Miri.Concurrency.instReprThreadLocalAllocation.repr : ThreadLocalAllocation → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.ThreadError : Type

• threadIdOverflow : ThreadError
• invalidId : ThreadError
• terminated (thread : ThreadId) : ThreadError
• activeIdOutOfBounds (thread : ThreadId) : ThreadError
• activeThreadNotEnabled (thread : ThreadId) : ThreadError
• stackEmptyCallbackPending (thread : ThreadId) : ThreadError
• stackNotEmptyAtTermination (thread : ThreadId) : ThreadError
• targetNotBlocked (thread : ThreadId) : ThreadError
• wrongBlockReason (expected actual : BlockReason) : ThreadError
• detachAlreadyConsumed (thread : ThreadId) : ThreadError
• detachNotJoinable (thread : ThreadId) : ThreadError

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqThreadError : DecidableEq ThreadError

Equations

• Miri.Concurrency.instDecidableEqThreadError = Miri.Concurrency.instDecidableEqThreadError.decEq

def Miri.Concurrency.instDecidableEqThreadError.decEq (x✝ x✝¹ : ThreadError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadError : Repr ThreadError

Equations

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

def Miri.Concurrency.instReprThreadError.repr : ThreadError → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.BlockThreadSourceError : Type

Miri's EvalContext::block_thread restrictions, checked before mutating the ThreadManager. These are source panics/unsupported configurations, not UB or successful blocking outcomes.

• realTimeTimeoutInIsolation : BlockThreadSourceError
• thread (error : ThreadError) : BlockThreadSourceError

@[instance_reducible]

instance Miri.Concurrency.instReprBlockThreadSourceError : Repr BlockThreadSourceError

Equations

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

def Miri.Concurrency.instReprBlockThreadSourceError.repr : BlockThreadSourceError → Nat → Std.Format

Equations

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

def Miri.Concurrency.ThreadId.ofNat (value : Nat) : Except ThreadError ThreadId

Checked counterpart of rustc-index Idx::new for host vector indices.

Equations

• Miri.Concurrency.ThreadId.ofNat value = if bound : value < 4294967296 then Except.ok { value := ⟨value, bound⟩ } else Except.error Miri.Concurrency.ThreadError.threadIdOverflow

structure Miri.Concurrency.UnblockCallbackObligation : Type

A callback obligation created by unblockThread. It records the exact callback token and execution context. A caller must supply the actual callback execution result and resulting machine state; this model does not assume it returns normally.

• target : ThreadId
• previousActive : ThreadId
• reason : BlockReason
• callbackToken : Nat
• kind : UnblockKind

@[instance_reducible]

instance Miri.Concurrency.instReprUnblockCallbackObligation : Repr UnblockCallbackObligation

Equations

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

def Miri.Concurrency.instReprUnblockCallbackObligation.repr : UnblockCallbackObligation → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.StackEmptyCallbackResult : Type

Outcome that the caller obtained by actually invoking the thread's on_stack_empty callback.

• Ready : StackEmptyCallbackResult
• Pending : StackEmptyCallbackResult

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqStackEmptyCallbackResult : DecidableEq StackEmptyCallbackResult

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprStackEmptyCallbackResult : Repr StackEmptyCallbackResult

Equations

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

def Miri.Concurrency.instReprStackEmptyCallbackResult.repr : StackEmptyCallbackResult → Nat → Std.Format

Equations

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

structure Miri.Concurrency.TlsCleanupObligation : Type

A source TLS allocation that must be deallocated or retained as an exit static root before the vector-clock termination hook runs.

• thread : ThreadId
• pointerToken : Nat
• leakAsStaticRoot : Bool

@[instance_reducible]

instance Miri.Concurrency.instReprTlsCleanupObligation : Repr TlsCleanupObligation

Equations

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

def Miri.Concurrency.instReprTlsCleanupObligation.repr : TlsCleanupObligation → Nat → Std.Format

Equations

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

structure Miri.Concurrency.ThreadTerminationObligation : Type

Ordered work emitted when Miri marks a thread terminated. TLS cleanup and the data-race termination hook precede waking joiners in the original source.

• thread : ThreadId
• tlsCleanup : List TlsCleanupObligation
• joinWaiters : List ThreadId
• forExit : Bool

def Miri.Concurrency.instReprThreadTerminationObligation.repr : ThreadTerminationObligation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadTerminationObligation : Repr ThreadTerminationObligation

Equations

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

inductive Miri.Concurrency.TlsCleanupResult : Type

• Deallocated (pointerToken : Nat) : TlsCleanupResult
• RetainedAsStaticRoot (pointerToken : Nat) : TlsCleanupResult
• Failed (pointerToken : Nat) : TlsCleanupResult

def Miri.Concurrency.instDecidableEqTlsCleanupResult.decEq (x✝ x✝¹ : TlsCleanupResult) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqTlsCleanupResult.decEq (Miri.Concurrency.TlsCleanupResult.Deallocated pointerToken) (Miri.Concurrency.TlsCleanupResult.Failed pointerToken_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqTlsCleanupResult.decEq (Miri.Concurrency.TlsCleanupResult.Failed pointerToken) (Miri.Concurrency.TlsCleanupResult.Deallocated pointerToken_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqTlsCleanupResult.decEq (Miri.Concurrency.TlsCleanupResult.Failed a) (Miri.Concurrency.TlsCleanupResult.Failed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqTlsCleanupResult : DecidableEq TlsCleanupResult

Equations

• Miri.Concurrency.instDecidableEqTlsCleanupResult = Miri.Concurrency.instDecidableEqTlsCleanupResult.decEq

def Miri.Concurrency.instReprTlsCleanupResult.repr : TlsCleanupResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprTlsCleanupResult : Repr TlsCleanupResult

Equations

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

inductive Miri.Concurrency.ThreadTerminationError : Type

• threadError (error : ThreadError) : ThreadTerminationError
• callbackFailedOrIncomplete : ThreadTerminationError
• cleanupResultCountMismatch : ThreadTerminationError
• cleanupResultMismatch (expected actual : TlsCleanupResult) : ThreadTerminationError

@[instance_reducible]

instance Miri.Concurrency.instReprThreadTerminationError : Repr ThreadTerminationError

Equations

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

def Miri.Concurrency.instReprThreadTerminationError.repr : ThreadTerminationError → Nat → Std.Format

Equations

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

structure Miri.Concurrency.ThreadManager : Type

ThreadManager state from pinned Miri, with opaque TLS pointers and callback tokens retained as data. Threads remain in the list after termination.

• activeThread : ThreadId
• threads : List ThreadRecord
• threadLocalAllocs : List ThreadLocalAllocation
• yieldActiveThread : Bool
• fixedScheduling : Bool

def Miri.Concurrency.instReprThreadManager.repr : ThreadManager → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprThreadManager : Repr ThreadManager

Equations

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

structure Miri.Concurrency.ThreadTerminationContinuation : Type

The continuation after successful TLS work. dataRaceHookThread must be passed to GlobalState.threadTerminated before joinWaiters are unblocked.

• manager : ThreadManager
• dataRaceHookThread : ThreadId
• joinWaiters : List ThreadId

@[instance_reducible]

instance Miri.Concurrency.instReprThreadTerminationContinuation : Repr ThreadTerminationContinuation

Equations

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

def Miri.Concurrency.instReprThreadTerminationContinuation.repr : ThreadTerminationContinuation → Nat → Std.Format

Equations

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

def Miri.Concurrency.ThreadManager.initial (fixedScheduling : Bool) : ThreadManager

Equations

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

def Miri.Concurrency.ThreadManager.initializeMainThread (manager : ThreadManager) (windowsTarget : Bool) (stackEmptyCallback : Nat) : Except ThreadError ThreadManager

Miri's post-construction initialization: install the main stack callback; on non-Windows targets the main thread is detached.

Equations

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

def Miri.Concurrency.ThreadManager.totalThreadCount (manager : ThreadManager) : Nat

Equations

• manager.totalThreadCount = manager.threads.length

def Miri.Concurrency.ThreadManager.liveThreadCount (manager : ThreadManager) : Nat

Equations

• manager.liveThreadCount = List.countP (fun (thread : Miri.Concurrency.ThreadRecord) => !thread.isTerminated) manager.threads

def Miri.Concurrency.ThreadManager.activeThread? (manager : ThreadManager) : Option ThreadRecord

Equations

• manager.activeThread? = Miri.Concurrency.ThreadManager.get?✝ manager.threads manager.activeThread.toNat

def Miri.Concurrency.ThreadManager.thread? (manager : ThreadManager) (id : ThreadId) : Option ThreadRecord

Equations

• manager.thread? id = Miri.Concurrency.ThreadManager.get?✝ manager.threads id.toNat

def Miri.Concurrency.ThreadManager.threadIdTryFrom (manager : ThreadManager) (rawId : Nat) : Except ThreadError ThreadId

Equations

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

def Miri.Concurrency.ThreadManager.setActiveThread (manager : ThreadManager) (id : ThreadId) : Except ThreadError (ThreadManager × ThreadId)

Equations

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

def Miri.Concurrency.ThreadManager.createThread (manager : ThreadManager) (onStackEmpty : Nat) : Except ThreadError (ThreadManager × ThreadId)

create_thread allocates the next never-reused ID and an enabled, joinable thread whose stack-empty callback is retained.

Equations

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

def Miri.Concurrency.ThreadManager.setThreadName (manager : ThreadManager) (id : ThreadId) (name : List UInt8) : Except ThreadError ThreadManager

Equations

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

def Miri.Concurrency.ThreadManager.detachThread (manager : ThreadManager) (id : ThreadId) (allowTerminatedJoined : Bool) : Except ThreadError ThreadManager

Detach follows the two source branches, including Windows' allowance for detaching an already-terminated joined thread exactly once.

Equations

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

def Miri.Concurrency.ThreadManager.markJoined (manager : ThreadManager) (id : ThreadId) : Except ThreadError ThreadManager

Equations

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

def Miri.Concurrency.ThreadManager.blockThread (manager : ThreadManager) (reason : BlockReason) (deadline : Option ThreadDeadline) (callbackToken : Nat) : Except ThreadError ThreadManager

Equations

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

def Miri.Concurrency.ThreadManager.blockThreadWithRuntimeConstraints (manager : ThreadManager) (reason : BlockReason) (deadline : Option ThreadDeadline) (callbackToken : Nat) (communicate : Bool) : Except BlockThreadSourceError ThreadManager

Equations

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

def Miri.Concurrency.ThreadManager.unblockThread (manager : ThreadManager) (id : ThreadId) (reason : BlockReason) (kind : UnblockKind := UnblockKind.Ready) : Except ThreadError (ThreadManager × UnblockCallbackObligation)

Put a blocked thread back in Enabled state and switch to it for execution. The callback is returned as an obligation, not executed or assumed successful.

Equations

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

def Miri.Concurrency.ThreadManager.restoreAfterCallback (managerAfterCallback : ThreadManager) (obligation : UnblockCallbackObligation) : ThreadManager

Successful callback return restores the previous active thread while preserving every state change made by the supplied callback execution.

Equations

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

def Miri.Concurrency.ThreadManager.callbackFailedState (managerAfterFailure : ThreadManager) (_obligation : UnblockCallbackObligation) : ThreadManager

The callback's exceptional return preserves its post-call machine state; the source's ? returns before restoring the old active thread.

Equations

• managerAfterFailure.callbackFailedState _obligation = managerAfterFailure

def Miri.Concurrency.ThreadManager.yield (manager : ThreadManager) : ThreadManager

set_active_thread accepts any existing ID, including blocked or terminated IDs; callers own source-level scheduling conditions.

Equations

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

def Miri.Concurrency.ThreadManager.beginTerminateActive (manager : ThreadManager) (forExit : Bool) (stackEmptyResult : StackEmptyCallbackResult) : Except ThreadTerminationError (ThreadManager × ThreadTerminationObligation)

Begin Miri's termination path after the stack-empty callback has returned Poll::Ready. The state is marked Terminated first and TLS entries are removed from the manager exactly as the source's retain does; cleanup itself remains an explicit ordered obligation.

Equations

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

def Miri.Concurrency.ThreadManager.completeTlsCleanup (managerAfterMarking : ThreadManager) (obligation : ThreadTerminationObligation) (results : List TlsCleanupResult) : Except ThreadTerminationError ThreadTerminationContinuation

Continue only when the external interpreter reports exactly the source TLS action for each pointer. A failed deallocation stops before the data-race termination hook and before joiner callbacks, as in Miri's ? propagation.

Equations

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