Research Projects

  • image

    Weak Consistency Models

    Developing and formalising semantic models in weakly consistent settings.

    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.

  • image

    Persistent (Non-Volatile) Memory

    Developing and formalising the persistence semantics of emerging non-volatile technology.

    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. I currently work on formalising the semantics of persistency model in the context of mainstream architectures and programming languages in a weakly consistent setting. This, however, is a challenging task, as it requires capturing the subtle interactions between (weak) memory consistency and persistency models.

    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. Together with John Wickerson, Viktor Vafeadis and I recently formalised the persistency semantics of the ARMv8 architecture, and developed and formalising a language-level transactional persistency model (to appear in OOPSLA 2019). We are currently working on formalising the persistency semantics of the Intel architecture.

  • image

    Concurrent Program Logics

    Developing program logics for compositional specification and verification of concurrent programs.

    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.

    I am 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.

    Previously, I developed the program logic CoLoSL, as a compositional verification technique where each thread is verified with respect to its subjective view of the state. The subjective views of different threads 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. I demonstrated the application of CoLoSL by verifying several non-trivial graph algorithms.

Collaborators

I have been fortunate enough to work with a number of excellent people. My past and current collaborators include:
Andrea Cerone, Simon Colton, Michael Cook, Marko Doko, Sophia Drossopoulou, José Fragoso Santos, Philippa Gardner, Aquinas Hobor, Michalis Kokologiannakis, Ori Lahav, Matthew Parkinson, Lovro Rožić, Viktor Vafeadis, Jules Villard, Mark Wheelhouse, John Wickerson, Adam Wright and Shale Xiong.