Axiomatic Concurrency Model

Overview

An axiomatic concurrency model is a declarative specification of the concurrent behavior of an instruction set architecture. Instead of describing how a processor executes step by step (as in an operational model), an axiomatic model characterizes which candidate executions of a program are allowed by defining relations—such as program order (po), reads-from (rf), coherence order (co), from-reads (fr), and memory order—and stating constraints that these relations must satisfy.

These constraints typically include:

Internal visibility requirements (e.g., a write must propagate to the same thread before that thread observes it).
Coherence (a total per-location order on writes).
Atomicity conditions such as multicopy atomicity, in which writes become visible to all other threads simultaneously.
Preserved program order relations for specific pairs of memory operations.

An execution is valid with respect to an axiomatic model if there exists an assignment of events to relations that satisfies all constraints; the architecture permits precisely those executions that are valid.

Role in ISA Specification

Axiomatic concurrency models are used to give a precise, mathematical definition of the memory model part of an ISA specification. They complement:

Operational semantics of the core ISA, which define what each instruction does in isolation.
Pseudocode specifications in architecture reference manuals, which are typically non-formal.

By axiomatizing memory behavior, hardware designers, compiler writers, and verification tool developers obtain a single reference against which implementations, compilers, and litmus tests can be checked.

Notable Examples

Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 (Pulte et al., POPL 2017) introduced a multicopy-atomic axiomatic model together with a corresponding operational model for ARMv8, aimed at simplifying the ARMv8 memory model while remaining faithful to hardware behavior. ^[1]
Modelling the ARMv8 Architecture Operationally: Concurrency and ISA (Flur et al., POPL 2016) provided the operational foundation that the subsequent axiomatic model formalized and simplified. ^[2]
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models (Armstrong et al., CAV 2021) combines a full ISA semantics (in Sail) with an axiomatic concurrency model to enable litmus-test style memory-model verification at the architectural level. ^[1]

Tool Support

The Isla tool uses an axiomatic concurrency model alongside Sail-based ISA semantics to check candidate executions derived from hardware or litmus tests. ^[1]

Related Technique

Axiomatic hardware–software contracts use axiomatic-style specifications to characterize the interface between hardware and software (for example for security properties), treating hardware behavior as a relation over candidate traces. ^[3]

Connection to Other Formalisms

Operational concurrency models define concurrency via abstract machines with explicit nondeterministic choices; axiomatic models are typically derived by collecting the executions admitted by an operational model and constraining them with relations.
Operational ISA semantics (e.g., Sail specifications of ARMv8-A, RISC-V, CHERI-MIPS) provide the per-instruction behavior; axiomatic models layer on top to define memory behavior across threads.

References

Pulte et al., Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8, POPL 2017. ^[1]
Flur et al., Modelling the ARMv8 Architecture Operationally: Concurrency and ISA, POPL 2016. ^[2]
Armstrong et al., Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models, CAV 2021. ^[1]
Mosier et al., Axiomatic hardware-software contracts for security, ISCA 2022 (background on axiomatic hardware–software contracts). ^[3]