Source: Miri concurrency/thread.rs::get_or_create_thread_local_alloc; rustc GlobalAlloc static queries and eval_static_initializer. Exported TLS initializers are compiler results; each runtime thread receives a fresh mutable copy via the source allocation-adjustment pipeline.

structure Miri.Input.CompilerThreadLocal.Entry : Type

• definition : MIR.DefId
• info : StaticGlobalInfo
• initializer : Option AllocationMemory
• payload : Lean.Json

def Miri.Input.CompilerThreadLocal.ofProgram (program : LoweredProgram) : Except String (Array Entry)

Missing, failed and foreign initializer queries remain explicit failures; no TLS identity is obtained by interpreting diagnostic names.

Equations

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

def Miri.Input.CompilerThreadLocal.forDefinition (program : LoweredProgram) (definition : MIR.DefId) : Except String Entry

Select this exact compiler definition before decoding any initializer. Other TLS declarations, including unsupported initializers, are not demanded by this source lookup. The canonical definition table is unchanged.

Equations

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

def Miri.Input.CompilerThreadLocal.queries {P E H Params : Type} (target : ABI.RuntimeTargetDataLayout) (entries : Array Entry) (machine : Interpreter.ThreadLocalQueries P E H Params) : Interpreter.ThreadLocalQueries P E H Params

Machine leaves supply byte storage, provenance adjustment and allocation hooks. Compiler leaves are replaced by checked evidence keyed by shared DefId. The source runtime cache is checked before any of these query leaves are used.

Equations

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