[e-lang] Non-local Exits vs Defensive Consistency - David Wagner

[Mark Miller]

---------- Forwarded message ----------
From: David Wagner
Date: Jan 26, 2007 5:35 PM
Subject: Re: VirtualMachineError


I'm Cc:ing my student Naveen Sastry, who I've also talked with about
this question.

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.)

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.

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);
    }

 Note: I didn't use System.exit(), because System.exit() will call
 shutdown hooks and may run finalizers upon exit.  We might be able
 to use taming to prevent Joe-E from registering shutdown hooks or
 enabling run-finalizers-on-exit, but we don't know whether the class
 libraries might do one of those things.

 Note: This assumes that Runtime.getRuntime() always returns non-null
 and that halt() always terminates.  Strictly speaking, halt() might
 throw a security exception if there is a security manager enabled and
 its checkExit() method forbids calling halt(), but for pure Joe-E
 code, I don't think we have to worry about that.  If we were really
 worried, we could require the clause to take the following form:

    catch (VirtualMachineError e) {
        while (true) {
            java.lang.Runtime.getRuntime().halt(1);
        }
    }

 but maybe this is overkill and more onerous on the programmer than
 necessary.

 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?

-- David