Auteur : Gabriel Kerneis (Computer Laboratory, University of Cambridge)

Titre : QEMU/CPC: Static Analysis and CPS Conversion for Safe, Portable, and Efficient Coroutines

Abstract :

Coroutines and events are two common abstractions for writing
concurrent programs. Because coroutines are often more convenient,
but events more portable and efficient, it is natural to want to
translate the former into the latter. CPC is such a source-to-source
translator for C programs, based on a partial conversion into
continuation-passing style (CPS conversion) of functions annotated
as cooperative.

In this article, we study the application of the CPC translator to
QEMU, an open-source machine emulator which also uses annotated
coroutine functions for concurrency. We first propose a new type of
annotations to identify functions which never cooperate, and we
introduce CoroCheck, a tool for the static analysis and inference of
cooperation annotations. Then, we improve the CPC translator,
defining CPS conversion as a calling convention for the C language,
with support for indirect calls to CPS-converted function through
function pointers. Finally, we apply CoroCheck and CPC to QEMU (750
000 lines of C code), fixing hundreds of missing annotations and
comparing performance of the translated code with existing
implementations of coroutines in QEMU.

Our work shows the importance of static annotation checking to
prevent actual concurrency bugs, and demonstrates that CPS
conversion is a flexible, portable, and efficient compilation
technique, even for very large programs written in an imperative
language.