[gclist] meta gc (was: gc interface)

boehm.PARC@xerox.com boehm.PARC@xerox.com
Mon, 25 Mar 1996 09:29:08 PST


Francois-Rene Rideau said:

"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]."

I haven't seen the thesis itself either.  As far as I know, his GC is quite
competitive.  But the POPL '94 paper by Doligez and Gonthier said:

"A "proof" of a garbage collection algorithm is never a proof of an actual
implementation of that algorithm; it is a proof of some mathematical model that
conveys the essential ideas of the algorithm."

and later

"We purport to provide a proof that does provide for all the details of the
actual implementation ..., but that remains abstract enough to be tractable."

"The formalism we chose is a cross between Algol, UNITY, and TLA."

The actual algorithm model they use is about 2.5 pages in the Proceedings.
This is quite detailed compared to a lot of other work along these lines, but
certainly much shorter, and much higher level, than our collector
implementation, and presumably than his.  It's also above the level where
collector/OS interactions, or tweaks to reduce syncronization overhead are
likely to show up.

Hans
Standard disclaimer ...