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 [MOG+14, Cle14]. Lem supports the definition language of a typed higher-order logic, and compiles to LaTeX and (for various fragments) to OCaml, LaTeX, HTML, Coq, HOL4, and Isabelle/HOL. Lem is available under an open-source licence6. It is used in our work on Sail, concurrent architecture specification, CakeML, ELF linking, Concurrent C semantics, Sequential C semantics, and SibylFS POSIX filesystem semantics.
- L3, a domain-specific language for sequential processor instruction-set semantic definition [Fox15, FMTK17]. L3 exports to HOL4 and Isabelle/HOL, including Hoare-triple generation, and to SML, providing reasonably fast emulation. L3 is available under an open-source licence7. It is used in our work on CakeML, CHERI, and instruction testing.
- Sail, a domain-specific language for concurrent and sequential processor instruction-set definition [GKM+15, FGP+16]. Sail has a richer type system than L3, with lightweight dependent types for vector lengths and indices and for integer ranges; it supports integration of instruction-set semantics with concurrency models. Sail exports 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 an open-source licence8. It is used in our work on concurrent architecture speification and CHERI.
We continue to maintain the Ott tool for programming language semantic definition (supporting user-defined syntax and inductive relations over it, and compiling to LaTeX, Coq, HOL4, and Isabelle/HOL). Ott is available under an open-source licence9, and it is available as an OPAM package.
We also study the foundations needed for future semantic tools, focussed on Nominal Type Theory [PMD15].
In Year 4:
- Paper [FMTK17] was published.
- We continue to maintain Lem, L3, Sail, and Ott as needed. We have shifted Sail and Ott development to public repositories (respectively bitbucket and github) and packaged Ott as an OPAM package.
- We have extended Sail with support for generating shallow embeddings of Sail definitions in various targets, for more efficient execution and to produce usable theorem-prover definitions. [Pulte, Gray]
- We have written a draft manual for Sail (distributed also to ARM).
- We have worked on the translation from the ARM-internal ARMv8-A instruction specification into Sail, as discussed in Task 2. [Gray]
- Two new PhD students with interests in Semantic tools have started at Cambrige: Conrad Watt (moved from the Imperial REMS group), and Mark Wassell.
The first key interface we address is the architectural interface between hardware and software, specifying the multiprocessor behaviours that processor implementations guarantee and that systems code relies on. Normal industrial practice is to specify this interface in informal-prose architecture reference manuals, sometimes with pseudocode descriptions of the sequential instruction semantics, but these descriptions cannot be used directly to test either the hardware below the interface or software above it, or to build verification tools, let alone as a basis for proof. Compounding the problem, architectures must be nondeterministic loose specifications, to accommodate microarchitectural variation, so one cannot simply characterise them with reference implementations.
We are pursuing several directions here, focussed on the ARM and IBM POWER production architectures and on the CHERI research architecture. The ARM architecture is the basis for the processors used in the majority of mobile phones and many other devices; the IBM POWER architecture is used, among other things, for high-performance server machines. For each of those, we have addressed two aspects of the architecture: the behaviour of individual instructions, in the instruction-set architecture (ISA), and the concurrency model describing how instructions in different hardware threads interact.
ARM ISA For the sequential user-mode fragment of the ARMv8-A architecture, we hand-wrote Sail and L3 models (covering the user-mode fragment, without vector instructions, floating-point, or exceptions) [FGP+16]. These are available online10. We tested the Sail model by generating around 8400 single-instruction tests and comparing their behaviour in the model and on ARMv8 hardware. For the sequential aspects of the ARMv8-A architecture, ARM have internally a machine-readable and well-tested description of their full ISA, in their ASL language by Reid et al. We have established a legal agreement with ARM giving us access to this, enabling us to port it to a mathematical model in our Sail language (work in progress) and to distribute that model under a usable licence for other groups to use as a basis for verification. From preliminary discussions there is strong interest in this, e.g. from the seL4 group in NICTA Australia and the DeepSpec NSF Expeditions project. We obtained additional EPSRC Impact Acceleration Account (IAA) funding for some of this work, in the form of a Knowledge Transfer Fellowship for Kathy Gray, with ARM. We also developed sequential L3 models for the ARMv6-A and ARMv7-A architectures and the ARM Cortex-M0 implementations, the former including floating-point and some system-level instructions, and the latter equipped with accurate cycle counts for work on resource-aware compilation [Gray, Flur, Pulte, Fox, Reid (ARM), Campbell, Stark, Sewell]
In Year 4:
- We have worked on the translation from ASL to Sail, to support integration of the ARM instruction semantics with our concurrency models, and to support generation of theorem-prover definitions for the ISA. [Gray, Reid (ARM), Sewell]
We have developed operational models covering substantial parts of the
ARMv8-A concurrency architecture, in close collaboration with ARM staff, and
integrated with the above Sail models of substantial fragments of the user-mode
instruction set architecture [FGP+16, FSP+17].
Our concurrency test suite, maintained jointly with Maranget (INRIA Paris), now includes 11812 ARMv8 tests.
We have found bugs in the hardware produced by a number of vendors
(reported to them and acknowledged as such).
Part of this work is additionally funded by an EPSRC/ARM iCASE PhD studentship
[Flur, Pulte, Gray, Sarkar (St Andrews), Sezgin, Maranget (INRIA Paris), Deacon (ARM), Grisenthwaite (ARM), Sewell]
In Year 4:
- We have extended our models to cover concurrent mixed-size memory accesses; Paper [FSP+17] was published.
- We continue to discuss the intended concurrency semantics with ARM on a regular basis, together identifying and resolving many deep and highly technical questions about what the intended architecture is and how it can be modelled.
ARM Virtual Memory In Year 3, as first steps towards extending our concurrency models to cover virtual memory, TLBs, etc., we hosted a three-week visit from a member of the ARM Linux team, to identify the key concurrent use-patterns, and visits from Mads Dam’s group in KTH Stockholm, who use our L3 ARM ISA model and are developing a virtual memory model. [Martin (ARM), Dam (KTH), Baumann (KTH), Flur, Gray, Pulte, Sezgin, Sewell]
IBM POWER ISA The instruction semantics of IBM POWER are largely described in the vendor documentation with an informal pseudocode, that has not previously been parsed or type-checked. We were provided with an XML export of this, from which we have built a semi-automatic translation to provide a Sail model for the user-mode fragment, without vector instructions, floating-point, or exceptions [GKM+15]. We tested this by generating single-instruction test cases and comparing their behaviour in the model and on POWER 7 hardware; for the 154 user-mode branch and fixed-point instructions, we generated 6984 tests. We also received a donation of a Power 8 server machine from IBM, for concurrency and ISA testing, and hosted a visit from our collaborator there, with other members of the group from St Andrews and INRIA Paris. [Gray, Flur, Kerneis, Mulligan, Pulte, Sarkar (St Andrews), Maranget (INRIA Paris), Williams (IBM), Sewell]
IBM POWER Concurrency
We continue to develop our operational models covering substantial parts of the
IBM POWER architecture, in close collaboration with IBM staff, and
integrated with the above Sail models of substantial fragments of the user-mode
instruction set architecture.
Our concurrency test suite, maintained jointly with Maranget (INRIA
Paris), now includes 27689 POWER tests.
[Flur, Pulte, Sarkar (St Andrews), Maranget (INRIA Paris), Williams
In Year 4:
- We have extended our models to cover concurrent mixed-size memory accesses; Paper [FSP+17] was published.
- We continue to discuss the intended concurrency semantics with IBM on a regular basis.
Model engineering For the above ARM and POWER ISA and concurrency models, we have devoted significant effort to ‘model engineering’: tidying the definitions, addressing performance issues, and establishing an automated regression system. [Flur, Pulte, Gray]
Concurrent Semantics Tool
The above ARM and POWER models
are integrated into a tool that can input either concurrency tests
(“litmus tests”) or ELF binaries, e.g. produced by compilation by
GCC or Clang from C files. This uses our ELF model from Task 3. It supports interactive exploration of
their behaviour in the model and (for small tests) computation of the
sets of all their model-allowed behaviours, which can then be compared
with experimental data, obtained using the litmus tool
(principally developed by Maranget), from
production silicon or simulation.
[Flur, Pulte, French, Sewell]
In Year 4:
- We continue to develop this tool, maintaining the web interface.
- We have added support for the DWARF debug information of C programs.
- We have added functionality akin to a debugger, e.g. allowing setting breakpoints, to let one explore the behaviour of concurrent algorithms with respect to the full concurrency models.
CHERI ISA Clean Slate Trustworthy Secure Research and Development (CTSRD) is a joint research project between SRI International and the University of Cambridge, led by Robert Watson and Simon Moore at Cambridge and Peter Neumann at SRI, supported by DARPA (part of the DARPA CRASH programme) and Google. The project is revisiting the hardware-software security interface for general-purpose CPUs to fundamentally improve security. A key part of this is CHERI [WNW+16, WNW+15, WCD+15, WWN+15]: a processor architecture and implementations supporting hardware-accelerated in-process memory protection and sandboxing model based on a hybrid capability model, together with an open-source operating system and toolchain based on FreeBSD and Clang/LLVM. In contrast to ARM and IBM POWER, this is a research architecture, not a mainstream production architecture, but it is being developed at scale, e.g. with a software stack including a variant of a production OS (FreeBSD).
The CHERI development [WNW+15] uses a formal definition
of the CHERI ISA as a central design tool, supported by REMS: the
primary definition is expressed in our L3 ISA description language,
and we are currently porting it to Sail, including a Sail MIPS model.
These models are complete enough to boot FreeBSD.
The CHERI compiler and operating-system work [WCD+15]
builds on this and also feeds into our Task 3 Cerberus C work, as described below.
We have also started work on formal verification in Isabelle/HOL and
HOL4 of properties of the CHERI ISA.
[CHERI team, Roe, Norton-Wright, Nienhuis, Fox, Gray]
In Year 4:
- Paper [WNW+16] was published.
- We continue to develop our L3 and Sail CHERI and MIPS models, with a focus this year on modelling, testing, and performance assessment for the 128-bit version of CHERI.
- The HOL4 theorem prover was used to verify critical properties of the bit-vector computations that form the basis of CHERI’s 128-bit compressed capability scheme. This helped identify ambiguities and mistakes made in presenting and implementing this scheme.
- We have proved (with mechanised Isabelle proof) some fundamental security properties of the CHERI architecture as a whole.
Processor Testing We have developed a flow for automatically generating interesting sequences of instructions, using theorem-prover and SMT technology to ensure that any necessary preconditions are met [CS14, CS16b, CS16a]. We have applied this to testing our model of the ARM Cortex-M0 microcontroller and to our MIPS and CHERI L3 models, including coverage of exceptions, and found several modelling bugs. We also developed a novel semi-automatic technique to prove invariants of the M0 and CHERI models needed as assumptions in test generation. The method is based on some HOL4 tactics akin to refinement typing, and scales up to models with hundreds of functions. [Campbell, Stark. Roe]
We have produced a generic synthesisable test bench, BlueCheck [NM15]. This has been used to check various microarchitectural properties of CHERI, finding some bugs. It has also been used for teaching in MIT (in the 6.175 Computer Architecture course). [Naylor, Moore]
Our Axe tool [NMM16] for testing the concurrency behaviour of processor storage subsystems (including their cache implementations) has been invaluable in testing multicore CHERI implementations and has also found substantial bugs in the Berkeley RISC-V processor design; it has been incorporated into the main design flow in both cases. [Naylor, Moore]
In Year 4:
- For our instruction-sequence testing, we have improved usability to help others generate tests, increased coverage with all-exceptions mode, tested CHERI in user mode, automatically derived instruction generation from simple instruction decoders, used to quickly set up test generation for 64-bit RISC-V, and started cross testing Sail CHERI model
- It has been used to find a number of bugs in the QEMU-based emulation of CHERI (which have been fixed).
- It also discovered some bugs in the upstream QEMU emulation of the MIPS ISA, which have been reported to QEMU’s maintainers.
- It now has improved testing of load-linked/store-conditional (single core, not multicore); the L3 model of these has also been improved.
- Papers [CS16a, NMM16] were published.
CakeML Architecture Models
This task also provides the L3 architecture models used in the CakeML
verified compiler, further discussed in Task 3.
CakeML uses the above ARMv6-A and ARMv8-A models, together
with MIPS and x86-64 models developed here and a RISC-V model
developed by Prashanth Mundkur at SRI International. [Fox, Mundkur
In Year 4:
- Paper [FMTK17] was published.
- Most of the CakeML activity has centred around adding target support for bignum arithmetic for those models.
- We have completed some bit-vector proofs within the backend verification and worked on speeding up the machine-code encoder evaluation within the logic (for bootstrapping).
- We are currently working on adding floating-point support to CakeML, and to its target models, and extending/improving HOL4’s floating-point development.
GPU Concurrency We studied the concurrency semantics of GPUs, conducting a large empirical study of their behaviour and proposing a model of Nvidia GPU hardware [ABD+15]. [Batty, with colleagues in UCL, Imperial, Utah, and Oxford]
Sequential C (Cerberus)
The C programming language remains central to systems programming, but
its semantics is problematic.
Our work on the sequential aspects of C semantics proceeds on several fronts:
investigating the de facto standards of C as it is implemented and
addressing the ISO standard produced by the ISO WG14 C committee;
and building an executable formal model, Cerberus.
Here we have another strong collaboration with the CHERI work,
with their experience in systems software (and specifically in porting
it to the C supported by CHERI) informing our semantic understanding,
and with this discussion identifying issues with the CHERI design.
We are also investing significant effort in model engineering.
Our initial paper on this [MML+16] was awarded a PLDI 2016 Distinguished
We are participating in the ISO WG14 C standards committee: we
April 2016 (London) and October 2016 (Pittsburgh) committee meetings,
producing committee discussion papers ([MS16b, CMM+16, MS16e, MS16f]
and [MS16d, MS16a, MS16c]),
several issues at length with them.
[Memarian, Borges, Matthiesen, Lingard, Nienhuis, Chisnall, Watson, Sewell]
In Year 4:
- Development of Cerberus continues, especially its de facto standard memory object model and model engineering, and we continue to discuss key issues with the ISO WG14 committee members and others.
- Paper [MML+16] was published and WG14 Committee Papers [MS16d, MS16a, MS16c] were produced.
Concurrent C For concurrent C, we are addressing both the ISO C/C++11 concurrency model we previously contributed to and formalised (Batty et al., POPL 2011) and potential future models that would fix the so-called ‘thin-air problem’ that C/C++11 suffers from.
Batty’s 2014 Cambridge PhD thesis The C11 and C++11 Concurrency Model was awarded the 2015 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award, presented annually to the author of the “outstanding doctoral dissertation in the area of Programming Languages”, and was the winner of the 2015 CPHC/BCS Distinguished Dissertations competition, selected as “the best British PhD/DPhil dissertations in computer science”. The WG14 C committee also approved his remaining defect reports w.r.t. the C11 concurrency model.
We developed 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 [NMS16]. [Nienhuis, Memarian]
We showed that no straightforward adaptation of the C/C++11 axiomatic model, phrased as a consistency predicate over candidate executions, can exclude thin-air reads while also admitting some standard optimisations, identified additional difficulties with undefined behaviour and with mixtures of atomic and nonatomic accesses. We also proved (in HOL4) that the C/C++11 model actually provides the DRF-SC guarantee [BMN+15]. [Batty, Memarian, Nienhuis, Pichon-Pharabod, Sewell]
We proposed a model that admits compiler optimisation while avoiding the thin-air problem [PS16]; we are currently working on extending this and developing its metatheory. [Pichon-Pharabod, Sewell]
Along with the extension of our ARM and IBM POWER hardware models to support mixed-size accesses, we proposed a corresponding extension to the C/C++11 axiomatic model to support mixed-size non-atomic accesses [FSP+17]. [Nienhuis, Batty]
We also discussed a new problem with C/C++11, uncovered by groups in Princeton and MPI-SWS/SNU, that contradicts the soundness of compilation schemes from C/C++11 to ARM and POWER (pre-REMS, we had published hand proofs of those that now turn out to be flawed); this will require additional changes to C/C++11.
In Year 4:
ELF 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. We have 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 [KMS16].
This ELF model is used in our Task 2 architectural 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.
[Kell, Mulligan, Zappa Nardelli, Sewell]
In Year 4:
- Paper [KMS16] was published.
C runtime type checking: libcrunch In a more systems-oriented vein, we are developing a system for run-time type checking in C, libcrunch, extending it to additionally check array/pointer bounds [Kel16]. Using run-time type information, we have found it possible to tolerate real C idioms not supportable by fat-pointer schemes. Early indications suggest that the available run-time performance is comparable or better than competing approaches. This work also suggests potential tie-in with the CHERI project, currently being investigated.
We have continued to refine the run-time type infrastructure underlying
libcrunch into a more general-purpose infrastructure with a variety of
other applications [Kel15] including debugging, interfacing native code
with dynamic languages, and dealing with memory-mapped files. Its
run-time metadata is also used by the system call work below.
In Year 4:
- Paper [Kel16] was published.
System call modelling We have begun developing a partial semantics for system calls on x86-64 Linux. We created a domain-specific language for binary-level interfaces including a notion of memory footprint. We developed experimental apparatus for validating these footprints against real executions, using stock tools with detailed scripts to observing data flow across the user/kernel boundary. A preliminary integration with our Task 2 architectural emulation tool was also achieved. [Kell, French (intern)]
Compiler Verification: CakeML and cost-lifting decompilation We continue to contribute to the CakeML development of a verified ML implementation, especially w.r.t. the backend ISA models and proof, as discussed in Task 2; we also envisage integrating the above ELF semantics into CakeML. [Fox, Mulligan]
Cost-lifting decompilation aims to take resource requirements known at
the machine code level, such as the timing information attached to our
L3 model of ARMv6M, and express them in terms of the original
high-level source code. Our starting point for this work is the
decompilation and refinement work by Thomas Sewell, Magnus Myreen and
which establishes a functional refinement between source and object
code using translation validation.
In Year 4:
- For cost-lifting decompilation, we selected a few examples from the Mälardalen WCET test suite, adapted them for ARM Cortex-M0 and fixed several M0-specific problems with decompilation. We now have a good basis for experimenting with cost lifting. [Campbell, Stark]
SOAAP Application compartmentalization, a vulnerability mitigation technique employed in programs such as OpenSSH and the Chromium web browser, decomposes software into isolated components to limit privileges leaked or otherwise available to attackers. We presented a new conceptual framework embodied in an LLVM-based tool: the Security-Oriented Analysis of Application Programs (SOAAP) that allows programmers to reason about compartmentalization using source-code annotations (compartmentalization hypotheses) [GWA+15]. [Gudka, Watson, et al.]
POSIX Filesystem Specification and Reasoning We have pursued two directions here: operational modelling, validated by extensive testing against production filesystem implementations, and program-logic work oriented towards reasoning about filesystems.
SibylFS is a semantics and filesystem test oracle for POSIX filesystems [RST+15]. SibylFS has been used to validate and identify bugs in existing production filesystems and in two verified filesystems (FSCQ and Flashix) from academia. [Ridge et al. (Leicester), Sheets, Madhavapeddy, Sewell]
We have developed a separation logic style program logic for path-addressable structured data. We have applied this logic to develop a sequential specification of a core subset of POSIX file systems. This work demonstrated the modularity and scalability of reasoning about file-system client programs using simplified paths that allow updates to appear local [GNW14]. [Ntzik, Wright, Gardner]
We have developed fusion logic, a file-system specific program logic based on separation logic, for reasoning about non-local properties of arbitrary paths using symbolic links or dot-dots. We have extended the previous sequential specification of core POSIX file systems to arbitrary paths. The extended specification and fusion logic were then used to reason about implementations of the rm utility, discovering bugs in popular implementations due to mishandling of symbolic links and dot-dots in paths [NG15]. [Ntzik, Gardner]
We have extended concurrent program logics with reasoning about how programs are affected by, and recover from, host failures (crashes), as in file systems and databases [NdG15]. This extends the Views framework, which acts as a basis for many concurrent program logics, with host failure and recovery semantics; we instantiated this with a Fault-tolerant Concurrent Separation Logic and used it to verify properties of an ARIES recovery algorithm used in databases. [Ntzik, da Rocha Pinto, Gardner]
In another collaboration between our systems and semantics groups, we
have developed a clean-slate specification and implementation of the
Transport Layer Security (TLS) protocol – this is fundamental to
internet use, but its implementations have a history of
security flaws [MM14, KMMS15].
We are engaged in the TLS 1.3 design process [KMM16],
providing extensive testing facilities for other implementations;
and we presented an outreach talk at 31C3 [MM15].
[Kaloper Meršinjak, Mehnert, Madhavapeddy, Sewell]
In Year 4:
- We developed libnqsb-tls1 [DYM16], a drop-in replacement for the C libtls library that wraps our pure OCaml TLS implementation ocaml-tls. The code is available11. We have also demonstrated unmodified OpenBSD system software running against our replacement library.
- We also developed a generic approach to defining partially-static data and corresponding operations [KMY16].
- We designed and implemented conex [MG16], a tool which allows developers to cryptographically sign their released software, and users to verify them, ensuring integrity and authenticity without a centralised trust authority. The OCaml community approached us to work on this, based on our nqsb-TLS work [KMMS15], and is currently deploying conex. The design is based on Justin Cappos’s (NYU) work on “the update framework”, who will review conex (in May 2017, in Cambridge).
TCP/IP We have resurrected the NetSem network semantics from 10 years ago. 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 DTrace12; 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. [Mehnert, Norrish (NICTA), CADETS, Sewell]
We focus on challenging problems of concurrent systems that include correctness properties, such as atomicity and termination, abstract specifications for concurrent modules and modular reasoning, and memory models. We have approached these problems from varying yet complementary directions, by developing new program logics models and type systems, algebraic reasoning, linearisability correctness conditions and proof techniques, reduction theories and automated verification tools.
Program logics, models, type systems We have proposed a logic, iCAP-TSO, for reasoning about programs running on a TSO memory model. The logic supports direct reasoning about the buffering observable on TSO machines. It also supports a fiction of sequential consistency that hides this buffering behaviour from clients for libraries that contain sufficient synchronisation. This allows us to recover standard separation logic reasoning for well-synchronised clients and still support linking with code that requires explicit reasoning about buffering. [SSBPP15] [Svendsen, Pichon-Pharabod, and colleagues]
We have proposed a refinement of the mathematical technique of step-indexing [SSB16]. Step-indexing is used to break circularities that arises when constructing models of advanced program logics and type systems. Our refinement provides a more flexible way of breaking these circularities that increases compositionality when reasoning about program equivalence. We are currently investigating whether the same is true for program logics. [Svendsen, Sieczkowski (Aarhus), Birkedal (Aarhus)]
We have defined a relational semantics for an expressive type-and-effect system to validate effect-based program transformations. The type-and-effect system combines effect tracking with a lightweight mechanism for tracking state ownership. This combination is intended to simplify concurrent programming by allowing a compiler to automatically parallelise sub-computations based on inferred effect types. We use the semantics to prove that such automatic parallelisation is sound. [KJSB17] [Svendsen and colleagues]
We have studied abstract local reasoning for concurrent libraries [GRWW14]. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. We generalise our SSL reasoning and results to arbitrary concurrent data libraries. [Gardner, Raad, Wheelhouse, Wright]
We show how to verify four challenging concurrent fine-grained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation [RHVG16]. We demonstrate how to use a logic without abstraction (CoLoSL) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic. [Raad, Hobor, Villard, Gardner]
We have developed TaDA, a separation logic for fine-grained concurrency which introduces atomic triples for specifying the observable atomicity exhibited by operations of concurr ent modules. The atomic triples can be used to specify the atomicity of operations at the granularity of a particular data-abstraction, such as an abstract queue, and under restricted interf erence from the concurrent environment [dRPDYG14]. This approach leads to strong specifications of concurrent modules, such as locks, double-compare-and-swap, and concurrent queues, that do not depend on particular usage patterns. [da Rocha Pinto, Dinsdale-Young, Gardner]
We have demonstrated the scalability of TaDA reasoning by studying concurrent maps. In particular, we defined two abstract specifications for a concurrent map module, one focusing on the entire abstract map and the other on individual key-value pairs, which we proved to be equivalent by applying TaDA. We have applied the TaDA program logic to produce the first partial correctness proof of core operations of ConcurrentSkipListMap in java.util.concurrent [XdRPNG17]. [Xiong, da Rocha Pinto, Ntzik, Gardner]
We have extended TaDA with well-founded termination reasoning. This led to the development of Total-TaDA, the first program logic for reasoning about total correctness of fine-grained concurrent programs [dDYGS16]. [da Rocha Pinto, Dinsdale-Young, Gardner, Sutherland]
We have surveyed a range of verification techniques to specify concurrent programs, from Owicki-Gries to modern logics. We show how auxiliary state, interference abstraction, resource ownership, and atomicity are combined to provide powerful approaches to specify concurrent modules in CAP and TaDA [dDYG15]. [da Rocha Pinto, Dinsdale-Young, Gardner]
A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency typically require reasoning about either the entire shared state or disjoint parts of the shared state, impeding compositionality. We have introduced the program logic CoLoSL, where each thread is verified with respect to its subjective view of the global shared state [RVG15]. This subjective view describes only that part of the state accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread. This flexibility gives rise to small specifications and, hence, more compositional reasoning for concurrent programs. We demonstrate our reasoning on a range of examples, including a concurrent computation of a spanning tree of a graph. [Raad, Villard, Gardner]
Algebraic reasoning We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from modal semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis [GGH+16]. [Gomes and colleagues]
We describe the application of Modal Kleene algebra in program correctness. Starting from a weakest precondition based component, we show how variants for Hoare logic, strongest postconditions and program refinement can be built in a principled way. Modularity of the approach is demonstrated by variants that capture program termination and recursion, memory models for programs with pointers, and trace semantics relevant to concurrency verification [GS16a, GS16b]. [Gomes and colleagues]
We have summarised the progress in the research towards the construction of links between algebraic presentations of the principles of programming and the exploitation of concurrency in modern programming practice [HvSM+14]. The research concentrates on the construction of a realistic family of partial order models for Concurrent Kleene Algebra (aka, the Laws of Programming). The main elements of the model are objects and the events in which they engage. Further primitive concepts are traces, errors and failures, and transferrable ownership. In terms of these we can define other concepts which have proved useful in reasoning about concurrent programs, for example causal dependency and independence, sequentiality and concurrency, allocation and disposal, synchrony and asynchrony, sharing and locality, input and output. [Villard and colleagues]
Linearizability and reduction theory
We generalized Lipton’s reduction theory for TSO programs. We developed a methodology with which one can check whether a given program allows non-SC behaviours and transform any given program P to another program P’ such that P under TSO is observationally equivalent to P’ under SC [ST15]. [Sezgin, Tasiran (Koç)]
Linearisability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearisability of concurrent queue algorithms that does not involve identifying linearization points [CHSV15]. We reduce the task of proving linearisability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. [Sezgin and colleagues]
We developed local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations [HHH+16] [Sezgin and colleagues].
We have developed Caper, a tool for automating poofs in concurrent separation logic with shared regions, aimed at proving functional correctness for fine-grained concurrent algo rithms. The tool supports a logic in the spirit of concurrent abstract predicates taking inspiration from recent developments such as TaDA [dRPDYG14]. Caper provides a foundation for exploring the possibilities for automation with such a logic [DdRPAB17]. [Dinsdale-Young, da Rocha Pinto, Just Andersen, Birkedal][Task 1 papers] [Task 1 bib] [Task 2 papers] [Task 2 bib] [Task 3 papers] [Task 3 bib] [Task 4 papers] [Task 4 bib]