Lazy compiler-global conversion, pinned machine.rs:967–1032,1678–1693. Byte backing is acquired before relocation conversion. Global race clocks start at zero on the main thread, independently of the accessing thread. The returned owned allocation is cached by MemoryLifecycle, never by this callback.

@[reducible, inline]

abbrev Miri.Interpreter.GlobalAllocationMachine.M (K User A : Type) : Type

Equations

• Miri.Interpreter.GlobalAllocationMachine.M = Miri.Interpreter.PlaceMachine.MachineM

structure Miri.Interpreter.GlobalAllocationMachine.Bytes (K U : Type) : Type

Real storage effects; native preparation must reserve the actual backing identity used by global-root address resolution. Managed storage explicitly returns no host owner. Release runs on failed conversion, like Rust's drop.

• prepare : Memory.AllocId → Array UInt8 → ABI.Align → M K U (Array UInt8 × Option Memory.NativeBufferOwnership)
• commit : Memory.NativeBufferOwnership → Array UInt8 → ABI.Align → M K U Unit
• release : Memory.NativeBufferOwnership → ABI.Size → ABI.Align → M K U Unit

def Miri.Interpreter.GlobalAllocationMachine.managedBytes {K U : Type} : Bytes K U

The managed backend's semantic bytes have no native ownership. Receiving a native owner here is an inconsistent backend construction, not a no-op.

Equations

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

structure Miri.Interpreter.GlobalAllocationMachine.Leaves (K U : Type) : Type

• bytes : Bytes K U
• globalRootPointer : Memory.Pointer Memory.CtfeProvenance → M K U (Memory.Pointer Memory.Provenance)
• diagnostic : Memory.AllocId → ABI.Size → ABI.Align → M K U Unit

def Miri.Interpreter.GlobalAllocationMachine.initExtra {K U P : Type} [DecidableEq K] (extras : MemoryExtras.Hooks K U P) (diagnostic : Memory.AllocId → ABI.Size → ABI.Align → M K U Unit) (id : Memory.AllocId) (size : ABI.Size) (align : ABI.Align) : M K U TreeBorrows.BorrowTree

Equations

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

def Miri.Interpreter.GlobalAllocationMachine.init {K U P : Type} [DecidableEq K] (extras : MemoryExtras.Hooks K U P) (leaves : Leaves K U) (id : Memory.AllocId) (size : ABI.Size) (align : ABI.Align) : M K U TreeBorrows.BorrowTree

Global and TLS kinds share this source zero/main-thread race category; both may leak and neither stores an allocation span (machine.rs:222–239).

Equations

• Miri.Interpreter.GlobalAllocationMachine.init extras leaves id size align = Miri.Interpreter.GlobalAllocationMachine.initExtra extras leaves.diagnostic id size align

def Miri.Interpreter.GlobalAllocationMachine.adjust {K U P : Type} [DecidableEq K] (target : ABI.TargetDataLayout) (extras : MemoryExtras.Hooks K U P) (leaves : Leaves K U) (id : Memory.AllocId) (source : Memory.Allocation) : M K U (Memory.AdjustedGlobalAllocation Memory.Provenance TreeBorrows.BorrowTree)

Equations

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

def Miri.Interpreter.GlobalAllocationMachine.hooks {K U P : Type} [DecidableEq K] (target : ABI.TargetDataLayout) (extras : MemoryExtras.Hooks K U P) (leaves : Leaves K U) (initializer : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K → PlaceMachine.AccessState K U → Nat → Memory.GlobalMemoryHookResult Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K U) Memory.Allocation) : Memory.GlobalAllocationHooks Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K U)

Equations

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

def Miri.Interpreter.GlobalAllocationMachine.ensure {K U : Type} [DecidableEq K] (globalKind : K) (hooks : Memory.GlobalAllocationHooks Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K U)) (id : Memory.AllocId) : MachineHooks.M K U Unit

Driver used by ensureTreeExtra. It follows the same lazy conversion/cache path as ordinary reads; typed callback failures survive the string boundary.

Equations

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