There are four interlinked Tasks:
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 :
- Lem, a tool for large-scale portable semantic specification (supporting a typed higher-order logic and compiling to OCaml, LaTeX, Coq, HOL4, and Isabelle/HOL),
- L3, a domain-specific language for sequential processor instruction-set semantic definition, exporting to HOL4, Isabelle/HOL, and SML;
- Sail, a domain-specific language for concurrent and sequential processor instruction-set definition, currently principally exporting to a Lem interpreter that can be linked with our multiprocessor concurrency models.
- For production multiprocessor semantics, for IBM POWER we have integrated an operational concurrency model with an ISA model for the sequential behaviour of all the non-floating-point non-vector user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in our Sail ISA description language).
- For ARMv8 we have developed operational concurrency models that have a clear relationship to the intuitions of the ARM designers; these are integrated with an user-mode Sail ISA description, currently manually derived from the ARM documentation.
- We are currently porting an ARM-internal machine-readable ISA definition, covering essentially the full ISA, to Sail; we have a legal agreement with ARM in place to let us make this available for verification research in due course.
- Our collaboration between semantic modelling researchers and systems researchers working on CHERI (a multiprocessor hardware design with explicit capabilities) has developed into a central tool for the latter, using L3 ISA models for CHERI (and MIPS) for testing and debugging CHERI hardware and software, and for exploring new design options. These models are complete enough to boot FreeBSD. We are also currently porting them to Sail.
- Semantics-driven random testing has been developed both for CHERI and for an L3 model of ARMv6, and ARM Cortex-M0 implementations, equipped with accurate cycle counts.
- We also continue to develop and maintain sequential L3 models for ARMv6-A, ARMv8 and x86-64, to support CakeML, a verified ML compiler, and also other research groups elsewhere.
- We have also studied the concurrency behaviour of GPUs, for NVIDIA and AMD hardware.
- Sequential C: our Cerberus project is building a semantic model for a significant fragment of C as it exists in current practice. We investigating the de facto standards of C as it is implemented and used, and also addressing the ISO standard produced by the ISO WG14 C committee. The Cerberus thread-local semantics is factored via an elaboration into a simpler Core language, to make it conceptually and mathematically tractable. Cerberus is executable, to explore all behaviours or single paths of test programs; a preliminary experiment in translation validation for the front-end of Clang, for very simple programs, uses it for verification. We are also engaging with the ISO WG14 C Standard Committee.
- Another view of the C de facto standard is provided by our work on how to make existing systems software run on the CHERI experimental processor, identifying the tensions between the additional safety guarantees that CHERI's capability system enforces vs the more freewheeling assumptions of some existing software.
- For concurrent C, we are addressing both the ISO C/C++11 concurrency model we previously formalised (Batty et al.) and potential future models that would fix the so-called `thin-air problem' that C/C++11 suffers from. For the former, we have a C11 operational semantics that is proved equivalent (in Isabelle/HOL) to the Batty et al. axiomatic model, and moreover has been integrated into our Cerberus sequential C model to allow litmus tests to be executed. For the latter, we have published a proposal for a model that admits compiler optimisation while avoiding the thin-air problem; we are currently working on extending this and developing its metatheory.
- ELF Linking: Systems software in reality is written not just in more-or-less conventional programming languages, like C and C++, but also using a complex menagerie of techniques to control the linking process. This `linker speak' is often poorly understood by working programmers and has largely been neglected by language researchers. Our linksem project has surveyed the many use-cases that linkers support and developed the first validated formalisation of a realistic executable and linkable format, ELF, together with an executable specification of linking with substantial coverage. This ELF model is used in our ppcmem2 ARM/Power emulation tool and we are looking to incorporate it into CakeML; we have started to prove metatheory (in Isabelle/HOL), currently focussed on relocation correctness.
From a more systems-oriented perspective, we continue to develop our
libcrunchtool to dynamically detect type errors in C code, and to use the underlying machinery for metadata to evolve the runtime services provided by Unix processes towards those of VMs.
- We explored the use of coroutines for concurrency in C, based on a continuation-passing style translator.
- Linking with our GPU architectural modelling described in Task 2, we have also worked on precise specification of (and corrections to) the OpenCL 2.0 concurrency memory model, which incorporates features similar to those of the C/C++11 concurrency model we studied earlier.
- We have also worked on concurrency optimisation, adding optimisations to remove redundant memory barriers in the ARM backend of LLVM, in work incorporated into the main LLVM codebase.
- We have studied C compilation under GCC to the ARMv6-M instruction set of the Cortex-M0 embedded processor, as in Task 2. Results suggest that this preserves enough code structure to support using the translation validation approach of Thomas Sewell, Myreen and Klein (see Task 4) to lift execution costs from machine instructions up to C~source.
- Our compiler verification work has contributed to the CakeML verified ML compiler project, and extended the seL4 verification down to the binary level. We also contributed to the CerCo verified compiler.
- Work on compositional verification has developed more modular verification techniques, addressed vertical compositionality, and developed a proof system for reasoning about concurrent algorithms above the x86-TSO architecture model.
- We have extended concurrent program logics with reasoning about how programs are affected by, and recover from, host failures (crashes). [link]
- We have also introduced a logic, Total-TaDA, to prove total correctness of fine-grained concurrent programs. This logic was created by extending TaDA with well-founded termination reasoning.[link]
- New tool support for Hybrid Separation Logic supports verification of some simple programs operating on graphs and acyclic graphs (whereas separation logic based approaches have up to now mostly only been able to work on lists and trees).
- We have also continued to work on linearisability-based approaches to concurrent algorithm verification, and developed new consistency conditions weaker than linearisability.
- Looking in detail at the POSIX filesystem interface, a theoretical and empirical investigation into the behaviour of filesystem implementations has produced an extensively tested model, SibylFS, of POSIX, Linux, and MacOSX filesystems.
- We developed a program logic characterisation for a core of POSIX, covering fine-grain concurrency. [link]
- We have developed a clean-slate specification and implementation of the Transport Layer Security (TLS) protocol, nqsb-TLS. This is fundamental to internet use, but its implementations have a history of security flaws.
- We have restarted the NetSem network semantics from 10 years ago, as Huginn-TCP. In collaboration with the FreeBSD project, and with the DARPA CADETS project at BAE/Cambridge/Memorial, we now collect traces from a current FreeBSD system using DTrace; CADETS is extending DTrace to support this work. Initial traces validate with a slightly adapted model. Exploiting DTrace lets us substantially simplify the instrumentation and to instrument in more places, which should allow nondeterminism to be resolved early; together with Moore's-law advances in checking speed, this should let us produce a more usable test oracle.