3 ms·

I'm not an OS designer or OS programmer so I'm just arm-chairing here. Mirage OS (also Haskell's HaLVm) are layers on-top of Xen. It would seem to me that the

by Ixiaus 12y ago

I'm not an OS designer or OS programmer so I'm just arm-chairing here. Mirage OS (also Haskell's HaLVm) are layers on-top of Xen. It would seem to me that the microkernel and exokernel designs wouldn't really be used the way Mirage is on-top of Xen except that Mirage / HaLVm could replace much of the userland on the microkernel or be its own os library on an exokernel. The overlap I think you're seeing is that Xen acts a bit like a "microkernel" and Mirage is the userland implementing the lower-level interfaces provided by the kernel. Minix in this sense is a more complete picture but I don't see why Mirage or HaLVm couldn't be "userland libraries" for microkernels and exokernels. I think it's a great idea actually. Build a small kernel with very few responsibilities so it's easier to prove safety, then construct the whole of userland on-top of a known type-safe language (Haskell or OCaml) and you get a potent platform!

chubot 12y ago
I think it's a great idea actually. Build a small kernel with very few responsibilities so it's easier to prove safety That already exists and was just open sourced! See seL4: http://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 http://en.wikipedia.org/wiki/L4_microkernel_family#High_assu...
AceJohnny2 12y ago
> I think it's a great idea actually. Build a small kernel with very few responsibilities so it's easier to prove safety, then construct the whole of userland on-top of a known type-safe language (Haskell or OCaml) and you get a potent platform! While I like constructing a userland using a safe language over a small safe microkernel, I am annoyed by the hype this is getting because it's not new. Thinks like QNX, Symbian, GNU Hurd are based on this very concept. The only difference nowadays is the renewed interest in safer languages, which I suppose is only enabled thanks to Moore's Law giving us the headroom. It's also like everyone forgot the flamewars (Torvalds-Tanenbaum anyone?) about how microkernels were inherently slower. I'm sure that demon is going to reemerge soon enough, and we'll be back mucking around in C/C++ for performance. Just like 20 years ago. Those who don't learn from history...
- chubot 12y ago
  Torvalds' argument wasn't that microkernels were slower though. It was that distributed algorithms are harder than shared memory algorithms. Having not written a kernel, I can't judge those claims. It would be interesting to know if Minix has any "harder" algorithms than Linux because of this. I think L4 already existed around that time, and got 10x or 100x improvement in IPC times, showing that microkernels could be fast enough.
imanaccount247 12y ago
Xen doesn't just act a bit like a microkernel, it is a microkernel.

by Ixiaus 12y ago

chubot 12y ago

I think it's a great idea actually. Build a small kernel with very few responsibilities so it's easier to prove safety That already exists and was just open sourced! See seL4: http://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 http://en.wikipedia.org/wiki/L4_microkernel_family#High_assu...

AceJohnny2 12y ago

> I think it's a great idea actually. Build a small kernel with very few responsibilities so it's easier to prove safety, then construct the whole of userland on-top of a known type-safe language (Haskell or OCaml) and you get a potent platform! While I like constructing a userland using a safe language over a small safe microkernel, I am annoyed by the hype this is getting because it's not new. Thinks like QNX, Symbian, GNU Hurd are based on this very concept. The only difference nowadays is the renewed interest in safer languages, which I suppose is only enabled thanks to Moore's Law giving us the headroom. It's also like everyone forgot the flamewars (Torvalds-Tanenbaum anyone?) about how microkernels were inherently slower. I'm sure that demon is going to reemerge soon enough, and we'll be back mucking around in C/C++ for performance. Just like 20 years ago. Those who don't learn from history...

chubot 12y ago
Torvalds' argument wasn't that microkernels were slower though. It was that distributed algorithms are harder than shared memory algorithms. Having not written a kernel, I can't judge those claims. It would be interesting to know if Minix has any "harder" algorithms than Linux because of this. I think L4 already existed around that time, and got 10x or 100x improvement in IPC times, showing that microkernels could be fast enough.

imanaccount247 12y ago

Xen doesn't just act a bit like a microkernel, it is a microkernel.