Thomas Dinsdale-Young

We look at approaches to specifying concurrent program modules based on disjointness (the abstraction that concurrent operations act on disjoint resources) and atomicity (the abstraction that concurrent operations occur at disjoint times). We illustrate the limitations of these approaches, and propose a novel approach, using atomic triples, that overcomes them.

To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.

Building on separation logic with concurrent abstract predicates (CAP), we introduce TaDA, a program logic which combines the benefits of abstract atomicity and abstract disjointness. We give several examples: an atomic lock module, a CAP example with a twist, which cannot be done using linearisability; an atomic MCAS module implemented using our lock module, a classic linearisability example which cannot be done using CAP; and a double-ended queue module implemented using MCAS.

Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating conjunction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables.

In this paper, we present the "Concurrent Views Framework", a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Concurrent Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics.

This thesis tackles problems concerning abstract data structures — expressibility and decidability results for logics for reasoning about abstract data structures, and techniques for proving the correctness of programs that implement abstract data structures. The main expressivity issue addressed is the question of whether certain spatial adjunct connectives contribute to the expressive power of context logic for trees. The question is answered in the affirmative for context logic in its basic form, but in the negative for a multi-holed variant of context logic. This result is interesting, since the adjunct connectives play an important role in expressing the weakest preconditions of programs. The decidability results show that multi-holed context logic is decidable for trees, sequences and terms, by encoding logical formulae with automata.

Concerning the correctness of programs that implement abstract data structures, this thesis presents two techniques for justifying abstract local reasoning about such implementations in the sequential setting. In the concurrent setting, this thesis presents an approach to verifying implementations of abstract specifications that incorporate a fiction of disjointness using a fine-grained permissions model.

Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is insufficient for reasoning about indexes that are accessed concurrently.

We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, however, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and B^Link trees. The complexity of these algorithms, in particular the B^Link tree algorithm, can be completely hidden from the client's view by our abstract specification.

Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state. We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations. We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level "fiction" of locality.

Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a program logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module's implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.

We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.

We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.

© Springer-Verlag GmbH Berlin Heidelberg

In recent years, interest has been growing in the field of spatial logics, which have a variety of useful applications, including modular reasoning about data update and specifying safety properties. Context Logic is a new spatial logic designed for reasoning about data on the level of data-structures. It extends first-order logic with connectives that permit reasoning about disjoint portions of data. A feature of this and related logics is the presence of adjunct connectives, which are important for defining weakest preconditions in Hoare reasoning and for specifying perfect firewalls, for instance. Recent results, first by Lozes, then Dawar, Gardner and Ghelli, have shown that adjuncts can be eliminated from related logics.

In this report, we consider adjunct elimination in Context Logic, particularly based on the model of ordered trees. We provide a counterexample to the elimination of one of the adjuncts and a proof of elimination of the other. We also discuss possible avenues for future investigation, such as modifications to the Logic that may permit the elimination of the adjunct that was not possible within the current definition for Context Logic for Trees.