Modern data-structures are so complex that it is hard to be sure they are correct without mathematical proof. Program logics are a way of writing these proofs. Most of my work in this area builds on separation logic.
I have developed several logics for data-structure verification. The most important is Concurrent Abstract Predicates (CAP), a logic targeting the most complex class of non-blocking data-structure. Such data-structures rely on a complex interplay between reads and writes -- CAP's innovation was to combine these protocols with a powerful abstraction mechanism.
Concurrent data-structures often implicitly enforce a total order over elements in their underlying memory layout. However, much of this order is expensive and unnecessary. By using verification theory we can design data-structures which eliminate redundant orders, enabling world-class scalability. We call this approach frugal synchronisation.
Our model of a frugal data-structure is our timestamped (TS) stack. The TS stack uses timestamping to avoid unnecessary ordering. Pairs of elements can be left unordered if their associated insert operations ran concurrently, and order imposed as necessary at the eventual removal. In our experiments, the TS stack outperforms its best competitor by a factor of two.
Data-structures are correct if they are guaranteed to satisfy expected properties - for example, FIFO ordering for a queue. Correctness conditions are a rigorous way of expressing these correctness properties. The de-facto standard correctness condition is linearizability.
However, linearizability often seems too restrictive for real-world applications. I've worked on fixing this in two ways: by defining more permissive conditions suitable for realistic applications, and by relaxing the constraints imposed by linearizability.
Proofs play two roles in software verification: firstly establish that the program is correct, and secondly explaining why it is correct. Increasingly complex program logics often emphasise the first and neglect the second. However, if they are to be used by engineers, verification techniques must be understandable to programmers.
Ribbon proofs are a graphical notation intended to explain programs as well as verify them. A single ribbon represents one portion of a data-structure: a single cell, or a sub-section of a list or tree. The flow of a ribbon follows the data-structure through its life in the program, allowing programmers to see how they evolve.
Dr. John Wickerson
(joint-supervised with Matthew Parkinson, graduated 2013).
Worked on concurrent logics and proof visualisation.
Currently a post-doctoral researcher at Imperial College.
Thesis: Concurrent verification for sequential programs.
If you're interested in being a research student with me, look at my page for prospective students.