Virtualisation overheads are highly dependent on workload and hardware platform. This paper’s aim wasn’t to evaluate virtualisation overheads. In fact, the RapiLog workload did not create high interrupt loads, so overheads can be expected to be low. The work was done years before seL4 was open-sourced, and the VMM has significantly bitrotted in the meantime, as has the multikernel it was running on. We’ll announce our roadmap soon, which will contain a re-written VMM. As the paper explains, the driver is very simple, it doesn’t need to do much, and only sequential writes are performance-critical. Yes, we could do the same Dom-0 hack Xen uses, which results in a multi-million-line TCB, so what’s the point? The whole point of seL4 is dependability, which is fundamentally at odds with such an approach. Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.