[e-lang] Non-local Exits vs Defensive Consistency - MarkM

[Mark Miller]

---------- Forwarded message ----------
From: Mark Miller
Date: Jan 26, 2007 8:25 PM
Subject: Re: VirtualMachineError


On 1/26/07, David Wagner wrote:
> I'm Cc:ing my student Naveen Sastry, who I've also talked with about
> this question.

Hi Naveen!

I'm also sending to David Hopwood, as today's discussion was triggered
by his concerns about exception handling in E. Hi David!

And to Hans Boehm, who has expressed an interest.

> Forbidding 'finally' is pretty devastating and seems out of proportion.
> (I once heard the advice that in well-written code, you may see ten times
> as many 'finally' clauses as 'catch' clauses.  That resonated with me.)

After Tyler sent his message, Alan Karp came up with a less severe proposal:

* Have Joe-E outlaw the catching of Errors.
* Have Joe-E require all try-finally code to follow the following boilerplate:

    try {
        stuff1 // only normal Joe-E restrictions
    } finally {
        try {
            stuff2 // no non-local exit via return, break, continue, or goto
        } catch (Exception ex) {
            throw new Error(ex)
        }
    }

The second restriction prevents a thrown Error being downgraded to a
non-local exit that's not an Error. The first restriction prevents
Joe-E code from recovering from an Error. Taken together, this
prevents Joe-E code in which an Error has been thrown from completing
sequential execution in any way other than by throwing a (possibly
different) Error. But it still allows the writing of the finally
clauses we'd like to write, only with moderate syntactic burden, and
with this burden paid only by finally clauses.


> The solution MarkM had recommended earlier was a VM modification to cause
> the VM to terminate immediately rather than throwing a VirtualMachineError.
> I'm curious to hear what made you reconsider this stance.

We haven't. We'd still like to see such a JSR happen. If it does, at
that time we can alter Joe-E to allow code that it previously forbade.
This would be upwards compatible. The issue is: What do we need to do
to Joe-E code to be defensively consistent before this JSR gets
adopted?



> If you don't like this, there is only one other alternative I've seen that
> I believe to be viable.  The Joe-E verifier would check the following rules:
>
>  1) Any 'catch' clause whose declared type is VirtualMachineError, or
>  a subtype of VirtualMachineError, must have exactly the following body:
>
>     catch (VirtualMachineError e) {
>         java.lang.Runtime.getRuntime().halt(1);
>     }
> [...]
>  2) Any 'catch' clause whose declared type is Error or Throwable
>  (the supertypes of VirtualMachineError, other than Object) must be
>  preceded by a 'catch' clause whose declared type is VirtualMachineError
>  (and thus is of the above form).
>
>  3) Every 'finally' clause must be preceded by a 'catch' clause whose
>  declared type is VirtualMachineError (and thus is of the above form).
>
> Those would be the rules that the Joe-E verifier.  To ease compliance
> with these rules, the Joe-E Eclipse plug-in could provide a refactoring
> tool to add in the needed 'catch' clauses.  You could even imagine that
> if the Joe-E verifier flags your code as violating the above rules, it
> might present you with an option to automatically fix your code by adding
> the needed catch clause (or even to add catch clauses everywhere they are
> needed throughout your project without further confirmation, if you like
> to live dangerously).
>
> Any comments?

I agree that the issue is only critical for VirtualMachineErrors. In
today's discussion, we largely ignored the difference between these
and Errors. Rather, we treated all Errors as non-recoverable.

I think this would work as well, would perhaps be less burdensome than
Tyler's original proposal, but would be more burdensome than Alan's
proposal.

Then there's the issue of how to express non-recovery. Your proposal
does it by calling a static abort routine. Tyler & Alan's does it by
ensuring that the sequential program, if it completes at all,
completes by throwing an Error. The latter is perhaps more flexible
regarding how non-Joe-E framework code (the launching powerbox and/or
concurrency framework) reacts to this expression of non-recoverable
termination. In particular, in an E and/or Waterken context, the
framework has the option of terminating only the offending vat, rather
than the entire JVM process.

Btw, to be safe, we's need to add to the above rules:

* Joe-E code cannot declare and direct subclasses of Throwable, i.e.,
it cannot introduce the possibility of a Throwable that's not an Error
nor an Exception.

--
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM