Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground.
In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite.
We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq. We use the former for validation, and to assess specification coverage. To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation. We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration. We prove (on paper) the soundness of the core Sail type system.
We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.
Thu 17 JanDisplayed time zone: Belfast change
10:36 - 12:04
|Iron: Managing Obligations in Higher-Order Concurrent Separation Logic|
Aleš Bizjak Aarhus University, Daniel Gratzer , Robbert Krebbers Delft University of Technology, Lars Birkedal Aarhus UniversityLink to publication DOI Media Attached File Attached
José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela Sampaio Imperial College London, UK, Philippa Gardner Imperial College LondonLink to publication DOI Media Attached File Attached
|ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS|
Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Arm Ltd, Kathryn E. Gray University of Cambridge, 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, Shaked Flur University of Cambridge, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of CambridgeLink to publication DOI Media Attached File Attached
|Exploring C Semantics and Pointer Provenance|
Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Brooks Davis SRI International, Stephen Kell University of Kent, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge, Peter Sewell University of CambridgeLink to publication DOI Media Attached File Attached