Correct, fast, maintainable — choose any three!
Authors
NICTA
UNSW
Abstract
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
@inproceedings{Blackham_Heiser_12, publisher = {ACM}, doi = {10.1145/2349896.2349909}, author = {Blackham, Bernard and Heiser, Gernot}, month = jul, slides = {http://ts.data61.csiro.au/publications/nicta_slides/5858.pdf}, 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} }