Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os?
Cheers, Qing Wei
On 16 Jul 2015, at 21:22 , Qing Wei wq_idol@163.com wrote:
Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os?
For general microkernel and L4 introduction, I recommend - wikipedia, try “microkernel” and “L4 microkernel family”. - the FAQ on sel4.systems - our Advanced OS course: https://www.cse.unsw.edu.au/~cs9242/current/
You’ll find answers to most of your more specific questions in this paper: https://ssrg.nicta.com.au/publications/nictaabstracts/Heiser_SDBSA_13.abstra...
Re multicore, you’ll find more in this paper (only abstract for now, the PDF will go up next week): https://ssrg.nicta.com.au/publications/nictaabstracts/Peters_DEH_15.abstract...
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.
On Thu, Jul 16, 2015 at 7:22 AM, Qing Wei wq_idol@163.com wrote:
Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability?
I do not think sel4 support multicore completely
(2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os?
Cheers, Qing Wei _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Dear Professor Heiser, I have read the eurosys paper you recommended, I think it is a good idea to leverage a reliable second os to handle disk write requests. I am curious about the following questions, 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 2 Does the user space VMM open source? 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?
Cheers, Li Wang
At 2015-07-16 19:50:24, "Gernot Heiser" gernot@nicta.com.au wrote:
On 16 Jul 2015, at 21:22 , Qing Wei wq_idol@163.com wrote:
Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os?
For general microkernel and L4 introduction, I recommend
- wikipedia, try “microkernel” and “L4 microkernel family”.
- the FAQ on sel4.systems
- our Advanced OS course: https://www.cse.unsw.edu.au/~cs9242/current/
You’ll find answers to most of your more specific questions in this paper: https://ssrg.nicta.com.au/publications/nictaabstracts/Heiser_SDBSA_13.abstra...
Re multicore, you’ll find more in this paper (only abstract for now, the PDF will go up next week): https://ssrg.nicta.com.au/publications/nictaabstracts/Peters_DEH_15.abstract...
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. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 22 Aug 2015, at 13:09 , Qing Wei wq_idol@163.com wrote:
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.
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.
-
Gernot Heiser -
Qing Wei -
Yuxin Ren