> I worked with L4, and we had to throw it out because the microkernel overhead caused a 2x performance hit on frames per second for animations on a 400MHz ARM9.

Were you sending individual graphics commands and rasters over IPC or something, or was that just the cost of the flips, and maybe a second flip from a compositor (or blitter)?

Userspace would render its local window and send the invalidated regions to the kernel.

The problem was two fold. L4 ipc was just slower then a swi, and l4 driver model would lock the page table for every region instead of just checking every region all at once.

Which L4 was this, by the way? Did you replace it with an RTOS, a POSIX system?

We had an internal bear metal implementation already.

L4 was just pushed as the “hotness”, and ironically as a way to get around the linux GPL issues at the time.

I don’t want to sound to critical. L4 is actually easier to build drivers for than Linux, and you are much less likely to shoot yourself in the foot.

It’s a great microckernel. It’s just that 4% may all come from the most human sensitive application.

I still can't tell what L4 you're talking about. I've heard that there are some pretty big differences in performance between other L4s and seL4, for example.

The 4% come from a application-level benchmark that was popular back then. This is about ARM9/armv5 too, which is not suited for any multi-user OS as address spaces switching is very expensive compared to today's architectures (armv6+) due to the needed cache flushing on every address space switch. This has nothing to do with L4 variants, this is an architectural issue.

ARM9's cache architecture is not suited for frequent address space switches due to the requirement to flush caches on every switch. All multi-user OSes suffer there it's just more accentuated on microkernels.

Yep! If I recall correctly we had to blow away the entire cache on every system call because the line invalidate was so slow.