On 22 Aug 2015, at 13:09 , Qing Wei
1 How could the virtulization overhead achieve only 9%, according to the
report, KVM (theoretically faster?) would cause 20% - 30% overhead for
io intensive workloads
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.
2 Does the user space VMM open source?
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.
3 What is the device model of the VMM, take the
virtual disk in this paper
as an example, is it to some extent, like the device model in XEN? The VD
driver in guest os sends the requests to VMM, VMM does the hard work
to write the data into physical disk? If the understanding is correct, then
VMM must implement the real device driver? For XEN, it could leverage
the os in domain 0 to avoid reimplement device drivers. So in a word,
is it necessary to rewrite device driver for seL4 or there are some ways
to leverage legacy drivers by passthrough something?
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.
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.