[cap-talk] small notes re: waterken

[David Wagner]

Marc Stiegler  wrote:
> Since Joe-E is a verifier, not a rewriter, what exactly do you do in
> Joe-E to make those errors fatal?

Joe-E statically enforces restrictions on code which ensure that:
 - Joe-E code cannot catch any Error
 - finally clauses are prohibited
The goal is that after an error is thrown, no Joe-E code should be able
to run.  This goal is achieved in a pure Joe-E program.

In a pure Joe-E program, all that can happen is that the Error propagates
up the stack, unwinding stack frames as it goes, until it reaches the top
level and the program is terminated.  No Joe-E code can execute during
this process, as the stack unwinds.  As far as the Joe-E code can tell,
this is basically equivalent to killing the program as soon as the Error
is thrown.

However, there is an important caveat for programs that are constructed
as a mixture of Java and Joe-E code.  Java code is not subject to these
restrictions, so Java code can catch Errors or introduce finally clauses
that might execute after an Error is thrown.  Consequently, in a mixed
Java+Joe-E program, we cannot guarantee that errors are immediately
fatal, since for all we know, the Java code might catch the error.
However, if the Java code is written appropriately, then the property
that Errors are always fatal can be preserved.

My recollection is that Waterken is structured as follows: there is
a main loop, written in Java, which calls Joe-E code for each turn.
I believe there is a top-level exception handler in the main loop which
catches any exceptions or errors thrown by the Joe-E code and handles them
appropriately.  I am hoping it handles VirtualMachineErrors by aborting
the turn and rolling back its state, or something else equally fatal,
rather than exposing the inconsistent state of the Joe-E code to others.
However, I haven't verified that this is indeed the case and I might be
totally confused.  Hopefully Tyler can correct any mistakes in the above.

I don't know what the tradeoffs are with making Errors fatal.  Perhaps the
main loop could add an exception handler that catches all Errors, so that
if an Error occurs, the turn is aborted and the state is rolled back to
that before the turn was attempted?  I'm speculating wildly here...

More detail on Joe-E's handling of errors can be found here:

http://www.cs.berkeley.edu/~daw/papers/joe-e-ndss10.pdf
(Section 4.3, starting at paragraph 4)

http://www.cs.berkeley.edu/~daw/joe-e/spec-20090918.pdf
(Section 4.8)