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:

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

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.