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

Joint work with Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell

Sail is a custom domain-specific language for ISA semantics, in which we have developed formal models for ARMv8-A, RISC-V, and MIPS, as well as CHERI-based capability extensions for both RISC-V and MIPS. Our model of ARMv8-A is automatically translated from the authoritative Arm-internal architecture specification language (ASL) definitions. All the above models contain enough system-level features to boot various operating systems, including Linux and FreeBSD, and various smaller microkernels and hypervisors.

Using Sail we are able to generate executable emulators for testing and validation, generate theorem prover definitions for Isabelle, HOL4 and Coq, translate into SMT for automatic verification, and also integrate into our RMEM tool for operational relaxed-memory concurrency semantics.

Recently, we have added a symbolic execution tool for Sail specifications, Isla, which allows us to also support axiomatic concurrency models in the style of Alglave and Maranget’s herd7 tool. This allows us to evaluate the allowed relaxed-memory behaviours for tests that span the full range of the instruction-set architecture. For example, we can specify how instruction cache maintenance instructions interact with self-modifying code in a relaxed-memory setting, or other interesting architectural features not well-covered by existing tools.

Github sail: https://github.com/rems-project/sail, and the Sail-ARM https://github.com/rems-project/sail-arm, Sail-RISC-V https://github.com/rems-project/sail-riscv models.

Mon 15 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change

07:00 - 09:00: REMS-DeepSpec Session 2REMS-DeepSpec at REMS/DeepSpec live stream
07:00 - 07:40
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
07:50 - 08:30
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