Per-location weak-memory store buffers from pinned Miri

This module ports the local StoreBuffer state and operations in the pinned upstream/miri-source/src/concurrency/weak_memory.rs (Miri revision 7fa591d7d4dd9af8154becbc8332f8096f8323b1, Git blob 4838144d1d8625379f28ead9864bcfea72a16cc0). It preserves modification-order entries, their per-store synchronization clocks, SC marks, values, and first-load metadata, plus Miri's 128-entry limit and all fetch_store candidate restrictions.

Miri chooses uniformly at random from the legal candidate set. Lean models the support of that choice as a finite list and permits an explicit rank to select any member; it does not model probabilities. Enumerating the list is an over-approximation of individual source executions by construction: every selected result is a member of the exact source filter's set, and every source result lies in that set. No single random seed is used to justify a safety claim.

Interpreter memory updates, RNG distribution, atomic-access validation callback, diagnostics, and Miri's complete operation dispatch are outside this local slice. bufferedReadAt accepts the validation transition explicitly and runs it after selecting an entry but before recording load metadata, matching the source order. Scalar values are abstracted as a Lean type parameter; none is the source's uninitialized scalar case. This is not a complete Rust or Miri weak-memory semantics.

def Miri.Concurrency.STORE_BUFFER_LIMIT : Nat

Maximum number of retained modification-order entries in Miri.

Equations

• Miri.Concurrency.STORE_BUFFER_LIMIT = 128

inductive Miri.Concurrency.LoadRecency : Type

Whether a selected weak-memory load returned the newest modification-order entry or an older one.

• Latest : LoadRecency
• Outdated : LoadRecency

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqLoadRecency : DecidableEq LoadRecency

Equations

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

def Miri.Concurrency.instReprLoadRecency.repr : LoadRecency → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprLoadRecency : Repr LoadRecency

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedLoadRecency : Inhabited LoadRecency

Equations

• Miri.Concurrency.instInhabitedLoadRecency = { default := Miri.Concurrency.instInhabitedLoadRecency.default }

inductive Miri.Concurrency.WeakMemoryError : Type

Explicit failures for invalid local buffer/rank operations. Normal buffers cannot be empty or exceed the source capacity.

• emptyStoreBuffer : WeakMemoryError
• bufferTooLong : WeakMemoryError
• choiceOutOfBounds : WeakMemoryError
• selectedIndexOutOfBounds : WeakMemoryError

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqWeakMemoryError : DecidableEq WeakMemoryError

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprWeakMemoryError : Repr WeakMemoryError

Equations

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

def Miri.Concurrency.instReprWeakMemoryError.repr : WeakMemoryError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedWeakMemoryError : Inhabited WeakMemoryError

Equations

• Miri.Concurrency.instInhabitedWeakMemoryError = { default := Miri.Concurrency.instInhabitedWeakMemoryError.default }

structure Miri.Concurrency.LoadInfo : Type

First-load metadata stored on each source store element. The list is a finite-map representation keyed by VectorIdx.toNat; insertion preserves the first timestamp, as FxHashMap::try_insert does.

• timestamps : List (VectorIdx × VTimestamp)
• scLoaded : Bool

def Miri.Concurrency.instReprLoadInfo.repr : LoadInfo → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprLoadInfo : Repr LoadInfo

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedLoadInfo : Inhabited LoadInfo

Equations

• Miri.Concurrency.instInhabitedLoadInfo = { default := Miri.Concurrency.instInhabitedLoadInfo.default }

def Miri.Concurrency.LoadInfo.timestampFor? (info : LoadInfo) (index : VectorIdx) : Option VTimestamp

Read the recorded first timestamp for one thread, if present.

Equations

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

def Miri.Concurrency.LoadInfo.record (info : LoadInfo) (index : VectorIdx) (clock : VClock) (isSeqCst : Bool) : LoadInfo

Record a load by a thread only if that thread has not loaded this element before, and remember whether any load was SC.

Equations

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

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

One store in a location's modification order. Value abstracts Rust's Scalar; none is an uninitialized stored value.

• storeThread : VectorIdx
• storeTimestamp : VTimestamp
• syncClock : VClock
• isSeqCst : Bool
• val : Option Value
• loadInfo : LoadInfo

def Miri.Concurrency.StoreElement.hasLoadBefore {Value : Type} (element : StoreElement Value) (clock : VClock) : Bool

Whether an earlier recorded load from this element happens before the current store, matching Miri's SC-store closure condition.

Equations

• element.hasLoadBefore clock = element.loadInfo.timestamps.any fun (pair : Miri.Concurrency.VectorIdx × Miri.Concurrency.VTimestamp) => decide (pair.snd.time ≤ (clock.index pair.fst).time)

def Miri.Concurrency.StoreElement.loadImpl {Value : Type} (element : StoreElement Value) (index : VectorIdx) (clocks : ThreadClockSet) (isSeqCst : Bool) : StoreElement Value × Option Value

Apply Miri's ATOMIC LOAD IMPL metadata update and return the stored value.

Equations

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

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

A nonempty source store buffer. oldest plus newer stores the exact oldest-to-newest modification order; the proof field enforces the source's 128-entry retention bound.

• oldest : StoreElement Value
• newer : List (StoreElement Value)
• bounded : self.newer.length < STORE_BUFFER_LIMIT

def Miri.Concurrency.StoreBuffer.entries {Value : Type} (buffer : StoreBuffer Value) : List (StoreElement Value)

The retained entries in modification order.

Equations

• buffer.entries = buffer.oldest :: buffer.newer

def Miri.Concurrency.StoreBuffer.last {Value : Type} (buffer : StoreBuffer Value) : StoreElement Value

The latest modification-order element.

Equations

• buffer.last = match buffer.newer.getLast? with | some element => element | none => buffer.oldest

def Miri.Concurrency.StoreBuffer.new {Value : Type} (initial : Option Value) : StoreBuffer Value

Construct the source's initial non-atomic store, which has no acquireable clock and is not SC. Its thread and timestamp are the source's zero values.

Equations

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

def Miri.Concurrency.StoreBuffer.blocksEarlier {Value : Type} (element : StoreElement Value) (isSeqCst : Bool) (clocks : ThreadClockSet) : Bool

Exact blocking condition used by Miri's fetch_store prefix scan.

Equations

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

structure Miri.Concurrency.StoreBuffer.LoadChoice (Value : Type) : Type

One supported outcome of Miri's randomized fetch_store.

• position : Nat
• element : StoreElement Value
• recency : LoadRecency

def Miri.Concurrency.StoreBuffer.fetchChoices {Value : Type} (buffer : StoreBuffer Value) (isSeqCst : Bool) (clocks : ThreadClockSet) : List (LoadChoice Value)

The finite support of Miri fetch_store: candidates are presented in newest-to-oldest order, preserving distinct modification-order entries.

Equations

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

theorem Miri.Concurrency.StoreBuffer.fetchChoices_nonempty {Value : Type} (buffer : StoreBuffer Value) (isSeqCst : Bool) (clocks : ThreadClockSet) : buffer.fetchChoices isSeqCst clocks ≠ []

The initial element and inclusive prefix rule ensure at least one legal candidate for every valid store buffer and clock state.

def Miri.Concurrency.StoreBuffer.fetchAt {Value : Type} (buffer : StoreBuffer Value) (isSeqCst : Bool) (clocks : ThreadClockSet) (rank : Nat) : Except WeakMemoryError (LoadChoice Value)

Equations

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

def Miri.Concurrency.StoreBuffer.recordSelectedLoad {Value : Type} (buffer : StoreBuffer Value) (choice : LoadChoice Value) (index : VectorIdx) (clocksAfterValidation : ThreadClockSet) (isSeqCst : Bool) : Except WeakMemoryError (StoreBuffer Value × Option Value)

Record the selected load after external atomic validation has succeeded. The passed clock is the post-validation thread-clock state, as in Miri.

Equations

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

structure Miri.Concurrency.StoreBuffer.BufferedReadResult (Value : Type) : Type

Result of one buffered atomic load, including the selected synchronization clock, chosen value, recency diagnostic bit, and post-validation thread state.

• buffer : StoreBuffer Value
• value : Option Value
• choice : LoadChoice Value
• clocks : ThreadClockSet

def Miri.Concurrency.StoreBuffer.bufferedReadAt {Value Error : Type} (buffer : StoreBuffer Value) (isSeqCst : Bool) (clocksBeforeValidation : ThreadClockSet) (loadIndex : VectorIdx) (rank : Nat) (validate : VClock → Except Error ThreadClockSet) : Except (Error ⊕ WeakMemoryError) (BufferedReadResult Value)

Execute one legal source read choice. Validation observes that entry's per-element synchronization clock after selection. Load metadata changes only if validation succeeds, in the same order as the source implementation.

Equations

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

def Miri.Concurrency.StoreBuffer.readFromLastStore {Value : Type} (buffer : StoreBuffer Value) (index : VectorIdx) (clocks : ThreadClockSet) (isSeqCst : Bool) : Except WeakMemoryError (StoreBuffer Value × Option Value)

Perform Miri's RMW-side read from the latest modification-order element. The RMW does not use randomized stale reads.

Equations

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

def Miri.Concurrency.StoreBuffer.storeImpl {Value : Type} (buffer : StoreBuffer Value) (value : Value) (index : VectorIdx) (threadClock : VClock) (isSeqCst : Bool) (syncClock : VClock) : StoreBuffer Value

Add a store, dropping the oldest element when the current buffer is already at the source limit. SC marking follows the pinned source's two HB/CoWR tests.

Equations

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

def Miri.Concurrency.StoreBuffer.bufferedWrite {Value : Type} (buffer : StoreBuffer Value) (value : Value) (thread : ThreadClockSet) (index : VectorIdx) (isSeqCst : Bool) (syncClock : VClock) : StoreBuffer Value

Miri's ordinary buffered write: capture the writer's timestamp and the caller-provided release-sequence clock, then append/trim/SC-mark.

Equations

• buffer.bufferedWrite value thread index isSeqCst syncClock = buffer.storeImpl value index thread.clock isSeqCst syncClock

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

Allocation-local range map of atomic objects to their store buffers.

• storeBuffers : DataStructures.RangeObjectMap (StoreBuffer Value)

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

A detached value handle for one perfectly overlapping object. Callers commit it explicitly after their operation; a changed range map invalidates the handle instead of silently updating some other object.

• range : Memory.AllocRange
• position : DataStructures.Position
• buffer : StoreBuffer Value

inductive Miri.Concurrency.StoreBufferAllocError : Type

• rangeMap (error : DataStructures.RangeObjectMapError) : StoreBufferAllocError
• handleInvalidated : StoreBufferAllocError

def Miri.Concurrency.instReprStoreBufferAllocError.repr : StoreBufferAllocError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprStoreBufferAllocError : Repr StoreBufferAllocError

Equations

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

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

Pure transition result retains RangeObjectMap's partial mutation on error, matching its insert-before-check behavior.

• allocation : StoreBufferAlloc Value
• outcome : Except StoreBufferAllocError (Option (StoreBufferHandle Value))

def Miri.Concurrency.StoreBufferAlloc.newAllocation {Value : Type} : StoreBufferAlloc Value

Equations

• Miri.Concurrency.StoreBufferAlloc.newAllocation = { storeBuffers := Miri.DataStructures.RangeObjectMap.new }

def Miri.Concurrency.StoreBufferAlloc.bufferCount {Value : Type} (allocation : StoreBufferAlloc Value) : Nat

Equations

• allocation.bufferCount = allocation.storeBuffers.length

def Miri.Concurrency.StoreBufferAlloc.bufferRanges {Value : Type} (allocation : StoreBufferAlloc Value) : Array Memory.AllocRange

Equations

• allocation.bufferRanges = allocation.storeBuffers.ranges

def Miri.Concurrency.StoreBufferAlloc.nonAtomicWrite {Value : Type} (allocation : StoreBufferAlloc Value) (range : Memory.AllocRange) (global : GlobalState) : StoreBufferAllocTransition Value

Remove or retain buffered state after a non-atomic write exactly according to Miri's ongoing_action_data_race_free flag and overlap classification.

Equations

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

def Miri.Concurrency.StoreBufferAlloc.getStoreBuffer {Value : Type} (allocation : StoreBufferAlloc Value) (range : Memory.AllocRange) : Except StoreBufferAllocError (Option (StoreBufferHandle Value))

Return a store-buffer handle only for a perfectly overlapping object. Empty and imperfect overlaps return no buffer, as in Miri.

Equations

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

def Miri.Concurrency.StoreBufferAlloc.getOrCreateStoreBuffer {Value : Type} (allocation : StoreBufferAlloc Value) (range : Memory.AllocRange) (init : Option Value) : StoreBufferAllocTransition Value

Get an exactly matching buffer or initialize a new one. On imperfect overlap, the old intersecting buffers are removed before insertion, matching Miri's range invalidation order.

Equations

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

def Miri.Concurrency.StoreBufferAlloc.commitStoreBuffer {Value : Type} (allocation : StoreBufferAlloc Value) (handle : StoreBufferHandle Value) : Except StoreBufferAllocError (StoreBufferAlloc Value)

Commit a returned buffer handle after the modeled atomic operation.

Equations

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