Doing it better 1998-10-18
###

> We may as well do so, and admit to every computer scientist's hubris: we
> think We Can Do It Better, and build the ultimate computer system. I'm
> particularly interested in doing it from the ground up, starting with a VM
> that is essentially a suitable calculus with an escape hatch ("execute
> this") and building from there. My idea is that the very barest version
> should be a few pages of C (to bootstrap it; thereafter a couple of kb of
> virtual/machine code) containing enough of a user interface to allow the
> entire system to be built up within itself in an exponentially
> accelerating manner.
>
> I think we should arrange regular but infrequent times to talk about
> aspects of the ultimate project, which should by rights be called Project
> Omega, but that's terribly clichéd, so let's call it...er...something
> else. Suggestions? Project Tau (last letter of the Hebrew alphabet);
> Project One (last letter of the binary alphabet); Project Zero (first
> ditto, simplicity)...I think we can be more involved.
>
> Anyway, it'd be nice if we could (slowly) make progress...even if we end
> up doing things and throwing them away. (I saw a group called "Programmers
> Without Deadlines" which sums up the spirit.)

Absolutely. VMs, Process Algebrae, Midas, Slave processors, no more
Acorns, Bill Gates, Your jammy year, ... it all points in the same
direction.

I've been thinking. Funnily enough.

If we could make an assembler which simultaneously checked a proof about
the code's behaviour (which is trivial compared to creating one), we could
make a computer which doesn't crash. I know this is not a new idea. Surely
it's a good one, though.

It needn't make the thing a bugger to code, either. For example, a Java
compiler can easily create a proof about any legal Java program. C would
be harder, but I don't really want people to use C. Any interpreted
language would be fine.

The next question is how to go about it. Briefly, here is a possible
scheme:

We invent a datatype called a fact. It obeys ML-like pattern matching. We
invent a directive ASSERT which returns a fact, after assembling a check
that the fact is true. The way in which an ASSERT is assembled could be
defined when the fact operators are declared...?

_Amazing! I've been working on this last week (Nov 2004)! [Alistair|A]_

A normal instruction is a macro which takes a few operands and
destinations, and also takes facts about them. It assembles the
instruction and returns facts about the state after executing the
instruction.

There are also dummy instructions which assemble nothing, but which
perform pure reasoning on facts. For example, a=>b and b=>c could be
combined to form a=>c. Another example is an instruction which weakens a
fact. For example, at the label of a loop, you might want to weaken x=10
to x>0.

Explicit induction would not be necessary. Inductive proofs can be checked
by unifying the facts at a branch and its target label. For example, to
prove that x is always in [1..10] at PRINT x in the following program:

x:=10
{x=10}
Weaken
{0<x<=10}
.loop
PRINT x
x:=x-1
{0<=x<10}
CMP x,#0
{eq and x=0 or ne and 0<x<10}
Weaken
{eq and x=0 or ne and 0<x<=10}
BNE loop
{eq and x=0}

...it is sufficient to observe that the the facts at the branch and at the
label match.

This doesn't prove that the program terminates, of course. It only proves
facts about the state of the computer at intermediate points in the
program.

This sort of proof can ensure that programs only access certain areas of
memory, that they always compute the correct answer, that they respect the
structure of a heap, and so on. It is much stronger than an ordinary
type-checking scheme. It is also much more flexible: you can do all the
nasty bit-twiddling tricks that machine-code allows, and still be
confident that the program works. It is also much more readable, or could
be.

The next step would be to get the assembler to assemble itself. This is
only a consistency check: It is in principle possible to invent an
ingenious bug which prevents its own detection. There's no way around
this. However, it reduces the assumptions from 'the instruction set fits
its specification and the assembler works'.


One problem with this idea is it precludes running Linux on it, as it it
written in C. A verified Linux wouldn't be all that bad an idea, though...


Anyway.

The next step is to write one or two virtual processors, and implement
them for every platform, including each other.

Then we make ourselves a HAL. Something which assumes PCI cards is
probably sufficient. We shouldn't rule out other options. I don't think we
need to worry about memory protection too much: we can handle protection
at the virtual processor level. Timers and interrupts, on the other hand,
are necessary.

The next level is threads, messages, and so on. At this stage we should
probably write all the device drivers, as they can benefit from existing
outside the threads model.

At this point, we consider ourselves to have a BIOS for a single processor
single memory single keyboard, single screen machine. Essentially, the
BIOS of a single-user workstation.

On top of this we build an I.P. stack. We should use I.P. because
everybody else does, and we might want them to forward our messages for
us. However, we shouldn't rule out other options.

On top of this we build some sort of model of distributed computation. The
one I played with for my Diploma project might be good.

Unless we have done our verification thoroughly, the system is probably
becoming a little unstable at this point, because there are so many things
which the user is not allowed to do but which he is not prevented from
doing. We therefore write a few more virtual processors, which translate
themselves into the existing virtual or physical languages. A range of
translators is never a bad idea.

Then we need a naming model. This should be universal. It should name
machines, devices, languages, fonts, files, ... the works. It should
provide a uniform model for configuring things, so that any changes are
reported to the things configured. We should not regard re-booting as a
viable option. We should also anticipate revisions, especially backward
compatible ones.

Then we start thinking about a filing system. Hierarchical is necessary
only for supporting ports from Unix and things. Fully relational is buch
better. I don't think the distinction between disk and memory is a useful
one. However, knowledge about devices is important, particularly the
difference between persistent ones and volatile ones. This can be
incorporated a bit like filetypes and access permissions.

Eventually, we have a nice uniform system. It is a sort of distributed
BIOS.

Then we think about resource allocation. We have reached a point where the
resources are available, but that is only half the work. I suggest a
market economy might be a good model. We can charge virtual credits for
bandwidth, memory, time and so on, and pay every user a social security
benefit, and tax their savings.

Then we hack it to pieces in an attempt to make it user-friendly. We
invent shells, window managers, font servers, logins, background tasks,
internationalisation, filetypes, etc.

Then we make compilers, telnet clients, web browsers, Acorn Emulators,
games, and so on. This phase is blurred with the previous one.

During these last phases, it is crucial to maintain an emphasis on
managing complexity. At every stage, everything must be accounted.
Dependencies of code, version numbers, memory requirements, device
requirements, bandwidth requirements, ... all information must be
available to the user through a uniform interface.



As you see, the task is a big one. It can only be managed using multiple
levels of complexity. This is my overall plan.

Comments?

Alistair