[Grace-core] Minutes of Teleconference 23-24.8.12

[James Noble]

> Aha, exceptions! I've been looking at exception handling for my program verification research.

well there's been a version in the spec forever... 

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

Hmm. interesting.  At least this avoids the "full Eiffel" of exception mechanisms!

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

Hmm... so one solution would be to make all methods transactional - in STM style:
an exception going out through a method would roll it back. 

alternatively we could encourage (hard to see how to require) programmers to 
write exception handlers that would ensure their objects were in a constituent state.

but yes, we should look at failboxes, to see i the basic exception mechanism is enough
to put them into a library - just as we should look at the various other "ARM" designs too

James 

On 26/08/2012, at 00:16 AM, Bart Jacobs wrote:

> Hi Andrew,
> 
> On 24/08/2012 19:58, Andrew P. Black wrote:
>> I did not understand the interaction of Failboxes with objects.  In particular, what happens if there are inter-object invariants that are manipulated by a failing computation?  Each of the objects, in its own Failbox, may be consistent, but the program as a whole is not.  This sounds like the problem that transactions were designed to solve.
> 
> The simplest solution would be to simply associate both objects with the same failbox.
> 
> More generally: while the failboxes mechanism supports fine-grained "units of failure", it was definitely not intended to promote this; rather, the intended default is for the entire program to be a single unit of failure and for an exception to simply cause the program to terminate immediately.
> 
> (Note that this is different from the Java's behavior: when a thread's "run" method ends with an exception, other threads continue to run. In the .NET Framework since version 2.0, the program is terminated, but there is still a window between the time the exception is raised and the time the exception reaches the toplevel of the thread when finally blocks run and abandoned locks can be acquired by other threads.)
> 
> The envisaged programming pattern for protecting objects by failboxes is for the object's constructor to record a reference to the current failbox (rather than a newly created failbox) in a field, and for each method to enter this failbox for the duration of its execution. That is, an object adopts is creator's failbox. (Syntactic sugar can be introduced so that this can be achieved by marking a class as "failboxed" or something like that.)
> 
> If the objects do need to be separate units of failure, then the objects' failboxes can be nested inside a parent failbox. The computation that manipulates the objects should run in the parent failbox.
> 
>> 
>> 
>> On 24 Aug 2012, at 3:05, Bart Jacobs wrote:
>> 
>>> - 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!)
>>> 
>>> 
>> Can you explain a bit more why one needs this and when one would use it?  This is different from theBlock.fork, right, in that theBlock runs in a particular existing thread, rather than a new thread.
> 
> I assume you mean it the other way around: yes, fork spawns a new thread, and t.runCode(theBlock) runs theBlock in existing thread t. This is useful for implementing the failboxes mechanism's Fail Fast feature: when an exception occurs in a failbox F in one thread, then not only can F no longer be entered by other threads, but other threads currently running in F get an asynchronous exception, i.e. they get cancelled. It's important, however, that when the asynchronous exception arrives at a target thread, it is actually raised only if that thread is still running inside F. This could be accomplished as follows:
> 
> method fail {
>    foreach (allThreads) do { t ->
>        if (t.currentFailbox == self) then {
>            t.runCode {
>                if (t.currentFailbox == self) then { FailboxCancellationException.raise }
>            }
>        }
>    }
> }
> 
> I have implemented failboxes as a Scala library on top of the JVM, but cancellation exceptions can leak outside the failbox being cancelled due to the lack of a runCode-like mechanism in the Java API. (Note that a similar feature, called Asynchronous Procedure Calls, is available in the Windows API.)
> 
> Bart
> 
> 
> Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core