Complete pinned unix/freebsd/sync.rs _umtx_op WAIT/WAKE policy.

@[reducible, inline]

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

Equations

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

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

• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readI32 : OpTy Memory.Provenance → M S Int32
• readUsize : OpTy Memory.Provenance → M S UInt64
• libcI32 : String → M S Int32
• libcU32 : String → M S UInt32
• layout : String → M S LocalLayout
• place : Memory.Pointer (Option Memory.Provenance) → LocalLayout → M S (MPlaceTy Memory.Provenance)
• project : MPlaceTy Memory.Provenance → Nat → M S (MPlaceTy Memory.Provenance)
• readPlaceU32 : MPlaceTy Memory.Provenance → M S UInt32
• readPlaceScalar : MPlaceTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• readTimespec : MPlaceTy Memory.Provenance → M S (Option Clock.Duration)
• parseClockId : Memory.Scalar Memory.Provenance → M S (Option Clock.TimeoutClock)
• noIsolation : String → M S Unit
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• seqCstFence : M S Unit
• readAcquireBits : MPlaceTy Memory.Provenance → M S ABI.U128
• metadata : Concurrency.SyncObject.MetadataHooks S R
• newFutex : M S R
• runtime : Concurrency.SyncRuntime.Hooks S R Int32 (MPlaceTy Memory.Provenance)
• timeout : Clock.TimeoutClock → Clock.TimeoutStyle → Clock.Duration → M S Concurrency.ThreadDeadline
• errnoNegOne : String → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• hostUsizeBits : Nat

structure Miri.Interpreter.FreeBsdSync.UmtxTime : Type

• duration : Clock.Duration
• absolute : Bool
• clock : Clock.TimeoutClock

def Miri.Interpreter.FreeBsdSync.readUmtxTime {S R : Type} (h : Hooks S R) (place : MPlaceTy Memory.Provenance) : M S (Option UmtxTime)

Equations

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

def Miri.Interpreter.FreeBsdSync.operation {S R : Type} (h : Hooks S R) (obj op value uaddr uaddr2 : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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