Outcome classification for the pinned clock/atomic/store-buffer code. data_race.rs::report_data_race returns TerminationInfo::DataRace: although upstream transports this as a machine stop, it is a detected Rust UB outcome. Clock overflow, invalid metadata indices and impossible buffer handles are source assertions/panics, not races. They remain explicit internal stops. Sources: concurrency/{data_race,vector_clock,weak_memory}.rs and data_structures/range_object_map.rs. This does not classify pointer accesses, atomic alignment, invalid orderings or unsupported atomic sizes; their source checks happen in the interpreter before these clock/buffer callbacks.

def Miri.Interpreter.ConcurrencyErrors.global : Concurrency.GlobalStateError → StepError

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ConcurrencyErrors.global Miri.Concurrency.GlobalStateError.childIsActiveThread = Miri.Interpreter.StepError.invalidProgram "spawn clock child is the active thread"
• Miri.Interpreter.ConcurrencyErrors.global Miri.Concurrency.GlobalStateError.invalidReuseChoice = Miri.Interpreter.StepError.invalidProgram "clock-index reuse choice outside source candidates"

def Miri.Interpreter.ConcurrencyErrors.storeBuffer : Concurrency.StoreBufferAllocError → StepError

Equations

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

def Miri.Interpreter.ConcurrencyErrors.dataRace : Concurrency.DataRaceResult → StepError

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ConcurrencyErrors.dataRace Miri.Concurrency.DataRaceResult.ok = Miri.Interpreter.StepError.invalidProgram "successful data-race result supplied as an error"
• Miri.Interpreter.ConcurrencyErrors.dataRace Miri.Concurrency.DataRaceResult.race = Miri.Interpreter.StepError.undefinedBehavior "DataRace"
• Miri.Interpreter.ConcurrencyErrors.dataRace Miri.Concurrency.DataRaceResult.internalInvariantViolation = Miri.Interpreter.StepError.invalidProgram "data-race metadata invariant"
• Miri.Interpreter.ConcurrencyErrors.dataRace Miri.Concurrency.DataRaceResult.outOfBounds = Miri.Interpreter.StepError.invalidProgram "data-race metadata range outside allocation"

def Miri.Interpreter.ConcurrencyErrors.weakMemory : Concurrency.WeakMemoryError → StepError

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ConcurrencyErrors.weakMemory Miri.Concurrency.WeakMemoryError.emptyStoreBuffer = Miri.Interpreter.StepError.invalidProgram "source store buffer is empty"
• Miri.Interpreter.ConcurrencyErrors.weakMemory Miri.Concurrency.WeakMemoryError.bufferTooLong = Miri.Interpreter.StepError.invalidProgram "source store-buffer length invariant"
• Miri.Interpreter.ConcurrencyErrors.weakMemory Miri.Concurrency.WeakMemoryError.selectedIndexOutOfBounds = Miri.Interpreter.StepError.invalidProgram "selected source store-buffer index is absent"

def Miri.Interpreter.ConcurrencyErrors.atomic : Concurrency.AtomicDispatchError → StepError

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ConcurrencyErrors.atomic (Miri.Concurrency.AtomicDispatchError.globalState error) = Miri.Interpreter.ConcurrencyErrors.global error
• Miri.Interpreter.ConcurrencyErrors.atomic (Miri.Concurrency.AtomicDispatchError.validation error) = Miri.Interpreter.ConcurrencyErrors.dataRace error
• Miri.Interpreter.ConcurrencyErrors.atomic (Miri.Concurrency.AtomicDispatchError.syncClock error) = Miri.Interpreter.ConcurrencyErrors.dataRace error
• Miri.Interpreter.ConcurrencyErrors.atomic (Miri.Concurrency.AtomicDispatchError.storeBuffer error) = Miri.Interpreter.ConcurrencyErrors.storeBuffer error
• Miri.Interpreter.ConcurrencyErrors.atomic (Miri.Concurrency.AtomicDispatchError.weakMemory error) = Miri.Interpreter.ConcurrencyErrors.weakMemory error
• Miri.Interpreter.ConcurrencyErrors.atomic Miri.Concurrency.AtomicDispatchError.missingCreatedBuffer = Miri.Interpreter.StepError.invalidProgram "source atomic store did not create its buffer"