Frame-local vector clocks and their transfer into addressable memory from pinned src/concurrency/data_race.rs:1303–1404. Diagnostic spans are omitted; timestamp times and packed read kinds are preserved.

structure Miri.Concurrency.LocalRace.LocalClocks : Type

• write : VTimestamp
• writeType : NaWriteType
• read : VTimestamp

@[instance_reducible]

instance Miri.Concurrency.LocalRace.instReprLocalClocks : Repr LocalClocks

Equations

• Miri.Concurrency.LocalRace.instReprLocalClocks = { reprPrec := Miri.Concurrency.LocalRace.instReprLocalClocks.repr }

def Miri.Concurrency.LocalRace.instReprLocalClocks.repr : LocalClocks → Nat → Std.Format

Equations

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

structure Miri.Concurrency.LocalRace.FrameState : Type

• localClocks : Array (Nat × LocalClocks)

@[instance_reducible]

instance Miri.Concurrency.LocalRace.instReprFrameState : Repr FrameState

Equations

• Miri.Concurrency.LocalRace.instReprFrameState = { reprPrec := Miri.Concurrency.LocalRace.instReprFrameState.repr }

def Miri.Concurrency.LocalRace.instReprFrameState.repr : FrameState → Nat → Std.Format

Equations

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

def Miri.Concurrency.LocalRace.FrameState.get (frame : FrameState) (localId : Nat) : LocalClocks

Equations

• frame.get localId = (Option.map Prod.snd (Array.find? (fun (entry : Nat × Miri.Concurrency.LocalRace.LocalClocks) => entry.fst == localId) frame.localClocks)).getD { }

def Miri.Concurrency.LocalRace.FrameState.set (frame : FrameState) (localId : Nat) (clocks : LocalClocks) : FrameState

Equations

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

def Miri.Concurrency.LocalRace.FrameState.remove (frame : FrameState) (localId : Nat) : FrameState

Equations

• frame.remove localId = { localClocks := Array.filter (fun (entry : Nat × Miri.Concurrency.LocalRace.LocalClocks) => entry.fst != localId) frame.localClocks }

inductive Miri.Concurrency.LocalRace.Error : Type

• global (error : GlobalStateError) : Error
• clock (error : ClockError) : Error
• memory (error : DataRaceResult) : Error
• allocationWriterMismatch (expected actual : VectorIdx) : Error

@[instance_reducible]

instance Miri.Concurrency.LocalRace.instReprError : Repr Error

Equations

• Miri.Concurrency.LocalRace.instReprError = { reprPrec := Miri.Concurrency.LocalRace.instReprError.repr }

def Miri.Concurrency.LocalRace.instReprError.repr : Error → Nat → Std.Format

Equations

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

structure Miri.Concurrency.LocalRace.Result (A : Type) : Type

• frame : FrameState
• global : GlobalState
• outcome : Except Error A

def Miri.Concurrency.LocalRace.localWrite (frame : FrameState) (global : GlobalState) (threads : ThreadManager) (localId : Nat) (storageLive : Bool) : Result Unit

Source local_write only records clocks when race_detecting is true. StorageLive resets the previous read timestamp; ordinary writes retain it.

Equations

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

def Miri.Concurrency.LocalRace.localRead (frame : FrameState) (global : GlobalState) (threads : ThreadManager) (localId : Nat) : Result Unit

Source local_read first sets the active timestamp's packed read type, then saves that full timestamp into the local map, without incrementing time.

Equations

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

structure Miri.Concurrency.LocalRace.MaterializeResult : Type

• frame : FrameState
• allocation : VClockAlloc
• outcome : Except Error Unit

def Miri.Concurrency.LocalRace.localMovedToMemory (frame : FrameState) (global : GlobalState) (threads : ThreadManager) (localId : Nat) (allocation : VClockAlloc) : MaterializeResult

Transfer historical local times, not allocation/materialization time. Each byte's atomic metadata is retained. The local map entry is removed before any assertion; earlier bytes remain updated on a later invariant failure.

Equations

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