Armv8-A System Semantics: Instruction Fetch ArmIF
A rigorous concurrency model for the 'system semantics' of instruction fetch and instruction/data-cache maintenance in Armv8-A, capturing self-modifying code, program loading, dynamic linking and JIT patterns (Sec. 4-5). It extends the base Armv8-A user-mode concurrency (Flat) model with instruction-fetch events, a fetched-from (fetch-read) relation, and instruction-cache (IC) and data-cache (DC) maintenance events, showing that instruction fetches are more relaxed than data accesses and that even coherence for the fetched stream is not guaranteed without explicit IC/DC/ISB synchronisation. Given in both an operational (extending Flat) and a functionally-equivalent axiomatic style. On programs that perform no instruction fetch or cache maintenance it coincides with the base Armv8-A user-mode model (validated identical over the 8950-test Flat regression suite, Sec. 6); outside that fragment it admits additional executions arising from stale instruction caches.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Reasoning guarantees
- yes Coherence
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Equivalent to
- ARMv8 / AArch64 Memory Model — Simner et al., ESOP 2020: the instruction-fetch system-semantics model is built by extending the base Armv8-A user-mode concurrency (Flat) model with instruction-fetch and IC/DC cache-maintenance events (Sec. 4-5, 'extending previous work on user-mode concurrency'). Validation (Sec. 6) reports the model's results are identical to the base model over all 8950 non-instruction-fetch Flat regression tests, so on the fragment with no instruction fetch or cache maintenance it coincides with base ARMv8; outside that fragment (self-modifying code, IC/DC) it admits additional relaxed executions, hence the equivalence is fragment-restricted.
References
- Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell. ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures. ESOP 2020, 2020. doi:10.1007/978-3-030-44914-8_23