Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistence guarantees of NVM, several memory persistency models have been proposed to date. Over the last few years, I have worked on formalising the semantics of persistency models in the context of mainstream architectures and programming languages, in a weakly consistent setting. I have also worked on developing rigorous verification methods for persistency, including stateless model checking techniques and program logics.

In our OOPSLA 2018 work, we formalised the semantics of the epoch persistency model in the context of the x86-TSO architecture, and developed the PTSO (peristent TSO) model. In our OOPSLA 2019 work, we worked with engineers at ARM to formalise the persistency semantics of the ARMv8 architecture, and developed and formalised a language-level transactional persistency model. In close collaboration with engineers at Intel, we recently formalised the persistency semantics of the Intel-x86 architecture in our POPL 2020 work.

In our recent work, we developed the very first persistent program logic in a weakly consistent setting. Specifically, we developed the POG (Persistent Owicki-Gries) program logic for reasoning about the persistency behaviour of programs under the Intel-x86 architecture. This work will appear in OOPSLA 2020. Together with Kokologionnakis, Kaysin and Vafeiadis, we are currently developing a stateless model checking technique for automatically verifying the persistency behaviour of programs.

In a uni-processor machine with a non-optimising compiler, the semantics of a concurrent program is described by the memory access interleavings of its constituent threads, a model which is known as sequential consistency (SC). However, in multiprocessor machines (with or without optimising compilers), more behaviours are possible; such models are commonly described as weak memory consistency (WMC). My main research interest is developing and formalising semantics models in weakly consistent settings.

Concurrent libraries are the building blocks of concurrency. However, while there has been a lot of work on verifying such libraries in the SC setting, little is known about how to specify and verify them under WMC. In our POPL 2019 work, we developed a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is general in that it is memory-model agnostic and can encode SC, as well as well-known WMC models such as (R)C11 and TSO. Additionally, we used our framework to specify and verify well-known libraries such as locks, queues and stacks.

In a recent project with Kokologiannakis and Vafeiadis, we developed GenMC, a general model checking algorithm for concurrent programs that is parametric in the choice of memory model (be it SC or WMC) and can be used for verifying clients of concurrent libraries. Subject to a few basic conditions on 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. Despite its generality, the performance of GenMC is comparable to the state-of-art specialised model checkers for specific memory models, and in certain cases exponentially faster.

I am also interested in studying weak memory consistency in the context of software transactional memory (STM). In particular, I am interested in understanding the interactions of transactional and non-transactional code in STM, and formalising the STM guarantees in the presence of non-transactional code. In our ESOP 2018 work with Lahav and Vafeiadis, we studied the semantics of the well-known weak consistency model parallel snapshot isolation (PSI). We developed an operational PSI model that is equivalent to its existing declarative model. We then extended the PSI model to robust PSI (RPSI), in order to account for the presence of non-transactional code. We formalised the semantics of RPSI both operationally and declaratively. In our later work at VMCAI 2019, we achieved similar results for the weak snapshot isolation (SI) model: we developed an equivalent operational SI model; we extended SI to robust SI (RSI) to take into account non-transactional accesses; and we formalised the RSI semantics both operationally and declaratively.

Verifying the correctness of shared-memory concurrent programs is difficult, as the interactions of simultaneously executing threads must be taken into account. A key difficulty in verifying such programs is reasoning compositionally about each thread in isolation. To this end, a number of concurrent program logics have been developed over the years, with their genealogy accurately recorded by Ilya Sergey.

In our recent work with the Infer team at Facebook (including Prof. Peter O'Hearn), we recently developed ISL, a compositional under-approximate program logic for bug catching. This work is published at CAV2020, and is based on the recent work of O'Hearn on under-approximate reasoning. In collaboration with Facebook, we are currently extending ISL with concurrency to facilitate bug catching tools for race detection, deadlock detection and so forth.

I am also interested in developing program logics based on concurrent separation logic, particularly in a weakly consistent setting. Together with Vafeiadis, we are currently working on developing a general program logic that is parametric in the choice of memory model, with its semantic underpinning described by our POPL 2019 work.