[gclist] meta gc (was: gc interface)

[Francois-Rene Rideau]

Hans Boehm said:

> Re: formal methods for meta GC:
>
> It's clear that formal methods would need to be part of the answer.
   Formal methods need be the part of the answer
to every computing problem where reliability has any meaning
(that is, all computing problems).

> But it still seems to me you're embarking on a very ambitious program.
   Seems to me, too, and to everyone, which is (partly) why
I can't seem to find anyone to home my projects.

> I don't know of any exisitng performance-competitive GC
> that has been formally verified.
   Well, isn't Damien Doligez' GC competitive ?
His thesis was to build such a GC and prove it
[I shamefully didn't read it yet].
See around www.inria.fr and the cristal project that
brought us Caml-Light...

> The high-level algorithms often have at least an informal correctness proof,
> and that should certainly be the case.

> But there tends to be a big gap between
> those proofs and the implementation.

> And the implementation often lives on an
> OS interface that has a poorly-written, very informal specification.
> And the implementation is ceratinly not formally verified.
   Which again is why existing OSes should *eventually* be thrown
down the garbage bin together with C, C++ and all the crap,
and replaced by ones that have been formally verified,
written in and for languages that allow formal verification.
Of course, until such OSes emerge, C, C++ and POSIX are very useful;
but people should stop investing so much in these,
and spend their money much more usefully at developping formal methods.

> To make life harder, a lot of the facts that are relevant for picking a GC
> (e.g. object lifetimes, data structure shapes) are very global in nature,
> and tend to be hard to infer automatically.
   Which again is why the manual method for building GC is not
adapted to make the most out of computer software,
and why it *is* worth to spend a few years developping a
computing system in which we can build a meta-GC,
even though it may be used only for such a meta-GC
(which hopefully would not be the case),
as it'll then do in a few weeks what takes year to do currently.

> That's especially true if you don't
> have complete information about the program, due to separate compilation,
> third-party libraries, etc.
   Well, to me, this means that the computing system that should emerge
should not be limited to a particular purpose,
but be as widespread as possible (i.e. free or mostly free),
be able to express just any information that users may
want to require or provide,
and be such that efficient precompiled modules be possible.
   All these are doable, and have been done already,
as separate features of various software;
now is the time to gather them in a same system.

--    ,        	                                ,           _ v    ~  ^  --
-- Fare -- rideau@clipper.ens.fr -- Francois-Rene Rideau -- +)ang-Vu Ban --
--                                      '                   / .          --
Join the TUNES project for a computing system based on computing freedom !
		   TUNES is a Useful, Not Expedient System
WWW page at URL: "http://www.eleves.ens.fr:8080/home/rideau/Tunes/"