Pinned Miri thread.rs::get_or_create_thread_local_alloc. The actual manager TLS map remains authoritative; a typed side table supplies its opaque pointer tokens. Allocation copying, relocation adjustment, mutability, fresh identity, kind, insertion hooks and failure-state ordering follow the source. Host byte storage and compiler queries are required leaves, not successful defaults.

inductive Miri.Interpreter.ThreadLocalError : Type

• query (message : String) : ThreadLocalError
• foreignStatic (definition : MIR.DefId) : ThreadLocalError
• allocationAdjustment (error : Memory.AllocationAdjustError ThreadLocalError) : ThreadLocalError
• insertion (error : Memory.MemoryLifecycleError) : ThreadLocalError
• missingPointerToken (token : Nat) : ThreadLocalError
• duplicateTlsEntry : ThreadLocalError
• pointerIdentityMismatch : ThreadLocalError
• changedByteCopy : ThreadLocalError

partial def Miri.Interpreter.instReprThreadLocalError.repr : ThreadLocalError → Nat → Std.Format

@[instance_reducible]

instance Miri.Interpreter.instReprThreadLocalError : Repr ThreadLocalError

Equations

• Miri.Interpreter.instReprThreadLocalError = { reprPrec := Miri.Interpreter.instReprThreadLocalError.repr }

structure Miri.Interpreter.ThreadLocalEntry (P : Type) : Type

• definition : MIR.DefId
• thread : Concurrency.ThreadId
• runtimeId : Memory.AllocId
• pointer : Memory.Pointer P

structure Miri.Interpreter.ThreadLocalState (P E H : Type) : Type

• memory : Memory.MemoryState P E Memory.MiriMemoryKind
• hooks : H
• manager : Concurrency.ThreadManager
• pointers : Array (ThreadLocalEntry P)

@[reducible, inline]

abbrev Miri.Interpreter.ThreadLocalM (P E H A : Type) : Type

Equations

• Miri.Interpreter.ThreadLocalM P E H A = EStateM Miri.Interpreter.ThreadLocalError (Miri.Interpreter.ThreadLocalState P E H) A

structure Miri.Interpreter.ThreadLocalQueries (P E H Params : Type) : Type

• isForeignItem : MIR.DefId → ThreadLocalM P E H Bool
• defaultAllocationParams : ThreadLocalM P E H Params
• evaluateStaticInitializer : MIR.DefId → ThreadLocalM P E H Memory.Allocation
• copyBytes : Params → Array UInt8 → ABI.Align → ThreadLocalM P E H (Array UInt8)
• globalRootPointer : Memory.Pointer Memory.CtfeProvenance → ThreadLocalM P E H (Memory.Pointer P)
• maximumAllocationSize : ThreadLocalM P E H ABI.Size

  Source max_size_of_val query, including any machine-specific limit.

• globalKind : Option (Memory.MemoryKind Memory.MiriMemoryKind)
• synchronizeMemory : Memory.MemoryState P E Memory.MiriMemoryKind → H → H
• initExtra : Memory.MemoryState P E Memory.MiriMemoryKind → H → Memory.AllocId → Memory.MemoryKind Memory.MiriMemoryKind → ABI.Size → ABI.Align → Memory.MemoryStateHookResult P E Memory.MiriMemoryKind H E
• adjustAllocationRoot : Memory.MemoryState P E Memory.MiriMemoryKind → H → Memory.AllocId → Memory.MemoryKind Memory.MiriMemoryKind → Memory.MemoryStateHookResult P E Memory.MiriMemoryKind H (Memory.Pointer P)

def Miri.Interpreter.ThreadLocalState.pointerForToken {P E H : Type} (state : ThreadLocalState P E H) (token : Nat) : Except ThreadLocalError (Memory.Pointer P)

Recover real pointers for the existing thread manager's TLS visitation and cleanup protocol. A missing typed token is an obligation, never a dropped root.

Equations

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

def Miri.Interpreter.ThreadLocalState.roots {P E H : Type} (state : ThreadLocalState P E H) : Except ThreadLocalError (Array (Memory.Pointer P))

Equations

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

def Miri.Interpreter.getOrCreateThreadLocal {P E H Params : Type} [Memory.PointerProvenance P] (target : ABI.RuntimeTargetDataLayout) (queries : ThreadLocalQueries P E H Params) (definition : MIR.DefId) : ThreadLocalM P E H (Memory.Pointer P)

The cached branch performs no compiler query or machine allocation work. The new branch copies first, then makes the allocation mutable and inserts it as MiriMemoryKind::Tls. Only successful root adjustment publishes the TLS map entry; failures retain any earlier allocation and hook state changes.

Equations

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