[gclist] Finalization, again

[Nick Barnes]

At 2001-10-04 20:26:41+0000, David Chase writes:
> At 03:38 PM 10/4/2001 -0400, David F. Bacon wrote:
> >the other sensible alternative would be to statically require that finalizer
> >methods execute no unbounded loops or blocking operations.
> 
> Do you know of anyone working seriously on this problem?
> 
> It would also make sense in exception handlers; it would
> be lovely to be able to assert that a thread would, when
> told to go away, actually go away.  The fact that this isn't
> possible (for, say, Java) limits the contexts in which
> you'd actually be willing to download and run code from
> strangers.

Proof-carrying code, Necula et al, addresses exactly this sort of
point.  You need to know that some code (e.g. a downloaded applet) has
certain properties (runs in a given amount of time, doesn't perform
"illegal" accesses, doesn't raise exceptions).  So you require that
the code should come with a proof of these properties.  You can check
the proof in a small finite time.  Generating such a proof is very
much harder(!).

Nick B