Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (e.g. locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot of work on verifying such libraries in a sequentially consistent (SC) environment, little is known about how to specify and verify them under weak memory consistency (WMC). We propose a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is sufficient to encode standard models such as SC, (R)C11 and TSO. Additionally, we specify several concurrent libraries, including mutual exclusion locks, reader-writer locks, exchangers, queues, stacks and sets. We then use our framework to verify multiple weakly consistent implementations of locks, exchangers, queues and stacks.
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the formal semantics of such persistency models in the context of existing mainstream hardware has been unexplored to date. To close this gap, we integrate the buffered epoch persistency model with the ‘total-store-order’ (TSO) memory model of the x86 and SPARC architectures. We thus develop the PTSO (‘persistent’ TSO) model and formalise its semantics both operationally and declaratively. We demonstrate that the two characterisations of PTSO are equivalent. We then formulate the notion of persistent linearisability to establish the correctness of library implementations in the context of persistent memory. To showcase our formalism, we develop two persistent implementations of a queue library, and apply persistent linearisability to show their correctness.
Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). It is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing timestamps. In this paper, we develop two simpler equivalent operational definitions of SI as lock-based reference implementations that do not use timestamps. Our first locking implementation is prescient in that requires a priori knowledge of the data accessed by a transaction and carries out transactional writes eagerly (in-place). Our second implementation is non-prescient and performs transactional writes lazily by recording them in a local log and propagating them to memory at commit time. Whilst our first implementation is simpler and may be better suited for developing a program logic for SI transactions, our second implementation is more practical due to its non-prescience. We show that both implementations are sound and complete against the declarative SI specification and thus yield equivalent operational definitions for SI. We further consider, for the first time formally, the use of SI in a context with racy non-transactional accesses, as can arise in STM implementations of SI. We introduce robust snapshot isolation (RSI), an adaptation of SI with similar semantics and guarantees in this mixed setting. We present a declarative specification of RSI as an acyclicity axiom and analogously develop two operational models as lock-based reference implementations (one eager, one lazy). We show that these operational models are both sound and complete against the declarative RSI model.
Parallel snapshot isolation (PSI) is a standard transactional consistency model that is used in databases and distributed systems. We argue that PSI is also useful as a formal model for software transactional memory (STM) as it has certain advantages over other consistency models. However, the formal PSI definition is given declaratively by acyclicity axioms, which most programmers find hard to understand and reason about. To solve this problem, we develop a simple lock-based reference implementation for PSI built on top of the release-acquire memory model, which is a well-behaved subset of the C/C++11 memory model. We prove that our reference implementation is sound and complete with respect to its higher-level declarative specification. We further consider an extension of PSI allowing transactional and non-transactional code to interact, and provide a sound and complete reference implementation for the more general setting. Supporting this interaction is necessary for adopting a transactional model in programming languages.
This thesis explores the challenges in abstract library specification, library refinement and reasoning about fine-grained concurrent programs.
For abstract library specification, this thesis applies structural separation logic (SSL) to formally specify the behaviour of several libraries in an abstract, local and compositional manner. This thesis further generalises the theory of SSL to allow for library specifications that are language-independent. Most notably, we specify a fragment of the Document Object Model (DOM) library. This result is compelling as it significantly improves upon existing DOM formalisms in that the specifications produced are local, compositional and language-independent.
As to concurrent reasoning, this thesis introduces concurrent local subjective logic (CoLoSL) for compositional reasoning about fine-grained concurrent programs. CoLoSL introduces subjective views, where each thread is verified with respect to a customised local view of the state, as well as the general composition and framing of interference relations, allowing for better proof reuse.
We show how to verify four challenging concurrent finegrained 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. 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 present an axiomatic specification of a key fragment of DOM using structural separation logic. This specification allows us to develop modular reasoning about client programs that call the DOM.
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. This paper introduces the program logic CoLoSL, where each thread is verified with respect to its subjective view of the global shared state. 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.
We study abstract local reasoning for concurrent libraries. 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. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.
Chalice is a verification tool for object-based concurrent programs. It supports verification of functional properties of the programs as well as providing a deadlock prevention mechanism. It is built on Implicit Dynamic Frames, fractional permissions and permission transfer. Implicit Dynamic Frames have been formulated and proven sound using verification conditions and axiomatisation of the heap and stack. Verification in Chalice is specified in terms of weakest preconditions and havocing the heap. In this paper we give a formalisation of the part of Chalice concerned with functional properties. We describe its operational semantics, Hoare logic and sketch the soundness proof. Our system is parametric with respect to the underlying assertion language.
As computer programs shift towards highly distributed and parallel environments, the importance of reliable and safe communication rises and hence the challenges of safe concurrent computing march to the forefront of modern computing research. One of the most prominent of these is the provision of a verification method for inter-process communication which has proven extremely challenging and has led to one of the most common bugs in concurrent computing - synchronisation bugs. Session types have been proposed as a means of solving this problem via efficient type-checking. Several variants of session types have been studied for various use-cases; these have all attempted to exploit the benefits of type checking by binding the interacting participants to strictly-typed protocols, forcing them to conform to the said protocol and hence guaranteeing the communication safety. However, these approaches have various constraints and limitations, and a more suitable solution is sought. This project specifies Roles, a language based on a form of session types suited to dynamic multiparty communication with a number of interesting and useful features. We define the syntax and the operational semantics of Roles, present its type system and conjecture about its properties before evaluating it with respect to contemporary approaches.