Clock and store-buffer dispatch for atomic accesses

This module composes the source-backed vector-clock and weak-memory state operations at the same callback boundaries as Miri's validate_atomic_op/buffered_atomic_* hooks. It does not implement MPlaceTy, pointer validation, scalar memory, scalar RMW operators, UB diagnostics, or the interpreter's allow_data_races_* callbacks. Those remain caller obligations. In particular, buffered writes and RMWs are post-memory- write hooks; their arguments are the values already produced/written by the interpreter. Atomic loads receive the already-read latest-in-modification-order value used by Miri's fallback path.

The global state stores an optional per-allocation weak-memory map because Miri attaches StoreBufferAlloc only when that backend is active. SC read metadata is updated before lookup/choice, SC store metadata after validation, and SC RMW read/write metadata after validation. Per-byte validation retains partial cell/clock changes on an error and stops at the first failing byte.

structure Miri.Concurrency.AtomicState (Value : Type) : Type

Full state slice needed by the pinned atomic clock/store-buffer hooks. The caller owns interpreter memory and scheduler transitions. none means this allocation has no weak-memory AllocExtra payload.

• global : GlobalState
• allocation : VClockAlloc
• weakMemoryAllocation : Option (StoreBufferAlloc Value)

inductive Miri.Concurrency.AtomicDispatchError : Type

Explicit failures at the atomic clock/store-buffer boundary.

• globalState (error : GlobalStateError) : AtomicDispatchError
• validation (error : DataRaceResult) : AtomicDispatchError
• syncClock (error : DataRaceResult) : AtomicDispatchError
• storeBuffer (error : StoreBufferAllocError) : AtomicDispatchError
• weakMemory (error : WeakMemoryError) : AtomicDispatchError
• missingCreatedBuffer : AtomicDispatchError
• syncOperationUnexpectedlySkipped : AtomicDispatchError

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicDispatchError : Repr AtomicDispatchError

Equations

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

def Miri.Concurrency.instReprAtomicDispatchError.repr : AtomicDispatchError → Nat → Std.Format

Equations

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

structure Miri.Concurrency.AtomicTransition (Value Result : Type) : Type

State is returned alongside every success or failure, including an error after DedupRangeMap/per-byte clock mutation.

• state : AtomicState Value
• outcome : Except AtomicDispatchError Result

inductive Miri.Concurrency.WeakMemoryDiagnostic : Type

A source outdated-load diagnostic request. Rendering the pointer/span and emitting Miri's non-halting diagnostic remain interpreter callbacks.

• outdatedLoad : WeakMemoryDiagnostic

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqWeakMemoryDiagnostic : DecidableEq WeakMemoryDiagnostic

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprWeakMemoryDiagnostic : Repr WeakMemoryDiagnostic

Equations

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

def Miri.Concurrency.instReprWeakMemoryDiagnostic.repr : WeakMemoryDiagnostic → Nat → Std.Format

Equations

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

structure Miri.Concurrency.AtomicReadResult (Value : Type) : Type

Value returned by the source buffered-load hook. choice = none denotes the latest-memory fallback; a buffered none value still represents an uninitialized selected store and is deliberately not coerced to a value.

• value : Option Value
• choice : Option (StoreBuffer.LoadChoice Value)
• diagnostic : Option WeakMemoryDiagnostic

def Miri.Concurrency.accessRangeOfAllocRange (range : Memory.AllocRange) : AccessRange

Convert the same allocation interval between Miri's AllocRange and the data-race module's byte-count view.

Equations

• Miri.Concurrency.accessRangeOfAllocRange range = { start := Miri.Concurrency.dataRaceSize✝ range.start, size := Miri.Concurrency.dataRaceSize✝ range.size }

def Miri.Concurrency.allocRangeOfAccessRange (range : AccessRange) : Memory.AllocRange

Equations

• Miri.Concurrency.allocRangeOfAccessRange range = { start := Miri.ABI.Size.ofBytes (UInt64.ofNat range.start.bytes), size := Miri.ABI.Size.ofBytes (UInt64.ofNat range.size.bytes) }

def Miri.Concurrency.validateAtomicOp {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (operation : VClockAlloc → ThreadClockSet → VectorIdx → VClockAlloc.RangeTransition) : AtomicTransition Value Unit

Run one source validate_atomic_op body. Its operation closure is applied to each byte in increasing offset order by VClockAlloc.runRange; successful operations conservatively increment once through GlobalState.maybePerformSyncOperation. Race/error paths preserve the failed cell and all earlier byte updates, but do not increment the outer clock.

Equations

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

inductive Miri.Concurrency.BufferedAtomicReadPlan (Value : Type) : Type

A cut at the actual source RNG operation. SC metadata, buffer lookup and active-clock errors precede the cut; fallback reads never request a draw.

• ready {Value : Type} (result : AtomicReadResult Value) : BufferedAtomicReadPlan Value
• select {Value : Type} (handle : StoreBufferHandle Value) (clocks : ThreadClockSet) : BufferedAtomicReadPlan Value

def Miri.Concurrency.prepareBufferedAtomicRead {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicReadOrd) (latestInMemory : Value) : AtomicTransition Value (BufferedAtomicReadPlan Value)

Equations

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

def Miri.Concurrency.finishBufferedAtomicRead {Value : Type} (working : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicReadOrd) (handle : StoreBufferHandle Value) (clocks : ThreadClockSet) (choiceRank : Nat) : AtomicTransition Value (AtomicReadResult Value)

Continue the same source operation after selecting a supported store. Callers commit prepare's state before requesting an effectful choice.

Equations

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

def Miri.Concurrency.bufferedAtomicRead {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicReadOrd) (latestInMemory : Value) (choiceRank : Nat) : AtomicTransition Value (AtomicReadResult Value)

Deterministic explicit-rank API retained as composition of the exact source prefix and continuation. No choice is used on a fallback path.

Equations

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

def Miri.Concurrency.performReadOnBufferedLatest {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicReadOrd) : AtomicTransition Value Unit

Port weak_memory.rs::perform_read_on_buffered_latest, used only after a failed compare-exchange. Unlike ordinary buffered loads it never selects an older store and does not run a second atomic validation. The source SC-read mark occurs before the buffer lookup and therefore remains on a missing-buffer fallback.

Equations

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

def Miri.Concurrency.atomicCompareExchangeFailureState {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicReadOrd) : AtomicTransition Value Unit

The failed compare-exchange path: source validates an atomic load with no selected-store override, then records a load from the latest retained buffer element.

Equations

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

def Miri.Concurrency.bufferedAtomicWrite {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicWriteOrd) (value : Value) (initial : Option Value) : AtomicTransition Value Unit

The buffered_atomic_write hook. Callers must have completed Miri's atomic_access_check, vanilla memory write, and successful validate_atomic_store before invoking it. The source SC-write mark occurs before range sync-clock collection and buffer creation.

Equations

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

def Miri.Concurrency.bufferedAtomicRmw {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicRwOrd) (oldValue newValue : Value) : AtomicTransition Value Unit

The buffered_atomic_rmw hook. Callers supply the already-read old value and already-computed/written new value after a successful validate_atomic_rmw. The hook marks both SC edges, reads metadata from the latest buffered store, then appends the new store using the updated allocation sync clock.

Equations

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

def Miri.Concurrency.atomicStoreState {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicWriteOrd) (value : Value) (initial : Option Value) : AtomicTransition Value Unit

Compose Miri's validate_atomic_store then buffered_atomic_write state hooks. The interpreter must already have performed its normal memory write; this function does not create or mutate the scalar memory allocation.

Equations

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

def Miri.Concurrency.atomicRmwState {Value : Type} (state : AtomicState Value) (threads : ThreadManager) (range : Memory.AllocRange) (ordering : AtomicRwOrd) (oldValue newValue : Value) : AtomicTransition Value Unit

Compose Miri's validate_atomic_rmw then buffered_atomic_rmw state hooks. Actual memory read, RMW scalar computation, and write remain caller operations performed before this post-write state transition.

Equations

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