Pinned linux_like/sync.rs syscall policy. Fence/load/comparison is one shim action, so no scheduler preemption is introduced between these events.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.LinuxFutex.ArgType : Type

• u32Pointer : ArgType
• timespecPointer : ArgType
• i32 : ArgType
• u32 : ArgType
• voidPointer : ArgType
• usize : ArgType
• charPointer : ArgType
• sockaddrPointer : ArgType
• socklenPointer : ArgType

@[instance_reducible]

instance Miri.Interpreter.LinuxFutex.instDecidableEqArgType : DecidableEq ArgType

Equations

• Miri.Interpreter.LinuxFutex.instDecidableEqArgType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.LinuxFutex.instReprArgType : Repr ArgType

Equations

• Miri.Interpreter.LinuxFutex.instReprArgType = { reprPrec := Miri.Interpreter.LinuxFutex.instReprArgType.repr }

def Miri.Interpreter.LinuxFutex.instReprArgType.repr : ArgType → Nat → Std.Format

Equations

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

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

• takeArgs : Array ArgType → ShimSignatures.Varargs Memory.Provenance → M S (Array (OpTy Memory.Provenance))
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readI32 : OpTy Memory.Provenance → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• i32Place : Memory.Pointer (Option Memory.Provenance) → M S (MPlaceTy Memory.Provenance)
• libcI32 : String → M S Int32
• timespecPlace : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• readTimespec : MPlaceTy Memory.Provenance → M S (Option Clock.Duration)
• timeout : Clock.TimeoutClock → Clock.TimeoutStyle → Clock.Duration → M S Concurrency.ThreadDeadline
• noIsolation : String → M S Unit
• seqCstFence : M S Unit
• readAcquire : MPlaceTy Memory.Provenance → M S UInt32
• metadata : Concurrency.SyncObject.MetadataHooks S R
• newFutex : M S R
• wait : R → UInt32 → Option Concurrency.ThreadDeadline → MPlaceTy Memory.Provenance → M S Unit
• wake : R → UInt32 → Nat → M S Nat
• errnoNegOne : String → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• writeIsize : Int → MPlaceTy Memory.Provenance → M S Unit

  Source scalar from_target_isize uses target width, not the syscall buffer.

• hostUsizeBits : Nat

def Miri.Interpreter.LinuxFutex.syscall {S R : Type} (h : Hooks S R) (args : ShimSignatures.Varargs Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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