Atomic intrinsic ordering and access checks

This module ports the ordered pre-memory portion of Miri's atomic path: machine.rs converts intrinsic orderings before calling the atomic operation, and data_race.rs::atomic_access_check derives the required alignment from the access size, checks it, resolves allocation identity, then applies the read-only-memory rules. The pointer resolver, machine alignment policy, live allocation lookup, and mutability lookup are explicit callbacks because they belong to the concrete interpreter state.

This does not perform a scalar load/store, RMW calculation, bounds/permission hook, or the later race-clock and store-buffer updates. Callers pass callbacks closed over the actual place and must invoke this check before those effects, matching Miri's source order.

inductive Miri.Concurrency.AtomicAccessKind : Type

The access class tested by atomic_access_check.

• load (ordering : AtomicReadOrd) : AtomicAccessKind
• store : AtomicAccessKind
• rmw : AtomicAccessKind

def Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq (x✝ x✝¹ : AtomicAccessKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq (Miri.Concurrency.AtomicAccessKind.load a) (Miri.Concurrency.AtomicAccessKind.load b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq (Miri.Concurrency.AtomicAccessKind.load ordering) Miri.Concurrency.AtomicAccessKind.store = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq (Miri.Concurrency.AtomicAccessKind.load ordering) Miri.Concurrency.AtomicAccessKind.rmw = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq Miri.Concurrency.AtomicAccessKind.store (Miri.Concurrency.AtomicAccessKind.load ordering) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq Miri.Concurrency.AtomicAccessKind.store Miri.Concurrency.AtomicAccessKind.store = isTrue ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq Miri.Concurrency.AtomicAccessKind.rmw (Miri.Concurrency.AtomicAccessKind.load ordering) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq Miri.Concurrency.AtomicAccessKind.rmw Miri.Concurrency.AtomicAccessKind.rmw = isTrue ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicAccessKind : DecidableEq AtomicAccessKind

Equations

• Miri.Concurrency.instDecidableEqAtomicAccessKind = Miri.Concurrency.instDecidableEqAtomicAccessKind.decEq

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicAccessKind : Repr AtomicAccessKind

Equations

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

def Miri.Concurrency.instReprAtomicAccessKind.repr : AtomicAccessKind → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.ReadOnlyAtomicViolation : Type

The first read-only-memory restriction selected by the source match.

• storeOrRmw : ReadOnlyAtomicViolation
• oversizedLoad : ReadOnlyAtomicViolation
• nonRelaxedLoad : ReadOnlyAtomicViolation

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqReadOnlyAtomicViolation : DecidableEq ReadOnlyAtomicViolation

Equations

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

def Miri.Concurrency.instReprReadOnlyAtomicViolation.repr : ReadOnlyAtomicViolation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprReadOnlyAtomicViolation : Repr ReadOnlyAtomicViolation

Equations

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

inductive Miri.Concurrency.AtomicAccessError (PointerError MutabilityError : Type) : Type

Failures from the source-owned stages of atomic_access_check. The alignment-construction and allocation-expectation variants record the pinned Rust unwrap/expect boundaries; they are never treated as successful accesses.

• alignmentConstructionPanic {PointerError MutabilityError : Type} (reason : ABI.AlignError) : AtomicAccessError PointerError MutabilityError
• pointerAlignment {PointerError MutabilityError : Type} (reason : PointerError) : AtomicAccessError PointerError MutabilityError
• allocationExpectationPanic {PointerError MutabilityError : Type} (reason : PointerError) : AtomicAccessError PointerError MutabilityError
• mutabilityLookup {PointerError MutabilityError : Type} (reason : MutabilityError) : AtomicAccessError PointerError MutabilityError
• undefinedBehavior {PointerError MutabilityError : Type} (violation : ReadOnlyAtomicViolation) : AtomicAccessError PointerError MutabilityError

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicAccessError {PointerError✝ MutabilityError✝ : Type} [DecidableEq PointerError✝] [DecidableEq MutabilityError✝] : DecidableEq (AtomicAccessError PointerError✝ MutabilityError✝)

Equations

• Miri.Concurrency.instDecidableEqAtomicAccessError = Miri.Concurrency.instDecidableEqAtomicAccessError.decEq

def Miri.Concurrency.instDecidableEqAtomicAccessError.decEq {PointerError✝ MutabilityError✝ : Type} [DecidableEq PointerError✝] [DecidableEq MutabilityError✝] (x✝ x✝¹ : AtomicAccessError PointerError✝ MutabilityError✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqAtomicAccessError.decEq (Miri.Concurrency.AtomicAccessError.pointerAlignment reason) (Miri.Concurrency.AtomicAccessError.mutabilityLookup reason_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessError.decEq (Miri.Concurrency.AtomicAccessError.pointerAlignment reason) (Miri.Concurrency.AtomicAccessError.undefinedBehavior violation) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessError.decEq (Miri.Concurrency.AtomicAccessError.mutabilityLookup reason) (Miri.Concurrency.AtomicAccessError.pointerAlignment reason_1) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessError.decEq (Miri.Concurrency.AtomicAccessError.mutabilityLookup reason) (Miri.Concurrency.AtomicAccessError.undefinedBehavior violation) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessError.decEq (Miri.Concurrency.AtomicAccessError.undefinedBehavior violation) (Miri.Concurrency.AtomicAccessError.pointerAlignment reason) = isFalse ⋯
• Miri.Concurrency.instDecidableEqAtomicAccessError.decEq (Miri.Concurrency.AtomicAccessError.undefinedBehavior violation) (Miri.Concurrency.AtomicAccessError.mutabilityLookup reason) = isFalse ⋯

def Miri.Concurrency.instReprAtomicAccessError.repr {PointerError✝ MutabilityError✝ : Type} [Repr PointerError✝] [Repr MutabilityError✝] : AtomicAccessError PointerError✝ MutabilityError✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicAccessError {PointerError✝ MutabilityError✝ : Type} [Repr PointerError✝] [Repr MutabilityError✝] : Repr (AtomicAccessError PointerError✝ MutabilityError✝)

Equations

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

structure Miri.Concurrency.AtomicAccessOps (AllocId PointerError MutabilityError : Type) : Type

Interpreter-owned callbacks used by the source atomic access check. pointerTryGetAllocId is the ptr_try_get_alloc_id(ptr, 0) operation. Its address error is kept distinct because the pinned source immediately calls expect on this result.

• checkPtrAlign : ABI.Align → Except PointerError Unit
• pointerTryGetAllocId : Except PointerError AllocId
• getAllocMutability : AllocId → Except MutabilityError Memory.Mutability

def Miri.Concurrency.atomicAccessCheck {AllocId PointerError MutabilityError : Type} (size pointerSize : ABI.Size) (kind : AtomicAccessKind) (ops : AtomicAccessOps AllocId PointerError MutabilityError) : Except (AtomicAccessError PointerError MutabilityError) Unit

Port of atomic_access_check after its concrete MPlace callbacks are supplied. The order is size-to-alignment conversion, pointer alignment, allocation identity, mutability lookup, and the ordered read-only rules.

Equations

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

inductive Miri.Concurrency.AtomicIntrinsicError (PointerError MutabilityError : Type) : Type

Errors before an atomic operation reaches its place access check. Invalid read/write/fence orderings correspond to the pinned conversion panics and are kept explicit rather than weakened.

• invalidOrdering {PointerError MutabilityError : Type} (reason : AtomicOrderingError) : AtomicIntrinsicError PointerError MutabilityError
• accessCheck {PointerError MutabilityError : Type} (reason : AtomicAccessError PointerError MutabilityError) : AtomicIntrinsicError PointerError MutabilityError

def Miri.Concurrency.instDecidableEqAtomicIntrinsicError.decEq {PointerError✝ MutabilityError✝ : Type} [DecidableEq PointerError✝] [DecidableEq MutabilityError✝] (x✝ x✝¹ : AtomicIntrinsicError PointerError✝ MutabilityError✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqAtomicIntrinsicError {PointerError✝ MutabilityError✝ : Type} [DecidableEq PointerError✝] [DecidableEq MutabilityError✝] : DecidableEq (AtomicIntrinsicError PointerError✝ MutabilityError✝)

Equations

• Miri.Concurrency.instDecidableEqAtomicIntrinsicError = Miri.Concurrency.instDecidableEqAtomicIntrinsicError.decEq

def Miri.Concurrency.instReprAtomicIntrinsicError.repr {PointerError✝ MutabilityError✝ : Type} [Repr PointerError✝] [Repr MutabilityError✝] : AtomicIntrinsicError PointerError✝ MutabilityError✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprAtomicIntrinsicError {PointerError✝ MutabilityError✝ : Type} [Repr PointerError✝] [Repr MutabilityError✝] : Repr (AtomicIntrinsicError PointerError✝ MutabilityError✝)

Equations

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

def Miri.Concurrency.prepareAtomicLoad {AllocId PointerError MutabilityError : Type} (ordering : AtomicOrdering) (size pointerSize : ABI.Size) (ops : AtomicAccessOps AllocId PointerError MutabilityError) : Except (AtomicIntrinsicError PointerError MutabilityError) AtomicReadOrd

Machine atomic_load: ordering conversion precedes the access check.

Equations

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

def Miri.Concurrency.prepareAtomicStore {AllocId PointerError MutabilityError : Type} (ordering : AtomicOrdering) (size pointerSize : ABI.Size) (ops : AtomicAccessOps AllocId PointerError MutabilityError) : Except (AtomicIntrinsicError PointerError MutabilityError) AtomicWriteOrd

Machine atomic_store: ordering conversion precedes the access check.

Equations

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

def Miri.Concurrency.prepareAtomicRmw {AllocId PointerError MutabilityError : Type} (ordering : AtomicOrdering) (size pointerSize : ABI.Size) (ops : AtomicAccessOps AllocId PointerError MutabilityError) : Except (AtomicIntrinsicError PointerError MutabilityError) AtomicRwOrd

Machine atomic_rmw: its ordering conversion accepts every ordering, then the shared atomic access check runs before the interpreter reads memory.

Equations

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

def Miri.Concurrency.prepareAtomicCompareExchange {AllocId PointerError MutabilityError : Type} (successOrdering failureOrdering : AtomicOrdering) (size pointerSize : ABI.Size) (ops : AtomicAccessOps AllocId PointerError MutabilityError) : Except (AtomicIntrinsicError PointerError MutabilityError) (AtomicRwOrd × AtomicReadOrd)

Machine compare-exchange converts the success ordering, then the failure read ordering, before atomic_compare_exchange performs its access check.

Equations

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

def Miri.Concurrency.prepareAtomicFence (ordering : AtomicOrdering) (singlethread : Bool) : Except AtomicOrderingError (Option AtomicFenceOrd)

A single-thread fence is a source NOP and skips ordering conversion. A multithread fence uses the checked AtomicFenceOrd::from conversion.

Equations

• Miri.Concurrency.prepareAtomicFence ordering singlethread = if singlethread = true then Except.ok none else Except.map some (Miri.Concurrency.AtomicFenceOrd.ofOrdering ordering)