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.
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.