On 16 Jul 2015, at 21:22 , Qing Wei
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.