Micronoyau L4

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir L4.
Article principal : Noyau de système d'exploitation.

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 a lui-même décidé de développer ses propres micronoyaux. Il développe ainsi ses micronoyaux L3 et ensuite L4. Les nombreuses améliorations apportées à ceux-ci et leurs successeurs ont depuis permis de réduire considérablement la vitesse de ces anciens noyaux pour en arriver ensuite à nos 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 noyau seulement si son déplacement à l'extérieur du noyau empêchait l'implémentation de la fonctionnalité requise par le système »[1].

Motivations[modifier | modifier le code]

Les micronoyaux minimisent les fonctionnalités qui sont fournies par le noyau : le noyau fournit un ensemble de mécanismes généraux tandis que les serveurs en mode utilisateur mettent en œuvre les services du système d'exploitation[2]. Les systèmes d'exploitation ayant un noyaux monolithiques et ceux ayant un micronoyaux ont tous deux un type de fonctionnement différent ce qui en font deux systèmes d'exploitation différents. Les OS à base d'un noyau monolithique mettent plutôt l'accent sur la haute performance alors que les micronoyaux misent plus sur la sécurité et la stabilité. Cependant, les premiers systèmes d'exploitation à base de micronoyaux étaient lents, leur efficacité n'était donc pas aussi élevée. C'est dans l'objectif d'améliorer les performances des systèmes d'exploitation à base de noyau minimal que Jochen Liedtke a commencé à développer les noyaux L3 et 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 mapping, etc. Il impose également les politiques. Un micronoyau ne fait aucun travail réel (Le travail du micronoyau consiste juste au contrôle et à la gestion des tâches qu'il délègue aux processus dans l'espace utilisateur)[3].

Histoire[modifier | modifier le code]

Il y a 20 ans, Jochen Liedtke a démontré avec son noyau L4 que les communications IPC des micronoyaux pouvaient être 10 à 20 fois plus rapides à ce que l'on aurait pu s'attendre à l'époque[4]. L4 a été construit à partir d'une version antérieure appelée L3, développé 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 les écoles). Comme tous les micronoyaux de l'époque, L3 souffrait du coût des communications IPC de l'ordre de 100 microsecondes[4].

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 (Application binary interface) déjà présent dans la communauté depuis 1995. Il a, par la suite, complètement été implémenté en assembleur sur les ordinateurs i486 et a très vite été porté sur les Pentium [5].

Ce travail initial a déclenché 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 sur les processeurs Alpha et MIPS, ces derniers ont intégré toutes les longues opérations en C. Ces deux noyaux ont ainsi pu atteindre une performance pour les IPC inférieure à une microseconde et étaient par ailleurs open-source. Le noyau UNSW Alpha constituait le premier noyau L4 multiprocesseur[5].

Liedtke qui avait quitté GMD pour IBM Watson, a apporté 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 ont imposé une politique de propriété intellectuelle très restrictive pour les autres chercheurs. Ceci poussa le projet Dresde à repartir de zéro en implémentant une nouvelle version appelée Fiasco en référence à leur mauvaise expérience et en essayant de traiter les questions de propriété intellectuelle[5].

Fiasco est la première version du noyau L4 qui a complètement été écrite en langage de haut niveau (C++) et la plus ancienne version du code de base des noyaux L4 encore activement maintenu. Il a été la premier noyau L4 commercialisé de manière significative (estimation: plus de 100 000 ventes)[5].

Quand Liedtke est arrivé à Karlsruhe, lui et son étudiant ont adapté dans une nouvelle version écrite en C, Hazelnut, qui fut le premier noyau L4 porté sur d'autres architectures (de Pentium à ARM)[5].

L'expérience de Karlsruhe avec Version X et Hazelnut a entraîné une révision majeure de l'ABI V4, visant à améliorer la portabilité du noyau. Après la mort de Liedtke en 2001, ses étudiants ont implémenté un nouveau noyau open-source, L4Ka::Pistachio de L4Ka. Il fut été écrit en C++, d'abord porté sur X86 et PowerPC, ensuite sur UNSW/NICTA et peu après sur MIPS, Alpha, PowerPC 64 bits et ARM[5].

À la NICTA, ils ont tout de suite reciblé leur installation afin de l'utiliser dans des systèmes embarqués avec des contraintes de ressources. En conséquence, une nouvelle version du noyau d'un fork de Psitachio vu le jour et fut appelée NICTA::Pistachio-embedded (« L4-embarqué »). Il a été massivement commercialisé lorsque Qualcomm décida de le diffuser en tant qu'OS en mode protégé pour les processeurs du firmware de leur modem sans fil. La filiale de NICTA Open Kernel Labs devint le support et le développement du noyau qu'il a rebaptisé OKL4. Une autre version fut déployée, PikeOS, un clône commercial par SYSGO, certifié pour une utilisation dans l’aéronautique de sécurité critique et également utilisé dans les avions et les trains[5].

Graphe de la famille L4

Quelques concepts de base[modifier | modifier le code]

L'idée principale de L4 étant d'améliorer la vitesse des micronoyaux, plus particulièrement celles concernant les IPC, tout en conservant les concepts des micronoyaux, il a fallu réadapter certains concepts et en introduire d'autres. Nous présenterons ci-dessous les concepts qui ont permis à Liedtke de relever son défi.

Minimalité[modifier | modifier le code]

Les micronoyaux L4 fournissent une API simple, minimale et une abstraction qui couvre la création, l'exécution des threads, la communication inter-processus (IPC) entre threads, l'isolation et la gestion des tâches [6].

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

Ce principe fut le fondement de la conception des noyaux L4[7]. 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[7].

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

Espaces d’adressages[modifier | modifier le code]

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

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[9].

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[9].

Threads et IPC[modifier | modifier le code]

La communication inter-processus par passage de message 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é[10].

Pour communiquer entre des threads possédant des espaces d'adressages différents, la méthode classique consiste à faire transmettre les messages entre threads via le noyau. IPC applique 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[11].

Selon Liedtke, « les performances des communications IPC sont plus importantes ». Il existe deux types d'IPC : les IPC synchrone et asynchrone. Les micronoyaux de première génération ont utilisé L'IPC asynchrone (par exemple Mach). Le noyau garde le message dans un buffer jusqu'à ce que le récepteur soit prêt à recevoir le message ; cela a pour conséquence la double copie du message. C'est de cette manière que Mach à beaucoup perdu en performance. Les micronoyaux de deuxième génération (p. ex L4) ont adopté l'IPC synchrone pour la communication entre les threads. Dans ces communications, le premier communiquant se bloque jusqu'à ce que l'autre soit prêt. Le message est directement copié entre threads ce qui évite une mise en buffer inutile en noyau. L'IPC synchrone satisfait ainsi une implémentation efficace et nécessaire[9].

Interruptions[modifier | modifier le code]

L'abstraction naturelle des interruptions est les communication IPC. Le matériel est considéré comme un ensemble de threads qui ont des identifiants spéciaux et envoient des messages contenant que l'identifiant de l'expéditeur aux threads logiciels qui leurs sont associés. Le thread récepteur vérifie l'identifiant de l'expéditeur du message, si le message est une interruption matériel, alors il est interrompu. 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 vérité, le noyau ignore complètement la sémantique de traitement des interruptions[12].

Les drivers dans l'espace utilisateur[modifier | modifier le code]

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 hardware à travers les mécanismes standard 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ériques comme des serveurs de l'espace utilisateur[13].

Famille du micronoyau L4[modifier | modifier le code]

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

Fiasco[modifier | modifier le code]

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. On dit souvent « L4/Fiasco » pour parler de Fiasco. Ceci met en œuvre la relation entre Fiasco et L4[14].

Un micronoyau fournit les mécanismes inévitables, mais n'applique pas la politique dont les plupart sont implémentés en espace utilisateur. Dans le système L4/Fiasco, il y a un système un environnement L4 (L4Env) qui est un environnement de programmation pour les applications qui devront tourner au-dessus d'un noyau L4/Fiasco[14].

Le modèle de programmation de "L4/Fiasco" est basé sur l'architecture client/serveur. L'ordonnanceur est préemptif de propriété basse, et un ordonnancement de type round-robin entre les threads de même propriété[15].

L4Ka::Pistachio[modifier | modifier le code]

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

Il a été porté sur les architectures suivantes : Alpha (21164, 21264), AMD64 (Opteron 242, Simics), ARM (SA1100, XScale, ARM925T), IA32 (Pentium et plus), IA-64 (Itanium1, Itanium2, Ski), MIPS 64bit (R4000, R5000 (en)), PowerPC 32bit (IBM 750), PowerPC 64bit (Power3, Power4). Il propose un support multiprocesseur.

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

SeL4[modifier | modifier le code]

Le micronoyau seL4 est un membre de la famille 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 dans l'utilisation réelle[17]. C'est un micronoyau de troisième génération et est complètement basé sur un noyau de type L4. Comme L4, il dispose d'abstractions pour les espaces d'adressages virtuels, threads, IPC[18].

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 (à partir ceux réservés au noyau seL4 lui-même)[18].

Les threads sont des entités actives de seL4. En associant un CNode et un espace d'adressage virtuel avec un thread, les politiques dans le niveau utilisateur créent une abstraction de haut niveau comme les processus ou des machines virtuelles [18].

L'IPC est supporté sous deux formes : passage de message synchrone par passage de paramètres (port, destination donc sans bufferisation dans le noyau), et des notifications asynchrones via des paramètres asynchrones (les objets rendez-vous composés d'un seul mot noyau)[18].

Les pilotes de périphériques sont exécutés comme des applications en mode utilisateur qui ont accès aux registres et mémoire des périphériques. soit par mapping du périphérique dans l'espace d'adressage virtuel ou par contrôle des accès au port du périphérique sur les matériels X86. Sel4 fourni des mécanismes pour la réception de notification d'interruption (via IPC asynchrone) et pour l'accusé de réception[18].

Les noyaux seL4 tournent sur ARM et x86. Mais les versions vérifiées de seL4 qui existent actuellement sont pour ARMv6 et ARMv7. Le port sur les plateformes x86 n'est actuellement pas vérifié, mais il existe une version expérimentale de seL4 sur multi-cœurs x86[18].

Projets utilisant L4[modifier | modifier le code]

  • DROPS (Dresden Real-Time Operating System Project), basé sur le micronoyau Fiasco.
  • L4Linux (en), port du noyau Linux sur L4Ka et Fiasco.
  • Port du Hurd sur L4Ka::Pistachio : l'objectif de ce projet est de remplacer le micronoyau sur lequel fonctionne le Hurd. Actuellement, celui-ci tourne sur une version GNU de Mach. Ce projet est encore au stade expérimental.

Références[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

Document utilisé pour la rédaction de l’article : 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,‎ , p. 137-140 (ISBN 978-1-4244-3928-7, DOI 10.1109/ITIME.2009.5236446) Document utilisé pour la rédaction de l’article
  • (en) kevin Elphinstone et Gernot Heiser, « From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels? », ACM,‎ , p. 133-150 (ISBN 978-1-4503-2388-8, DOI 10.1145/2517349.2522720)Document utilisé pour la rédaction de l’article
  • (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,‎ , p. 133 - 136 (ISBN 978-1-4244-3928-7, DOI 10.1109/ITIME.2009.5236445)Document utilisé pour la rédaction de l’article
  • (en) Hironao Takahashi, Kinji Mori et Hafiz Farooq Ahmad, « Efficient I/O intensive multi tenant SaaS system using L4 level cache », IEEE Concurrency,‎ , 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,‎ , p. 175-188 (ISBN 0-89791-632-8, DOI 10.1145/168619.168633)Document utilisé pour la rédaction de l’article
  • (en) Tae-You Lee, Hyung-Rok Seo et Dong-Ryeol Shim, « Fault Isolation Using Stateless Server Model in L4 Microkernel », IEEE, vol. 2,‎ , 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,‎ , p. 512 - 520 (ISBN 0-8186-2865-0, DOI 10.1109/ICDCS.1992.235002)
  • (en) Jochen Liedtke, « On micro-kernel construction », ACM, vol. 29,‎ , p. 237-250 (ISBN 0-89791-715-4, DOI 10.1145/224056.224075)Document utilisé pour la rédaction de l’article
  • (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,‎ , 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,‎ , 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,‎ , 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,‎ , 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,‎ , 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,‎ , 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,‎ , 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 Dr Jamalul-lail Ab. Manan, « Experience with the Implementation of AES256 on L4 Microkernel using DROPS (BID) Environment », IEEE, vol. 3,‎ , p. 1-5 (ISBN 978-1-4244-2327-9, DOI 10.1109/ITSIM.2008.4632027)Document utilisé pour la rédaction de l’article
  • (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,‎ , p. 1-70 (ISSN 0734-2071, DOI 10.1145/2560537)Document utilisé pour la rédaction de l’article

Liens externes[modifier | modifier le code]