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 papers, listed below. Given a Sail definition, the tool will type-check it and generate executable emulators, in C and OCaml, theorem-prover definitions for Isabelle, HOL4, and Coq, and definitions to integrate with our RMEM tool for concurrency semantics. This is all work in progress, and some theorem-prover definitions do not yet work for the more complex models; see the most recent papers and the ARMv8.5-A model 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 concurrency semantics.

People

Papers

Funding

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. 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.