Internal synchronization state from pinned Miri

This file starts a source-shaped port of upstream/miri-source/src/concurrency/sync.rs (blob 3e848a071e2a67792eada4625b1751eec119b21d). It preserves the state fields of Mutex, RwLock, Condvar, Semaphore, and Futex. The lock transitions below preserve Miri's mutation order and use the existing GlobalState clock hooks and ThreadManager blocking/wakeup state.

Unblock callbacks are returned as explicit obligations. A transition carrying one has not completed the source operation yet. OS object lookup, shim-side memory checks, interpreter callback execution, futex/semaphore callback bodies, and actual memory writes remain outside this component; none is interpreted as success here. This is not a complete Rust concurrency semantics.

inductive Miri.Concurrency.SyncClockHandler : Type

• none : SyncClockHandler
• vectorClocks : SyncClockHandler

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqSyncClockHandler : DecidableEq SyncClockHandler

Equations

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

def Miri.Concurrency.instReprSyncClockHandler.repr : SyncClockHandler → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprSyncClockHandler : Repr SyncClockHandler

Equations

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

structure Miri.Concurrency.MutexState : Type

The actual defaulted state held by Miri's Mutex.

• owner : Option ThreadId
• lockCount : Nat
• queue : List ThreadId
• clock : VClock

@[instance_reducible]

instance Miri.Concurrency.instReprMutexState : Repr MutexState

Equations

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

def Miri.Concurrency.instReprMutexState.repr : MutexState → Nat → Std.Format

Equations

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

structure Miri.Concurrency.RwLockState : Type

The actual defaulted state held by Miri's RwLock. Reader counts use a finite association list as a representation of the source FxHashMap; all operations preserve unique thread keys and positive counts.

• writer : Option ThreadId
• readers : List (ThreadId × Nat)
• writerQueue : List ThreadId
• readerQueue : List ThreadId
• clockUnlocked : VClock
• clockCurrentReaders : VClock

@[instance_reducible]

instance Miri.Concurrency.instReprRwLockState : Repr RwLockState

Equations

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

def Miri.Concurrency.instReprRwLockState.repr : RwLockState → Nat → Std.Format

Equations

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

structure Miri.Concurrency.CondvarState : Type

• waiters : List ThreadId
• clock : VClock

def Miri.Concurrency.instReprCondvarState.repr : CondvarState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprCondvarState : Repr CondvarState

Equations

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

structure Miri.Concurrency.SemaphoreState : Type

• waiters : List ThreadId
• value : UInt64
• clock : VClock

def Miri.Concurrency.instReprSemaphoreState.repr : SemaphoreState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprSemaphoreState : Repr SemaphoreState

Equations

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

structure Miri.Concurrency.FutexWaiter : Type

• thread : ThreadId
• bitset : UInt32

def Miri.Concurrency.instReprFutexWaiter.repr : FutexWaiter → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprFutexWaiter : Repr FutexWaiter

Equations

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

structure Miri.Concurrency.FutexState : Type

• waiters : List FutexWaiter
• clock : VClock

@[instance_reducible]

instance Miri.Concurrency.instReprFutexState : Repr FutexState

Equations

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

def Miri.Concurrency.instReprFutexState.repr : FutexState → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.SyncCallbackProgram : Type

Built-in callback bodies created by the generic sync layer. Pointer and scalar destinations are opaque interpreter tokens; this file never writes through them.

• mutexAcquire : SyncCallbackProgram
• rwlockReaderAcquire (returnValueToken destinationToken : Nat) : SyncCallbackProgram
• rwlockWriterAcquire (returnValueToken destinationToken : Nat) : SyncCallbackProgram
• mutexAcquireAndWrite (returnValueToken destinationToken : Nat) : SyncCallbackProgram
• writeScalar (valueToken destinationToken : Nat) : SyncCallbackProgram
• condvarWait (mutexToken successValueToken timeoutValueToken destinationToken : Nat) : SyncCallbackProgram
• futexWait (userCallbackToken : Nat) : SyncCallbackProgram
• semaphoreWait (userCallbackToken : Nat) : SyncCallbackProgram
• opaqueInterpreterCallback (callbackToken : Nat) : SyncCallbackProgram

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqSyncCallbackProgram : DecidableEq SyncCallbackProgram

Equations

• Miri.Concurrency.instDecidableEqSyncCallbackProgram = Miri.Concurrency.instDecidableEqSyncCallbackProgram.decEq

def Miri.Concurrency.instDecidableEqSyncCallbackProgram.decEq (x✝ x✝¹ : SyncCallbackProgram) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqSyncCallbackProgram.decEq Miri.Concurrency.SyncCallbackProgram.mutexAcquire Miri.Concurrency.SyncCallbackProgram.mutexAcquire = isTrue ⋯
• Miri.Concurrency.instDecidableEqSyncCallbackProgram.decEq Miri.Concurrency.SyncCallbackProgram.mutexAcquire (Miri.Concurrency.SyncCallbackProgram.futexWait userCallbackToken) = isFalse ⋯
• Miri.Concurrency.instDecidableEqSyncCallbackProgram.decEq Miri.Concurrency.SyncCallbackProgram.mutexAcquire (Miri.Concurrency.SyncCallbackProgram.semaphoreWait userCallbackToken) = isFalse ⋯
• Miri.Concurrency.instDecidableEqSyncCallbackProgram.decEq (Miri.Concurrency.SyncCallbackProgram.futexWait userCallbackToken) Miri.Concurrency.SyncCallbackProgram.mutexAcquire = isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instReprSyncCallbackProgram : Repr SyncCallbackProgram

Equations

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

def Miri.Concurrency.instReprSyncCallbackProgram.repr : SyncCallbackProgram → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.SyncError : Type

• globalState (error : GlobalStateError) : SyncError
• missingGlobalClock : SyncError
• threadManager (error : ThreadError) : SyncError
• mutexSourceAssertion (message : String) : SyncError
• mutexLockCountOverflow (bits : Nat) : SyncError
• mutexLockCountUnderflow : SyncError
• rwlockSourceAssertion (message : String) : SyncError
• rwlockReaderMapInvariant : SyncError
• rwlockReaderCountOverflow (bits : Nat) : SyncError
• callbackProgramMismatch (expected actual : SyncCallbackProgram) : SyncError
• callbackUnblockedWithTimeout : SyncError
• callbackReasonMismatch (expected actual : BlockReason) : SyncError
• callbackKindMismatch (expected actual : UnblockKind) : SyncError
• callbackTargetMismatch (expected actual : ThreadId) : SyncError
• callbackReturnedError : SyncError
• blockThreadSource (error : BlockThreadSourceError) : SyncError
• condvarWaitMutexNotLocked : SyncError
• condvarWaitRecursiveMutex (lockCount : Nat) : SyncError
• condvarMutexOwnedByActiveThread (thread : ThreadId) : SyncError
• futexThreadAlreadyWaiting (thread : ThreadId) : SyncError
• semaphoreCounterOverflow : SyncError

@[instance_reducible]

instance Miri.Concurrency.instReprSyncError : Repr SyncError

Equations

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

def Miri.Concurrency.instReprSyncError.repr : SyncError → Nat → Std.Format

Equations

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

def Miri.Concurrency.SyncError.ofClock : SyncClockError → SyncError

Equations

• Miri.Concurrency.SyncError.ofClock Miri.Concurrency.SyncClockError.missingGlobal = Miri.Concurrency.SyncError.missingGlobalClock
• Miri.Concurrency.SyncError.ofClock (Miri.Concurrency.SyncClockError.global error) = Miri.Concurrency.SyncError.globalState error

structure Miri.Concurrency.SyncCallbackRequest : Type

• unblock : UnblockCallbackObligation
• program : SyncCallbackProgram
• remainingWakeups : List ThreadId

def Miri.Concurrency.instReprSyncCallbackRequest.repr : SyncCallbackRequest → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprSyncCallbackRequest : Repr SyncCallbackRequest

Equations

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

structure Miri.Concurrency.SyncTransition (State Value : Type) (G : Type := GlobalState) : Type

A callback request is a live, unresolved action in the source operation. outcome records the component's return value only as a continuation value; callers must run the request and use the corresponding completion function before treating the enclosing operation as returned.

• syncState : State
• global : G
• threads : ThreadManager
• outcome : Except SyncError Value
• callback : Option SyncCallbackRequest
• callbackRegistration : Option (Nat × SyncCallbackProgram)

@[instance_reducible]

instance Miri.Concurrency.instReprSyncTransition {State✝ Value✝ G✝ : Type} [Repr State✝] [Repr Value✝] [Repr G✝] : Repr (SyncTransition State✝ Value✝ G✝)

Equations

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

def Miri.Concurrency.instReprSyncTransition.repr {State✝ Value✝ G✝ : Type} [Repr State✝] [Repr Value✝] [Repr G✝] : SyncTransition State✝ Value✝ G✝ → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.MutexUnlockResult : Type

• returnedNone : MutexUnlockResult
• returnedSome (oldLockCount : Nat) : MutexUnlockResult

def Miri.Concurrency.instDecidableEqMutexUnlockResult.decEq (x✝ x✝¹ : MutexUnlockResult) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqMutexUnlockResult.decEq Miri.Concurrency.MutexUnlockResult.returnedNone Miri.Concurrency.MutexUnlockResult.returnedNone = isTrue ⋯
• Miri.Concurrency.instDecidableEqMutexUnlockResult.decEq Miri.Concurrency.MutexUnlockResult.returnedNone (Miri.Concurrency.MutexUnlockResult.returnedSome oldLockCount) = isFalse ⋯
• Miri.Concurrency.instDecidableEqMutexUnlockResult.decEq (Miri.Concurrency.MutexUnlockResult.returnedSome oldLockCount) Miri.Concurrency.MutexUnlockResult.returnedNone = isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqMutexUnlockResult : DecidableEq MutexUnlockResult

Equations

• Miri.Concurrency.instDecidableEqMutexUnlockResult = Miri.Concurrency.instDecidableEqMutexUnlockResult.decEq

def Miri.Concurrency.instReprMutexUnlockResult.repr : MutexUnlockResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprMutexUnlockResult : Repr MutexUnlockResult

Equations

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

def Miri.Concurrency.SyncTransition.outcomeIsOk {State Value G : Type} (transition : SyncTransition State Value G) : Prop

Equations

• transition.outcomeIsOk = match transition.outcome with | Except.ok a => True | Except.error a => False

def Miri.Concurrency.SyncTransition.hasPendingWork {State Value G : Type} (transition : SyncTransition State Value G) : Bool

Equations

• transition.hasPendingWork = (transition.callback.isSome || transition.callbackRegistration.isSome)

structure Miri.Concurrency.SyncQueuePrefix (S : Type) : Type

Mutation/check queuedResult before constructing a source blocking callback.

• state : S
• outcome : Except SyncError Unit

def Miri.Concurrency.MutexState.queueForBlock (state : MutexState) (threads : ThreadManager) : SyncQueuePrefix MutexState

Equations

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

def Miri.Concurrency.RwLockState.queueReaderForBlock (state : RwLockState) (threads : ThreadManager) : SyncQueuePrefix RwLockState

Equations

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

def Miri.Concurrency.RwLockState.queueWriterForBlock (state : RwLockState) (threads : ThreadManager) : SyncQueuePrefix RwLockState

Equations

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

def Miri.Concurrency.CondvarState.queueForBlock (state : CondvarState) (threads : ThreadManager) (unlocked : MutexUnlockResult) : SyncQueuePrefix CondvarState

Equations

• One or more equations did not get rendered due to their size.
• state.queueForBlock threads Miri.Concurrency.MutexUnlockResult.returnedNone = { state := state, outcome := Except.error Miri.Concurrency.SyncError.condvarWaitMutexNotLocked }

def Miri.Concurrency.FutexState.queueForBlock (state : FutexState) (threads : ThreadManager) (bitset : UInt32) : SyncQueuePrefix FutexState

Equations

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

def Miri.Concurrency.SemaphoreState.queueForBlock (state : SemaphoreState) (threads : ThreadManager) : SyncQueuePrefix SemaphoreState

Equations

• state.queueForBlock threads = { state := { waiters := state.waiters ++ [threads.activeThread], value := state.value, clock := state.clock }, outcome := Except.ok () }

def Miri.Concurrency.MutexState.queueIsEmpty (state : MutexState) : Bool

Equations

• state.queueIsEmpty = state.queue.isEmpty

def Miri.Concurrency.MutexState.lock {G : Type} [SyncClockState G] (state : MutexState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) (usizeBits : Nat := 64) : SyncTransition MutexState Unit G

Exact source operation mutex_lock: owner/count mutations precede acquire_clock, and therefore remain visible if that hook reports an error.

Equations

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

def Miri.Concurrency.MutexState.enqueueAndBlock {G : Type} (state : MutexState) (global : G) (threads : ThreadManager) (callbackToken : Nat) : SyncTransition MutexState Unit G

Exact source operation mutex_enqueue_and_block through block_thread. Queue insertion precedes the source assertion and blocking; the callback registration names the closure body installed by Miri.

Equations

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

def Miri.Concurrency.MutexState.unlock {G : Type} [SyncClockState G] (state : MutexState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition MutexState MutexUnlockResult G

Exact source operation mutex_unlock. A woken thread is enabled and made active by unblockThread; the callback must then be completed with finishMutexAcquireCallback before the source operation has returned.

Equations

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

def Miri.Concurrency.finishMutexAcquireCallback {G : Type} [SyncClockState G] (state : MutexState) (global : G) (threadsAfterUnblock : ThreadManager) (request : SyncCallbackRequest) (handler : SyncClockHandler) (unlockResult : MutexUnlockResult) (usizeBits : Nat := 64) : SyncTransition MutexState MutexUnlockResult G

Execute the known internal callback installed by mutex_enqueue_and_block: it requires a Ready unblock, asserts that ownership was transferred to an unlocked mutex, acquires the lock/clock, and restores the previously active thread only after normal callback return.

Equations

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

def Miri.Concurrency.finishMutexAcquireAndWriteCallback {G : Type} [SyncClockState G] (state : MutexState) (global : G) (threadsAfterUnblock : ThreadManager) (request : SyncCallbackRequest) (handler : SyncClockHandler) : SyncTransition MutexState Unit G

Continuation used by condvar_reacquire_mutex when the mutex is still owned. It runs Miri's installed callback through lock/clock acquisition, then leaves the captured scalar store as an explicit interpreter obligation.

Equations

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

def Miri.Concurrency.RwLockState.isWriteLocked (state : RwLockState) : Bool

Equations

• state.isWriteLocked = state.writer.isSome

def Miri.Concurrency.RwLockState.isLocked (state : RwLockState) : Bool

Equations

• state.isLocked = (state.writer.isSome || !state.readers.isEmpty)

def Miri.Concurrency.RwLockState.queueIsEmpty (state : RwLockState) : Bool

Equations

• state.queueIsEmpty = (state.writerQueue.isEmpty && state.readerQueue.isEmpty)

def Miri.Concurrency.RwLockState.readerLock {G : Type} [SyncClockState G] (state : RwLockState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) (usizeBits : Nat := 64) : SyncTransition RwLockState Unit G

Exact rwlock_reader_lock state update and following clock acquire.

Equations

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

def Miri.Concurrency.RwLockState.writerLock {G : Type} [SyncClockState G] (state : RwLockState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) : SyncTransition RwLockState Unit G

Exact rwlock_writer_lock state update and following clock acquire.

Equations

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

def Miri.Concurrency.RwLockState.enqueueReaderAndBlock {G : Type} (state : RwLockState) (global : G) (threads : ThreadManager) (callbackToken returnValueToken destinationToken : Nat) : SyncTransition RwLockState Unit G

Queue a reader behind a writer, preserving the source's push-before-assert and block_thread order. The closure's scalar write is an opaque token.

Equations

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

def Miri.Concurrency.RwLockState.enqueueWriterAndBlock {G : Type} (state : RwLockState) (global : G) (threads : ThreadManager) (callbackToken returnValueToken destinationToken : Nat) : SyncTransition RwLockState Unit G

Queue a writer behind an existing reader or writer, using the source's writer queue and callback registration.

Equations

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

def Miri.Concurrency.RwLockState.readerUnlock {G : Type} [SyncClockState G] (state : RwLockState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition RwLockState Bool G

Exact rwlock_reader_unlock ordering. It first removes/decrements the reader entry, then releases and joins the active clock, then transfers the joined-reader clock and wakes one queued writer if the lock becomes free.

Equations

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

def Miri.Concurrency.RwLockState.writerUnlock {G : Type} [SyncClockState G] (state : RwLockState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition RwLockState Bool G

Exact rwlock_writer_unlock: the writer clears ownership before the clock release; queued writers have priority, otherwise all waiting readers are removed from the queue before their callbacks are invoked in FIFO order.

Equations

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

def Miri.Concurrency.RwLockState.continueReaderWakeups {G : Type} (state : RwLockState) (global : G) (threadsAfterCallback : ThreadManager) (request : SyncCallbackRequest) (returnedNormally : Bool) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition RwLockState Bool G

Continue a source loop that is waking the readers drained by rwlock_writer_unlock. The caller must first execute the callback in the previous request and provide its resulting manager.

Equations

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

def Miri.Concurrency.finishRwLockAcquireCallback {G : Type} [SyncClockState G] (state : RwLockState) (global : G) (threadsAfterUnblock : ThreadManager) (request : SyncCallbackRequest) (handler : SyncClockHandler) : SyncTransition RwLockState Unit G

Run the internal callback body installed while a reader/writer waited for an RwLock: acquire the appropriate lock/clock, then expose the source's write_scalar as a pending interpreter action.

Equations

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

def Miri.Concurrency.CondvarState.queueIsEmpty (state : CondvarState) : Bool

Equations

• state.queueIsEmpty = state.waiters.isEmpty

def Miri.Concurrency.CondvarState.blockAfterMutexUnlock {G : Type} (state : CondvarState) (global : G) (threads : ThreadManager) (unlockResult : MutexUnlockResult) (deadline : Option ThreadDeadline) (callbackToken mutexToken successValueToken timeoutValueToken destinationToken : Nat) (communicate : Bool) : SyncTransition CondvarState Unit G

Continue condvar_wait only after mutex_unlock returned successfully with an original count of one. The call preserves the source order: waiter queue insertion, then checked blocking with its timeout constraints.

Equations

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

def Miri.Concurrency.CondvarState.signal {G : Type} [SyncClockState G] (state : CondvarState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition CondvarState Bool G

Exact condvar_signal: release the signal clock before popping a waiter, then unblock at most the FIFO head. The callback stays pending until the interpreter executes the captured condvar/mutex continuation.

Equations

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

def Miri.Concurrency.CondvarState.finishWaitCallback {G : Type} [SyncClockState G] (state : CondvarState) (mutex : MutexState) (global : G) (threadsAfterUnblock : ThreadManager) (request : SyncCallbackRequest) (handler : SyncClockHandler) (mutexToken newMutexCallbackToken : Nat) : SyncTransition (CondvarState × MutexState) Unit G

Execute the internal condvar callback through its source effects. On Ready it acquires the signal clock; on timeout it first removes the waiter. It then reacquires the captured mutex. If another thread owns it, this thread blocks on that mutex with the source lock-and-write callback registered. If the mutex is free, it acquires it and leaves the captured scalar write pending.

Equations

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

def Miri.Concurrency.FutexState.waiterCount (state : FutexState) : Nat

Equations

• state.waiterCount = state.waiters.length

def Miri.Concurrency.FutexState.wait {G : Type} (state : FutexState) (global : G) (threads : ThreadManager) (bitset : UInt32) (deadline : Option ThreadDeadline) (callbackToken userCallbackToken : Nat) (communicate : Bool) : SyncTransition FutexState Unit G

Exact source futex_wait registration: reject a duplicate waiter, append the thread/bitset pair, then apply Miri's timeout checks and block it. Its callback wrapper is retained as an explicit registration for the wake path.

Equations

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

def Miri.Concurrency.FutexState.wake {G : Type} [SyncClockState G] (state : FutexState) (global : G) (threads : ThreadManager) (bitset : UInt32) (count : Nat) (handler : SyncClockHandler) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition FutexState Nat G

Exact futex_wake: release the clock before filtering and removing waiters; the first unblock callback and every continuation are returned explicitly.

Equations

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

def Miri.Concurrency.FutexState.finishWaitCallback {G : Type} [SyncClockState G] (state : FutexState) (global : G) (threadsAfterUnblock : ThreadManager) (request : SyncCallbackRequest) (handler : SyncClockHandler) : SyncTransition FutexState Unit G

Miri's futex wrapper acquires the futex clock on Ready, removes the active waiter on timeout, then invokes the OS-shim callback. That last callback is opaque here and remains pending until the caller supplies its actual result.

Equations

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

def Miri.Concurrency.FutexState.continueWake {G : Type} (state : FutexState) (global : G) (threadsAfterCallback : ThreadManager) (request : SyncCallbackRequest) (wokenCount : Nat) (returnedNormally : Bool) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition FutexState Nat G

Continue the futex_wake source loop only after the previous outer and OS-shim callbacks returned normally. Callback failure stops the loop before active-thread restoration, as Miri's ? propagation does.

Equations

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

def Miri.Concurrency.finishScalarWriteCallback {G State : Type} (state : State) (global : G) (threadsAfterWrite : ThreadManager) (request : SyncCallbackRequest) (writeSucceeded : Bool) : SyncTransition State Unit G

Complete the actual interpreter write_scalar hook at the end of a mutex/rwlock/condvar unblock callback. A failed write preserves the callback's state and active-thread context, matching source ? propagation.

Equations

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

def Miri.Concurrency.finishOpaqueSyncCallback {G State : Type} (syncState : State) (global : G) (threadsAfterCallback : ThreadManager) (request : SyncCallbackRequest) (returnedNormally : Bool) : SyncTransition State Unit G

Complete a callback body whose implementation belongs to an OS shim or the interpreter. The caller supplies the post-callback manager and the actual return status; errors preserve its active-thread state, while normal return restores the previous active thread exactly once.

Equations

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

def Miri.Concurrency.SemaphoreState.queueIsEmpty (state : SemaphoreState) : Bool

Equations

• state.queueIsEmpty = state.waiters.isEmpty

def Miri.Concurrency.SemaphoreState.decrement {G : Type} [SyncClockState G] (state : SemaphoreState) (global : G) (threads : ThreadManager) (deadline : Option ThreadDeadline) (blockCallbackToken userCallbackToken : Nat) (handler : SyncClockHandler) (communicate : Bool) : SyncTransition SemaphoreState Unit G

Exact source semaphore decrement through value update, clock acquire, and callback registration. If the counter is zero, queue insertion precedes checked blocking and the callback remains attached to the thread.

Equations

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

def Miri.Concurrency.SemaphoreState.increment {G : Type} [SyncClockState G] (state : SemaphoreState) (global : G) (threads : ThreadManager) (handler : SyncClockHandler) (callbackRegistry : List (Nat × SyncCallbackProgram) := []) : SyncTransition SemaphoreState Bool G

Equations

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