Publications
Filter by type:
Non-Termination Proving at Scale
![[Artifacts available]](https://www.soundandcomplete.org/img/aec-available.jpeg)
![[Artifacts evaluated & reusable]](https://www.soundandcomplete.org/img/aec-reusable.jpeg)
Abstract
Program termination is a classic non-safety property whose falsification cannot in general be witnessed by a finite trace. This makes testing for non-termination challenging, and also a natural target for symbolic proof. A number of works in the literature apply non-termination proving to small, self-contained benchmarks, but it has not been developed for large, real-world projects; as a consequence, despite its allure, non-termination proving has had limited practical impact. We develop a compositional theory for non-termination proving, paving the way for its scalable application to large codebases. Discovering non-termination is an under-approximate problem, and we present UNTer, a sound and completeunder-approximate logic for proving non-termination. We then extend UNTer with separation logic and develop UNTerSL for heap-manipulating programs, yielding a compositional proof method amenable to automation via under-approximation and bi-abduction. We extend the Pulse analyser from Meta and develop Pulse∞, an automated, compositional prover for non-termination based on UNTerSL. We have run Pulse∞ on large codebases and libraries, each comprising hundreds of thousands of lines of code (LOC), including OpenSSL, libxml2, CryptoPP and libxpm; we discovered several previously-unknown non-termination bugs and have reported them to developers of these libraries.
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
Abstract
Remote direct memory access (RDMA) is a modern technology enabling networked machines to exchange information without involving the operating system of either side, and thus significantly speeding up data transfer in computer clusters. While RDMA is extensively used in practice and studied in various research papers, a formal underlying model specifying the allowed behaviours of concurrent RDMA programs running in modern multi-core architectures is still missing. This paper aims to close this gap and provide semantic foundations of RDMA on x86-TSO machines. We propose three equivalent formal models, two operational models in different levels of abstraction and one declarative model, and prove that the three characterisations are equivalent. To gain confidence in the proposed semantics, the more concrete operational model has been reviewed by NVIDIA experts, a major vendor of RDMA systems, and we have empirically validated the declarative formalisation on various subtle litmus tests by extensive testing. We believe that this work is a necessary initial step for formally addressing RDMA-based systems by proposing language-level models, verifying their mapping to hardware, and developing reasoning techniques for concurrent RDMA programs.
Extending the C/C++ Memory Model with Inline Assembly
Abstract
Programs written in C/C++ often include inline assembly: a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive to simulate in the source language. Although inline assembly is widely used, its semantics has not yet been formally studied. In this paper, we overcome this deficiency by investigating the effect of inline assembly to the consistency semantics of C/C++ programs. We propose the first memory model of the C++ Programming Language with support for inline assembly for Intel's x86 including non-temporal stores and store fences. We argue that previous provably correct compiler optimizations and correct compiler mappings should remain correct under such an extended model and we prove that this requirement is met by our proposed model.
Challenges in Empirically Testing Memory Persistency Models
Abstract
Memory persistency models provide the foundational rules for software engineers to develop applications that take advantage of non-volatile memory (NVM), dictating which (and when) writes to NVM are deemed persistent. Though formalised for Intel-x86 and Arm architectures, these models remain empirically unvalidated on actual machines. Conventional validation methods for memory consistency models fall short as test programs cannot differentiate between volatile cache reads and those from NVM. To address this, we employed a commercial device designed to intercept and log data on a system's memory bus in their order of arrival. We used this device to conduct a campaign using litmus tests---small programs designed to assess specific memory persistency behaviours---aimed at empirically validating Intel-x86 and Arm machine persistency guarantees.
We noted out-of-order memory writes and ensured they were not merely artifacts of our test setup. Analysis revealed Intel-x86's architecture cannot be validated via memory bus interception due to legitimate early subsystem reordering. Intel engineers confirmed the absence of dependable validation methods for the persistency claims of their architectures. Meanwhile, an expert-recommended Arm machine did not align with the formal persistency model due to a specification loophole, and further investigation suggests that no market-available Arm machine fully supports NVM.
Our finding for Intel highlights a major concern for software developers wishing to take advantage of NVM: currently there is, to our knowledge, no viable way to confirm the persistency guarantees claimed by Intel. Our results for Arm suggest that our interception-based approach is viable for reliably detecting reorderings in the memory subsystem, which will be valuable for empirical validation once NVM-supporting machines become available.
Intel PMDK Transactions: Specification, Validation and Concurrency
Abstract
Software Transactional Memory (STM) is an extensively studied paradigm that provides an easy-to-use mechanism for thread safety and concurrency control. With the recent advent of byte-addressable persistent memory, a natural question to ask is whether STM systems can be adapted to support failure atomicity. In this paper, we answer this question by showing how STM can be easily integrated with Intel’s Persistent Memory Development Kit (PMDK) transactional library (which we refer to as TXPMDK) to obtain STM systems that are both concurrent and persistent. We demonstrate this approach using known STM systems, TML and NOREC, which when combined with TXPMDK result in persistent STM systems, referred to as PMDK-TML and PMDK-NOREC, respectively. However, it turns out that existing correctness criteria are insufficient for specifying the behaviour of TXPMDK and our concurrent extensions. We therefore develop a new correctness criterion, dynamic durable opacity, that extends the previously defined notion of durable opacity with dynamic memory allocation. We provide a model of TXPMDK, then show that this model satisfies dynamic durable opacity. Moreover, dynamic durable opacity supports concurrent transactions, thus we also use it to show correctness of both PMDK-TML and PMDK-NOREC.
Specifying and Verifying Persistent Libraries
Abstract
We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correctness of individual libraries (horizontal and vertical compositionality) and is general enough to encompass all existing persistent library specifications ranging from hardware architectural specifications to correctness conditions such as durable linearizability. As case studies, we specify the FliT and Mirror libraries, verify their implementations over Px86, and use them to build higher-level durably linearizable libraries, all within our framework. We also specify and verify a persistent transaction library that highlights some of the technical challenges which are specific to persistent memory compared to weak memory and how they are handled by our framework.
A General Approach to Under-approximate Reasoning about Concurrent Programs
Abstract
There is a large body of work on concurrent reasoning including Rely-Guarantee (RG) and Concurrent Separation Logics. These theories are over-approximate: a proof identifies a superset of program behaviours and thus implies the absence of certain bugs. However, failure to find a proof does not imply their presence (leading to false positives in over-approximate tools). We describe a general theory of under-approximate reasoning for concurrency. Our theory incorporates ideas from Concurrent Incorrectness Separation Logic and RG based on a subset rather than a superset of interleavings. A strong motivation of our work is detecting software exploits; we do this by developing concurrent adversarial separation logic (CASL), and use CASL to detect information disclosure attacks that uncover sensitive data (e.g. passwords) and out-of-bounds attacks that corrupt data. We also illustrate our approach with classic concurrency idioms that go beyond prior under-approximate theories which we believe can inform the design of future concurrent bug detection tools.
Memento: A Framework for Detectable Recoverability in Persistent Memory
Abstract
Persistent memory (PM) is an emerging class of storage technology that combines the performance of DRAM with the durability of SSD, offering the best of both worlds. This had led to a surge of research on persistent objects in PM. Among such persistent objects, concurrent data structures (DSs) are particularly interesting thanks to their performance and scalability. One of the most widely used correctness criteria for persistent concurrent DSs is detectable recoverability, ensuring both thread safety (for correctness in non-crashing concurrent executions) and crash consistency (for correctness in crashing executions). However, the existing approaches to designing detectably recoverable concurrent DSs are either limited to simple algorithms or suffer from high runtime overheads.
We present Memento: a general and high-performance programming framework for detectably recoverable concurrent DSs in PM. To ensure general applicability to various DSs, Memento supports primitive operations such as checkpoint and compare-and-swap and their composition with control constructs. To ensure high performance, Memento employs a timestamp-based recovery strategy that requires fewer writes and flushes to PM than the existing approaches. We formally prove that Memento ensures detectable recoverability in the presence of crashes. To showcase Memento, we implement a lock-free stack, list, queue, and hash table, and a combining queue that detectably recovers from random crashes in stress tests and performs comparably to existing hand-tuned persistent DSs with and without detectable recoverability.
The Path to Durable Linearizability
Abstract
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of durable linearizability (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent with the real-time order and, moreover, that recovering from a crash return a state corresponding to a prefix of that sequence. Sadly, however, there are hardly any formal DL proofs, and those that do exist cover the correctness of rather simple persistent algorithms on specific (simplified) persistency models. In response, we propose a general, powerful, modular, and incremental proof technique that can be used to guide the development and establish DL. Our technique is (1) general, in that it is not tied to a specific persistency and/or consistency model, (2) powerful, in that it can handle the most advanced persistent algorithms in the literature, (3) modular, in that it allows the reuse of an existing linearizability argument, and (4) incremental, in that the additional requirements for establishing DL depend on the complexity of the algorithm to be verified. We illustrate this technique on various versions of a persistent set, leading to the link-free set of Zuriel et al.
Finding Real Bugs in Big Programs with Incorrectness Logic
Abstract
Incorrectness Logic (IL) has recently been advanced as a logical theory for compositionally proving the presence
of bugs—dual to Hoare Logic, which is used to compositionally prove their absence. Though IL was motivated
in large part by the aim of providing a logical foundation for bug-catching program analyses, it has remained
an open question: is IL useful only retrospectively (to explain existing analyses), or can it actually be useful in
developing new analyses which can catch real bugs in big programs?
In this work, we develop Pulse-X, a new, automatic program analysis for catching memory errors, based
on ISL, a recent synthesis of IL and separation logic. Using Pulse-X, we have found 15 new real bugs in
OpenSSL, which we have reported to OpenSSL maintainers and have since been fixed. In order not to be
overwhelmed with potential but false error reports, we develop a compositional bug-reporting criterion based
on a distinction between latent and manifest errors, which references the under-approximate ISL abstractions
computed by Pulse-X, and we investigate the fix rate resulting from application of this criterion. Finally, to
probe the potential practicality of our bug-finding method, we conduct a comparison to Infer, a widely used
analyzer which has proven useful in industrial engineering practice.
View-Based Owicki-Gries Reasoning for Persistent x86-TSO
![[Artifacts available]](https://www.soundandcomplete.org/img/aec-available-eapls.png)
![[Artifacts evaluated & reusable]](https://www.soundandcomplete.org/img/aec-reusable-eapls.png)
Abstract
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about x86 code that uses low-level operations such as memory accesses and fences, as well as persistency primitives such as flushes. Our logic, PIEROGI, benefits from a simple underlying operational semantics based on views, is able to handle optimised flush operations, and is mechanised in the Isabelle/HOL proof assistant. We detail the proof rules of PIEROGI and prove them sound. We also show how PIEROGI can be used to reason about a range of challenging single- and multi-threaded persistent programs.
Concurrent Incorrectness Separation Logic
Abstract
Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.
Extending Intel-x86 Consistency and Persistency
Abstract
Existing semantic formalisations of the Intel-x86 architecture cover only a small fragment of its available features that are relevant for the consistency semantics of multi-threaded programs as well as the persistency semantics of programs interfacing with non-volatile memory.
We extend these formalisations to cover: (1) non-temporal writes, which provide higher performance and are used to ensure that updates are flushed to memory; (2) reads and writes to other Intel-x86 memory types, namely uncacheable, write-combined, and write-through; as well as (3) the interaction between these features. We develop our formal model in both operational and declarative styles, and prove that the two characterisations are equivalent. We have empirically validated our formalisation of the consistency semantics of these additional features and their subtle interactions by extensive testing on different Intel-x86 implementations.
Revamping Hardware Persistency Models
Abstract
Non-volatile memory (NVM) is a cutting-edge storage technology that promises the performance of DRAM with the durability of SSD. Recent work has proposed several persistency models for mainstream architectures such as Intel-x86 and ARMv8, describing the order in which writes are propagated to NVM. However, these models have several limitations; most notably, they either lack operational models or do not support persistent synchronization patterns.
We close this gap by revamping the existing persistency models. First, we propose a unified axiomatic style for describing hardware persistency, allowing us to recast and repair the existing axiomatic models of Intel-x86 and ARMv8 persistency. We prove that our axiomatic models are equivalent to the authoritative semantics reviewed by Intel and ARM engineers. Next, inspired by the recent work on promising semantics, we propose a unified operational style for describing hardware persistency using views, and develop view-based operational persistency models for Intel-x86 and ARMv8, thus presenting the first operational model for ARMv8 persistency. We prove that each axiomatic hardware persistency model is equivalent to its operational counterpart. Finally, we develop a persistent model checking algorithm and tool, and use it to verify several representative examples.
PerSeVerE: Persistency Semantics for Verification under Ext4
![[Artifacts functional]](https://www.soundandcomplete.org/img/aec-functional.jpeg)
Abstract
Although ubiquitous, modern filesystems have rather complex behaviours that are hardly understood by programmers and lead to severe software bugs such as data corruption. As a first step to ensure correctness of software performing file I/O, we formalize the semantics of the Linux ext4 filesystem, which we integrate with the weak memory consistency semantics of C/C++. We further develop an effective model checking approach for verifying programs that use the filesystem. In doing so, we discover and report bugs in commonly-used text editors such as vim, emacs and nano.
Persistent Owicki-Gries Reasoning
Abstract
The advent of non-volatile memory (NVM) technologies has fundamentally transformed how software systems are structured, making the task of correct programming significantly harder. This is because ensuring that memory stores persist in the correct order is challenging, and requires low-level programming to flush the cache at appropriate points. This has in turn resulted in a noticeable verification gap. To address this, we study the verification of NVM programs, and present Persistent Owicki-Gries (POG), the first program logic for reasoning about such programs. We prove the soundness of POG over the recent Intel-x86 model, which formalises the out-of-order persistence of memory stores and the semantics of the Intel cache line flush instructions. We then use POG to verify several programs that interact with NVM.
Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic
Abstract
There has been a large body of work on local reasoning for proving the absence of bugs, but none for proving their presence. We present a new formal framework for local reasoning about the presence of bugs, building on two complementary foundations: 1) separation logic and 2) incorrectness logic. We explore the theory of this new incorrectness separation logic (ISL), and use it to derive a begin-anywhere, intra-procedural symbolic execution analysis that has no false positives by construction. In so doing, we take a step towards transferring modular, scalable techniques from the world of program verification to bug catching.
Data Consistency in Transactional Storage Systems: A Centralised Semantics
Abstract
We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. Using our abstract states, we present operational definitions of well-known consistency models in the literature, and prove them to be equivalent to their existing declarative definitions using abstract executions. We explore two applications of our operational framework: (1) verifying that the COPS replicated database and the Clock-SI partitioned database satisfy their consistency models using trace refinement, and (2) proving invariant properties of client programs.
Persistency Semantics of the Intel-x86 Architecture
Abstract
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of 6 volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the persistency semantics of the ubiquitous x86 architecture remains unexplored to date. To close this gap, we develop the Px86 (‘persistent x86’) model, formalising the persistency semantics of Intel-x86 for the first time. We formulate Px86 both operationally and declaratively, and prove that the two characterisations are equivalent. To demonstrate the application of Px86 and to make persistent programming accessible to the uninitiated programmer, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael–Scott queue library. Finally, we encode our declarative Px86 model in Alloy and use our encoding to generate persistency litmus tests automatically. This process guided our design of Px86, allowing us to identify its corner cases and to clarify their behaviour in close discussions with research engineers at Intel.
Weak Persistency Semantics from the Ground Up
Abstract
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 persistency semantics of mainstream hardware is unexplored to date. To close this gap, we develop the PARMv8 persistency model, formalising the persistency semantics of the ARMv8 architecture for the first time. To facilitate correct persistent programming, we study transactions as a simple abstraction for concurrency and persistency control. We thus develop the PSER (persistent serialisability) persistency model, formalising transactional semantics in the NVM context for the first time, and demonstrate that PSER correctly compiles to PARMv8. This then enables programmers to write correct, concurrent and persistent programs, without having to understand the low-level architecture-specific persistency semantics of the underlying hardware.
Effective Lock Handling in Stateless Model Checking
Abstract
Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread interleavings. SMC is usually coupled with Partial Order Reduction (POR), which exploits the independence of instructions to avoid redundant explorations when an equivalent one has already been considered. While very effective POR techniques have been developed for many different memory models, they are only able to exploit independence at the instruction level, which makes them unsuitable for programs with coarse-grained synchronization mechanisms such as locks. We present LAPOR, a lock-aware POR algorithm that exploits independence at both instruction and critical section levels. This enables LAPOR to explore exponentially fewer interleavings than the state-of-the-art techniques for programs that use locks conservatively. Our algorithm is sound, complete, and optimal, and can be used for verifying programs under many different memory models. We implement LAPOR in a tool and show that it can be exponentially faster than the state-of-the-art model checkers.
Hyperstate Space Graphs for Automated Game Analysis
Abstract
Automatically analysing games is an important challenge for automated game design, general game playing, and co-creative game design tools. However, understanding the nature of an unseen game is extremely difficult due to the lack of a priori design knowledge and heuristics. In this paper we formally define hyperstate space graphs, a compressed form of state space graphs which can be constructed without any prior design knowledge about a game. We show how hyperstate space graphs produce compact representations of games which closely relate to the heuristics designed by hand for search-based AI agents; we show how hyperstate space graphs also relate to modern ideas about game design; and we point towards future applications for hyperstates across game AI research.
Model Checking for Weakly Consistent Libraries
Abstract
We present GenMC, a model checking algorithm for concurrent programs that is parametric in the choice of memory model and can be used for verifying clients of concurrent libraries. Subject to a few basic conditions about the memory model, our algorithm is sound, complete and optimal, in that it explores each consistent execution of the program according to the model exactly once, and does not explore in- consistent executions or embark on futile exploration paths. We implement GenMC as a tool for verifying C programs. Despite the generality of the algorithm, its performance is comparable to the state-of-art specialized model checkers for specific memory models, and in certain cases exponentially faster thanks to its coarse equivalence class on executions.
On Library Correctness under Weak Memory Consistency
Abstract
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.
On the Semantics of Snapshot Isolation
Abstract
Snapshot Isolation(SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). Its semantics is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing timestamps. 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.
Persistence Semantics for Weak Memory
Abstract
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.
On Parallel Snapshot Isolation and Release/Acquire Consistency
Abstract
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.
Inferring Design Constraints from Game Ruleset Analysis
Abstract
Designing game rulesets is an important part of automated game design, and often serves as a foundation for all other parts of the game, from levels to visuals. Popular ways of understanding game rulesets include using AI agents to play the game, which can be unreliable and computationally expensive, or restricting the design space to a set of known good game concepts, which can limit innovation and creativity. In this paper we detail how ANGELINA, an automated game designer, uses an abductive analysis of game rulesets to rapidly cull its design space. We show how abduction can be used to provide an understanding of possible paths through a ruleset, reduce unplayable or undesirable rulesets without testing, and can also help discover dynamic heuristics for a game that can guide subsequent tasks like level design.
Abstract
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. Concerning library refinement, this thesis explores two existing approaches to library refinement for separation logic, identifying their advantages and limitations in different settings. This thesis then introduces a hybrid approach to refinement, combining the strengths of both techniques for simple scalable library refinement. These ideas are then adapted to refinement for SSL by presenting a JavaScript implementation of the DOM fragment studied and establishing its correctness with respect to its specification using the hybrid refinement approach. 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.
Verifying Concurrent Graph Algorithms
Abstract
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. 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.
DOM: Specification and Client Reasoning
Abstract
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.
CoLoSL: Concurrent Local Subjective Logic
Abstract
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.
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
Abstract
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.
Mechanic Miner: Reflection-Driven Game Mechanic Discovery and Level Design
Abstract
We introduce Mechanic Miner, an evolutionary system for discovering simple two-state game mechanics for puzzle platform games. We demonstrate how a reflection-driven generation technique can use a simulation of gameplay to select good mechanics, and how the simulation-driven process can be inverted to produce challenging levels specific to a generated mechanic. We give examples of levels and mechanics generated by the system, summarise a small pilot study conducted with example levels and mechanics, and point to further applications of the technique, including applications to automated game design.
Abstract
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.
Ludic considerations of tablet-based Evo-art
Abstract
With the introduction of the iPad and similar devices, there is a unique opportunity to build tablet-based evolutionary art software for general consumption, and we describe here the i-ELVIRA iPad application for such purposes. To increase the ludic enjoyment users have with i-ELVIRA, we designed a GUI which gives the user a higher level of control and more efficient feedback than usual for desktop evo-art software. This relies on the efficient delivery of crossover and mutation images which bear an appropriate amount of resemblance to their parent(s). This requirement in turn led to technical difficulties which we resolved via the implementation and experimentation described here.
Smelling of Roses (ROles - Specification , Exploration, Scrutiny)
Abstract
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.