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.