Canonical pthread lifecycles and thread-name byte effects. Pointer/ABI compiler services remain explicit; create and join invoke actual ThreadMachine.
def
Miri.Interpreter.UnixThreadMachine.bind
{K U C O X F A Aff : Type}
[DecidableEq K]
(thread : ThreadMachine.Hooks K U C O X F A Aff)
(access : PlaceMachine.AccessConfig K (ThreadStacks.Storage U))
(choice : C)
(cNonUnwindAbi : X)
(reuseClock : Option Concurrency.VectorIdx)
(misalignment : Memory.Pointer (Option Memory.Provenance) → ABI.Align → ThreadStacks.M K U (Option Memory.Misalignment))
(base : UnixThread.Hooks (ThreadStacks.State K U))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixThreadMachine.bindStrings
{S D MD B I : Type}
(strings : MemoryShims.Hooks Memory.Provenance S D MD B I)
(scanBudget : Nat)
(base : UnixThread.Hooks S)
:
Keep the required source C-string scan plus second full initialized read.
Equations
- One or more equations did not get rendered due to their size.