Physical pthread TLS bindings share ThreadTlsMachine.Data with the existing TLS destructor loop. No shadow key arena or copied persistent memory is kept.

@[reducible, inline]

abbrev Miri.Interpreter.UnixTlsMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.UnixTlsMachine.M K U A = Miri.Interpreter.MachineHooks.M K U A

structure Miri.Interpreter.UnixTlsMachine.DataAccess (U : Type) : Type

• get : U → ThreadTlsMachine.Data
• put : U → ThreadTlsMachine.Data → U

def Miri.Interpreter.UnixTlsMachine.threadData {U C O X F A Aff : Type} (h : ThreadTlsMachine.Hooks U C O X F A Aff) : DataAccess (ThreadStacks.Storage U)

Reuse precisely the existing destructor engine's arena accessor.

Equations

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

def Miri.Interpreter.UnixTlsMachine.createKey {U K : Type} (a : DataAccess U) (destructor : Option TlsDestructor) (size : ABI.Size) : M K U TlsKey

The source inserts/increments before checking target key width. Both mutations survive exhausted-key-space and subsequent destination-write errors.

Equations

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

def Miri.Interpreter.UnixTlsMachine.deleteKey {U K : Type} (a : DataAccess U) (key : TlsKey) : M K U Unit

Equations

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

def Miri.Interpreter.UnixTlsMachine.load {U K : Type} (a : DataAccess U) (key : TlsKey) (thread : Concurrency.ThreadId) : M K U (Memory.Pointer (Option Memory.Provenance))

Equations

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

def Miri.Interpreter.UnixTlsMachine.store {U K : Type} (a : DataAccess U) (key : TlsKey) (thread : Concurrency.ThreadId) (pointer : Memory.Pointer (Option Memory.Provenance)) : M K U Unit

Equations

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

def Miri.Interpreter.UnixTlsMachine.hooks {K U C Other D B I : Type} [DecidableEq K] (a : DataAccess U) (access : PlaceMachine.AccessConfig K U) (place : PlaceHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra) (choice : C) (functions : FunctionPointers.Hooks K U Other) (spans : AllocationDriver.SpanHooks) (misalignment : Memory.Pointer (Option Memory.Provenance) → ABI.Align → M K U (Option Memory.Misalignment)) (signatures : ShimSignatures.PrimitiveHooks Memory.Provenance (MachineHooks.State K U)) (signature : String → M K U (ABI.FnAbi MIR.TyId)) (keyLayout : M K U LocalLayout) : UnixTlsDispatch.Hooks (MachineHooks.State K U) D B I

Genuine source signature/type/alignment capabilities remain explicit; all scalar, pointer, frame/span and TLS arena operations are source-bound.

Equations

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

def Miri.Interpreter.UnixTlsMachine.fromExecution {K U C Other Extern Host D B I : Type} [DecidableEq K] (a : DataAccess U) (config : ExecutionMachine.Config K U C Other Extern Host) (limits : ExecutionMachine.Limits) (choice : C) (spans : AllocationDriver.SpanHooks) (misalignment : Memory.Pointer (Option Memory.Provenance) → ABI.Align → M K U (Option Memory.Misalignment)) (signatures : ShimSignatures.PrimitiveHooks Memory.Provenance (MachineHooks.State K U)) (signature : String → M K U (ABI.FnAbi MIR.TyId)) (keyLayout : M K U LocalLayout) : UnixTlsDispatch.Hooks (MachineHooks.State K U) D B I

Equations

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