ARMv8 and RISC-V relaxed memory concurrency
Five years ago the concurrency semantics of the ARM processor architecture, while pervasive in practice, was poorly documented, understudied, and hard to reliably program, let alone formally reason about. Since then, partly due to our extended collaboration with Arm, its concurrency architecture has received a major revision, clarifying the semantics, simplifying and restricting the allowed concurrency behaviour, and including in the architecture an official formal concurrency specification co-developed and proved-equivalent with ours. RISC-V has recently adopted a semantics closely following that of ARMv8. In this talk we present three formal models of the ARMv8 and RISC-V concurrent architectures: (1) an abstract micro-architectural operational model, (2) an axiomatic model, and (3) a Promising-style operational model, together with their equivalence proofs, executable tools for exploring the semantics and checking the correctness of small concurrent data structure implementations, and ongoing work to extend the concurrency semantics to cover more features (the concurrency semantics of instruction fetches, synchronous exceptions, and virtual memory).
The rmem web interface http://www.cl.cam.ac.uk/users/pes20/rmem supports interactive exploration of these operational models, and the isla-axiomatic web interface https://isla-axiomatic.cl.cam.ac.uk/ supports exploration of the axiomatic models.
| Slides (both parts) (slides.pdf) | 926KiB |
Mon 15 JunDisplayed time zone: Pacific Time (US & Canada) change
07:00 - 09:00 | |||
07:00 40mTalk | Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V REMS-DeepSpec P: Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Google Research, Kathryn E. Gray Facebook, Robert M. Norton University of Cambridge, Prashanth Mundkur SRI International, Mark Wassell University of Cambridge, Jon French University of Cambridge, Christopher Pulte University of Cambridge, UK, Shaked Flur Google, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of Cambridge | ||
07:50 40mTalk | ARMv8 and RISC-V relaxed memory concurrency REMS-DeepSpec P: Shaked Flur Google, P: Christopher Pulte University of Cambridge, UK, Luc Maranget Inria Paris, Will Deacon ARM Ltd., Susmit Sarkar University of St. Andrews, Ben Simner , Jean Pichon-Pharabod University of Cambridge, UK, Jeehoon Kang KAIST, Sung-Hwan Lee Seoul National University, South Korea, Chung-Kil Hur Seoul National University, South Korea, Alasdair Armstrong University of Cambridge, Ohad Kammar University of Edinburgh, Jon French University of Cambridge, Kathryn E. Gray Facebook, Ali Sezgin University of Cambridge, Peter Sewell University of Cambridge File Attached | ||