Skip to main content


Correct, fast, maintainable – choose any three!


Bernard Blackham and Gernot Heiser




The common-case IPC handler in microkernels, referred to as the fastpath, is performance-critical and thus is often optimised using hand-written assembly. However, compiler technology has advanced significantly in the past decade, which suggests that we should reevaluate this approach.

We present a case-study in the optimisation of the IPC fastpath in the seL4 microkernel. This fastpath is written in C and relies on an optimising C compiler for good performance. We present our techniques in modifying the C sources to assist with compiler optimisation. We compare our results with a hand-optimised assembly implementation, which gains no extra benefit from hand-tuning.

BibTeX Entry

    publisher        = {ACM},
    doi              = {10.1145/2349896.2349909},
    author           = {Blackham, Bernard and Heiser, Gernot},
    month            = {jul},
    slides           = {},
    year             = {2012},
    keywords         = {optimization, microkernels, verification, trustworthy systems},
    title            = {Correct, fast, maintainable – choose any three!},
    booktitle        = {Asia-Pacific Workshop on Systems (APSys)},
    pages            = {7},
    address          = {Seoul, Korea}