[bitc-dev] Use Case: GC correctness

[Jonathan S. Shapiro]

Always best to start with one that is driven by current pain. :-)

I recently took over TinyScheme. One change I decided to do was to
introduce a pluggable GC interface so that I could later implement a
copying collector. The problem is to ensure that the implementation
doesn't use any pointer whose address may have changed following
collection.

Here is an attempt to state the problem informally. What I'm after is
suggestions on how one might reason about this property.

1. At the moment the GC procedure is called, there is a set of
   currently outstanding, valid pointers. Some of these are global,
   some local, some are fields of structures.

2. A subset of these are "traceable" pointers -- ones that can be
   reliably identified by the collector and can therefore be updated
   successfully. The rest are not traceable, and therefore should not
   be used after GC returns (i.e. these values are dead).

The goal: demonstrate that if a pointer is non-traceable, it is not used
following GC.


Naively, this appears to be a typestate property. The problem is that it
is a *non-local* typestate property. That is, what we more or less seem
to want is something like the following

  Action on GC-entry:
    forall locations of type ObRef
      location.typestate = pre-gc

then in the middle of GC, update specific type states to post-gc as the
mark-copy pass operates over them.

then change all remaining pointers to typestate 'bad', and show that
globally there is never a reference using a bad pointer.

There are a bunch of pieces of this that I am not sure how to do, but
here are two specific parts that I'm not seeing:

  1. How best to mark the typestates?

  2. How to express that forall constraint, which appears to need to
     query the current system state.


shap