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. L'idée générale de L4 est résumée ainsi 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êcherait l'implémentation de la fonctionnalité requise par le système[1].

Motivations[modifier | modifier le code]

Les micro-noyaux 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 à base de noyau monolithique et ceux à base de micronoyaux ont deux différents styles du design de système d'exploitation. Les SE avec les noyaux monolithiques mettent l'accent sur la haute performance et les micronoyaux plus sur la sécurité et la stabilité. D'abord, les système d'exploitation à base de micro-noyaux sont lents, l'efficacité n'est 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 commencer à développer L3 puis L4. Le principe fondamental étant : « un concept est permis dans le noyau seulement quand il ne peut pas être implémenté dans l'espace utilisateur ». Le noyau fournit uniquement les fonctions inévitables telles que les communications, le mapping et ainsi de suite, et impose les politiques. Un micronoyau ne fait aucun réel travail[3].

Histoire[modifier | modifier le code]

Il y a 20 ans, John Liedtke a démontré avec son noyau L4 que les communications IPC des micronoyaux pouvaient être 10 à 20 fois plus rapide que les micronoyaux sur le marché à cette époque[4]. L4 a été développé à partir d'une version antérieure appelé L3, développé par John Liedtke dans le debut des année 1980 sur les plateformes i386. Il a été commercialement déployé sur quelques milliers d'installation (principalement les écoles). Comme tous les micronoyaux à 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, et il utilise pour la première fois le nom "L4" avec l'ABI V2 (Application Binary Interface) déjà dans le communauté depuis 1995. Il a été implémenté complètement en assembleur sur les ordinateurs i486 très tôt portés sur les Pentium [5].

Ce travail initial a déclenché une évolution de 20 ans avec des multiples révisions des ABI et des implémentations à partir de zéro. Celle-ci a commencé par la ré-implémentation de l'ABI Dresden et UNSW sur 64 bits sur les processeurs Alpha et MIPS, ces derniers ont implémenté toutes les longues opération en C. Ces deux noyaux ont atteint une performances des IPC en dessous de la microsecondes et étaient open-source. Le noyau UNSW Alpha était le premier noyau L4 multi-processeur[5].

Liedtke qui avait quitté GMD pour IBM Watson, a apporté son expérience dans l'implémentation d'une ABI qui sera connu 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 Dresden à implémenter une nouvelle version à partir de zéro appelé Fiasco en référence à leur mauvaise expérience en essayant de traiter les questions de propriété intellectuelle[5].

Fiasco est la première version du noyau L4 complètement écrit en langage de haut niveau (C++) et la plus vielle version du code de base des noyaux L4 encore massivement maintenu. Il a été la premier noyau L4 qui a été commercialisé de manière significative (estime plus de 100000 ventes)[5].

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

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

À la NICTA, ils ont tout de suite ré-ciblés pour l'utiliser dans des systèmes embarqués qui avaient des contraintes de ressources. Ceci sera la conséquence d'un fork de Psitachio qui sera appelé NICTA::Pistachio-embedded ("L4-embarqué"). Il a été massivement commercialisé quand Qualcomm a décidé de comme un OS en mode protégé pour les processeurs du firmware de leur modem sans fil. La filiale de NICTA Open Kernel Labs devient 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 déployés dans les avions et les trains[5].

Graphe de la famille L4

Quelques concepts de base[modifier | modifier le code]

Minimalité[modifier | modifier le code]

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

Les principaux moteurs de conception de Liedtke étaient la minimalité et la performance de l'IPC avec 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 bouger en dehors du noyau empêcherait la mise en œuvre d'une fonctionnalité requise par le système [7].

Ce principe a été le fondement de la conception des noyaux L4[7]. Mais selon Kevin Elphinstone et Gernot Heiser, aucun concepteur de micro-noyau ne peut affirmer avoir créé un micronoyau pur dans le strict respect du principe de minimalité. Comme exemple, ils ont tous un ordonnanceur dans le noyau qui met en œuvre une politique d'ordonnancement particulière. A cette date selon eux, personne n'avait un micronoyau dans lequel toute la politique planification est déléguée dans l'espace utilisateur sans imposer de coûts énormes[7].

Difference entre la taille d'unnoyau 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 le marque 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 qui sont directement accessibles par un thread. L'espace d'adressage dans L4 peut être construit récursivement. Un thread peut mapper des parties communes de son espace d'adressage dans celui d'un autre thread et peut 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é, sécurité et la scalabilité[10].

Pour communiquer entre threads qui ont des espaces d'adressages différents, la méthode classique est de passer des messages entre threads par le noyau. IPC applique toujours un certains accord entre les deux parties: l'expéditeur décide d'envoyer des informations et détermine son contenu et le récepteur détermine s'il est disposé de recevoir des informations et 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: IPC synchrone et asynchrone. Les micronoyaux de première génération ont utilisé L'IPC asynchrone ( p.ex Mach). Le noyau garde le message dans un buffer jusqu'à ce que le récepteur soit prêt à recevoir le message, ceci à 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 copie directement entre threads et pas besoin de mise en buffer dans le noyau. L'IPC synchrone satisfait l'implémentation efficace 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 on des identifiant de threads 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 le mécanismes standard IPC. Dans la philosophie des micronoyaux L4, ils ne doivent jamais être intégré dans le micronoyau. Les interruptions entrantes sont transformés 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]

Il existe plusieurs implémentations du micronoyau L4 : 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é pas l'équipe Fiasco à de l'université technique de Dresden 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 fournissent les les mécanismes inévitable , 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), 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é fortes tout en conservant la haute-performance qui est d'usage dans la famille L4 et considéré comme essentiel 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é par manipulation explicite de la mémoire virtuelle connexe aux objets noyaux: chemin des pages, table des pages ... Ils n'ont pas de structure de base définie ( à partr ceux réservé 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 des 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 notification 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érique. 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 version 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].

OKL4[modifier | modifier le code]

²

Projets utilisant L4[modifier | modifier le code]

  • DROPS (Dresden Real-Time Operating System Project), basé sur le micronoyau Fiasco.
  • L4Linux, 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]

Modèle:Legende plume

  • (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) 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,‎ novembre 2013, 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,‎ 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)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,‎ 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)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,‎ 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 Dr 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)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,‎ février 2014, 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]