seL4 Micro-Kernel Working Towards A General-Purpose, Multi-Server OS

[kvuj]

Yes https://genode.org/documentation/articles/sel4_part_2

Genode has a bunch of kernels under his belt https://genode.org/documentation/platforms/index

Looking around, I couln't find if SculptOS (their precompiled binary) was using SeL4 by default under the hood.

If so, I'm definitely trying it! It looks so cool.

[pabloski]

Wasn't Genode OS used with L4?

Yes https://genode.org/documentation/articles/sel4_part_2

Genode has a bunch of kernels under his belt https://genode.org/documentation/platforms/index

[pabloski]

l4linux is monolithic linux running on hypervisor

Yes and it is faster than Linux, even in the face of the hypeolithic linux runnrvisor overhead!!

can you share benchmark of some modern game on l4linux?

Games are programs. If business/office/utility programs go fast, games will go fast too!

well you have no clue what you are talking about(see first part of this post)

Because asking about games benchmarks means having a clue!?! Ok God!

Also, what part of my last post don't you answer? A lot of mobile phones run on L4 + Android on top!!! And they are damn fast. Some of them even compartmentalize Android subsystems under isolated virtual machines. And they are damn fast!!

[Nemerian]

Wasn't Genode OS used with L4?

[pal666]

They did just this with L4linux and it was faster than stock Linux!!!

l4linux is monolithic linux running on hypervisor, it isn't more secure than plain linux. btw, can you share benchmark of some modern game on l4linux?

I repeat, you people are living in the past. You have no clue at all of the improvements in the microkernel space.

well you have no clue what you are talking about(see first part of this post)

[pal666]

No, but the capability mechanisms in seL4 would allow the browser to be really well isolated from the rest of the system.

for most people browser is the system. it contains all your passwords, all your credit card numbers etc. and i wasn't even thinking about chromeos

[pal666]

If a microkernel is ABI-compatible with the Linux kernel, then by definition it isn't actually a microkernel.

i'm pretty sure "micro" part refers to implementation rather than interface

[pal666]

Will using synthetic oil in your car engine prevent your muffler from rusting out?

Obviously having fewer kernel bugs doesn't solve all problems in other system components, but that doesn't mean that it's not worthwhile to use a kernel with fewer bugs.

obviously any approach is not worthwhile unless it's scalable

[pabloski]

When it comes to Minix 3, especially when compared to seL4, it's not a misconception. Minix3 has some interesting overall design decisions in user space, but seL4 is by far the better kernel. I'd be down for a port of the Minix3 userspace to seL4 (yes, I am aware this is a lot of work because of the different ideas of just how micro the kernel should be).

I agree. Let's not forget that Minix was born to teach OSdev. seL4 has been built to be used in the wild. Also, L4 has changed the way microkernels work. No more IPC everywhere, but page sharing between process boundaries. Definitely a revolution, giving us a bing performance boost.

[pabloski]

all you have to do to get rid of this "misconception" is to provide microkernel, abi-compatible with linux, running just as fast. what was stopping you all those years?

They did just this with L4linux and it was faster than stock Linux!!!

I repeat, you people are living in the past. You have no clue at all of the improvements in the microkernel space. Did you know that a bunch of Android OEMs run Android virtualized on top of seL4????