[Grace-core] Minutes of Teleconference 23-24.8.12

Bart Jacobs bart.jacobs at cs.kuleuven.be
Fri Aug 24 03:05:01 PDT 2012


Dear all,

Aha, exceptions! I've been looking at exception handling for my program 
verification research. It turns out that the classical exception 
handling mechanism (which is used by most programming languages) leads 
to some verification issues. It'd be great if we could come up with a 
design for Grace that addresses these.

The main issue that I see is the following:

If a mutator method call on an object terminates with an "unchecked" 
exception (i.e. not one raised explicitly as part of the method's normal 
behavior, but one that signals an "I give up" type failure), it's 
possible/likely that the object's internal representation is left in an 
inconsistent state. As a result, subsequent method calls on the object 
are unsafe and shouldn't happen. Current languages provide no support 
for this.

At ECOOP 2009, I presented a mechanism to address this issue, called 
failboxes. The programmer can create failboxes and run code inside of 
them. The effect is that after code in a failbox throws an unchecked 
exception, no further code is allowed to run in the failbox. Therefore, 
associating a failbox with an object and running all calls on the object 
in the failbox solves the issue.

Failboxes, when applied consistently in the program and in the language 
runtime, have the additional advantage that they enable safe 
cancellation (i.e., Java's Thread.stop done right), as well as safe 
compensation (try-finally done right). Also, they solve a liveness 
problem that can occur in concurrent programs when process A waits on 
process B and B dies with an exception before signalling A.

Now, the good news is that failboxes can probably be implemented in 
Grace as a library, with the following caveats to enable safe cancellation:
- global data structures in the Grace runtime library (in so far as they 
are temporarily brought into inconsistent states by Grace code that is 
subject to cancellation) should be protected by failboxes.
- there should be a mechanism to (asynchronously) run code in another 
thread. I.e., there should be a method runCode(code) on Thread objects. 
(This method should probably not be available for general use!)

So, this is just a heads up that I'll be looking to see if I can help 
address this issue in Grace, and of course also a request for comments.

Thanks,
Bart

On 24/08/2012 3:50, James Noble wrote:
>   * exceptions, talked around this.  Decided we needed a design.
>         Michael to write something up


Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm


More information about the Grace-core mailing list