[gclist] gc interface

[Daniel C. Wang]

boehm.PARC@xerox.com writes:
> Re: formal methods for meta GC:
> 
> It's clear that formal methods would need to be part of the answer.  But it
> still seems to me you're embarking on a very ambitious program.  I don't know
> of any exisitng performance-competitive GC that has been formally verified.
> The high-level algorithms often have at lerast 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.
> 

{stuff deleted}

Just thought, I'd mention this to the rest of the list. It's been on my list
of papers to read sometime in the future, but it seems relevant since we're
on the topic. I haven't had time to do anything but skim it, but the
biblography seems useful if nothing else.

A Larch Specification of Copying Garbage Collection, CMU-CS-92-219,
              December 1992.

ftp://reports.adm.cs.cmu.edu/usr/anon/1992/CMU-CS-92-219.ps

(* Larch is an abstract specification langauge that also has a
implementation langauge specific interface. Currently larch has language
specific interfaces for C, C++, and Modula-3. The above paper is a
specification for a gc written in C *)