[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