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.