[ENS]
[ENS students]
[David Madore]
[Mathematics]
[Computer science]
[Programs]
[Linux]
[Literature]
This is my presentation of the TUNES project (me = David Madore). Faré (François-René Rideau), who is the main instigator and coordinator of the Tunes project, has written a Tunes presentation page already. But though Faré is very good at explaining things orally (my humble opinion, of course), nothing he says is comprehensible when he starts writing things down (my humble opinion again, of course). Upon reading the initial Tunes page, I did not understand at all what the whole thing was about, but since Faré is a very intelligent person (my humble opinion, once again), I believed there must be something interesting behind it. So I had him explain it to me, and I consequently wrote this page, which hopefully will prevent others from having the same misconceptions about Tunes as I had.
Tunes stands for ``Tunes is a Useful, Not Expedient, System''.
To put it simply, Tunes is the Ultimate Operating System. But in a way, Tunes is much more than an OS, and also much less (sorry for the annoying use of rhetoric). It uses (or rather, will use - or rather, would use) notions from theoretical computer science to correct some of the failures and shortcomings of present-day operating systems.
Essentially, that they are written, and force programmers to write, at such a terribly low level. The C programming language has imposed itself as a de facto standard for OS development, but it is little more than a portable assembler, and there is no reason why the operating system, apart from the device drivers, should be written in a low-level language. Besides, the C programming language has other disadvantages, such as ill-defined semantics, which prevent (or make more difficult) the use of such techniques from theoretical computer science as program proving or metaprogramming, from which OS design would stand to gain much.
Take a concrete example, to be more specific: with all current operating systems, in order to save some data on disk, one must choose a file name, open the file, write the data (and explicitly take care of the conversion, whether to a text or binary form), close the file, and all the time worry about possible error conditions and do the error handling by oneself. Reading the data from the disk is even worse as one must also verify that the data has not been corrupted. When reading a large file one has the painful choice between loading the file in memory, mmap()ing it, performing read()s on demand, or implementing yet another cache level. Now the whole situation is absurd: there is no conceptual distinction between memory and disk - both are used to store information, and the only valid difference is that the memory is faster so it acts with respect to the disk as a cache acts with respect to memory. Now a programmer will not usually choose to control the cache explicitely so the same should be true of the memory with respect to the disk: both should be accessible as an (essentially infinite) storage medium for data.
In the first place, Tunes places no arbitrary distinction between variables and files: the programmer sees all data as (typed) variables, and the user as files. Similarily, no arbitrary distinction is made between functions and programs. The ``contexts'' of high-level functional languages replace directories. Moreover, Tunes places even no arbitrary distinction between data and code, since functions themselves are considered first-class variables, like in functional languages, in the sense that they can be passed as parameters to other functions and can be operated upon exactly like any other piece of data.
Naturally, with this blurring of distinction between disk and memory comes the notion of persistent data storage: the programmer does not have to explicitely require that a variable be stored in persistent fashion (on disk, traditionally), this is done automatically at regular intervals, so that a user abruptly shutting the machine down will incur no more than a few minutes of work lost.
To compare Tunes with an already existent entity, it is better not to look at an operating system, but the main loop of a high-level functional language such as Scheme or Caml: the user can access variables, run functions/programs directly, and sees all data in a uniform fashion. Or one can compare Tunes with a debugger: it naturally includes the capacities of a debugger such as inspection of data, including the wonderful capabilities that gdb has under Hurd (dynamic debugging of running programs, and so on).
Of course, one can imagine a cool graphical interface also, not just the toplevel loop of a language interpreter. For example, one could have it look like a stack of variables. Perhaps the best image, as Faré has suggested, is that of the HP28/48 calculator, which is indeed like Tunes in some ways (the OS is a programming language, variables and files are the same thing, and directories appear as contexts of a sort).
No. There are many other concepts from theoretical computer science that have yet to make their way into actual computer tech and practice, and which the Tunes project could help develop. One important one is the notion of proofs of programs, which is what the security of the Tunes system is based on. In a traditional OS, system security is based on special hardware (a secure Memory Management Unit) built inside the processor. With Tunes, on the other hand, security is based on proofs: to put it shortly, a program will be allowed to take control of the machine provided it can prove that it will not endanger system security. This proof can be done in several ways: if the program was written in the Tunes native high level language, the proof may be trivial (it is impossible to endanger system security from that language - and the compilation is performed by the OS so that the binary cannot be corrupted); or the proof may rely on the special hardware within the chip if it is present; or it may be stated as an axiom by the system administrator. In general, the proof will be made by presenting an invariant and showing that the invariant is preserved by every operation made by the program.
So each program comes with specifications, and the role of the operating system is to check that it matches these specifications. One such secification is the type - and in fact for theoretical reasons all specification verifications amount to a type checking (this has to do with the Curry-Howard isomorphism). Incidentally, this idea of automating the verification of the program against its specs is a way of eliminating many bugs! (Not all of them unfortunately, because the specs can always be either too loose to trap the bugs or too rigid and themselves contain bugs.)
We can go even further than that and have automated code regeneration based on the specs. Concretely, this means that when one changes the version of one program in such a way as to possibly break another program that depends on it (something that I find happens all the time), the system is capable of automatically rewriting the program to work with the new version of the other program!
Does this sound like sci-fi? In a way, it is - but then any kind of progress is sci-fi until it has been made real. However, the theoretical notions behind program proving are well explored. I would advise those interested in this idea to try out the Coq program available at the INRIA: it works.
Since it doesn't exist for the moment, I can name all the features I want, can I not? :-)
Seriously, there are some more things that would naturally come with Tunes. The way things are done currently, each program comes with a certain set of functionalities, and those can be invoked only by the user, by performing certain GUI actions, not by other programs. Unless, of course, the program is actually a library, in which case the reverse is true. Thus, programs currently do not really communicate with each other except insofar as they avoid treading on each other's data. Tunes abolishes the difference between programs and libraries: each program is a set of functions, together with hooks to make those functions visible to the user. But the functions might also be called from other programs. This system also makes it possible for the user to write simple batch programs (scripts) which can call on the capabilities of any program. In particular, it is not necessary for a program to explicitely include an extensibility language (macro language, scripting language, etc), since Tunes will be the common language for all programs.
Another important feature of Tunes is reflexivity. Consider the DOS emulator on Linux (or any such system) to start with: it ``reflects'' DOS under Linux, through the use of the Intel 386 Virtual mode. Now is Linux capable of running a Linux emulator, in other words of reflecting itself? It isn't, because the Intel 386 Virtual mode is only capable of virtualizing (reflecting) real mode. It would be possible, however, to use a roundabout way, by writing an Intel 386 emulator, that is, reflecting the Intel chip under Linux, and then running Linux on that virtual Intel chip (but that would be slow). Now Tunes is capable of reflecting itself at a totally abstract level, that is, without need of any special properties of the hardware on which it is running, and without even needing to know what hardware it actually is. It is this property that is called reflexivity. Faré (François-René Rideau) has written a lot about reflexivity and its importance.
There is an existent version 0.0.0.35 of Tunes - it doesn't even compile, of course. My opinion, however, is that these files are a mess and we had better start anew, from scratch. And not write anything until we can work out precise semantics for the programming languages involved in the system.
I believe (though Faré disagrees) the starting point for Tunes should be Hurd+Guile. The Guile project implements many ideas that are central to Tunes, and is a very good starting point. And Hurd, with its translator system, makes it possible to put peripheral access in the system at fairly little cost.
[ENS]
[ENS students]
[David Madore]
[Mathematics]
[Computer science]
[Programs]
[Linux]
[Literature]