Write a Blog >>
Fri 22 Jan 2016 10:30 - 10:55 at Grand Bay South - Track 2: Semantics and memory models Chair(s): Alexey Gotsman

In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware.

Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor’s architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined. We therefore first develop a concurrency model with a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardware-designer intuition. This means it can be discussed in detail with ARM architects. We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t.~the first.

The instruction semantics involves further difficulties, handling the mass of detail and the subtle intensional information required to interface to the concurrency model. We have a novel ISA description language, with a lightweight dependent type system, letting us do both with a rather direct represention of the ARM reference manual instruction descriptions.

We build a tool from the combined semantics that lets one explore, either interactively or exhaustively, the full range of architecturally allowed behaviour, for litmus tests and (small) ELF executables. We prove correctness of some optimisations needed for tool performance.

We validate the models by discussion with ARM staff, and by comparison against ARM hardware behaviour, for ISA single- instruction tests and concurrent litmus tests.

poster (poster.pdf)411KiB

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10: Track 2: Semantics and memory modelsResearch Papers at Grand Bay South
Chair(s): Alexey GotsmanIMDEA
10:30 - 10:55
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Research Papers
Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity of Cambridge
Media Attached File Attached
10:55 - 11:20
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Research Papers
Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached
11:20 - 11:45
Overhauling SC atomics in C11 and OpenCL
Research Papers
John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London
Pre-print File Attached
11:45 - 12:10
Taming Release-Acquire Consistency
Research Papers
Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Pre-print Media Attached File Attached