Sail
Sail is a language for describing the instruction-set architecture
(ISA) semantics of processors. Sail aims to provide a
engineer-friendly, vendor-pseudocode-like language for describing
instruction semantics. It is essentially a first-order imperative
language, but with lightweight dependent typing for numeric types and
bitvector lengths, which are automatically checked using Z3. It has
been used for several models and papers, listed below.
Given a Sail definition, the tool will type-check it and generate
documentation, executable emulators (in C and OCaml), theorem-prover definitions (for
Isabelle, HOL4, and Coq), and definitions to integrate with our
RMEM
and
isla-axiomatic
tools for
concurrency semantics.
The Isla engine provides SMT-based symbolic evaluation for Sail models,
and the Islaris verification tool integrates Isla output with the Iris program logic to support proof about binary code in Coq.
Not all models are integrated with all tools - see the most recent papers and models for
descriptions of the current state.
The Sail source and documentation are available
from a github repository, and as an OPAM package as described there.
Sail is currently being used for ARM, RISC-V, MIPS, CHERI-MIPS, IBM Power, and x86 models, variously ranging from full definitions to core user-mode fragments, and either here or in separate repositories:
Sail Armv9.3-A and ARMv8.5-A ISA models, automatically generated from the ARM-internal ASL reference, as used in the ARM ARM.
Sail ARMv8.3-A ISA model. This is the "public" model described in our POPL 2019 paper, now superseded by the above.
Sail ARMv8-A ISA model, handwritten. This is a handwritten user-mode fragment.
Sail Morello (CHERI-Arm) ISA model, automatically generated from the Arm-internal ASL definition. This was the basis for our Morello security proofs.
Sail RISC-V ISA model, handwritten. This has been adopted by the RISC-V Foundation as their formal ISA specification.
Sail CHERI RISCV model, handwritten.
Sail MIPS and CHERI-MIPS ISA models, handwritten.
Sail IBM POWER ISA model, automatically generated from IBM XML documentation. This is a user-mode fragment.
Sail x86 ISA model, handwritten. This is a handwritten user-mode fragment.
The hand-written ARMv8-A, IBM POWER, and x86 models are currently not in sync with the latest version of Sail, which is the (default) sail2 branch on Github. These and the RISC-V model are integrated with our RMEM tool for operational-model concurrency semantics.
The complete Arm and RISC-V models are integrated with our isla-axiomatic tool for axiomatic-model concurrency semantics.
People
Papers
-
Multicore Semantics: Making Sense of Relaxed Memory (MPhil
slides), Peter Sewell, Christopher Pulte, Shaked Flur, Mark
Batty, Luc Maranget, and Alasdair Armstrong, October 2022.
[ bib |
.pdf ]
-
Islaris: Verification of Machine Code Against Authoritative
ISA Semantics.
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell,
Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell.
In PLDI 2022.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Verified Security for the Morello Capability-enhanced
Prototype Arm Architecture.
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong,
Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter
Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
In CAV 2021.
[ bib |
doi |
pdf |
http |
abstract ]
-
ISA Semantics for ARMv8-A, RISC-V, and
CHERI-MIPS.
Alasdair Armstrong, 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.
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
-
Formalisation of MiniSail in the Isabelle Theorem
Prover.
Alasdair Armstrong, Neel Krishnaswami, Peter Sewell, and Mark
Wassell.
In Automated Reasoning Workshop (ARW) 2018, Two-page abstract.
[ bib |
project page |
pdf |
abstract ]
-
Detailed Models of Instruction Set Architectures: From
Pseudocode to Formal Semantics.
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Shaked Flur,
Kathryn E. Gray, Prashanth Mundkur, Robert M. Norton, Christopher Pulte,
Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell.
In Automated Reasoning Workshop (ARW) 2018, Two-page abstract.
[ bib |
project page |
pdf |
abstract ]
-
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and
Operational Models for ARMv8.
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit
Sarkar, and Peter Sewell.
In POPL 2018.
[ bib |
doi |
project page |
errata |
pdf |
abstract ]
-
Mixed-size Concurrency: ARM, POWER, C/C++11, and
SC.
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc
Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell.
In POPL 2017.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Modelling the ARMv8 architecture, operationally: concurrency
and ISA.
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali
Sezgin, Luc Maranget, Will Deacon, and Peter Sewell.
In POPL 2016.
[ bib |
doi |
project page |
pdf |
abstract ]
-
An integrated concurrency and core-ISA architectural envelope
definition, and test oracle, for IBM POWER multiprocessors
.
Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher
Pulte, Susmit Sarkar, and Peter Sewell.
In MICRO 2015.
[ bib |
doi |
pdf |
abstract ]
Funding
This work was partially supported by the UK Government Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694).
This project has received funding from the European Research Council
(ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 789108).
This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous Engineering for
Mainstream Systems,
an ARM iCASE award, and EPSRC IAA KTF funding.
This work was partially supported by donations from Arm and Google.
Approved for public release; distribution is unlimited. This research
is sponsored by the Defense Advanced Research Projects Agency (DARPA)
and the Air Force Research Laboratory (AFRL), under contracts
FA8750-10-C-0237 ("CTSRD") and FA8650-18-C-7809 ("CIFV"). The views,
opinions, and/or findings contained in these articles OR presentations are
those of the author(s)/presenter(s) and should not be interpreted as
representing the official views or policies of the Department of
Defense or the U.S. Government.