Rigorous Architectural Modelling for Production Multiprocessors

Presented as part of the 2015 HCSS conference.

Abstract:

Processor architectures are critical interfaces in computing, but they are typically defined only by prose and pseudocode documentation. This is especially problematic for the subtle concurrency behaviour of weakly consistent multiprocessors such as ARM and IBM POWER: the traditional documentation does not define precisely what programmer-observable behaviour is (and is not) allowed for concurrent code; it is not executable as a test oracle for pre-Silicon or post-Silicon hardware testing; it is not executable as an emulator for software testing; and it is not mathematically rigorous enough to serve as a foundation for software verification.

We present a rigorous architectural envelope model for IBM POWER multiprocessors, and similar work in progress for ARM, that aims to support all of these for small-but-intricate test cases, integrating an operational concurrency model with an ISA model for the sequential behaviour of a substantial fragment of the user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in a new ISA description language).  The key question is the interface between these two: we have to allow all the required relaxed-memory behaviour, without overcommitting to some particular microarchitectural model.  Our models can be automatically translated into executable code, which, combined with front-ends for concurrency litmus tests and ELF executables, can interactively or exhaustively explore all the allowed behaviours of small test cases.

This is joint work by S. Flur, K. Gray, G. Kerneis*, L. Maranget**, C. Pulte, S. Sarkar***, and P. Sewel, University of Cambridge (* Google, ** Inria, *** St Andrews).  It is funded in part by the EPSRC REMS grant (Rigorous Engineering of Mainstream Systems), EP/K008528/1.