Linked by Thom Holwerda on Wed 22nd Jan 2014 13:47 UTC, submitted by fran
OSNews, Generic OSes

The Muen Separation Kernel is the world's first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. It is developed in Switzerland by the Institute for Internet Technologies and Applications (ITA) at the University of Applied Sciences Rapperswil (HSR). Muen was designed specifically to meet the challenging requirements of high-assurance systems on the Intel x86/64 platform. To ensure Muen is suitable for highly critical systems and advanced national security platforms, HSR closely cooperates with the high-security specialist secunet Security Networks AG in Germany.

The webpage contains instructions for building the kernel yourself, for installing it in a virtual machine, and for running it on real hardware.

Thread beginning with comment 581548
To read all comments associated with this story, please click here.
No basis in fact
by hackus on Fri 24th Jan 2014 03:38 UTC
Member since:

"Again, no actual basis in fact. Yes, IPC introduces some overhead that can impact speed (and therefore performance per watt.) How large that impact is depends on a lot of factors. Monolithic kernels have their own share of issues to resolve. There are trade-offs to any design decision."


I agree.

Microkernels have gigantic elephant sized tradeoffs, while Monolithic kernels have Mymaridae sized tradeoffs.


Reply Score: 1

RE: No basis in fact
by Alfman on Fri 24th Jan 2014 06:51 in reply to "No basis in fact"
Alfman Member since:


Your posts to this article sound very preachy to me. They keep saying things you want us to take as fact, but you haven't really shown any evidence to support your assertions. I wouldn't mind so much if you produced _something_ tangible, but these claims that microkernels are as horrible as you say they are, even on modern hardware, it's beginning to sound like dogma. If I am mistaken and you do have some factual information on which your view is formulated, then I apologize. However I will ask that you please post it here for the benefit of all to discuss.

I do expect microkernels to have some performance overhead when designed as a strait substitute for a macrokernel, but on modern hardware using the latest isolation techniques, overhead should be minimal. My preferred design for a microkernel would be based on async IO with zero-copy message queues that amortizing syscalls across a greater number of operations. This could reduce the overhead to practically NIL and even end up beating the conventional macrokernels that require one syscall/operation.

To put it in clearer terms:
CPU cycles =
A) userspace cycles/unit work +
B) context switch cycles/"syscall" +
C) kernel cycles/unit work

"syscall" is in quotes because I'm not defining the mechanism nor the number of context switches involved, my point is to show that the overhead, whatever it is, can be amortized across multiple operations.

Example 1:

A = 1000 cycles/task
B = 1000 cycles/syscall
C = 1000 cycles/task

A = 1000 cycles/task
B = 50 cycles/syscall
C = 1000 cycles/task

These numbers are merely illustrative, note that I'm giving macrokernels a large advantage by giving the microkernel a 20x syscall performance penalty for additional context switching. So under these circumstances the microkernel will require 3000 cycles to get the task completed, 46% MORE than the macrokernel's 2050 cycles.

Example 2:
A = 1000 cycles/task * 100
B = 1000 cycles/syscall
C = 1000 cycles/task * 100

A = 1000 cycles/task * 100
B = 50 cycles/syscall
C = 1000 cycles/task * 100

So by taking advantage of the amortization of syscalls over 100 tasks, the microkernel needs only 2010 cycles per task and the macrokernel needs 2005 cycles per task, a mere .5% advantage. Note that the amortized microkernel uses FEWER cycles per task than the original macrokernel above!

I also think there are also other potential optimizations as well. Zero-copy memory-mapped IPC could theoretically eliminate the microkernel IPC syscalls entirely, relying entirely on fixed overhead scheduling instead, thereby avoiding almost all syscall related overhead. I conceed this is quite a different (read "incompatible") approach from the kernel interfaces we're traditionally used to, but it'd still have very real potential to offer scalability in extremely demanding applications all the while offering benefits of secure isolation as well. We should not let labels like "microkernel" overshadow merit and should welcome innovation regardless of where it comes from.

Edited 2014-01-24 07:07 UTC

Reply Parent Score: 3

RE[2]: No basis in fact
by moondevil on Fri 24th Jan 2014 13:34 in reply to "RE: No basis in fact"
moondevil Member since:

Additionally as I mentioned in another thread, there are a few micro-kernels being used in production nowadays, some of them by well known companies.

It is no like we are discussing some OS design stuck in university labs.

Reply Parent Score: 2