Research

During my PhD, I worked on CPC, an experimental dialect of the C language, designed to write concurrent programs. A CPC program is compiled into plain C through a series of source-to-source transformations.

During my Post-Doc, I worked on a formal model of a user-mode fragment of the POWER instruction set, for the REMS project in Cambridge.

You can find find my publications below, or on my ResearchGate profile.

Continuation-Passing C (CPC)

CPC was a programming language for writing concurrent systems, designed and developped by Juliusz Chroboczek and Gabriel Kerneis.

The CPC programmer manipulates very lightweight threads, choosing whether they should be cooperatively or preemptively scheduled at any given point; the CPC program is then processed by the CPC translator, which produces highly efficient event-loop code. This approach gives the best of both worlds: the relative convenience of programming with threads, and the low memory usage of event-loop code.

The semantics of CPC is defined as a source-to-source translation from CPC into plain C using a technique known as conversion into Continuation Passing Style.

CPC has been used to write Hekate, a BitTorrent seeder designed to handle millions of simultaneous torrents and tens of thousands of simultaneously connected peers, and to compile coroutines in the QEMU emulator during Google Summer of Code 2013.

Code

CPC, Hekate and QEMU/CPC are not maintained anymore, but their archived source code is still available:

• CPC source code
• Hekate source code
• QEMU/CPC source code

Publications

Workshop paper on Hekate:

Gabriel Kerneis, Juliusz Chroboczek. CPC: programming with a massive number of lightweight threads. PLACES'11 (2011). Slides.

Workshop paper on QEMU/CPC:

Gabriel Kerneis, Charlie Shepherd, Stefan Hajnoczi. QEMU/CPC: Static Analysis and CPS Conversion for Safe, Portable, and Efficient Coroutines. PEPM'14, San Diego, CA, USA, January 20-21, 2014.

Journal article on CPC compilation:

Gabriel Kerneis, Juliusz Chroboczek. Continuation-Passing C, compiling threads to events through continuations. Higher-Order and Symbolic Computation 24(3): 239-279 (2011). Companion paper.

PhD thesis:

Gabriel Kerneis. Continuation-Passing C: Program Transformation for Compiling Concurrency in an Imperative Language. PhD thesis. Laboratoire PPS, Université Paris Diderot (2012).

Experiment on an alternative version of CPC where local variables are saved in environments rather than lambda-lifted:

Matthieu Boutier, Gabriel Kerneis. Generating events with style. Unpublished draft (2012).

Report on some early benchmarks:

Gabriel Kerneis, Juliusz Chroboczek. Are events fast?. Technical report, Université Paris Diderot (2009).

POWER ISA modelling

Code

• The Sail ISA specification language.
• I worked more specifically on the Sail IBM POWER ISA model, automatically generated from IBM XML documentation.

Publication

Kathryn E. Gray, Gabriel Kerneis, Dominic Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. MICRO-48, Waikiki, Hawaii, USA, December 5-9, 2015.