looping in unwind-protect cleanups

[David A. Moon <Moon@STONY-BROOK.SCRC.Symbolics.COM>]

    Date: Wed, 13 May 87 20:03:04 PDT
    From: edsel!bhopal!jonl@navajo.stanford.edu (Jon L White)

    ...you use the phrase "... this is not a valid Common Lisp program."  
    I have trouble with that characterization, since it seems to imply 
    some mechanically checkable property of programs.

I didn't mean to imply that.

    ...I think you see how this could be extended to produce an example that could
    not be mechanically proven invalid by the UWP-non-local-exit criterion,
    even though it would get into the disastrous loop.

Sure.  If you give me a few hours, I will mail you examples of programs
in Common Lisp, Ada, and Basic the determination of whose validity in
their respective languages is equivalent to the halting problem.  The
basic plan is to write a program where it cannot be mechanically proven
whether an array subscript is out of bounds.

    ....Implementationally, it would seem to require at most:
      (1) For each UWP frame, the "cleanup forms" have an associated lock ....

This is rather overcomplicated, so let me tell you how the versions of
Symbolics systems that implement my proposed checking do it.  None of
these are released yet.  This is from memory, I didn't write the code.

1. Every catch (including ones generated internally by tagbody and block
when nonlocal exits via go, return, or return-from are happening) contains
a validity bit, which is initially 1.

2. When throw plans to throw past a catch, it sets its validity bit to 0.
This happens after throw finds the target catch (since Common Lisp says if
there is no matching catch, the error is signalled in the dynamic environment
of the throw), and before throw starts removing state from the stack and
evaluating cleanup forms.  Here throw includes nonlocal go, return, and
return-from along with certain debugger commands.

3. An attempt to throw to a catch whose validity bit is 0 signals an error
that isn't caught by IGNORE-ERRORS.

4. The error in 3 is implemented by the Common Lisp function BREAK.

5. When throw evaluates an unwind-protect cleanup form, it first removes
it from the list of such forms, so that if you throw again it won't be
evaluated again.  (I'm pretty sure that a close reading of CLtL shows
that this is required.)

Note that the only data structure or dynamic state is one bit per catch,
the only overhead is in throw, and the error signalling is implemented
with an existing Common Lisp facility.