Source concurrency/sync.rs futex wait/wake with an actual optional clock handler and typed FnOnce captures. None never reads or manufactures a global clock. Callback tokens use the owner's shared thread callback identity supply.

@[reducible, inline]

abbrev Miri.Concurrency.FutexRuntime.M (σ α : Type) : Type

Equations

• Miri.Concurrency.FutexRuntime.M = EStateM Miri.Interpreter.StepError

structure Miri.Concurrency.FutexRuntime.Ref : Type

• index : Nat

def Miri.Concurrency.FutexRuntime.instDecidableEqRef.decEq (x✝ x✝¹ : Ref) : Decidable (x✝ = x✝¹)

Equations

• Miri.Concurrency.FutexRuntime.instDecidableEqRef.decEq { index := a } { index := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.FutexRuntime.instDecidableEqRef : DecidableEq Ref

Equations

• Miri.Concurrency.FutexRuntime.instDecidableEqRef = Miri.Concurrency.FutexRuntime.instDecidableEqRef.decEq

def Miri.Concurrency.FutexRuntime.instReprRef.repr : Ref → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.FutexRuntime.instReprRef : Repr Ref

Equations

• Miri.Concurrency.FutexRuntime.instReprRef = { reprPrec := Miri.Concurrency.FutexRuntime.instReprRef.repr }

structure Miri.Concurrency.FutexRuntime.Callback (D : Type) : Type

• futex : Ref
• destination : D

structure Miri.Concurrency.FutexRuntime.Storage (D : Type) : Type

• objects : Array FutexState
• callbacks : Array (Nat × Callback D)

structure Miri.Concurrency.FutexRuntime.Hooks (S D : Type) : Type

• handler : M S SyncClockHandler
• global : M S (Option GlobalState)
• putGlobal : GlobalState → M S Unit
• threads : M S ThreadManager
• putThreads : ThreadManager → M S Unit
• communicate : M S Bool
• futex : Ref → M S FutexState
• putFutex : Ref → FutexState → M S Unit
• register : Callback D → M S Nat
• take : Nat → M S (Callback D)
• cancel : Nat → M S Unit
• unblock : ThreadId → (Nat → UnblockKind → M S Unit) → M S Unit
• ready : D → M S Unit
• timedOut : D → M S Unit
• error : SyncError → Interpreter.StepError

def Miri.Concurrency.FutexRuntime.invoke {S D : Type} (h : Hooks S D) (token : Nat) (kind : UnblockKind) : M S Unit

Box<Self> is consumed before the first callback effect. Ready acquires; timeout removes the active waiter; only then does the syscall result write.

Equations

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

def Miri.Concurrency.FutexRuntime.wait {S D : Type} (h : Hooks S D) (ref : Ref) (bitset : UInt32) (deadline : Option ThreadDeadline) (destination : D) : M S Unit

Enqueue precedes callback creation and source block-thread constraints. A failed block drops the callback but retains the already appended waiter.

Equations

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

def Miri.Concurrency.FutexRuntime.wake {S D : Type} (h : Hooks S D) (ref : Ref) (bitset : UInt32) (count : Nat) : M S Nat

Release precedes extraction, including count=0. All matching removals precede any callback; unblocks execute FIFO with actual stack switching.

Equations

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