Data-race clock state from pinned Miri

This module ports the pure ordering, thread-clock, and per-memory-cell clock transitions in src/concurrency/data_race.rs at the pinned Miri revision. The allocation-level interpreter hooks, MIR integration, DedupRangeMap, diagnostic construction, and weak-memory store buffers are not modeled here. In particular, these definitions are source-backed state operations, not a standalone claim that a Rust program has been checked by Miri.

Miri Span values occur only in diagnostic attribution for the transitions ported here. They do not affect the vector-clock ordering or race decision, and are omitted from the Lean state. Atomic access sizes are represented as the exact u64 byte counts used by rustc_abi::Size.

inductive Miri.Concurrency.AtomicOrdering : Type

The five orderings accepted for read/write atomic operations.

• Relaxed : AtomicOrdering
• Acquire : AtomicOrdering
• Release : AtomicOrdering
• AcqRel : AtomicOrdering
• SeqCst : AtomicOrdering

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicOrdering : DecidableEq AtomicOrdering

Equations

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

def Miri.Concurrency.instReprAtomicOrdering.repr : AtomicOrdering → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicOrdering : Repr AtomicOrdering

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedAtomicOrdering : Inhabited AtomicOrdering

Equations

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

inductive Miri.Concurrency.AtomicRwOrd : Type

An atomic ordering accepted by either a read or a write.

• Relaxed : AtomicRwOrd
• Acquire : AtomicRwOrd
• Release : AtomicRwOrd
• AcqRel : AtomicRwOrd
• SeqCst : AtomicRwOrd

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicRwOrd : DecidableEq AtomicRwOrd

Equations

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

def Miri.Concurrency.instReprAtomicRwOrd.repr : AtomicRwOrd → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicRwOrd : Repr AtomicRwOrd

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedAtomicRwOrd : Inhabited AtomicRwOrd

Equations

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

inductive Miri.Concurrency.AtomicReadOrd : Type

The ordering subset accepted by atomic loads.

• Relaxed : AtomicReadOrd
• Acquire : AtomicReadOrd
• SeqCst : AtomicReadOrd

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicReadOrd : DecidableEq AtomicReadOrd

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicReadOrd : Repr AtomicReadOrd

Equations

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

def Miri.Concurrency.instReprAtomicReadOrd.repr : AtomicReadOrd → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedAtomicReadOrd : Inhabited AtomicReadOrd

Equations

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

inductive Miri.Concurrency.AtomicWriteOrd : Type

The ordering subset accepted by atomic stores.

• Relaxed : AtomicWriteOrd
• Release : AtomicWriteOrd
• SeqCst : AtomicWriteOrd

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicWriteOrd : DecidableEq AtomicWriteOrd

Equations

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

def Miri.Concurrency.instReprAtomicWriteOrd.repr : AtomicWriteOrd → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicWriteOrd : Repr AtomicWriteOrd

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedAtomicWriteOrd : Inhabited AtomicWriteOrd

Equations

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

inductive Miri.Concurrency.AtomicFenceOrd : Type

The ordering subset accepted by atomic fences.

• Acquire : AtomicFenceOrd
• Release : AtomicFenceOrd
• AcqRel : AtomicFenceOrd
• SeqCst : AtomicFenceOrd

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicFenceOrd : DecidableEq AtomicFenceOrd

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicFenceOrd : Repr AtomicFenceOrd

Equations

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

def Miri.Concurrency.instReprAtomicFenceOrd.repr : AtomicFenceOrd → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedAtomicFenceOrd : Inhabited AtomicFenceOrd

Equations

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

inductive Miri.Concurrency.AtomicOrderingError : Type

A source-invalid ordering is made explicit where pinned Miri panics.

• invalidRead (ordering : AtomicOrdering) : AtomicOrderingError
• invalidWrite (ordering : AtomicOrdering) : AtomicOrderingError
• invalidFence (ordering : AtomicOrdering) : AtomicOrderingError

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicOrderingError : DecidableEq AtomicOrderingError

Equations

• Miri.Concurrency.instDecidableEqAtomicOrderingError = Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq

def Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq (x✝ x✝¹ : AtomicOrderingError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq (Miri.Concurrency.AtomicOrderingError.invalidRead ordering) (Miri.Concurrency.AtomicOrderingError.invalidWrite ordering_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq (Miri.Concurrency.AtomicOrderingError.invalidRead ordering) (Miri.Concurrency.AtomicOrderingError.invalidFence ordering_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq (Miri.Concurrency.AtomicOrderingError.invalidWrite ordering) (Miri.Concurrency.AtomicOrderingError.invalidRead ordering_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq (Miri.Concurrency.AtomicOrderingError.invalidWrite ordering) (Miri.Concurrency.AtomicOrderingError.invalidFence ordering_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq (Miri.Concurrency.AtomicOrderingError.invalidFence ordering) (Miri.Concurrency.AtomicOrderingError.invalidRead ordering_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicOrderingError.decEq (Miri.Concurrency.AtomicOrderingError.invalidFence ordering) (Miri.Concurrency.AtomicOrderingError.invalidWrite ordering_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicOrderingError : Repr AtomicOrderingError

Equations

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

def Miri.Concurrency.instReprAtomicOrderingError.repr : AtomicOrderingError → Nat → Std.Format

Equations

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

def Miri.Concurrency.AtomicRwOrd.ofOrdering : AtomicOrdering → AtomicRwOrd

Total conversion corresponding to AtomicRwOrd::from.

Equations

• Miri.Concurrency.AtomicRwOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Relaxed = Miri.Concurrency.AtomicRwOrd.Relaxed
• Miri.Concurrency.AtomicRwOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Acquire = Miri.Concurrency.AtomicRwOrd.Acquire
• Miri.Concurrency.AtomicRwOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Release = Miri.Concurrency.AtomicRwOrd.Release
• Miri.Concurrency.AtomicRwOrd.ofOrdering Miri.Concurrency.AtomicOrdering.AcqRel = Miri.Concurrency.AtomicRwOrd.AcqRel
• Miri.Concurrency.AtomicRwOrd.ofOrdering Miri.Concurrency.AtomicOrdering.SeqCst = Miri.Concurrency.AtomicRwOrd.SeqCst

def Miri.Concurrency.AtomicReadOrd.ofOrdering : AtomicOrdering → Except AtomicOrderingError AtomicReadOrd

Checked conversion corresponding to AtomicReadOrd::from. Release and AcqRel are explicit invalid-ordering outcomes, matching the source panic rather than accepting or weakening them.

Equations

• Miri.Concurrency.AtomicReadOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Relaxed = Except.ok Miri.Concurrency.AtomicReadOrd.Relaxed
• Miri.Concurrency.AtomicReadOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Acquire = Except.ok Miri.Concurrency.AtomicReadOrd.Acquire
• Miri.Concurrency.AtomicReadOrd.ofOrdering Miri.Concurrency.AtomicOrdering.SeqCst = Except.ok Miri.Concurrency.AtomicReadOrd.SeqCst
• Miri.Concurrency.AtomicReadOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Release = Except.error (Miri.Concurrency.AtomicOrderingError.invalidRead Miri.Concurrency.AtomicOrdering.Release)
• Miri.Concurrency.AtomicReadOrd.ofOrdering Miri.Concurrency.AtomicOrdering.AcqRel = Except.error (Miri.Concurrency.AtomicOrderingError.invalidRead Miri.Concurrency.AtomicOrdering.AcqRel)

def Miri.Concurrency.AtomicWriteOrd.ofOrdering : AtomicOrdering → Except AtomicOrderingError AtomicWriteOrd

Checked conversion corresponding to AtomicWriteOrd::from. Acquire and AcqRel are explicit invalid-ordering outcomes.

Equations

• Miri.Concurrency.AtomicWriteOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Relaxed = Except.ok Miri.Concurrency.AtomicWriteOrd.Relaxed
• Miri.Concurrency.AtomicWriteOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Release = Except.ok Miri.Concurrency.AtomicWriteOrd.Release
• Miri.Concurrency.AtomicWriteOrd.ofOrdering Miri.Concurrency.AtomicOrdering.SeqCst = Except.ok Miri.Concurrency.AtomicWriteOrd.SeqCst
• Miri.Concurrency.AtomicWriteOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Acquire = Except.error (Miri.Concurrency.AtomicOrderingError.invalidWrite Miri.Concurrency.AtomicOrdering.Acquire)
• Miri.Concurrency.AtomicWriteOrd.ofOrdering Miri.Concurrency.AtomicOrdering.AcqRel = Except.error (Miri.Concurrency.AtomicOrderingError.invalidWrite Miri.Concurrency.AtomicOrdering.AcqRel)

def Miri.Concurrency.AtomicFenceOrd.ofOrdering : AtomicOrdering → Except AtomicOrderingError AtomicFenceOrd

Checked conversion corresponding to AtomicFenceOrd::from. Relaxed is an explicit invalid-ordering outcome.

Equations

• Miri.Concurrency.AtomicFenceOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Acquire = Except.ok Miri.Concurrency.AtomicFenceOrd.Acquire
• Miri.Concurrency.AtomicFenceOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Release = Except.ok Miri.Concurrency.AtomicFenceOrd.Release
• Miri.Concurrency.AtomicFenceOrd.ofOrdering Miri.Concurrency.AtomicOrdering.AcqRel = Except.ok Miri.Concurrency.AtomicFenceOrd.AcqRel
• Miri.Concurrency.AtomicFenceOrd.ofOrdering Miri.Concurrency.AtomicOrdering.SeqCst = Except.ok Miri.Concurrency.AtomicFenceOrd.SeqCst
• Miri.Concurrency.AtomicFenceOrd.ofOrdering Miri.Concurrency.AtomicOrdering.Relaxed = Except.error (Miri.Concurrency.AtomicOrderingError.invalidFence Miri.Concurrency.AtomicOrdering.Relaxed)

structure Miri.Concurrency.ThreadClockSet : Type

Per-thread vector-clock state, including all Miri fence and SC metadata.

• clock : VClock

  The increasing happens-before clock.

• fenceAcquire : VClock

  Clock to acquire on a later acquire fence.

• fenceRelease : VClock

  Clock released by the most recent release fence.

• writeSeqCst : VClock

  Per-thread SC-write metadata used by weak-memory emulation.

• readSeqCst : VClock

  Per-thread SC-fence metadata used by weak-memory emulation.

@[instance_reducible]

instance Miri.Concurrency.instReprThreadClockSet : Repr ThreadClockSet

Equations

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

def Miri.Concurrency.instReprThreadClockSet.repr : ThreadClockSet → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedThreadClockSet : Inhabited ThreadClockSet

Equations

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

def Miri.Concurrency.ThreadClockSet.default : ThreadClockSet

The source Default state: all five clocks are zero.

Equations

• Miri.Concurrency.ThreadClockSet.default = { }

def Miri.Concurrency.ThreadClockSet.applyReleaseFence (state : ThreadClockSet) : ThreadClockSet

Apply Miri's release-fence effect by copying the happens-before clock.

Equations

• state.applyReleaseFence = { clock := state.clock, fenceAcquire := state.fenceAcquire, fenceRelease := state.clock, writeSeqCst := state.writeSeqCst, readSeqCst := state.readSeqCst }

def Miri.Concurrency.ThreadClockSet.applyAcquireFence (state : ThreadClockSet) : ThreadClockSet

Apply Miri's acquire-fence effect by joining the accumulated acquire clock.

Equations

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

def Miri.Concurrency.ThreadClockSet.incrementClock (state : ThreadClockSet) (index : VectorIdx) : Except ClockError ThreadClockSet

Increment the known thread coordinate; timestamp overflow remains explicit.

Equations

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

def Miri.Concurrency.ThreadClockSet.joinWith (state other : ThreadClockSet) : ThreadClockSet

Join another thread's happens-before clock, leaving fence/SC metadata intact.

Equations

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

structure Miri.Concurrency.ByteSize : Type

Byte size from rustc_abi::Size, whose stored representation is u64.

• value : Fin 18446744073709551616

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqByteSize : DecidableEq ByteSize

Equations

• Miri.Concurrency.instDecidableEqByteSize = Miri.Concurrency.instDecidableEqByteSize.decEq

def Miri.Concurrency.instDecidableEqByteSize.decEq (x✝ x✝¹ : ByteSize) : Decidable (x✝ = x✝¹)

Equations

• Miri.Concurrency.instDecidableEqByteSize.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instReprByteSize : Repr ByteSize

Equations

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

def Miri.Concurrency.instReprByteSize.repr : ByteSize → Nat → Std.Format

Equations

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

def Miri.Concurrency.ByteSize.ofU64 (value : Nat) (h : value < 18446744073709551616) : ByteSize

Construct a byte size from an exact u64 value.

Equations

• Miri.Concurrency.ByteSize.ofU64 value h = { value := ⟨value, h⟩ }

def Miri.Concurrency.ByteSize.bytes (size : ByteSize) : Nat

The mathematical byte count.

Equations

• size.bytes = ↑size.value

@[simp]

theorem Miri.Concurrency.ByteSize.bytes_ofU64 (value : Nat) (h : value < 18446744073709551616) : (ofU64 value h).bytes = value

inductive Miri.Concurrency.DataRaceResult : Type

Result used for the source's Result<(), DataRace> cell transitions.

• ok : DataRaceResult
• race : DataRaceResult
• invalidClockUpdate (error : ClockError) : DataRaceResult
• internalInvariantViolation : DataRaceResult
• outOfBounds : DataRaceResult

def Miri.Concurrency.instDecidableEqDataRaceResult.decEq (x✝ x✝¹ : DataRaceResult) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.ok Miri.Concurrency.DataRaceResult.ok = isTrue ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.ok (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.race Miri.Concurrency.DataRaceResult.race = isTrue ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.race (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) Miri.Concurrency.DataRaceResult.ok = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) Miri.Concurrency.DataRaceResult.race = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) Miri.Concurrency.DataRaceResult.internalInvariantViolation = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) Miri.Concurrency.DataRaceResult.outOfBounds = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.internalInvariantViolation (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.internalInvariantViolation Miri.Concurrency.DataRaceResult.internalInvariantViolation = isTrue ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.outOfBounds (Miri.Concurrency.DataRaceResult.invalidClockUpdate error) = isFalse ⋯
• Miri.Concurrency.instDecidableEqDataRaceResult.decEq Miri.Concurrency.DataRaceResult.outOfBounds Miri.Concurrency.DataRaceResult.outOfBounds = isTrue ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqDataRaceResult : DecidableEq DataRaceResult

Equations

• Miri.Concurrency.instDecidableEqDataRaceResult = Miri.Concurrency.instDecidableEqDataRaceResult.decEq

@[instance_reducible]

instance Miri.Concurrency.instReprDataRaceResult : Repr DataRaceResult

Equations

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

def Miri.Concurrency.instReprDataRaceResult.repr : DataRaceResult → Nat → Std.Format

Equations

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

structure Miri.Concurrency.AtomicMemoryCellClocks : Type

Per-byte metadata attached to atomic memory.

• readVector : VClock

  Most recent atomic reads by thread.

• writeVector : VClock

  Most recent atomic writes by thread.

• syncVector : VClock

  Clock released by the current modification/release sequence.

• size : Option ByteSize

  One uniform size, or none after concurrent differently-sized reads.

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicMemoryCellClocks : Repr AtomicMemoryCellClocks

Equations

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

def Miri.Concurrency.instReprAtomicMemoryCellClocks.repr : AtomicMemoryCellClocks → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedAtomicMemoryCellClocks : Inhabited AtomicMemoryCellClocks

Equations

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

def Miri.Concurrency.AtomicMemoryCellClocks.new (size : ByteSize) : AtomicMemoryCellClocks

Initialize atomic metadata for the first access of a given size.

Equations

• Miri.Concurrency.AtomicMemoryCellClocks.new size = { size := some size }

inductive Miri.Concurrency.NaWriteType : Type

Non-atomic write kinds counted by the detector, including lifetime writes.

• Allocate : NaWriteType
• Write : NaWriteType
• Retag : NaWriteType
• Deallocate : NaWriteType

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqNaWriteType : DecidableEq NaWriteType

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprNaWriteType : Repr NaWriteType

Equations

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

def Miri.Concurrency.instReprNaWriteType.repr : NaWriteType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedNaWriteType : Inhabited NaWriteType

Equations

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

inductive Miri.Concurrency.AtomicAccessType : Type

Atomic accesses tracked by one memory cell.

• Load (ordering : AtomicReadOrd) : AtomicAccessType
• Store : AtomicAccessType
• Rmw : AtomicAccessType

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicAccessType : DecidableEq AtomicAccessType

Equations

• Miri.Concurrency.instDecidableEqAtomicAccessType = Miri.Concurrency.instDecidableEqAtomicAccessType.decEq

def Miri.Concurrency.instDecidableEqAtomicAccessType.decEq (x✝ x✝¹ : AtomicAccessType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqAtomicAccessType.decEq (Miri.Concurrency.AtomicAccessType.Load a) (Miri.Concurrency.AtomicAccessType.Load b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessType.decEq (Miri.Concurrency.AtomicAccessType.Load ordering) Miri.Concurrency.AtomicAccessType.Store = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessType.decEq (Miri.Concurrency.AtomicAccessType.Load ordering) Miri.Concurrency.AtomicAccessType.Rmw = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessType.decEq Miri.Concurrency.AtomicAccessType.Store (Miri.Concurrency.AtomicAccessType.Load ordering) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessType.decEq Miri.Concurrency.AtomicAccessType.Store Miri.Concurrency.AtomicAccessType.Store = isTrue ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessType.decEq Miri.Concurrency.AtomicAccessType.Rmw (Miri.Concurrency.AtomicAccessType.Load ordering) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessType.decEq Miri.Concurrency.AtomicAccessType.Rmw Miri.Concurrency.AtomicAccessType.Rmw = isTrue ⋯

def Miri.Concurrency.instReprAtomicAccessType.repr : AtomicAccessType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicAccessType : Repr AtomicAccessType

Equations

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

inductive Miri.Concurrency.AccessType : Type

Access category used by Miri's race classifier.

• NaRead (readType : NaReadType) : AccessType
• NaWrite (writeType : NaWriteType) : AccessType
• AtomicLoad : AccessType
• AtomicStore : AccessType
• AtomicRmw : AccessType

def Miri.Concurrency.instDecidableEqAccessType.decEq (x✝ x✝¹ : AccessType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaRead a) (Miri.Concurrency.AccessType.NaRead b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaRead readType) (Miri.Concurrency.AccessType.NaWrite writeType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaRead readType) Miri.Concurrency.AccessType.AtomicLoad = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaRead readType) Miri.Concurrency.AccessType.AtomicStore = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaRead readType) Miri.Concurrency.AccessType.AtomicRmw = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaWrite writeType) (Miri.Concurrency.AccessType.NaRead readType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaWrite a) (Miri.Concurrency.AccessType.NaWrite b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaWrite writeType) Miri.Concurrency.AccessType.AtomicLoad = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaWrite writeType) Miri.Concurrency.AccessType.AtomicStore = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq (Miri.Concurrency.AccessType.NaWrite writeType) Miri.Concurrency.AccessType.AtomicRmw = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicLoad (Miri.Concurrency.AccessType.NaRead readType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicLoad (Miri.Concurrency.AccessType.NaWrite writeType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicLoad Miri.Concurrency.AccessType.AtomicLoad = isTrue ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicStore (Miri.Concurrency.AccessType.NaRead readType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicStore (Miri.Concurrency.AccessType.NaWrite writeType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicStore Miri.Concurrency.AccessType.AtomicStore = isTrue ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicRmw (Miri.Concurrency.AccessType.NaRead readType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicRmw (Miri.Concurrency.AccessType.NaWrite writeType) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAccessType.decEq Miri.Concurrency.AccessType.AtomicRmw Miri.Concurrency.AccessType.AtomicRmw = isTrue ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAccessType : DecidableEq AccessType

Equations

• Miri.Concurrency.instDecidableEqAccessType = Miri.Concurrency.instDecidableEqAccessType.decEq

def Miri.Concurrency.instReprAccessType.repr : AccessType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAccessType : Repr AccessType

Equations

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

def Miri.Concurrency.AccessType.isAtomic : AccessType → Bool

Equations

• Miri.Concurrency.AccessType.AtomicLoad.isAtomic = true
• Miri.Concurrency.AccessType.AtomicStore.isAtomic = true
• Miri.Concurrency.AccessType.AtomicRmw.isAtomic = true
• (Miri.Concurrency.AccessType.NaRead readType).isAtomic = false
• (Miri.Concurrency.AccessType.NaWrite writeType).isAtomic = false

def Miri.Concurrency.AccessType.isRead : AccessType → Bool

Equations

• Miri.Concurrency.AccessType.AtomicLoad.isRead = true
• (Miri.Concurrency.AccessType.NaRead readType).isRead = true
• (Miri.Concurrency.AccessType.NaWrite writeType).isRead = false
• Miri.Concurrency.AccessType.AtomicStore.isRead = false
• Miri.Concurrency.AccessType.AtomicRmw.isRead = false

def Miri.Concurrency.AccessType.isRetag : AccessType → Bool

Equations

• (Miri.Concurrency.AccessType.NaRead Miri.Concurrency.NaReadType.Retag).isRetag = true
• (Miri.Concurrency.AccessType.NaWrite Miri.Concurrency.NaWriteType.Retag).isRetag = true
• (Miri.Concurrency.AccessType.NaRead Miri.Concurrency.NaReadType.Read).isRetag = false
• (Miri.Concurrency.AccessType.NaWrite Miri.Concurrency.NaWriteType.Allocate).isRetag = false
• (Miri.Concurrency.AccessType.NaWrite Miri.Concurrency.NaWriteType.Write).isRetag = false
• (Miri.Concurrency.AccessType.NaWrite Miri.Concurrency.NaWriteType.Deallocate).isRetag = false
• Miri.Concurrency.AccessType.AtomicLoad.isRetag = false
• Miri.Concurrency.AccessType.AtomicStore.isRetag = false
• Miri.Concurrency.AccessType.AtomicRmw.isRetag = false

structure Miri.Concurrency.MemoryCellClocks : Type

Per-byte vector-clock state exactly corresponding to MemoryCellClocks fields.

• write : VectorIdx × VTimestamp

  Last non-atomic write thread and timestamp.

• writeType : NaWriteType

  Kind of the most recent non-atomic write.

• read : VClock

  Vector clock of non-atomic reads since the last write.

• atomicOps : Option AtomicMemoryCellClocks

  Additional metadata, lazily created for atomic accesses.

@[instance_reducible]

instance Miri.Concurrency.instReprMemoryCellClocks : Repr MemoryCellClocks

Equations

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

def Miri.Concurrency.instReprMemoryCellClocks.repr : MemoryCellClocks → Nat → Std.Format

Equations

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

def Miri.Concurrency.MemoryCellClocks.new (allocationTimestamp : VTimestamp) (allocationIndex : VectorIdx) : MemoryCellClocks

Initialize one byte as a newly allocated non-atomic location.

Equations

• Miri.Concurrency.MemoryCellClocks.new allocationTimestamp allocationIndex = { write := (allocationIndex, allocationTimestamp), writeType := Miri.Concurrency.NaWriteType.Allocate }

def Miri.Concurrency.MemoryCellClocks.writeWasBefore (cell : MemoryCellClocks) (clock : VClock) : Bool

Whether the last non-atomic write happens before the supplied clock.

Equations

• cell.writeWasBefore clock = decide (cell.write.snd.time ≤ (clock.index cell.write.fst).time)

def Miri.Concurrency.MemoryCellClocks.writeClock (cell : MemoryCellClocks) : VClock

Materialize the singleton write clock used by diagnostics.

Equations

• cell.writeClock = Miri.Concurrency.VClock.newWithIndex cell.write.fst cell.write.snd

def Miri.Concurrency.MemoryCellClocks.atomicAccess (cell : MemoryCellClocks) (thread : ThreadClockSet) (accessSize : ByteSize) (isWrite : Bool) : Except DataRaceResult AtomicMemoryCellClocks

The source's size-state transition for an atomic access.

Equations

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

structure Miri.Concurrency.MemoryCellClocks.Transition : Type

A cell operation returns mutated states even when a race is detected. This matches the source's mutation-before-check order; execution then terminates at the caller.

• cell : MemoryCellClocks
• thread : ThreadClockSet
• result : DataRaceResult

def Miri.Concurrency.MemoryCellClocks.instReprTransition.repr : Transition → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.MemoryCellClocks.instReprTransition : Repr Transition

Equations

• Miri.Concurrency.MemoryCellClocks.instReprTransition = { reprPrec := Miri.Concurrency.MemoryCellClocks.instReprTransition.repr }

def Miri.Concurrency.MemoryCellClocks.atomicReadDetect (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : Transition

Record an atomic load, then check whether the non-atomic write is ordered.

Equations

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

def Miri.Concurrency.MemoryCellClocks.atomicWriteDetect (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : Transition

Record an atomic write, then check prior non-atomic writes and reads.

Equations

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

def Miri.Concurrency.MemoryCellClocks.loadAcquire (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) (syncClock : Option VClock := none) : Transition

Atomic load-acquire: detect the access and then acquire either the supplied weak-memory synchronization clock or the cell's release-sequence clock.

Equations

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

def Miri.Concurrency.MemoryCellClocks.loadRelaxed (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) (syncClock : Option VClock := none) : Transition

Atomic load-relaxed: it accumulates the synchronization clock for a later acquire fence instead of joining the happens-before clock immediately.

Equations

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

def Miri.Concurrency.MemoryCellClocks.storeRelease (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : Transition

Atomic release store publishes the thread's happens-before clock.

Equations

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

def Miri.Concurrency.MemoryCellClocks.storeRelaxed (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : Transition

Atomic relaxed store breaks the previous release sequence, replacing it with the thread's release-fence clock.

Equations

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

def Miri.Concurrency.MemoryCellClocks.rmwRelease (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : Transition

Release RMW extends (rather than replaces) the prior release sequence.

Equations

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

def Miri.Concurrency.MemoryCellClocks.rmwRelaxed (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : Transition

Relaxed RMW extends the release sequence with the current release-fence clock.

Equations

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

def Miri.Concurrency.MemoryCellClocks.nonAtomicReadDetect (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (readType : NaReadType) : Transition

Non-atomic read: mark the current thread timestamp with the exact read kind, check non-atomic and atomic writes, and record the read clock.

Equations

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

def Miri.Concurrency.MemoryCellClocks.nonAtomicWriteDetect (cell : MemoryCellClocks) (thread : ThreadClockSet) (index : VectorIdx) (writeType : NaWriteType) : Transition

Non-atomic write: check prior writes, reads, and atomic accesses; on success replace the write timestamp, reset read clocks, and remove atomic metadata.

Equations

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

structure Miri.Concurrency.AccessRange : Type

A memory byte range, using the exact rustc_abi Size byte counts.

• start : ByteSize
• size : ByteSize

def Miri.Concurrency.instDecidableEqAccessRange.decEq (x✝ x✝¹ : AccessRange) : Decidable (x✝ = x✝¹)

Equations

• Miri.Concurrency.instDecidableEqAccessRange.decEq { start := a, size := a_1 } { start := b, size := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAccessRange : DecidableEq AccessRange

Equations

• Miri.Concurrency.instDecidableEqAccessRange = Miri.Concurrency.instDecidableEqAccessRange.decEq

def Miri.Concurrency.instReprAccessRange.repr : AccessRange → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAccessRange : Repr AccessRange

Equations

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

structure Miri.Concurrency.AllocationRanges : Type

Sparse representation of DedupRangeMap<MemoryCellClocks>. Unmodified bytes share the allocation's initial cell; changed bytes are stored as overrides. Range boundaries and deduplication are storage details, while this representation preserves the per-byte values that the detector reads.

• length : ByteSize
• initialCell : MemoryCellClocks
• overrides : List (Nat × MemoryCellClocks)

@[instance_reducible]

instance Miri.Concurrency.instReprAllocationRanges : Repr AllocationRanges

Equations

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

def Miri.Concurrency.instReprAllocationRanges.repr : AllocationRanges → Nat → Std.Format

Equations

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

def Miri.Concurrency.AllocationRanges.cellAt (ranges : AllocationRanges) (offset : Nat) : Except DataRaceResult MemoryCellClocks

Read one byte; an absent override denotes its original allocation state.

Equations

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

def Miri.Concurrency.AllocationRanges.setCell (ranges : AllocationRanges) (offset : Nat) (value : MemoryCellClocks) : Except DataRaceResult AllocationRanges

Replace one byte, preserving an explicit bounds failure.

Equations

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

structure Miri.Concurrency.VClockAlloc : Type

Allocation-level vector-clock state (AllocState in pinned Miri). The construction input is the allocation timestamp already selected by Miri's MemoryKind classification; that interpreter classification is outside this pure clock-state module.

• allocRanges : AllocationRanges

def Miri.Concurrency.instReprVClockAlloc.repr : VClockAlloc → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprVClockAlloc : Repr VClockAlloc

Equations

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

@[reducible, inline]

abbrev Miri.Concurrency.AllocState : Type

Equations

• Miri.Concurrency.AllocState = Miri.Concurrency.VClockAlloc

def Miri.Concurrency.VClockAlloc.newAllocation (length : ByteSize) (allocationTimestamp : VTimestamp) (allocationIndex : VectorIdx) : VClockAlloc

Initialize every byte with the allocation write state, represented lazily.

Equations

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

def Miri.Concurrency.VClockAlloc.cellAt (allocation : VClockAlloc) (offset : Nat) : Except DataRaceResult MemoryCellClocks

Read one byte's effective clock state.

Equations

• allocation.cellAt offset = allocation.allocRanges.cellAt offset

def Miri.Concurrency.VClockAlloc.setCell (allocation : VClockAlloc) (offset : Nat) (cell : MemoryCellClocks) : Except DataRaceResult VClockAlloc

Replace one byte's clock state.

Equations

• allocation.setCell offset cell = do let ranges ← allocation.allocRanges.setCell offset cell pure { allocRanges := ranges }

structure Miri.Concurrency.VClockAlloc.RangeTransition : Type

Result of applying a per-cell race-detection hook to a byte range.

• allocation : VClockAlloc
• thread : ThreadClockSet
• result : DataRaceResult

@[instance_reducible]

instance Miri.Concurrency.VClockAlloc.instReprRangeTransition : Repr RangeTransition

Equations

• Miri.Concurrency.VClockAlloc.instReprRangeTransition = { reprPrec := Miri.Concurrency.VClockAlloc.instReprRangeTransition.repr }

def Miri.Concurrency.VClockAlloc.instReprRangeTransition.repr : RangeTransition → Nat → Std.Format

Equations

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

def Miri.Concurrency.VClockAlloc.runRange (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (action : MemoryCellClocks → ThreadClockSet → MemoryCellClocks.Transition) : RangeTransition

Apply a source per-byte operation over a validated allocation range. Earlier bytes remain updated if a later byte reports a race, matching Miri's mutable range iteration order.

Equations

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

def Miri.Concurrency.VClockAlloc.readNonAtomic (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (index : VectorIdx) (readType : NaReadType) : RangeTransition

Allocation-level non-atomic read hook, applying the exact per-byte read detector and preserving regular-read versus retag-read categorization.

Equations

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

def Miri.Concurrency.VClockAlloc.writeNonAtomic (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (index : VectorIdx) (writeType : NaWriteType) : RangeTransition

Allocation-level non-atomic write hook.

Equations

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

def Miri.Concurrency.VClockAlloc.atomicRead (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : RangeTransition

Allocation-level atomic-read race hook. Atomic ordering synchronization is applied by the corresponding per-cell load transition.

Equations

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

def Miri.Concurrency.VClockAlloc.atomicWrite (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) : RangeTransition

Allocation-level atomic-write race hook.

Equations

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

def Miri.Concurrency.VClockAlloc.atomicLoad (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) (ordering : AtomicReadOrd) (syncClock : Option VClock := none) : RangeTransition

Apply the source's ordering-specific atomic-load transition to every byte in a range. The optional clock overrides the cell's release-sequence clock, as it does when a weak-memory load selects a particular store.

Equations

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

def Miri.Concurrency.VClockAlloc.atomicStore (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) (ordering : AtomicWriteOrd) : RangeTransition

Apply Miri's atomic-store ordering to every byte in a range.

Equations

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

def Miri.Concurrency.VClockAlloc.atomicRmw (allocation : VClockAlloc) (range : AccessRange) (thread : ThreadClockSet) (index : VectorIdx) (accessSize : ByteSize) (ordering : AtomicRwOrd) : RangeTransition

Apply one atomic read-modify-write per byte, performing the read half before the write half and extending the release sequence according to the source ordering.

Equations

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

def Miri.Concurrency.VClockAlloc.syncClock (allocation : VClockAlloc) (range : AccessRange) : Except DataRaceResult VClock

Join the release-sequence clocks attached to every byte in a memory range, matching VClockAlloc::sync_clock. Uninitialized atomic metadata contributes the zero clock.

Equations

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