L4
Ursprünglich war L4 der Name eines Mikrokernels der zweiten Generation, entworfen und implementiert von Jochen Liedtke. Dieser war eine reine Assemblerimplementierung und lief lediglich auf Intel-x86-Basis. Später kamen weitere Umsetzungen hinzu, die auf anderen Plattformen liefen.
Inzwischen wird mit L4 hauptsächlich das API bezeichnet. Dieses wird nach den Stabilen Versionen Version 2 und Version 4 unterschieden, zwischen denen die Entwicklungsstadien X.0, X.1 und X.2 liegen. Aktueller Stand ist Version X.0.
Kernel, die auf dem L4-API basieren, bieten ein synchrones IPC und eine einfache, externe Speicherverwaltung.
Auf Basis von L4 können, dem modularen Prinzip der Mikrokerne folgend, graphische Nutzeroberflächen (wie DOpE), der Linux-Kern im Nutzermodus (L4Linux) und ganzheitlich echtzeitfähige Betriebssysteme (wie DROPS) laufen. L4 selbst kann in der Implementierung Fiasco/UX selbst auf Linux betrieben werden, was die Entwicklung deutlich vereinfacht, ähnlich dem Prinzip von User-Mode-Linux.
Für Entwickler von Anwendungen steht die Bibliothek L4Env zur Verfügung. Die Konstruktion von bewiesen sicheren Systemen wird mit dem Projekt VFiasco angestrebt, welches durch den Einsatz von aus der Mathematik und theoretischen Informatik bekannten Coalgebren verifiziert wird.
