Portable pthread wrappers from pinned shims/unix/sync.rs:532–1151.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.PthreadSync.Constant : Type

• mutexNormal : Constant
• mutexDefault : Constant
• mutexErrorCheck : Constant
• mutexRecursive : Constant
• einval : Constant
• ebusy : Constant
• edeadlk : Constant
• eperm : Constant
• etimedout : Constant
• clockRealtime : Constant

@[instance_reducible]

instance Miri.Interpreter.PthreadSync.instDecidableEqConstant : DecidableEq Constant

Equations

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

def Miri.Interpreter.PthreadSync.instReprConstant.repr : Constant → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PthreadSync.instReprConstant : Repr Constant

Equations

• Miri.Interpreter.PthreadSync.instReprConstant = { reprPrec := Miri.Interpreter.PthreadSync.instReprConstant.repr }

inductive Miri.Interpreter.PthreadSync.Attribute : Type

• mutex : Attribute
• condvar : Attribute

@[instance_reducible]

instance Miri.Interpreter.PthreadSync.instDecidableEqAttribute : DecidableEq Attribute

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PthreadSync.instReprAttribute : Repr Attribute

Equations

• Miri.Interpreter.PthreadSync.instReprAttribute = { reprPrec := Miri.Interpreter.PthreadSync.instReprAttribute.repr }

def Miri.Interpreter.PthreadSync.instReprAttribute.repr : Attribute → Nat → Std.Format

Equations

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

structure Miri.Interpreter.PthreadSync.Hooks (S R Duration : Type) : Type

• objects : PthreadObjects.Hooks S R
• constant : Constant → M S Int32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• attributeRead : OpTy Memory.Provenance → Attribute → ABI.Size → M S Int32
• attributeWrite : OpTy Memory.Provenance → Attribute → ABI.Size → Int32 → M S Unit
• attributeUninit : OpTy Memory.Provenance → Attribute → M S Unit
• objectUninit : OpTy Memory.Provenance → PthreadObjects.Kind → M S Unit
• parseClock : Int32 → M S (Option PthreadObjects.Clock)
• readTimespec : OpTy Memory.Provenance → M S (Option Duration)
• timeout : PthreadObjects.Clock → Bool → Duration → M S Concurrency.ThreadDeadline
• noIsolation : String → M S Unit
• setErrnoAndReturnNeg1 : Constant → MPlaceTy Memory.Provenance → M S Unit
• writeClockId : OpTy Memory.Provenance → Int32 → M S Unit

def Miri.Interpreter.PthreadSync.unchangedKind : Int32

Equations

• Miri.Interpreter.PthreadSync.unchangedKind = 134217728

def Miri.Interpreter.PthreadSync.translateKind {S R T : Type} (h : Hooks S R T) (kind : Int32) : M S PthreadObjects.MutexKind

Equations

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

def Miri.Interpreter.PthreadSync.mutexattrInit {S R T : Type} (h : Hooks S R T) (attr : OpTy Memory.Provenance) : M S Unit

Equations

• Miri.Interpreter.PthreadSync.mutexattrInit h attr = Miri.Interpreter.PthreadSync.attrWrite✝ h attr Miri.Interpreter.PthreadSync.Attribute.mutex Miri.Interpreter.PthreadSync.unchangedKind

def Miri.Interpreter.PthreadSync.mutexattrSettype {S R T : Type} (h : Hooks S R T) (attr : OpTy Memory.Provenance) (kind : Int32) : M S Int32

Equations

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

def Miri.Interpreter.PthreadSync.mutexattrDestroy {S R T : Type} (h : Hooks S R T) (attr : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.PthreadSync.mutexInit {S R T : Type} (h : Hooks S R T) (op attr : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.PthreadSync.mutexLock {S R T : Type} (h : Hooks S R T) (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.PthreadSync.mutexTrylock {S R T : Type} (h : Hooks S R T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.PthreadSync.mutexUnlock {S R T : Type} (h : Hooks S R T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

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

Equations

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

def Miri.Interpreter.PthreadSync.rwlockRead {S R T : Type} (h : Hooks S R T) (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.PthreadSync.rwlockTryread {S R T : Type} (h : Hooks S R T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.PthreadSync.rwlockWrite {S R T : Type} (h : Hooks S R T) (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.PthreadSync.rwlockTrywrite {S R T : Type} (h : Hooks S R T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

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

Equations

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

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

Equations

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

def Miri.Interpreter.PthreadSync.condattrInit {S R T : Type} (h : Hooks S R T) (attr : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.PthreadSync.condattrSetclock {S R T : Type} (h : Hooks S R T) (attr : OpTy Memory.Provenance) (clock : Int32) : M S Int32

Equations

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

def Miri.Interpreter.PthreadSync.condattrGetclock {S R T : Type} (h : Hooks S R T) (attr dest : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.PthreadSync.condattrDestroy {S R T : Type} (h : Hooks S R T) (attr : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.PthreadSync.condInit {S R T : Type} (h : Hooks S R T) (op attr : OpTy Memory.Provenance) : M S Unit

Equations

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

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

Equations

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

def Miri.Interpreter.PthreadSync.broadcastRef {S R T : Type} (budget : Nat) (h : Hooks S R T) (ref : R) : M S Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.PthreadSync.broadcastRef 0 h ref = throw (Miri.Interpreter.StepError.resourceExhaustion "pthread condvar broadcast budget exhausted")

def Miri.Interpreter.PthreadSync.condBroadcast {S R T : Type} (budget : Nat) (h : Hooks S R T) (op : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.PthreadSync.condWait {S R T : Type} (h : Hooks S R T) (op mutex : 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.PthreadSync.condTimedwait {S R T : Type} (h : Hooks S R T) (op mutex timeout : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) (macosRelative : Bool) : M S Unit

Equations

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

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

Equations

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

def Miri.Interpreter.PthreadSync.semInit {S R T : Type} (h : Hooks S R T) (op : OpTy Memory.Provenance) (_pshared : Int32) (value : UInt32) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.PthreadSync.semWait {S R T : Type} (budget : Nat) (h : Hooks S R T) (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.PthreadSync.semTimedwait {S R T : Type} (budget : Nat) (h : Hooks S R T) (op 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.PthreadSync.semPost {S R T : Type} (h : Hooks S R T) (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.PthreadSync.semDestroy {S R T : Type} (h : Hooks S R T) (op : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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