Low-level systems verification

Historically the semantics of programming languages have been defined in ad hoc ways, through a mix of prose description and reference implementations, leading
to ambiguity and errors. Attempts to avoid these pitfalls often result in complex standards documents, which suffer similar issues while simultaneously
being harder to consume for users. The alternative approach of describing the semantics of languages through mathematical formalism has attracted research
interest as a means to improve the robustness of the descriptions of practical languages. This approach allows language designers to specify a language with no ambiguity about its behaviour and to prove that desirable properties of the language hold, while also giving the users of the language a formal basis on which to reason about their programs. Unfortunately some language features are difficult to formalise. The behaviour of concurrent programs accessing shared memory is challenging to give an accurate semantics for, especially under weak memory models. Recently semantics for concurrent access to shared memory have been produced for both various assemblies and C, but the two have not been related directly.
The behaviour of software that accesses shared memory from multiple threads can be difficult to reason about as the order instructions are executed in varies. Consequently it is valuable to be able to use automated tooling to prove correctness, which requires a semantics of the programming language. Security critical software, like the kernel, is often multithreaded and uses shared memory for performance reasons. Such software is often programmed in a mix of C and assembly which expose different models of concurrent memory access, so it is necessary to reason using formal semantics of both languages in the same program.
The REMS project produced a number of useful artefacts in this area, including formal memory models or partial formal memory models of several ISAs, a formal memory model for C11 and operational semantics for ISO and de facto C. CompCertTSO is a verified compiler for a dialect of C, which verifiably correctly implements the memory model of the source language in the generated code. Unfortunately its memory model is not appropriate for a performance sensitive compiler because it forbids many optimisations, a problem exacerbated by weaker memory models (e.g. ARM). Work on provably correct compilation of C11 concurrency primitives has produced compilation schemes for the primitives. This work leaves scope for producing an actual certified compiler which handles these concurrency primitives.
The proposed work plans to build off of the work of the REMS project to show how compilation on one or more platforms correctly implements the C memory model in terms of the assembly memory model, potentially building on the CompCert formally verified C compiler. CompCert presently lacks support for C11's concurrency features and important non-standard important features like inline assembly. It may be desirable to work on semantics for both C and the ISAs that are more compositional in the structure of programs. Some existing semantics require proofs to be whole program arguments, which can be complex and less resilient to program modifications. One avenue of work in this direction is "promising semantics", which divorce the reordering of instructions and of their effects on memory. Related work may involve constructing semantics of concurrent programs' interaction with the cache. This is particularly significant since effects on the cache are a source of information leakage used in recent speculative execution exploits. Using formal methods to protect against speculative execution attacks may also require semantics of speculative execution, but improving the semantics of caching is a valuable first in this direction.