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

[Mark Miller]

---------- Forwarded message ----------
From: David Wagner <daw at cs.berkeley.edu>
Date: Jan 27, 2007 7:13 AM
Subject: Re: VirtualMachineError

Thanks for the analysis.  Interesting points.

Let me raise a few potential concerns with Alan's proposal.  I'm not
sure whether these are actually problematic, but I'd be interested to
hear people's thoughts on them.

1) Alan's proposal prohibits catching Error or Throwable.  Will this
restrict expressivity?  Example: When calling a method on an object in
another trust boundary, I had been imagining that one common idiom might
be something like:

    try {
        untrusted.m(...);
    } catch (Throwable t) { ... }

to ensure that the untrusted object cannot terminate your execution
partway through by throwing an exception.  Is there an argument that
we don't need to do this? Does it suffice to rewrite this as follows?

    try {
        untrusted.m(...);
    } catch (Exception t) { ... }

This might be ok, but I'd mostly like to hear someone tell me that
it is ok. :-)

For instance, here is one not-so-obvious but I think minor issue: taming.
With Alan's proposal, we have to know that no Java class libraries will
ever catch and handle Error or any subtype thereof.  If some class library
does catch and handle, say, FooError (where FooError is some subtype of
Error), then Joe-E code might call that class library, which might in
turn call other Joe-E code, and now the guarantees about Errors being
unrecoverable can be violated.  This may make taming more challenging.
That said, we already have this problem either way: if we only want
VirtualMachineErrors to be unrecoverable, we have to make sure that
Java class library code does not catch and handle Throwable, Error,
VirtualMachineError, or any subtype of VirtualMachineError, or else is
tamed awaay; but if we want all Errors to be unrecoverable, we also need
to make sure that Java class library code does not catch and handle any
subtype of Error, either.

2) I'm curious about the consequences of baking into the language
that Errors are unhandle-able by Joe-E code (they can only be caught
and re-thrown).  This does seem to more or less match Java's intent
behind Error, but I wonder whether there are some cases where Joe-E
applications might reasonably want to catch Error.  I don't have any
particular cases in mind where this would be a problem; just wanted
to check.  This is another case where I'd mostly just like someone to
tell me that this seems ok. :-)

3) Is Alan's proposal enough?  What about this code?

    public static void f(PrintStream p) {
        int x;
        try {
            x = 0;
            untrusted.m();
            x = 1;
        } finally {
            try {
                p.println(x);
            } catch (Exception ex) {
                throw new Error(ex);
            }
        }
    }

Note that this code provides access to non-determinism.  Of course,
we can replace "p.println(x)" by calls to other Joe-E code, which means
that Joe-E code has the ability to see non-deterministic values whose
value depends upon whether a VirtualMachineError was thrown or not.
That means, for instance, that the computation performed by f() is not
a deterministic function of the arguments to f(), even though none of
the arguments to f() would appear to provide access to non-determinism.
The return value of f() remains a deterministic function of its
arguments, assuming it doesn't throw an Error, but the computation
performed during the execution of f() is not deterministic.  This is
a little surprising.

Note that there are two issues with reasoning about determinism and
pure functions: understanding everything the method f() reads, and
understanding everything that f() writes.  The former is important so
that you can that f()'s return value is a deterministic function of S,
for some set S, and so that you know what the set S is.  The latter is
important so that you know that f() is pure and cannot side-effect other
state in the system.  In some cases, you might only need to know that
f()'s return value is a deterministic function of its arguments; in
others, you might only need to know that f() is pure and cannot side-effect
the world; in yet others you might need to know both.  I think that
VirtualMachineErrors are relevant to both determinism and purity.

(By the way: Are "deterministic" and "pure" the right names for these
concepts?  Are there standard names for these concepts?)

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

Ok.  I think the choice of whether we choose to apply these
techniques to all VirtualMachineErrors or just all Errors may be
more or less orthogonal to how we impose those restrictions on
Joe-E code (i.e., on what types of idioms we require Joe-E code
to follow when in catch{} and finally{} clauses).

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

Ok.  Here's a tweak to my proposal that addresses this issue.
Let's name this Dave's proposal #1:

  1) Any catch{} clause that catches an exception of declared type
  T (where T is VirtualMachineError or any subtype) must have this form:

    catch (T ex) {
        throw ex;
    }

  2) Any catch{} clause that catches an exception of declared type
  Error or Throwable must be preceded by:

    catch (VirtualMachineError ex) {
        throw ex;
    }

  3) Any finally{} clause must be preceded by the same catch clause.

If you prefer to treat all Errors as non-recoverable (not just
all VirtualMachineErrors), then here are two more ways to do this.
First, Dave's proposal #2:

  1) Any catch{} clause that catches an exception of declared type
  FooError (where FooError is Error or any subtype) must have this form:

    catch (FooError ex) {
        throw ex;
    }

  2) Any catch{} clause that catches an exception of declared type
  Throwable must be preceded by:

    catch (Error ex) {
        throw ex;
    }

  3) Any finally{} clause must be preceded by the same catch clause.

Second, Dave's proposal #3:

  1) Any catch{} clause that catches an exception of declared type
  FooError (where FooError is Error or any subtype) must have this form:

    catch (FooError ex) {
        throw ex;
    }

  2) No catch clause may catch an exception of declared type
  Throwable.  Joe-E code may not subclass Throwable or create new
  instances of runtime type Throwable.

  3) Any finally{} clause must be preceded by:

    catch (Error ex) {
        throw ex;
    }

I wanted to get the full suite of options on the table, so that we
can compare them.

I'm curious about why you say Alan's proposal is less onerous on the
programmer.  In particular, I'm mentally comparing Alan's proposal to,
say, Dave's proposal #1-#3.  It seems to me that, in Alan's proposal, you
have to write more stuff inside the finally{} clause than in my proposal.
Could you elaborate on your thinking on this?

Any further thoughts on how we ought to choose among all these options?