ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures

Computing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and “user-mode” concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the system semantics, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software.In this paper we establish a robust model for one aspect of system semantics: instruction fetch and cache maintenance for ARMv8-A. Systems code relies on executing instructions that were written by data writes, e.g. in program loading, dynamic linking, JIT compilation, debugging, and OS configuration, but hardware implementations are often highly optimised, e.g. with instruction caches, linefill buffers, out-of-order fetching, branch prediction, and instruction prefetching, which can affect programmer-observable behaviour. It is essential, both for programming and verification, to abstract from such microarchitectural details as much as possible, but no more. We explore the key architecture design questions with a series of examples, discussed in detail with senior Arm staff; capture the architectural intent in operational and axiomatic semantic models, extending previous work on “user-mode” concurrency; make these models executable as test oracles for small examples; and experimentally validate them against hardware behaviour (finding a bug in one hardware device). We thereby bring these subtle issues into the mathematical domain, clarifying the architecture and enabling future work on system software verification.

Parloom: A New Low-Power Set-Associative Instruction Cache Architecture Utilizing Enhanced Counting Bloom Filter and Partial Tags

The cache system dissipates a significant amount of energy compared to the other memory components. This will be intensified if a cache is designed with a set-associative structure to improve the system performance because the parallel accesses to the entries of a set for tag comparisons lead to even more energy consumption. In this paper, a novel method is proposed as a combination of a counting Bloom filter and partial tags to mitigate the energy consumption of set-associative caches. This new hybrid method noticeably decreases the cache energy consumption especially in highly-associative instruction caches. In fact, it uses an enhanced counting Bloom filter to predict cache misses with a high accuracy as well as partial tags to decrease the overall cache size. This way, unnecessary tag comparisons can be prevented and therefore, the cache energy consumption is considerably reduced. Based on the simulation results, the proposed method provides the energy reduction from 22% to 31% for 4-way–32-way set-associative L1 caches bigger than 16[Formula: see text]kB running the MiBench programs. The improvements are attained with a negligible system performance degradation compared to the traditional cache system.