Data-only source synchronization captures and execution. Every constructor corresponds to a pinned sync.rs or OS-shim FnOnce capture; no MIR/program IR or closure-valued state is introduced. Object and callback identities are source Rc/Box identities supplied by the one owning machine arena.

@[reducible, inline]

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

Equations

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

structure Miri.Concurrency.TypedSyncRuntime.Ref : Type

• index : Nat

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

Equations

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

@[instance_reducible]

instance Miri.Concurrency.TypedSyncRuntime.instDecidableEqRef : DecidableEq Ref

Equations

• Miri.Concurrency.TypedSyncRuntime.instDecidableEqRef = Miri.Concurrency.TypedSyncRuntime.instDecidableEqRef.decEq

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

Equations

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

@[instance_reducible]

instance Miri.Concurrency.TypedSyncRuntime.instReprRef : Repr Ref

Equations

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

@[reducible, inline]

abbrev Miri.Concurrency.TypedSyncRuntime.Dest : Type

Equations

• Miri.Concurrency.TypedSyncRuntime.Dest = Miri.Interpreter.MPlaceTy Miri.Memory.Provenance

inductive Miri.Concurrency.TypedSyncRuntime.Object : Type

• mutex (value : MutexState) : Object
• rwlock (value : RwLockState) : Object
• condvar (value : CondvarState) : Object
• semaphore (value : SemaphoreState) : Object
• futex (value : FutexState) : Object
• initOnce (value : InitOnce.State) : Object

@[reducible, inline]

abbrev Miri.Concurrency.TypedSyncRuntime.User : Type

Exact OS callback captures. Constants and errno writes are evaluated when source executes the callback, not eagerly while it is being registered.

Equations

• Miri.Concurrency.TypedSyncRuntime.User = Miri.Concurrency.SyncRuntime.UserCapture Miri.Concurrency.TypedSyncRuntime.Ref Miri.Concurrency.TypedSyncRuntime.Dest

@[reducible, inline]

abbrev Miri.Concurrency.TypedSyncRuntime.Capture : Type

Equations

• Miri.Concurrency.TypedSyncRuntime.Capture = Miri.Concurrency.SyncRuntime.Capture Miri.Concurrency.TypedSyncRuntime.Ref Int32 Miri.Concurrency.TypedSyncRuntime.Dest

structure Miri.Concurrency.TypedSyncRuntime.Storage : Type

• objects : Array Object
• callbacks : Array (Nat × Capture)
• pthreadMutexSanity : Bool
• pthreadRwlockSanity : Bool
• pthreadCondvarSanity : Bool
• pthreadSemaphoreSanity : Bool
• macFutexSettings : Array (Ref × UInt64 × Bool)

structure Miri.Concurrency.TypedSyncRuntime.Hooks (S : Type) : Type

• handler : SyncClockHandler
• usizeBits : Nat
• communicate : Bool
• global : M S (Option GlobalState)
• putGlobal : Option GlobalState → M S Unit
• threads : M S ThreadManager
• putThreads : ThreadManager → M S Unit
• get : Ref → M S Object
• put : Ref → Object → M S Unit
• register : Capture → M S Nat
• take : Nat → M S Capture
• cancel : Nat → M S Unit
• writeScalar : Int32 → Dest → M S Unit
• writeInt : Int → Dest → M S Unit
• errnoNegOne : String → Dest → M S Unit
• windowsTrue : M S Int32
• windowsFalse : M S Int32
• windowsTimeoutError : M S Unit
• error : SyncError → Interpreter.StepError

def Miri.Concurrency.TypedSyncRuntime.mutexLock {S : Type} (h : Hooks S) (ref : Ref) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.readerLock {S : Type} (h : Hooks S) (ref : Ref) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.writerLock {S : Type} (h : Hooks S) (ref : Ref) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.mutexEnqueue {S : Type} (h : Hooks S) (ref : Ref) (result : Option (Int32 × Dest)) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.enqueueReader {S : Type} (h : Hooks S) (ref : Ref) (value : Int32) (dest : Dest) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.enqueueWriter {S : Type} (h : Hooks S) (ref : Ref) (value : Int32) (dest : Dest) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.tryBegin {S : Type} (h : Hooks S) (ref : Ref) (pending dest : Dest) : M S Bool

Equations

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

def Miri.Concurrency.TypedSyncRuntime.executeUser {S : Type} (h : Hooks S) (user : User) (kind : UnblockKind) : M S Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.TypedSyncRuntime.executeUser h (Miri.Concurrency.SyncRuntime.UserCapture.pthreadSemaphore timed dest) Miri.Concurrency.UnblockKind.Ready = h.writeScalar 0 dest
• Miri.Concurrency.TypedSyncRuntime.executeUser h (Miri.Concurrency.SyncRuntime.UserCapture.futexErrno dest) Miri.Concurrency.UnblockKind.Ready = h.writeInt 0 dest
• Miri.Concurrency.TypedSyncRuntime.executeUser h (Miri.Concurrency.SyncRuntime.UserCapture.futexErrno dest) Miri.Concurrency.UnblockKind.TimedOut = h.errnoNegOne "ETIMEDOUT" dest
• Miri.Concurrency.TypedSyncRuntime.executeUser h (Miri.Concurrency.SyncRuntime.UserCapture.windowsAddress dest) Miri.Concurrency.UnblockKind.Ready = h.writeScalar 1 dest
• Miri.Concurrency.TypedSyncRuntime.executeUser h (Miri.Concurrency.SyncRuntime.UserCapture.macAddress ref dest) Miri.Concurrency.UnblockKind.TimedOut = h.errnoNegOne "ETIMEDOUT" dest

def Miri.Concurrency.TypedSyncRuntime.semaphoreDecrement {S : Type} (h : Hooks S) (ref : Ref) (deadline : Option ThreadDeadline) (user : User) : M S Unit

A retry after Ready is a fresh blocking callback, not recursive execution of an opaque closure. The source deadline and user captures are retained.

Equations

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

def Miri.Concurrency.TypedSyncRuntime.futexWait {S : Type} (h : Hooks S) (ref : Ref) (bitset : UInt32) (deadline : Option ThreadDeadline) (user : User) : M S Unit

Equations

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

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

Consume Box<Self> before the first body effect; callback failure cannot restore that box or the previously active thread.

Equations

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

def Miri.Concurrency.TypedSyncRuntime.mutexUnlock {S : Type} (h : Hooks S) (ref : Ref) : M S MutexUnlockResult

Equations

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

def Miri.Concurrency.TypedSyncRuntime.readerUnlock {S : Type} (h : Hooks S) (ref : Ref) : M S Bool

Equations

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

def Miri.Concurrency.TypedSyncRuntime.writerUnlock {S : Type} (h : Hooks S) (ref : Ref) : M S Bool

Equations

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

def Miri.Concurrency.TypedSyncRuntime.condvarWait {S : Type} (h : Hooks S) (ref mutex : Ref) (deadline : Option ThreadDeadline) (success timeout : Int32) (dest : Dest) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.condvarSignal {S : Type} (h : Hooks S) (ref : Ref) : M S Bool

Equations

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

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

Equations

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

def Miri.Concurrency.TypedSyncRuntime.semaphoreIncrement {S : Type} (h : Hooks S) (ref : Ref) : M S Bool

Equations

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

def Miri.Concurrency.TypedSyncRuntime.begin {S : Type} (h : Hooks S) (ref : Ref) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.enqueueInitOnce {S : Type} (h : Hooks S) (ref : Ref) (user : User) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.complete {S : Type} (h : Hooks S) (ref : Ref) : M S Unit

Equations

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

def Miri.Concurrency.TypedSyncRuntime.fail {S : Type} (h : Hooks S) (ref : Ref) : M S Unit

Equations

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