1 Task 1: Semantic tools
The mathematical models of mainstream-system abstractions that we need have to be expressed in well-defined formal languages, for the sake of mathematical precision, and those languages need good software tool support, to let us handle large and complex definitions. In this task we address the foundational question of what formal languages are suitable for this purpose; the pragmatic question of what facilities good tool support should provide; and the engineering question of actually building these tools to a sufficient quality to be usable by other researchers and by industry staff. In REMS we are developing and using the following tools.
- Sail is a domain-specific language for concurrent and sequential
processor instruction-set architecture (ISA)
definition, to define the architected behaviour of processor instructions [1, 7, 8, 10, 12].
Sail is a first-order functional/imperative language, with a lightweight dependent
types for vector lengths and indices and for integer ranges.
We have Sail models for ARMv8-A, RISC-V, MIPS, and CHERI-MIPS, each
complete enough to boot an OS, and for smaller fragments of IBM POWER
and x86.
Given a Sail ISA definition, the tool will automatically generate
emulators in C and OCaml; theorem-prover definitions in Isabelle,
HOL4, and Coq (via Lem for the first two); and versions of the
semantics integrated with our RMEM concurrency model tool
(both a deep embedding, in a form that can be executed by
a Sail interpreter written in Lem, and shallow embeddings to Lem and
OCaml).
Sail is available under a permissive open-source licence.
Sail web page: http://www.cl.cam.ac.uk/users/pes20/sail/.
Sail github repo: https://github.com/rems-project/sail.
Sail is also available as an OPAM package. - Lem is a tool for large-scale portable semantic specification [2, 6].
Lem supports the definition language of a typed higher-order
logic, for type, function, and inductive-relation definitions, in
an OCaml-like syntax. Given such a definition, the tool will
automatically generate (for various fragments) OCaml,
LaTeX, HTML, Isabelle, HOL4, and Coq versions.
Lem is used in our work on
Sail, concurrent architecture specification, CakeML, ELF linking,
Concurrent C semantics, Sequential C semantics, and SibylFS POSIX
filesystem semantics.
Lem is available under a permissive open-source licence.
Lem web page: http://www.cl.cam.ac.uk/users/pes20/lem/.
Lem github repo: https://github.com/rems-project/lem/. - Ott is a tool for
programming language
definitions, supporting user-defined syntax and inductive
relations over it, and compiling to LaTeX and to theorem-prover
definitions for Coq, HOL4, and
Isabelle; it can also generates some OCaml infrastructure,
e.g. concrete substitution functions and simple parser and
pretty-printer code.
Ott is available under a permissive open-source licence.
In 2017, the original Ott paper
Ott: Effective Tool Support for the Working Semanticist. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. ICFP 2007
was awarded the ACM SIGPLAN Most Influential ICFP Paper Award (the papers are judged by their influence over the past decade).
Ott web page: http://www.cl.cam.ac.uk/users/pes20/ott/.
Ott github repo: https://github.com/ott-lang/ott.
Ott is also available as an OPAM package. - L3 is an earlier domain-specific language for sequential processor
instruction-set architecture (ISA) semantic definition [4, 64].
L3 exports to HOL4 and Isabelle/HOL, including Hoare-triple
generation, and to SML, providing reasonably fast emulation.
L3 is used in our work on CakeML, CHERI, and instruction testing.
L3 is available under a permissive open-source licence.
L3 github repo: https://acjf3.github.io/l3.
In Task 1, we have also worked on: