5  Task 4b: Concurrency Reasoning

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

5.1  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. [105]

We have proposed a refinement of the mathematical technique of step-indexing [102]. 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.

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

We have studied abstract local reasoning for concurrent libraries [108]. 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.

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

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

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

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

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

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

5.2  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 [111].

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 [112, 113].

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

5.3  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 [104].

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

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 [100]

5.4  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 [109]. Caper provides a foundation for exploring the possibilities for automation with such a logic [95].

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

5.5  Recent concurrency reasoning

More recently, we have published several papers on reasoning about different aspects of concurrency:

Other

We have also published a few papers that do not fit exactly into the above task structure:

Verified trustworthy systems

We have published an opinion piece [87] with the goal of raising awareness about the pressing issues surrounding reliability of complex modern software systems and the importance of specification and verification in the industrial design process. This publication is part of a broader journal publication on Verified Trustworthy Software Systems, aimed at the general public.

Confidentiality verification

We have published a journal paper on earlier (largely non-REMS) work on formal verification of confidentiality in a social media system [114].

Programming and proving with classical types

We have published the following on programming and proving with classical types, building on an MPhil dissertation of the first author, supervised by REMS staff [115].