I work on the intersection of programming languages and (concurrent, parallel, distributed, operating) systems. My recent research has been under the two following topics:
The aim of the Multicore OCaml project is to build sound and efficient support for concurrency and parallelism in the OCaml programming language. I focus on all parts of the stack from language design, verification, compiler, runtime systems, and hardware support for efficient concurrency and parallelism.
Concurrency in Multicore OCaml is expressed through effect handlers, an abstraction for programming and reasoning about computational effects in a pure setting. The runtime behaviour of effect handlers is akin to delimited continuations. By providing efficient delimited continuations as a language mechanism rather than high-level constructs like coroutines and threads, we simplify the runtime system design and allow high-level abstractions to be expressed as libraries that live outside the core compiler distribution. Effect handlers are also part of the plan to make OCaml a pure (in the sense of Haskell purity) language.
Multicore OCaml is equipped with a mostly-concurrent garbage collector that optimises for latency. Multicore OCaml is one of the few languages to have a sane memory model that can be efficiently compiled to ARM and POWER. At the heart of the memory model is a new modular version of the DRF-SC property.
While the NoSQL revolution gave us scalable web services that we have all come to accept (and depend on!), it also gave us weak consistency. No longer was it possible (and profitable) to provide strongly consistent view of a replicated database and yet achieve the scalability demands of a popular web service. Weak consistency makes the development of correct applications quite difficult, even for expert programmers. The problem is analogous to the weak memory behaviours on modern multicore architectures, but unlike the multicore architectures, we do not have an efficient DRF-SC guarantee that we can fall back to. How can we then write correct programs on such weakly consistent stores.
My research has developed a series of approaches to better programmability under weak consistency. Quelea develops a programming model for expressing replicated data types as a purely functional program, and synthesizes the weakest consistency model under which the applications can be run given the application requirements. We have also developed better programming abstractions over Irmin, a distributed database developed on the principles of Git.