As far as I understand you want to find out whether:
- mklinux is really as bad as published
- L4Linux is really as fast as published
Start with the first one.
Then fetch a version of L4 from l4kabuild l4linux 2.0 against it and try to find out about the second point. (I don't know whether l4ka's version supports 4Mb pages and small address spaces but you will find out whether they do or not)
Hazelnut supports small spaces. We published a TR about the performance of small spaces for the P4 architecture using an L4Linux environment. See also: http://i30www.ira.uka.de/research/publications/
Actually, the relative syscall overhead using an adopted glibc was lower than the original numbers given by the SOSP paper. We ran L4Linux and the applications in small spaces. (Hazelnut supports different configurations for small spaces -- up to 2GB for the small space area.)
- Volkmar