Automated Reasoning with Fine-Grained Concurrent Collections

In this project, we are planning to pursue two main goals: the Automated inference of protocol templates and the Automated reasoning with history-based specifications, with the aim to pave the road to compositional automated reasoning about FG concurrent collections.

Compositionality and automation are the two key components for achieving scalable and practical verification of realistic code bases of an arbitrarily large size. Even though the recent advances in automated reasoning methods about programs based on Separation Logic made it possible to formally verify (or reveal the presence of bugs in) real-world software projects, compositional and automated verification of realistic concurrent programs is still out of reach by the state-of-the art techniques.

The challenge of building compositional logic-based verification methodologies is particularly acute in the area of reasoning about fine-grained (FG), i.e., lock-free, concurrent algorithms. The difficulty is due to the fact that FG concurrent implementations frequently rely on low-level synchronisation primitives and, thus, involve subtle interactions between multiple parallel threads, while striving to make such interactions transparent to the algorithm’s applications, hiding them via sufficiently abstract specifications.

Until recently, verification of concurrent data structures with known “reasonable” specifications has been predominantly conducted in a paper-and-pencil way or, at best, in an interactive proof assistant. The recent results in automating reasoning techniques for FG concurrency have opened new opportunities for scaling logic-based methods to tackle the problem of finding bugs and verifying realistic concurrent software, involving both core data structures (e.g., concurrent containers) and their client applications (e.g., multi-user task management systems). However, working with automated tools, such as CAPER or STARLING, still requires a lot of special expertise in modern concurrency logics, even just for stating a specification for a concurrent library of interest, let alone being able to interpret the output of the verification engine reporting possible issues with the code.

In this project, we are aiming at advancing the techniques for automated logic-based verification of FG concurrency to the level of “push-the-button” tools, enabled by inference techniques, by (a) focusing on a particular important subset of data structures, namely, concurrent collections, and (b) employing a particular fixed form of program specifications based on partial sequentially-consistent histories.

Concurrent collections, implemented in various production-quality libraries for all mainstream languages (e.g., java.util.concurrent), are ubiquitous in applications that have to do with task allocation, data exchange, scheduling, resource management etc. The typical patterns of interacting with collections and the corresponding collection-specific bugs introduced to the code, are based on assumptions that a certain element is or is not in a collection at a certain moment of time, as well as on assuming a certain ordering of the collection operations. For reasoning about interaction scenarios of this kind, the notions of “partial observations” and “partial contributions” made to the collections by individual threads, are of crucial importance. These notions are made explicit in recently proposed thread-local concurrent specifications, capturing the effects and observations of separate threads in terms of abstract execution histories. Quite remarkably, the laws of manipulating such histories are almost the same as for managing heap-based structures in ordinary Separation Logics. Furthermore, in their intuition, such histories are very close to semi-formal specifications, assumed by the designers of modern concurrent collections, enabling straightforward principles of reasoning about their usage in client code.

Relevant publications:

  1. I. Sergey, A. Nanevski, A. Banerjee, G.A. Delbianco. Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects, OOPSLA 2016
  2. I. Sergey, A. Nanevski, A. Banerjee. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity, ESOP 2015.

Researchers: Ilya Sergey, University College London and Nikos Gorogiannis, Middlesex University London and Facebook London.