Object lifecycle from pinned shims/unix/sync.rs:1–529. Compiler initializer bytes/layouts and actual memory operations are mandatory queries.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.PthreadObjects.Kind : Type

• mutex : Kind
• rwlock : Kind
• condvar : Kind
• semaphore : Kind

@[instance_reducible]

instance Miri.Interpreter.PthreadObjects.instDecidableEqKind : DecidableEq Kind

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PthreadObjects.instReprKind : Repr Kind

Equations

• Miri.Interpreter.PthreadObjects.instReprKind = { reprPrec := Miri.Interpreter.PthreadObjects.instReprKind.repr }

def Miri.Interpreter.PthreadObjects.instReprKind.repr : Kind → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.PthreadObjects.MutexKind : Type

• Normal : MutexKind
• Default : MutexKind
• Recursive : MutexKind
• ErrorCheck : MutexKind

@[instance_reducible]

instance Miri.Interpreter.PthreadObjects.instDecidableEqMutexKind : DecidableEq MutexKind

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PthreadObjects.instReprMutexKind : Repr MutexKind

Equations

• Miri.Interpreter.PthreadObjects.instReprMutexKind = { reprPrec := Miri.Interpreter.PthreadObjects.instReprMutexKind.repr }

def Miri.Interpreter.PthreadObjects.instReprMutexKind.repr : MutexKind → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.PthreadObjects.Clock : Type

• realTime : Clock
• monotonic : Clock

@[instance_reducible]

instance Miri.Interpreter.PthreadObjects.instDecidableEqClock : DecidableEq Clock

Equations

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

def Miri.Interpreter.PthreadObjects.instReprClock.repr : Clock → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PthreadObjects.instReprClock : Repr Clock

Equations

• Miri.Interpreter.PthreadObjects.instReprClock = { reprPrec := Miri.Interpreter.PthreadObjects.instReprClock.repr }

inductive Miri.Interpreter.PthreadObjects.Payload (R : Type) : Type

• mutex {R : Type} (ref : R) (kind : MutexKind) : Payload R
• rwlock {R : Type} (ref : R) : Payload R
• condvar {R : Type} (ref : R) (clock : Clock) : Payload R
• semaphore {R : Type} (ref : R) : Payload R

def Miri.Interpreter.PthreadObjects.Payload.kind {R : Type} : Payload R → Kind

Equations

• (Miri.Interpreter.PthreadObjects.Payload.mutex ref kind).kind = Miri.Interpreter.PthreadObjects.Kind.mutex
• (Miri.Interpreter.PthreadObjects.Payload.rwlock ref).kind = Miri.Interpreter.PthreadObjects.Kind.rwlock
• (Miri.Interpreter.PthreadObjects.Payload.condvar ref clock).kind = Miri.Interpreter.PthreadObjects.Kind.condvar
• (Miri.Interpreter.PthreadObjects.Payload.semaphore ref).kind = Miri.Interpreter.PthreadObjects.Kind.semaphore

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

• os : String
• sync : Concurrency.SyncObject.Hooks S (Payload R)
• runtime : Concurrency.SyncRuntime.Hooks S R Int32 (MPlaceTy Memory.Provenance)
• deref : OpTy Memory.Provenance → Kind → M S (MPlaceTy Memory.Provenance)
• initializer : String → M S (MPlaceTy Memory.Provenance)
• readBytes : MPlaceTy Memory.Provenance → ABI.Size → M S ByteArray
• readInitByte : MPlaceTy Memory.Provenance → ABI.Size → M S UInt8
• sanity : Kind → M S Bool
• putSanity : Kind → Bool → M S Unit
• newMutex : M S R
• newRwlock : M S R
• newCondvar : M S R
• newSemaphore : UInt64 → M S R

def Miri.Interpreter.PthreadObjects.initOffset {S R : Type} (h : Hooks S R) (kind : Kind) : M S ABI.Size

Equations

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

def Miri.Interpreter.PthreadObjects.mutexKindFromInitializer {S R : Type} (h : Hooks S R) (object : MPlaceTy Memory.Provenance) : M S MutexKind

Equations

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

def Miri.Interpreter.PthreadObjects.get {S R : Type} (h : Hooks S R) (kind : Kind) (operand : OpTy Memory.Provenance) : M S (Payload R)

Equations

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

def Miri.Interpreter.PthreadObjects.createAt {S R : Type} (h : Hooks S R) (object : MPlaceTy Memory.Provenance) (payload : Payload R) : M S Unit

Equations

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

def Miri.Interpreter.PthreadObjects.create {S R : Type} (h : Hooks S R) (operand : OpTy Memory.Provenance) (payload : Payload R) : M S Unit

Equations

• Miri.Interpreter.PthreadObjects.create h operand payload = do let __do_lift ← h.deref operand payload.kind Miri.Interpreter.PthreadObjects.createAt h __do_lift payload