Source data_race.rs atomic physical operations coupled to canonical PlaceMachine bytes, MemoryExtras clocks/store buffers, PointerMachine addresses, and ValidityMachine's single ghost/alignment policy. No shadow atomic memory.

@[reducible, inline]

abbrev Miri.Interpreter.AtomicMachine.User (User : Type) : Type

Equations

• Miri.Interpreter.AtomicMachine.User = Miri.Interpreter.ValidityMachine.UserState

@[reducible, inline]

abbrev Miri.Interpreter.AtomicMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.AtomicMachine.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

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

Equations

• Miri.Interpreter.AtomicMachine.M K U = Miri.Interpreter.ValidityMachine.M K U

def Miri.Interpreter.AtomicMachine.physicalRead {K U : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K (User U)) (place : RuntimePlace Memory.Provenance) : M K U (RvalueImmTy Memory.Provenance)

Equations

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

def Miri.Interpreter.AtomicMachine.ghostRead {K U : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K (User U)) (place : RuntimePlace Memory.Provenance) : M K U (Option (Memory.Scalar Memory.Provenance))

The source ghost scope suppresses machine read hooks, but retains pointer resolution, lazy allocation materialization, and raw-read errors/mutations. Only the read's error is discarded; invalid ghost nesting is not discarded.

Equations

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

def Miri.Interpreter.AtomicMachine.mutability {K U : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K (User U)) (id : Memory.AllocId) : M K U Memory.Mutability

Atomic mutability uses get_alloc_raw (not metadata-only get_alloc_info), so compiler globals materialize before read-only restrictions are applied.

Equations

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

def Miri.Interpreter.AtomicMachine.resolve {K U : Type} (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (pointer : Memory.Pointer (Option Memory.Provenance)) : M K U (Memory.AllocId × ABI.Size)

Source ptr_try_get_alloc_id(ptr,0). The assertion for an unresolved address belongs to atomic_access_check; this does not run physical access hooks.

Equations

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

def Miri.Interpreter.AtomicMachine.checkAlignment {K U : Type} (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (pointer : Memory.Pointer (Option Memory.Provenance)) (align : ABI.Align) : M K U Unit

Equations

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

def Miri.Interpreter.AtomicMachine.bind {K U C Payload : Type} [DecidableEq K] (base : IntrinsicAtomicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (access : PlaceMachine.AccessConfig K (User U)) (allocation : PlaceMachine.AllocationConfig K (User U)) (compiler : PlaceMachine.CompilerHooks K (User U) C) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (extras : MemoryExtras.Hooks K (User U) Payload) : IntrinsicAtomicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Concrete dictionary for source atomic access/load/store/CAS/RMW/fences. Compiler generic ordering/volatile evaluation, typed dereference, scalar type queries, finite weak-memory choices, and diagnostics are retained from base; every physical/race/weak/TB/sync operation below is canonical.

Equations

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