Scalar memory operations around Miri's atomic hooks

This is the concrete scalar-storage layer for one live allocation when the allocation has no borrow-tracker or synchronization-object payload. It uses the pinned rustc Allocation.read_scalar/write_scalar transitions and then the Miri clock/store-buffer hooks in AtomicDispatch, in source order. The allocation's Extra is Unit, so this module cannot represent a Miri allocation with active borrow tracking or synchronization objects. Callers must not treat this restricted slice as a complete interpreter execution.

atomicAccessCheck (place alignment, allocation resolution and read-only rules), interpreter before_memory_* hooks and diagnostics are outside this module. The concrete Miri path performs before_memory_* while ongoing_action_data_race_free is set, so this module mirrors that flag window around byte access; it does not claim to run the absent borrow/sync hooks. Every operation here is therefore a component of the dispatch, not a Miri program-safety result.

structure Miri.Concurrency.AtomicScalarMemory (Prov : Type) : Type

Scalar state for one allocation's interpreter bytes and its exact allocation-local data-race/store-buffer state.

• memory : Memory.Allocation Prov
• concurrency : AtomicState (Memory.Scalar Prov)

inductive Miri.Concurrency.AtomicScalarMemoryError : Type

Failures from the concrete scalar-storage and clock/buffer stages.

• allocation (error : Memory.AllocError) : AtomicScalarMemoryError
• scalar (error : Memory.ScalarError) : AtomicScalarMemoryError
• dispatch (error : AtomicDispatchError) : AtomicScalarMemoryError
• integerOperation (error : Interpreter.IntegerOpError) : AtomicScalarMemoryError
• integerTypeSizeMismatch (scalarSize typeSize : ABI.Size) : AtomicScalarMemoryError
• nestedAllowDataRaces : AtomicScalarMemoryError
• invalidUninitializedAtomicRead : AtomicScalarMemoryError
• missingWeakMemoryAllocation : AtomicScalarMemoryError
• unexpectedWeakMemoryAllocation : AtomicScalarMemoryError
• unexpectedRmwResult : AtomicScalarMemoryError

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicScalarMemoryError : Repr AtomicScalarMemoryError

Equations

• Miri.Concurrency.instReprAtomicScalarMemoryError = { reprPrec := Miri.Concurrency.instReprAtomicScalarMemoryError.repr }

def Miri.Concurrency.instReprAtomicScalarMemoryError.repr : AtomicScalarMemoryError → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.AtomicScalarSourceHook : Type

Outcome always carries the post-operation byte and concurrency state, including write errors after source-ordered partial allocation mutation. The nonempty requiredHooks field prevents the scalar/data-race fragment from being mistaken for a complete interpreter dispatch.

• atomicAccessCheck : AtomicScalarSourceHook
• interpreterBeforeMemoryRead : AtomicScalarSourceHook
• interpreterBeforeMemoryWrite : AtomicScalarSourceHook

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicScalarSourceHook : DecidableEq AtomicScalarSourceHook

Equations

• Miri.Concurrency.instDecidableEqAtomicScalarSourceHook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Concurrency.instReprAtomicScalarSourceHook.repr : AtomicScalarSourceHook → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicScalarSourceHook : Repr AtomicScalarSourceHook

Equations

• Miri.Concurrency.instReprAtomicScalarSourceHook = { reprPrec := Miri.Concurrency.instReprAtomicScalarSourceHook.repr }

structure Miri.Concurrency.AtomicScalarMemoryTransition (Prov Result : Type) : Type

• state : AtomicScalarMemory Prov
• outcome : Except AtomicScalarMemoryError Result
• requiredHooks : List AtomicScalarSourceHook

inductive Miri.Concurrency.AtomicScalarUnknown : Type

A component error or uncompleted interpreter hook is an obligation, not a successful terminal result. This adapter deliberately has no UB judgement: classification requires the actual interpreter hooks and diagnostics.

• componentError (error : AtomicScalarMemoryError) : AtomicScalarUnknown
• interpreterHooks (hooks : List AtomicScalarSourceHook) : AtomicScalarUnknown

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicScalarUnknown : Repr AtomicScalarUnknown

Equations

• Miri.Concurrency.instReprAtomicScalarUnknown = { reprPrec := Miri.Concurrency.instReprAtomicScalarUnknown.repr }

def Miri.Concurrency.instReprAtomicScalarUnknown.repr : AtomicScalarUnknown → Nat → Std.Format

Equations

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

def Miri.Concurrency.AtomicScalarMemoryTransition.asOperationalOutcome {Prov Result : Type} (transition : AtomicScalarMemoryTransition Prov Result) : OperationalSafety.Outcome Result Unit AtomicScalarUnknown

Interpret this component's state as an operational-safety outcome. Since its access-check and memory-hook obligations have not been discharged by this module, successful scalar/clock work remains blocked; it cannot establish Safe merely because the component returned a value.

Equations

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

def Miri.Concurrency.atomicScalarLoad {Prov : Type} [DecidableEq Prov] [Memory.PointerProvenance Prov] (state : AtomicScalarMemory Prov) (threads : ThreadManager) (layout : ABI.TargetDataLayout) (range : Memory.AllocRange) (readProvenance : Bool) (ordering : AtomicReadOrd) (choiceRank : Nat) : AtomicScalarMemoryTransition Prov (Memory.Scalar Prov)

The scalar-memory and buffered-clock implementation of the body after atomic_access_check in read_scalar_atomic. It reads the actual latest allocation scalar first, then delegates legal finite read choices and their validation/metadata order to bufferedAtomicRead. choiceRank is an explicit member of the exact source candidate set, not a random seed.

Equations

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

def Miri.Concurrency.atomicScalarStore {Prov : Type} [DecidableEq Prov] [Memory.PointerProvenance Prov] (state : AtomicScalarMemory Prov) (threads : ThreadManager) (layout : ABI.TargetDataLayout) (range : Memory.AllocRange) (readProvenance : Bool) (value : Memory.Scalar Prov) (ordering : AtomicWriteOrd) : AtomicScalarMemoryTransition Prov Unit

Source write_scalar_atomic's local path for the actual allocation and VClock weak-memory backend. The old scalar is a best-effort ghost read: its failure becomes an uninitialized initial store, as in Miri. The real write happens before validate_atomic_store; its memory mutation remains present if validation later fails.

Equations

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

inductive Miri.Concurrency.AtomicRmwScalarOp : Type

The supported source AtomicRmwOp forms. These mirror the cases used by rustc's atomic intrinsics: arithmetic/bitwise MIR operations, signedness-aware min/max, and scalar swap.

• mir (operation : MIR.BinOp) (negateResult : Bool) : AtomicRmwScalarOp
• minimum : AtomicRmwScalarOp
• maximum : AtomicRmwScalarOp
• swap : AtomicRmwScalarOp

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicRmwScalarOp : DecidableEq AtomicRmwScalarOp

Equations

• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp = Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq

def Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq (x✝ x✝¹ : AtomicRmwScalarOp) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq (Miri.Concurrency.AtomicRmwScalarOp.mir operation negateResult) Miri.Concurrency.AtomicRmwScalarOp.minimum = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq (Miri.Concurrency.AtomicRmwScalarOp.mir operation negateResult) Miri.Concurrency.AtomicRmwScalarOp.maximum = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq (Miri.Concurrency.AtomicRmwScalarOp.mir operation negateResult) Miri.Concurrency.AtomicRmwScalarOp.swap = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq Miri.Concurrency.AtomicRmwScalarOp.minimum (Miri.Concurrency.AtomicRmwScalarOp.mir operation negateResult) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq Miri.Concurrency.AtomicRmwScalarOp.minimum Miri.Concurrency.AtomicRmwScalarOp.minimum = isTrue ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq Miri.Concurrency.AtomicRmwScalarOp.maximum (Miri.Concurrency.AtomicRmwScalarOp.mir operation negateResult) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq Miri.Concurrency.AtomicRmwScalarOp.maximum Miri.Concurrency.AtomicRmwScalarOp.maximum = isTrue ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq Miri.Concurrency.AtomicRmwScalarOp.swap (Miri.Concurrency.AtomicRmwScalarOp.mir operation negateResult) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicRmwScalarOp.decEq Miri.Concurrency.AtomicRmwScalarOp.swap Miri.Concurrency.AtomicRmwScalarOp.swap = isTrue ⋯

def Miri.Concurrency.instReprAtomicRmwScalarOp.repr : AtomicRmwScalarOp → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicRmwScalarOp : Repr AtomicRmwScalarOp

Equations

• Miri.Concurrency.instReprAtomicRmwScalarOp = { reprPrec := Miri.Concurrency.instReprAtomicRmwScalarOp.repr }

structure Miri.Concurrency.AtomicCompareExchangeResult (Prov : Type) : Type

Result of the integer or thin-pointer compare-exchange path.

• oldValue : Memory.Scalar Prov
• succeeded : Bool

def Miri.Concurrency.atomicScalarRmw {Prov : Type} [DecidableEq Prov] [Memory.PointerProvenance Prov] (state : AtomicScalarMemory Prov) (threads : ThreadManager) (layout : ABI.TargetDataLayout) (range : Memory.AllocRange) (readProvenance : Bool) (operation : AtomicRmwScalarOp) (integerType : Interpreter.IntegerType) (rhs : Memory.Scalar Prov) (ordering : AtomicRwOrd) : AtomicScalarMemoryTransition Prov (Memory.Scalar Prov)

Source atomic_rmw's local scalar path: checked scalar read, exact MIR operator calculation, byte/provenance write, atomic RMW validation, then the store-buffer read of the last modification followed by append.

Equations

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

def Miri.Concurrency.atomicScalarCompareExchange {Prov : Type} [DecidableEq Prov] [Memory.PointerProvenance Prov] (state : AtomicScalarMemory Prov) (threads : ThreadManager) (layout : ABI.TargetDataLayout) (range : Memory.AllocRange) (readProvenance : Bool) (integerType : Interpreter.IntegerType) (expected newValue : Memory.Scalar Prov) (canFailSpuriously spuriousFailureChosen : Bool) (successOrdering : AtomicRwOrd) (failureOrdering : AtomicReadOrd) : AtomicScalarMemoryTransition Prov (AtomicCompareExchangeResult Prov)

The integer and thin-pointer branches of atomic_compare_exchange. For weak CAS, spuriousFailureChosen is the explicit outcome selected from the source RNG; it only changes an otherwise-successful comparison. On failure, validation is an atomic load followed by perform_read_on_buffered_latest; on success, the new scalar is written before atomic-RMW validation and buffered-RMW metadata.

Equations

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