Micronoyau L4

L4 est un micronoyau de seconde génération conçu par Jochen Liedtke (en). Les micronoyaux du début des années 1990 étant extrêmement lents par rapport à leurs concurrents monolithiques, Liedtke décide de développer ses propres micronoyaux. Il développe ainsi les micronoyaux L3 et ensuite L4. Les nombreuses améliorations apportées à ceux-ci et leurs successeurs ont depuis permis d'accroître considérablement la vitesse de ces anciens noyaux pour en arriver ensuite aux micronoyaux actuels.

L’idée générale de L4 est ainsi résumée par Liedtke lui-même : « un concept est toléré au sein du micronoyau seulement si son déplacement à l'extérieur du noyau, c'est-à-dire permettre des implémentations alternatives, empêcherait la mise en œuvre d'une fonctionnalité nécessaire au système. »

Motivations

Les micronoyaux minimisent les fonctionnalités du noyau. Le noyau fournit un ensemble de services de base : ordonnancement, synchronisation, messages etc. tandis que les services du système d'exploitation fonctionnent dans le monde utilisateur . Les systèmes d'exploitation à base de noyau monolithique comme le noyau de Linux mettent l’accent sur la performance en permettant à de nombreux services de fonctionner en mode privilégié et en simplifiant l'accès aux ressources du système. Les micronoyaux privilégient la sécurité et la stabilité. Ceci fait toujours l'objet de controverses, comme celle qui a opposé Linus Torvalds à Andrew S. Tanenbaum même si la popularité du noyau Linux a temporairement tranché la question. Les premiers systèmes d'exploitation à base de micronoyaux étaient notoirement lents.

C’est dans l’objectif d’améliorer les performances des systèmes d’exploitation à base de noyaux minimalistes que Jochen Liedtke commençe à développer les noyaux L3 puis L4. Le principe fondamental de ces noyaux consiste simplement en : « un concept est permis dans le noyau uniquement lorsqu’il ne peut être implémenté dans l’espace utilisateur ». Ce type de noyau fournit ainsi exclusivement les fonctions fondamentales telles que les communications, le mappage, etc. Il impose également les politiques. Un micronoyau ne fait aucun travail réel (le travail du micronoyau consiste seulement au contrôle et à la gestion des tâches qu’il délègue aux processus dans l’espace utilisateur).

Histoire

Il y a 20 ans, Jochen Liedtke démontra avec son noyau L4 que les communications interprocessus des micronoyaux pouvaient être 10 à 20 fois plus rapides que ce à quoi l’on aurait pu s’attendre à l’époque. L4 fut conçu à partir d’une version antérieure appelée L3 et développée par John Liedtke au début des années 1980 sur les plateformes i386. Il a été déployé commercialement sur plusieurs milliers d’installations (principalement dans des écoles). Comme tous les micronoyaux de l’époque, L3 souffrait d’un coût des communications interprocessus de l’ordre de 100 microsecondes.

Liedtke utilisait initialement L3 pour expérimenter de nouvelles idées. Celui-ci a utilisé pour la première fois le nom « L4 » avec l’ABI v2 déjà présent dans la communauté depuis 1995. Par la suite, il sera complètement réécrit en assembleur pour les ordinateurs i486 et fut très vite porté pour les Pentium.

Ce travail initial déclencha une évolution de 20 ans suivie de multiples révisions des ABI ainsi que de nouvelles implémentations. Celle-ci a commencé par la réimplémentation de l’ABI Dresde et UNSW sur 64 bits pour les processeurs Alpha et MIPS, ces derniers ayant intégré les opérations les plus lentes en langage C. Ces deux noyaux ont ainsi pu obtenir des communications interprocessus inférieures à une microseconde, ce qui fut facilité par le fait qu’ils étaient des noyaux à code source ouvert. Le noyau UNSW Alpha constitua le premier noyau L4 multiprocesseurs.

Liedtke, qui avait quitté GMD pour IBM Watson, apporta son expérience lors de l’implémentation d’une ABI qui sera par la suite connue sous le nom de Version X. GMD et IBM imposaient une politique de propriété intellectuelle très restrictive pour les autres chercheurs, ce qui poussa le projet « Dresde » à repartir à zéro en implémentant une nouvelle version appelée « Fiasco », en référence à leur mauvaise expérience et en essayant de mieux traiter les questions de propriété intellectuelle.

« Fiasco » est la première version du noyau L4 qui fut complètement écrite dans un langage de haut niveau (C++) et la plus ancienne version du code de base des noyaux L4 encore activement maintenue. Il a été le premier noyau L4 commercialisé de manière significative (estimation: plus de 100 000 ventes).

Quand Liedtke est arrivé à Karlsruhe en Allemagne, lui et son étudiant^[Lequel ?] adaptèrent dans une nouvelle version écrite en C et appelée « Hazelnut », qui fut le premier noyau L4 porté sur d’autres architectures (de Pentium I à ARM).

L’expérience de Karlsruhe avec l’ABI Version X et celle de L4Ka::Hazelnut entraîna une révision majeure de l’ABI V4 afin d’améliorer la portabilité du noyau. Après la mort de Liedtke en 2001, ses étudiants ont implémenté un nouveau noyau libre : L4Ka::Pistachio avec L4Ka. Il fut écrit en C++ et d’abord porté sur x86 et PowerPC, ensuite sur UNSW/NICTA et peu après sur MIPS, Alpha, PowerPC 64 bits et ARM.

À la NICTA (en), ils ont tout de suite reciblé leur installation afin de l’utiliser dans des systèmes embarqués contraints en ressources. En conséquence, une nouvelle version du noyau à partir d’une copie du code de « Pistachio » vit le jour et fut appelée NICTA::Pistachio-embarqué (« L4-embarqué »). Il fut massivement commercialisé lorsque Qualcomm décida de l’utiliser comme système d’exploitation dans le micrologiciel de leurs modems sans fil. La filiale de NICTA Open Kernel Labs (en) devint le support et le développement du noyau qu'il rebaptisa « OKL4 ». Une autre version fut déployée, PikeOS, un clone commercialisé par SYSGO (en) et certifié pour une utilisation dans les systèmes critiques de l’aéronautique et également dans les avions et les trains.

Graphe de la famille L4.

Quelques concepts de base

L’idée principale de L4 étant d’améliorer la vitesse des micronoyaux, plus particulièrement celle des communications interprocessus tout en conservant les concepts des micronoyaux, il fallut réadapter certains concepts et en introduire d’autres. Nous présenterons ci-dessous les concepts qui permirent à Liedtke de relever son défi.

Minimalité

Les micronoyaux L4 fournissent une API simple, minimale et une abstraction qui supportent la création, l’exécution et les communications interprocessus (IPC) entre les threads en plus de permettre l’isolation et la gestion des différentes tâches.

Les principaux moteurs de conception de Liedtke mettaient l'accent sur la minimalité et sur la performance des communications interprocessus en ayant la ferme conviction d’améliorer les points faibles de L3. Il formula le principe de minimalité des micronoyaux comme suit : « Un concept est accepté dans un micronoyau seulement si le mouvement en dehors du noyau empêcherait la mise en œuvre d'une fonctionnalité requise par le système. »

Ce principe fut le fondement de la conception des noyaux L4. Mais selon Kevin Elphinstone et Gernot Heiser, aucun concepteur de micronoyau ne peut affirmer avoir créé un micronoyau pur dans le strict respect du principe de minimalité. Pour preuve, ils possèdent tous un ordonnanceur dans le noyau qui met en œuvre une politique d'ordonnancement particulière. À cette époque, ils pensaient que personne ne pouvait concevoir un micronoyau dans lequel toute la politique de planification est déléguée dans l'espace utilisateur sans imposer de coûts énormes.

Différence entre la taille d'un noyau monolithique et un micronoyau. Ceci met en œuvre l'avantage du principe de minimalité.

Espaces d’adressage

Au niveau matériel, un espace d’adressage est un mappage qui associe chaque page virtuelle à une page physique, ou bien la marque comme « non accessible ». Le mappage est implémenté par la TLB et la table de pages.

C’est l’unité de gestion de la mémoire qui fournit l’isolation spatiale. Il contient toutes les données directement accessibles par un thread. L’espace d’adressage dans L4 peut être construit récursivement. Un thread peut mapper des parties communes à son espace d’adressage dans celui d’un autre thread et ainsi partager les données de ces parties de son espace mémoire.

Le concept de tâche est équivalent à celui de l’espace d’adressage. Dans L4, une tâche est un ensemble de threads partageant un espace d’adressage.

Threads et IPC

La communication interprocessus par passage de messages est l’un des paradigmes les plus utilisés par les micronoyaux et d’autres applications client-serveur. Il aide à améliorer la modularité, la flexibilité, la sécurité ainsi que la scalabilité.

Pour communiquer entre des threads possédant des espaces d’adressage différents, la méthode classique consiste à faire transmettre les messages entre threads via le noyau. IPC implique toujours un certain accord entre les deux parties : l’expéditeur décide d’envoyer des informations et détermine son contenu, alors que le récepteur détermine s’il est disposé à recevoir des informations et s’il est libre d’interpréter le contenu du message.

Selon Liedtke, « les performances des communications interprocessus sont plus importantes ». Il existe deux types d’IPC : les IPC synchrones et asynchrones. Les micronoyaux de première génération ont utilisé des IPC asynchrones (par exemple Mach). Le noyau garde le message dans une mémoire tampon jusqu’à ce que le récepteur soit prêt à recevoir le message ; cela a pour conséquence la double copie du message et c'est ceci qui fit perdre beaucoup de performance à Mach. Les micronoyaux de deuxième génération (comme L4) ont adopté les IPC synchrones pour la communication entre les threads. Dans ces communications, le premier communiquant attend jusqu’à ce que l’autre soit prêt : le message peut alors être directement copié entre ces threads, ce qui évite une copie temporaire inutile dans le noyau. Les IPC synchrones satisfont ainsi une implémentation efficace et nécessaire.

Interruptions

L’abstraction naturelle des interruptions correspond aux communications interprocessus. Le matériel est considéré comme un ensemble de threads qui ont des identifiants spéciaux et qui envoient des messages contenant uniquement l’identifiant de l’expéditeur aux threads logiciels qui leur sont associés. Le thread récepteur vérifie l’identifiant de l’expéditeur du message et si le message est une interruption matérielle, il est alors interrompu immédiatement. La transformation de l’interruption en message est faite par le noyau, mais ce dernier n’est pas impliqué dans le traitement de l’interruption. En réalité, le noyau ignore complètement la sémantique de traitement des interruptions.

Les pilotes dans l'espace utilisateur

Un pilote de périphérique est un processus qui a directement accès aux ports d’entrées-sorties mappés directement dans son espace d’adressage et reçoit des messages (interruptions) du matériel à travers les mécanismes standards IPC. Dans la philosophie des micronoyaux L4, ils ne doivent jamais être intégrés dans le micronoyau. Les interruptions entrantes sont transformées en messages aux threads associés. Ceci est la base pour implémenter les pilotes de périphérique comme des serveurs de l’espace utilisateur.

Famille du micronoyau L4

Depuis le développement de L4 par Liedtke, plusieurs implémentations ont suivi dont Fiasco, L4Ka::Pistachio, P4, L4 for PowerPC, L4Ka::Hazelnut, L4/MIPS, L4/Alpha, L4/x86, etc.

Fiasco

Fiasco a été développé par l’équipe Fiasco de l’université technique de Dresde en 1999 et il est à l’origine du système DROPS (Dresden Real-Time Operating System Project). On dit souvent « L4/Fiasco » pour parler de Fiasco, ce qui met en évidence sa relation avec L4.

Un micronoyau fournit les mécanismes qui sont indispensables, mais n’applique pas les politiques qui sont la plupart du temps implémentées dans l’espace utilisateur^[pas clair]. Dans le système L4/Fiasco, il y a un environnement L4 (L4Env) qui est un environnement de programmation pour les applications qui devront tourner au-dessus d’un noyau^{[Information douteuse]} L4/Fiasco.

Le modèle de programmation de “L4/Fiasco” est basé sur l’architecture client-serveur. L’ordonnanceur est préemptif avec une basse priorité, et un ordonnancement de type rotation entre les tâches ayant le même propriétaire.

L4Ka::Pistachio

Pistachio est développé par l’équipe System Architecture Group de l’Institut de technologie de Karlsruhe (Allemagne) en collaboration avec le DiSy group de l’Université de Nouvelle-Galles du Sud (Australie). Il est distribué sous la licence BSD.

Il a été porté sur les architectures suivantes : Alpha (21164 et 21264), AMD64 (Opteron 242, Simics), ARM (SA1100, XScale, ARM925T), IA32 (Pentium et compatibles), IA-64 (Itanium1, Itanium2, Ski), MIPS 64 bits (R4000, R5000 (en)), PowerPC 32 bits (IBM 750) et 64 bits (POWER3, POWER4). Il supporte les systèmes multiprocesseurs.

La dernière version, la X.2, est sortie en mai 2009.

seL4

Le micronoyau seL4 est un membre de la famille des micronoyaux L4 conçu pour offrir des mécanismes de sécurité forts tout en conservant la haute performance qui est d’usage dans la famille L4 et considérée comme essentielle pour les utilisations réelles. C’est un micronoyau de troisième génération qui est complètement basé sur un noyau de type L4. Comme ce dernier, il fait usage d’abstractions pour les espaces d’adressage virtuel, les threads, les communications interprocessus….

Les espaces d'adressages virtuels sont formés par manipulation explicite des objets noyaux : chemin des pages, table des pages, etc. Ils n'ont pas de structure de base définie (à part ceux réservés au noyau seL4 lui-même).

Les threads sont des entités actives de seL4. En associant un cNœud^{[Information douteuse]} et un espace d’adressage virtuel avec un thread, les politiques gérées au niveau utilisateur créent une abstraction de haut niveau comme les processus ou les machines virtuelles.

Les communications interprocessus sont supportées sous deux formes : par l’utilisation de messages synchrones par passage de paramètres (port, destination donc sans l’utilisation de mémoire tampon dans le noyau) et par des notifications asynchrones via des paramètres asynchrones (les objets rendez-vous composés d’un seul mot dans le noyau).

Les pilotes des périphériques sont exécutés comme des applications en mode utilisateur qui ont accès aux registres et à la mémoire des périphériques, soit par mappage du périphérique dans l’espace d’adressage virtuel du processus, soit par contrôle des accès au périphérique (c’est notamment le cas sur les architectures x86)). « sel4 » fournit les mécanismes pour gérer la réception des notifications des interruptions (via IPC asynchrones) et pour les accusés de réception.

Les noyaux seL4 fonctionnent sur les processeurs ARM et x86, mais les versions certifiées de seL4 qui existent actuellement sont pour ARMv6 (en) et ARMv7. Le portage sur les plateformes x86 ne bénéficie pas actuellement^[Quand ?] d’un support officiellement, mais il existe tout de même une version expérimentale multicœurs de seL4 pour x86.

Projets utilisant L4

• (en + de) « DROPS — Dresden Real-Time Operating System Project », sur os.inf.tu-dresden.de, 2013 (consulté le 2013).
• L⁴Linux (en), portage du noyau Linux pour L4Ka et Fiasco.
• Portage de GNU Hurd pour L4Ka::Pistachio : l’objectif de ce projet est de remplacer le micronoyau sur lequel fonctionne GNU Hurd. En 2014, celui-ci fonctionnait avec une version GNU de Mach, et en était encore au stade expérimental.

Bibliographie

 : document utilisé comme source pour la rédaction de cet article.

• (en) Qingguo ZHOU, Canyu LI, Ying DING, Ganghui CHENG et Hu BIN, « The Analysis of L4 Linux Implementation for education », IEEE Concurrency, vol. 1,‎ août 2009, p. 137–140 (ISBN 978-1-4244-3928-7, DOI 10.1109/ITIME.2009.5236446). 
• (en) kevin Elphinstone et Gernot Heiser, « From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels? », ACM,‎ novembre 2013, p. 133–150 (ISBN 978-1-4503-2388-8, DOI 10.1145/2517349.2522720). 
• (en) Qingguo ZHOU, Canyu LI, Ying DING, Ganghui CHENG, Hu BIN et Nicholas McGuire, « A Case Study of Microkernel for Education », IEEE Concurrency, vol. 1,‎ août 2009, p. 133–136 (ISBN 978-1-4244-3928-7, DOI 10.1109/ITIME.2009.5236445). 
• (en) Hironao Takahashi, Kinji Mori et Hafiz Farooq Ahmad, « Efficient I/O intensive multi tenant SaaS system using L4 level cache », IEEE Concurrency,‎ juin 2010, p. 222–228 (ISBN 978-1-4244-7327-4, DOI 10.1109/SOSE.2010.14).
• (en) Jochen Liedtke, « Improving IPC by Kernel Design », ACM, vol. 25,‎ décembre 1993, p. 175–188 (ISBN 0-89791-632-8, DOI 10.1145/168619.168633). 
• (en) Tae-You Lee, Hyung-Rok Seo et Dong-Ryeol Shim, « Fault Isolation Using Stateless Server Model in L4 Microkernel », IEEE, vol. 2,‎ février 2010, p. 518–522 (ISBN 978-1-4244-5585-0, DOI 10.1109/ICCAE.2010.5451638).
• (en) Peter Druschel, Larry L. Peterson et Norman C. Hutchinson, « Beyond Micro-Kernel Design: Decoupling Modularity and Protection in Lipto », IEEE, vol. 2,‎ juin 1992, p. 512–520 (ISBN 0-8186-2865-0, DOI 10.1109/ICDCS.1992.235002).
• (en) Jochen Liedtke, « On micro-kernel construction », ACM, vol. 29,‎ décembre 1995, p. 237–250 (ISBN 0-89791-715-4, DOI 10.1145/224056.224075). 
• (en) Ki-Seok Bang, Su-Young Lee, Ki-Hyuk Nam, Wan-Yeon Lee et Young-Woung Ko, « Verifying Behavior of L4 Microkernel based Mobile Phone », IEEE, vol. 1,‎ février 2007, p. 113–115 (ISBN 978-89-5519-131-8, DOI 10.1109/ICACT.2007.358317).
• (en) Amaury Gauthier, Clément Mazin, Julien Iguchi-Cartigny et Jean-Louis Lanet, « Enhancing fuzzing technique for OKL4 syscalls testing », IEEE, vol. 1,‎ août 2011, p. 728–733 (ISBN 978-1-4577-0979-1, DOI 10.1109/ARES.2011.116).
• (en) S. Hessel, F. Bruns, A. Lackorzynski, H. Härtig et J. Hausner, « Acceleration of the L4/Fiasco Microkernel Using Scratchpad Memory », ACM,‎ juin 2008, p. 6–10 (ISBN 978-1-60558-328-0, DOI 10.1145/1622103.1622106).
• (en) Dohun Kim, Jugwan Eom et Chanik Park, « L4oprof: A Performance-Monitoring-Unit-Based Software-Profiling Framework for the L4 Microkernel », ACM, vol. 41,‎ juillet 2007, p. 69–76 (ISSN 0163-5980, DOI 10.1145/1278901.1278911).
• (en) Chen Tian, Daniel Waddington et Jilong Kuang, « A Scalable Physical Memory Allocation Scheme For L4 Microkernel », IEEE,‎ juillet 2012, p. 488–493 (ISBN 978-1-4673-1990-4, DOI 10.1109/COMPSAC.2012.85).
• (en) Jianjun Shen, Sihan Qing et Qingni Shen, « Design of a Micro-kernel Based Secure System Architecture », IEEE,‎ juin 2006, p. 384–385 (ISBN 1-4244-0130-5, DOI 10.1109/IAW.2006.1652123).
• (en) Dong-Guen Kim, Sang-Min Lee et Dong-Ryeol Shin, « Design of the Operating System Virtualization on L4 Microkernel », IEEE,‎ septembre 2008, p. 307–310 (ISBN 978-0-7695-3322-3, DOI 10.1109/NCM.2008.165).
• (en) Lucyantie Mazalan, Raja Mariam Ruzila Raja Ahmed Sufian, Ahmad Kamal Abdul Aziz, Mohd Saufy Rohmad et D^r Jamalul-lail Ab. Manan, « Experience with the Implementation of AES256 on L4 Microkernel using DROPS (BID) Environment », IEEE, vol. 3,‎ août 2008, p. 1–5 (ISBN 978-1-4244-2327-9, DOI 10.1109/ITSIM.2008.4632027). 
• (en) Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, Tobby Murray, Dhammika Elkaduwe, Kolanski Rafal et Thomas Sewell, « Comprehensive Formal Verification of an OS Kernel », ACM Transactions on Computer Systems, vol. 32,‎ février 2014, p. 1–70 (ISSN 0734-2071, DOI 10.1145/2560537). 

Liens externes

• (de) « La famille des micronoyaux L4 ».
• (en) Site du projet L4Ka.