Pinned unix/thread.rs, including actual create/join/detach/name policy. The pthread ABI type is always a compiler query, never an assumed host integer.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixThread.NameResult : Type

• ok : NameResult
• tooLong : NameResult

@[instance_reducible]

instance Miri.Interpreter.UnixThread.instDecidableEqNameResult : DecidableEq NameResult

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixThread.instReprNameResult : Repr NameResult

Equations

• Miri.Interpreter.UnixThread.instReprNameResult = { reprPrec := Miri.Interpreter.UnixThread.instReprNameResult.repr }

def Miri.Interpreter.UnixThread.instReprNameResult.repr : NameResult → Nat → Std.Format

Equations

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

structure Miri.Interpreter.UnixThread.Hooks (S : Type) : Type

• pthreadLayout : M S LocalLayout
• unitPointerLayout : M S LocalLayout
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readImmediate : OpTy Memory.Provenance → M S (RvalueImmTy Memory.Provenance)
• dereference : OpTy Memory.Provenance → LocalLayout → M S (MPlaceTy Memory.Provenance)
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• scalarPointer : Memory.Scalar Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• scalarUsize : Memory.Scalar Memory.Provenance → M S UInt64
• readCString : Memory.Pointer (Option Memory.Provenance) → M S ByteArray
• writeCString : ByteArray → Memory.Pointer (Option Memory.Provenance) → UInt64 → M S (Bool × UInt64)
• threads : M S Concurrency.ThreadManager
• putThreads : Concurrency.ThreadManager → M S Unit
• start : Option (MPlaceTy Memory.Provenance) → Memory.Pointer (Option Memory.Provenance) → RvalueImmTy Memory.Provenance → LocalLayout → M S Unit
• join : Concurrency.ThreadId → Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• detach : Concurrency.ThreadId → M S Unit
• hostUsizeBits : Nat

def Miri.Interpreter.UnixThread.create {S : Type} (h : Hooks S) (thread _attr start argument : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.UnixThread.join {S : Type} (h : Hooks S) (thread result : 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.UnixThread.detach {S : Type} (h : Hooks S) (thread : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.UnixThread.self {S : Type} (h : Hooks S) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.UnixThread.setName {S : Type} (h : Hooks S) (thread name : Memory.Scalar Memory.Provenance) (maximum : UInt64) (truncate : Bool) : M S NameResult

Equations

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

def Miri.Interpreter.UnixThread.getName {S : Type} (h : Hooks S) (thread output length : Memory.Scalar Memory.Provenance) (truncate : Bool) : M S NameResult

Equations

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

def Miri.Interpreter.UnixThread.schedYield {S : Type} (h : Hooks S) : M S Unit

Equations

• Miri.Interpreter.UnixThread.schedYield h = do let __do_lift ← h.threads h.putThreads __do_lift.yield