[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 ...