Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Mon 15 Jun 2020 07:50 - 08:30 at REMS/DeepSpec live stream - REMS-DeepSpec Session 2

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

Conference Day
Mon 15 Jun

Displayed time zone: Pacific Time (US & Canada) change

07:00 - 09:00
REMS-DeepSpec Session 2REMS-DeepSpec at REMS/DeepSpec live stream
Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
P: Alasdair ArmstrongUniversity of Cambridge, Thomas BauereissUniversity of Cambridge, Brian CampbellUniversity of Edinburgh, Alastair ReidGoogle Research, Kathryn E. GrayFacebook, Robert M. NortonUniversity of Cambridge, Prashanth MundkurSRI International, Mark WassellUniversity of Cambridge, Jon FrenchUniversity of Cambridge, Christopher PulteUniversity of Cambridge, UK, Shaked FlurGoogle, Ian StarkThe University of Edinburgh, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Peter SewellUniversity of Cambridge
ARMv8 and RISC-V relaxed memory concurrency
P: Shaked FlurGoogle, P: Christopher PulteUniversity of Cambridge, UK, Luc MarangetInria Paris, Will DeaconARM Ltd., Susmit SarkarUniversity of St. Andrews, Ben Simner, Jean Pichon-PharabodUniversity of Cambridge, UK, Jeehoon KangKAIST, Sung-Hwan LeeSeoul National University, South Korea, Chung-Kil HurSeoul National University, South Korea, Alasdair ArmstrongUniversity of Cambridge, Ohad KammarUniversity of Edinburgh, Jon FrenchUniversity of Cambridge, Kathryn E. GrayFacebook, Ali SezginUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached