Correct, fast, maintainable – choose any three!

Select |




Print


Blackham, Bernard; Heiser, Gernot

Blackham, Bernard; Heiser, Gernot


2012-07-23


Conference Material


Asia-Pacific Workshop on Systems (APSys)


Seoul, Korea


7


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.


ACM


optimization, microkernels, verification, trustworthy systems


https://doi.org/10.1145/2349896.2349909


http://apsys2012.kaist.ac.kr/


nicta:5858


Blackham, Bernard; Heiser, Gernot. Correct, fast, maintainable – choose any three!. In: Asia-Pacific Workshop on Systems (APSys); Seoul, Korea. ACM; 2012-07-23. 7. https://doi.org/10.1145/2349896.2349909



Loading citation data...

Citation counts
(Requires subscription to view)