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
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
Sail is available under a permissive open-source licence.
- 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.
- Ott is a tool for
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
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).
- 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: