Allocation-local extras for machine.rs:1695–1838. Clocks remain in MachineHooks: neither the registry nor atomic lenses keep a second clock copy. Sync payloads are typed data; their required interpreter constructs real stateful Object callbacks, avoiding a negative recursive state definition.

@[reducible, inline]

abbrev Miri.Interpreter.MemoryExtras.Machine (K User : Type) : Type

Equations

• Miri.Interpreter.MemoryExtras.Machine = Miri.Interpreter.PlaceMachine.Machine

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.MemoryExtras.Entry (Payload : Type) : Type

• payload : Payload
• deleteOnWrite : Bool
• roots : Array Memory.Provenance

  Captured provenance must be supplied, including references in callbacks.

structure Miri.Interpreter.MemoryExtras.AllocationExtra (Payload : Type) : Type

• weakMemory : Option (Concurrency.StoreBufferAlloc (Memory.Scalar Memory.Provenance))
• sync : Array (ABI.Size × Entry Payload)

structure Miri.Interpreter.MemoryExtras.Registry (Payload : Type) : Type

• allocations : Array (Memory.AllocId × AllocationExtra Payload)

structure Miri.Interpreter.MemoryExtras.Hooks (K User Payload : Type) : Type

A lens into the owner's shared machine User; it may be nested with pointer, validity, threading, or pthread state without duplicating any of them.

• get : User → Registry Payload
• put : User → Registry Payload → User
• onAccess : Payload → Concurrency.SyncObject.AccessKind → M K User Unit
• weakError : Concurrency.StoreBufferAllocError → StepError

def Miri.Interpreter.MemoryExtras.discardUninserted {K User Payload : Type} [DecidableEq K] (h : Hooks K User Payload) (id : Memory.AllocId) (machine : Machine K User) (cleanRegistry cleanRace cleanSpan : Bool := true) : Machine K User

Remove only records for an allocation that never became a live owner. Callbacks may have changed other IDs while the initializer was running, so this cleanup is deliberately keyed to the reserved ID alone.

Equations

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

def Miri.Interpreter.MemoryExtras.lookup {K User Payload : Type} (h : Hooks K User Payload) (machine : Machine K User) (id : Memory.AllocId) : Except StepError (AllocationExtra Payload)

Equations

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

def Miri.Interpreter.MemoryExtras.putAllocation {K User Payload : Type} (h : Hooks K User Payload) (machine : Machine K User) (id : Memory.AllocId) (extra : AllocationExtra Payload) : Machine K User

Equations

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

def Miri.Interpreter.MemoryExtras.initAllocation {K User Payload : Type} [DecidableEq K] (h : Hooks K User Payload) (id : Memory.AllocId) (weak : Bool) : M K User Unit

Called in the allocation tail after the actual race allocation was installed.

Equations

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

def Miri.Interpreter.MemoryExtras.nonAtomicWrite {K User Payload : Type} (h : Hooks K User Payload) (id : Memory.AllocId) (range : Memory.AllocRange) : M K User Unit

Commit the transition before reporting failure: RangeObjectMap can mutate before a failed check. Called only after the successful non-atomic race write.

Equations

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

def Miri.Interpreter.MemoryExtras.lookupSync {K User Payload : Type} (h : Hooks K User Payload) (address : Concurrency.SyncObject.Address) : M K User (Option (Concurrency.SyncObject.Object (Machine K User) Payload))

Equations

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

def Miri.Interpreter.MemoryExtras.insertSync {K User Payload : Type} (h : Hooks K User Payload) (address : Concurrency.SyncObject.Address) (entry : Entry Payload) : M K User Unit

Insert typed payload together with its GC roots. Replacement agrees with BTreeMap::insert, including replacement after a failed dynamic downcast.

Equations

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

def Miri.Interpreter.MemoryExtras.accessHooks {K User Payload : Type} (h : Hooks K User Payload) : Concurrency.SyncObject.AccessHooks (Machine K User) Payload

Equations

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

def Miri.Interpreter.MemoryExtras.syncAccess {K User Payload : Type} (h : Hooks K User Payload) (write : Bool) (id : Memory.AllocId) (range : Memory.AllocRange) : M K User Unit

onMemoryAccess runs ascending callbacks and only then deletes write-sensitive metadata. A failing callback retains all prior effects and all registry entries.

Equations

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

def Miri.Interpreter.MemoryExtras.bindAccess {K User Payload : Type} (h : Hooks K User Payload) (base : PlaceMachine.AccessConfig K User) : PlaceMachine.AccessConfig K User

Portable hooks replace the two former leaves in the already ordered PlaceMachine diagnostic → race → weak → TB → sync pipeline.

Equations

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

def Miri.Interpreter.MemoryExtras.beforeDeallocationSync {K User Payload : Type} (h : Hooks K User Payload) (id : Memory.AllocId) : M K User Unit

Source deallocation sync stage, after race-deallocation and TB-deallocation. No metadata is removed here. MemoryLifecycle has already removed the live allocation before invoking this stage, including on callback failure.

Equations

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

def Miri.Interpreter.MemoryExtras.removeAllocation {K User Payload : Type} (h : Hooks K User Payload) (id : Memory.AllocId) : M K User Unit

Run only after successful complete deallocation, alongside race-index cleanup.

Equations

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

def Miri.Interpreter.MemoryExtras.getAtomic {K User Payload : Type} (h : Hooks K User Payload) (machine : Machine K User) (id : Memory.AllocId) : Except StepError (Concurrency.AtomicState (Memory.Scalar Memory.Provenance))

Atomic dispatch uses exactly the same global clock, allocation clocks and weak buffer as non-atomic accesses. Missing clocks remain an explicit error.

Equations

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

def Miri.Interpreter.MemoryExtras.setAtomic {K User Payload : Type} (h : Hooks K User Payload) (machine : Machine K User) (id : Memory.AllocId) (atomic : Concurrency.AtomicState (Memory.Scalar Memory.Provenance)) : Except StepError (Machine K User)

This setter is used after getAtomic succeeded; it updates the latest extras, so concurrent callback changes to the sync registry cannot be overwritten.

Equations

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

def Miri.Interpreter.MemoryExtras.commitAtomic {K User Payload : Type} (h : Hooks K User Payload) (id : Memory.AllocId) (atomic : Concurrency.AtomicState (Memory.Scalar Memory.Provenance)) : M K User Unit

Checked effectful setter for IntrinsicAtomic: absence is an error rather than a silently ignored write.

Equations

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

def Miri.Interpreter.MemoryExtras.bindAtomic {K User Payload C V : Type} (h : Hooks K User Payload) (base : IntrinsicAtomicHooks Memory.Provenance (Machine K User) C V) : IntrinsicAtomicHooks Memory.Provenance (Machine K User) C V

Install the canonical machine lenses into the full atomic dispatcher.

Equations

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

def Miri.Interpreter.MemoryExtras.bindAllocation {K User Payload : Type} [DecidableEq K] (h : Hooks K User Payload) (weak : Bool) (base : PlaceMachine.AllocationConfig K User) : PlaceMachine.AllocationConfig K User

Stack allocation's diagnostic/tree/race initialization precedes this tail; other compiler/machine tail effects execute after extras are installed.

Equations

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

def Miri.Interpreter.MemoryExtras.weakValues {Payload : Type} (registry : Registry Payload) : Array (Memory.Scalar Memory.Provenance)

All retained store-buffer values, including old modification-order entries, are roots. Consumers inspect scalar provenance using the canonical scalar API.

Equations

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

def Miri.Interpreter.MemoryExtras.syncRoots {Payload : Type} (registry : Registry Payload) : Array Memory.Provenance

Equations

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