From madore@news.ens.fr Path: eleves!not-for-mail From: madore@news.ens.fr (GroTeXdieck) Newsgroups: ens.forum.informatique Subject: Re: libX11.so.6.0 Date: 30 Oct 1998 00:53:15 GMT Lines: 157 Sender: madore@clipper.ens.fr Message-ID: <71b2lr$7hs$1@clipper.ens.fr> References: <717n6d$4uj$1@clipper.ens.fr> <717nlu$5v5$1@clipper.ens.fr> <719igk$25j$1@clipper.ens.fr> <719v36$nlb$1@clipper.ens.fr> <71a3a0$288$1@clipper.ens.fr> NNTP-Posting-Host: clipper.ens.fr Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: clipper.ens.fr 909708795 7740 129.199.129.1 (30 Oct 1998 00:53:15 GMT) X-Complaints-To: forum@clipper.ens.fr NNTP-Posting-Date: 30 Oct 1998 00:53:15 GMT X-Newsreader: Flrn (0.3.0 - 10/98) Xref: eleves ens.forum.informatique:211 Tunes, c'est une invention virtuelle de Faré (man Fare). C'est un système d'exploitation qui n'existe pas mais qui n'est pas non plus impossible. Et ce n'est même pas forcément irréalisable. En revanche, il ne faut surtout pas lire ce que Faré lui-même écrit sur le sujet parce que c'est totalement fumé et incompréhensible. Mais quand il parle il est très clair et très convaincant (à mon avis). Ce qu'on constate, c'est que le meilleur système d'exploitation à l'heure actuelle est Unix, qu'il a trente ans d'âge, et qu'il n'a pas fondamentalement changé depuis ce temps. Et on continue encore à programmer essentiellement en C, qui est un langage de très bas niveau. Tunes est à la fois un langage de programmation et un système d'exploitation, ce dernier étant à un système comme Unix à peu près ce que Scheme ou équivalent est au C. Premier grief envers les systèmes actuels : la notion de fichiers. Sous les systèmes d'exploitations actuels, on peut stocker des données soit en mémoire soit sur disque. Dans le premier cas, le langage de programmation quel qu'il soit sait *assez* bien se débrouiller pour fournir au programmeur une interface pas trop bas niveau (par exemple, on n'a généralement pas à donner des addresses absolues, et, avec un langage comme Scheme ou ML, on a des types puissants et facilement manipulables). Sur les fichiers, en revanche, c'est très merdique. Il faut ouvrir le fichier soi-même, y écrire à la main des données *binaires*, donc se fabriquer soi-même un codage merdique et se faire chier à tester les valeurs de retour et tout ça. C'est pénible. D'ailleurs, pourquoi le disque est-il géré de façon différente de la mémoire. Comme si on devait aussi s'occuper du cache de second niveau, du cache de premier niveau... Tunes abolit donc la différence entre fichiers et variables en mémoire, il ne reste que des ``données''. La mémoire vive n'est qu'un cache de la mémoire totale qui est sur le disque ou même sur le réseau (ou encore obtenue par d'autres moyens). Si on fait un shutdown propre, on n'a pas à tuer les processus, toutes leurs données étant sauvées sur disques, de sorte qu'ils recommenceront à tourner comme si de rien était lors du reboot. Même si on ne fait pas de shutdown propre, Tunes garantit l'intégrité des données dans le sens que ce qu'on récupère au reboot n'est peut-être pas le dernier état de la machine mais c'est au moins un état cohérent. Tunes abolit aussi la différence entre code et données. Dans un langage de haut niveau, le code devient lui aussi donnée de première classe, et peut être passé à des fonctions, être valeur de retour, faire partie d'un tableau, etc. Les fonctions de la bibliothèque, les procédures constituant un programme, et le programme lui-même, sont traités de façon homogène. Ceci facilite la communication entre les programmes. Plutôt que de se présenter comme un bloc monolithique, chaque programme présente de nombreux points d'entrées, de sous-programmes directement appelables par un autre programme. On pourra aussi très facilement écrire des scripts utilisant une fonction d'un programme puis une fonction d'un autre... Au niveau de la sécurité, Tunes est encore plus révolutionnaire. Alors que les OS protégés actuels basent tous leur sécurité sur une composante physique du microprocesseur, la MMU, Tunes procède de manière totalement différente. Avant de pouvoir acquérir le contrôle du processeur, un programme doit prouver, au sens mathématique du terme, qu'il ne va pas compromettre la sécurité du système. Cette preuve, en vertu de l'isomorphisme de Curry-Howard, est fournie sous la forme d'un objet dont le système calcule le type (l'assertion prouvée) et vérifie qu'il lui convient. Si le programme est écrit dans le langage natif du système, la preuve est par induction, et elle est immédiate (rien dans le langage ne peut compromettre le système), donc elle n'a pas à être fournie, c'est le système (ou plus précisément les spécifications du langage) qui s'en charge. Si le programme est écrit par exemple en code machine (ce qui est contraire à la philosophie Tunes), alors on peut utiliser la MMU grâce à un axiome qui décrit son comportement. La notion de preuves est généralisée à autre chose que la sécurité. Il est possible lors de l'écriture d'un programme de fournir des spécifications et simultanément de les prouver (du genre, cette variable est toujours positive, et la preuve pourrait consister à observer qu'elle l'est à sa création et que la seule opération effectuée dessus consiste à l'incrémenter), et le compilateur vérifie la correction des preuves. Au niveau de la protection des données, par exemple, ça donne : si je veux accéder aux données de Monsieur X, il faut que je prouve au système l'assertion je_peux_accéder_aux_données_de_X (un type opaque, disons jpaaddX), moyennant quoi le système sera prêt à me les retourner grâce à une fonction du type jpaaddX->données, où données représente en fait le contexte (``répertoire'') dans lequel sont ces données. Si je suis X, alors j'ai un axiome de type jpaaddX, qui m'est donné par le programme de login. Si je suis Y, X peut m'autoriser à accéder à ses données en fournissant une donnée du type je_suis_Y->jpaaddX (qu'il peut démontrer puisque pour lui jpaaddX est un axiome). C'est donc un système infiniment versatile puisqu'une condition arbitrairement complexe, voire un programme complet, peut servir à autoriser ou non l'accès à mes données. L'administrateur système dispose, lui, de l'axiome 0=1 (``faux''), qui est extrêmement puissant puisqu'il permet de tout démontrer. Bien entendu, preuves, types, contextes, tout cela sont des objets de première classe, et peuvent être passés comme paramètres à des programmes, être retournés par des fonctions, etc. La spécification formelle des programmes permet à Tunes de faire de la régénération automatique de programmes. Autrement dit, quand deux programmes communiquent et que vous changez la version de l'un, Tunes est capable d'adapter automatiquement l'autre à cette nouvelle version (si tant est que tout est correctement spécifié, bien sûr). Une autre propriété très importante de Tunes, c'est celle de la réflexivité. Ce n'est pas très facile à expliquer. Dans l'isomorphisme de Curry-Howard, c'est l'équivalent du théorème de déduction, ce que Hofstadter appelle une ``Fantasy'' dans Gödel, Escher, Bach. Un programme comme dosemu montre que Unix est capable de réfléchir MS-DOS (certes approximativement et incomplètement). Il offre une machine virtuel (grâce aux capacités du 386) que le DOS ``croit'' être un ordinateur complet avec rien à l'extérieur. Unix, cependant, n'est pas capable (du moins, pas simplement) de réfléchir Unix. Je ne peux pas, sous Unix, lancer un Unix avec sa propre hiérarchie de fichiers, ses propres processus et tout et tout. Ce qui en est le plus proche, c'est chroot(), mais ce n'est pas encore ça (par exemple, les processus sont partagés, et le root d'un Unix ``virtuel'' dans un chroot() peut faire des dégâts à l'Unix ``réel''). Donc Unix n'est pas réflexif. Le serveur Xnest montre que X possède d'assez bonnes propriétés de réflexivité. Tunes l'est complètement : tout utilisateur de Tunes peut créer un ``Tunes virtuel'', une ``Fantaisie'', sur laquelle il possède l'axiome 0=1, mais qui ne peut pas réagir sur le Tunes initial. Enfin, Tunes est pensé pour le parallélisme. On peut l'utiliser sur des machines multiprocesseurs, ou, mieux encore, sur un réseau de plusieurs machines. La communication entre les machines est aussi aisée qu'entre les programmes et se fait suivant la même philosophie. Tout le réseau se comporte finalement comme une seule machine. Autre chose : il n'y a pas de compilation séparée. Le système compile le programme tout seul quand c'est nécessaire. Le binaire, c'est une forme de cache, et comme tout cache, Tunes cherche à le rendre transparent. Tunes, enfin, n'a pas de noyau. Tous les processus sont égaux devant la machine. Quand on a besoin d'un gestionnaire de périphérique, on l'appelle comme un programme - une fonction - ordinaire. En pratique, Tunes ressemble plus à la boucle d'évaluation d'un langage comme Scheme, ou bien à un débuggueur comme gdb (on peut aller farfouiller dans des programmes qui tournent, les modifier, etc.), ou encore à la HP48 qui du point de vue du système d'exploitation est finalement assez proche de Tunes. On peut imaginer une jolie interface graphique avec des petites icônes qui représentent les données, un dessin différent pour chaque sorte (données, code, type, preuve, etc. - même si la distinction n'a pas tant de sens). Bref, Tunes a toutes les qualités. Il a cependant un gros défaut : il n'existe pas. Pour le moment, aussi furieux que je sois que quelque chose d'aussi évident n'ait pas encore été écrit, je dois me consoler avec ce qu'il y a de plus proche pour le moment : une sucette.