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:

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:

  Task 2: Architectural Multiprocessor Semantics

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:

ARM Concurrency   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 (Pulte). [Flur, Pulte, Gray, Sarkar (St Andrews), Sezgin, Maranget (INRIA Paris), Deacon (ARM), Grisenthwaite (ARM), Sewell]

In Year 4:

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 (IBM), Sewell]

In Year 4:

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:

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:

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:

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 (SRI), Roe]

In Year 4:

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]

  Task 3: Systems Programming Languages

Here our main focus is on abstractions used for real-world systems programming, looking at the C language (both sequential and concurrent aspects), linking (specifically at the ELF format), runtime typechecking for systems code (in the libcrunch system), and JavaScript. We are also contributing to the CakeML verified compiler.

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 used; 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 Paper Award. We are participating in the ISO WG14 C standards committee: we attended the April 2016 (London) and October 2016 (Pittsburgh) committee meetings, producing committee discussion papers ([MS16b, CMM+16, MS16e, MS16f] and [MS16d, MS16a, MS16c]), and discussing several issues at length with them. [Memarian, Borges, Matthiesen, Lingard, Nienhuis, Chisnall, Watson, Sewell]

In Year 4:

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:

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. [Kell]

In Year 4:

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 Gerwin Klein, which establishes a functional refinement between source and object code using translation validation.

In Year 4:

JavaScript   We have created an axiomatic specification of a key fragment of the Document Object Model (DOM) API using structural separation logic. This specification allows us to develop modular reasoning about client programs that call the DOM [RFG16]. We plan to develop a DOM plugin based on these specifications for the JavaScript verification tool currently in development at Imperial. [Raad, Fragoso Santos, Gardner]

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.]

  Task 4a: System APIs and Protocols

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]

TLS Security   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:

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]

  Task 4b: Concurrency Reasoning

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].

Automated verification  

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]