Thomas Dinsdale-Young
Department of Computing
180 Queen's Gate
Imperial College London
London
UK
SW7 2AZ
|
Thomas Dinsdale-Young
Department of Computing |
I'm currently a PhD student at DoC, supervised by Philippa Gardner and Cristiano Calcagno. My research is on Context Logic, which is a logic for reasoning about structured tree update. In particular, I have been studying expressivity results. More recently, I have been looking at verifying concurrent modules with abstract disjoint specifications.
I'm part of the Local Resource Reasoning group at Imperial, and part of the wider Resource Reasoning community.
Given at the Concurrency Theory Workshop, 13th Jan 2009
In this talk, I look at a concurrent B-Tree algorithm, the likes of which underpin large-scale databases, with a view to reasoning about it formally. I describe how RGSep — a recent development combining rely-guarantee and separation logic reasoning — can be used to prove specifications for the algorithm. With a view to providing high-level specifications (which abstract the implementation details), I show some limitations of the RGSep approach and discuss how the latest developments may overcome this and where further work may be required.
[PDF] [Demo Application] [Notes]
PhD Thesis
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.
[PDF]
VSTTE 2010
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.
ECOOP 2010
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.
[PDF]
Journal version submitted to I&C, 2007; revised 2008
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.
APLAS 2007
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
Masters Thesis, Imperial College London, 2006
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.
[PDF]