[gclist] Re: formal methods

[Mario Wolczko]

I just wanted to throw in a plug to my paper of several years ago
which describes a variety of GC techniques formally.  

	@incollection{Wolczko89:gc,
		author	    =	"Mario I. Wolczko",
		title	    =	"Garbage Collection",
		booktitle   =	"Case Studies in Systematic Software
				 Development",
		publisher   =	"Prentice-Hall International",
		year	    =	1990,
		editor	    =	"Cliff B. Jones and Roger C. F. Shaw",
		chapter	    =	8,
		pages	    =	"211-233"
	}

The paper contains descriptions of mark-sweep, ref counting, ref
counting with a free stack, deferred ref counting, incremental mark-sweep,
and generation scavenging, all done in VDM.

I'd agree that we are very, very far from formally proving real GC
systems are correct.

-Mario

Sun Microsystems Labs., 2550 Garcia Ave, M/S UMTV 29-116, Mountain View,
CA 94043, U.S.A.   tel: 415 336 6022, fax: 415 969 7269.

Statements are mine alone, not Sun's.