Rigorous Acrchitectural Modelling for Production Multiprocessors

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.

In this talk, I will present a rigorous architectural envelope model for IBM POWER and ARM multiprocessors, 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 (expressed in a new ISA description language). I will present the interface between
the two, whose requirements drove the development of our new language Sail. I will also present the interesting aspects of Sail's dependent
type system, which is a light-weight system balancing the benefits of static bounds and effects checking with the usability of the language
for engineers. Futher, 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.

Joint work with: S. Flur, G. Kerneis*, L. Maranget**, D. Mulligan, C. Pulte, S. Sarkar***, and P. Sewell, University of Cambridge
(* Google, ** Inria, *** St Andrews)