Pinned unix/macos/sync.rs. Atomic operations, compiler layouts and actual object allocation remain required effects; clock/queue/object policy is here.

@[reducible, inline]

abbrev Miri.Interpreter.MacOsSync.M (σ α : Type) : Type

Equations

• Miri.Interpreter.MacOsSync.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.MacOsSync.Unfair (R : Type) : Type

• active {R : Type} (ref : R) : Unfair R
• permanentlyLocked {R : Type} : Unfair R

structure Miri.Interpreter.MacOsSync.Semaphore (R : Type) : Type

• ref : R
• initial : UInt64

inductive Miri.Interpreter.MacOsSync.Timeout : Type

• none : Timeout
• relative (clock duration : OpTy Memory.Provenance) : Timeout
• absolute (clock duration : OpTy Memory.Provenance) : Timeout

structure Miri.Interpreter.MacOsSync.Hooks (S R : Type) : Type

• endian : ABI.Endian
• runtime : Concurrency.SyncRuntime.Hooks S R Int32 (MPlaceTy Memory.Provenance)
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readImmediate : OpTy Memory.Provenance → M S (RvalueImmTy Memory.Provenance)
• readUsize : OpTy Memory.Provenance → M S UInt64
• readIsize : OpTy Memory.Provenance → M S Int
• readU32 : OpTy Memory.Provenance → M S UInt32
• readU64 : OpTy Memory.Provenance → M S UInt64
• readI64 : OpTy Memory.Provenance → M S Int64
• libcU32 : String → M S UInt32
• timeout : Clock.TimeoutStyle → Clock.Duration → M S Concurrency.ThreadDeadline
• absoluteDeadline : UInt64 → M S Concurrency.ThreadDeadline

  epoch().add_lossy(Duration::from_nanos(value)).

• timeAfter : UInt64 → M S Nat

  now().add_lossy(delta).duration_since(epoch()), exact host/virtual clock.

• readAcquireBits : Memory.Pointer (Option Memory.Provenance) → UInt64 → M S ABI.U128
• seqCstFence : M S Unit
• futexMetadata : Concurrency.SyncObject.MetadataHooks S R
• newFutex : UInt64 → Bool → M S R
• settings : R → M S (UInt64 × Bool)
• putSettings : R → UInt64 → Bool → M S Unit
• lockMetadata : Concurrency.SyncObject.Hooks S (Unfair R)
• semaphoreMetadata : Concurrency.SyncObject.Hooks S (Semaphore R)
• derefLock : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• derefByte : RvalueImmTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• readLockValue : MPlaceTy Memory.Provenance → M S UInt32
• newMutex : M S R
• newSemaphore : UInt64 → M S R
• allocateRuntimeByte : M S (MPlaceTy Memory.Provenance)
• immediatePointer : RvalueImmTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• deallocateRuntime : Memory.Pointer (Option Memory.Provenance) → M S Unit
• resetLockRelaxed : OpTy Memory.Provenance → M S Unit
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• writeBool : Bool → MPlaceTy Memory.Provenance → M S Unit
• errnoNegOne : String → MPlaceTy Memory.Provenance → M S Unit
• hostUsizeBits : Nat
• semaphoreBudget : Nat

def Miri.Interpreter.MacOsSync.waitAddress {S R : Type} (h : Hooks S R) (address value size flags : OpTy Memory.Provenance) (timeout : Timeout) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.wakeAddress {S R : Type} (h : Hooks S R) (address size flags : OpTy Memory.Provenance) (all : Bool) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.lock {S R : Type} (h : Hooks S R) (op : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.tryLock {S R : Type} (h : Hooks S R) (op : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.unlock {S R : Type} (h : Hooks S R) (op : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.assertOwner {S R : Type} (h : Hooks S R) (op : OpTy Memory.Provenance) (owned : Bool) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.semaphoreCreate {S R : Type} (h : Hooks S R) (value : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.semaphoreWait {S R : Type} (h : Hooks S R) (sem timeout : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.semaphoreSignal {S R : Type} (h : Hooks S R) (sem : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.release {S R : Type} (h : Hooks S R) (sem : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.MacOsSync.dispatchTime {S R : Type} (h : Hooks S R) (when delta : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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