dok/paper/fail-boxes-resource-management

It is a syntax and semantic for describing when threads depends from each other, and managing errors in the proper way in case of excetpions, and resource deallocation.

The paper says that a problem is that unchecked-exceptions like OutOfRam and similar can happen in every point of a computation and so the finally part can work in an inconsistent state, and reasoning about the application is more difficult. Failboxes should be a solution to this problem.

Failboxes have this simple semantic

• x := currentfb;
• x := newfb;
• x := newfb(x);
• enter (x) { s } catch { s' }

Failboxes works on threads:

• they form an hierarchy
• take note of failed failboxes
• take note of which objects are under lock of a thread
• map thread to its state

MAYBE Dok should derive this information from analyzing the application source-code (i.e. it is not explicit syntax), and then apply the same semantic. So the paper is used from the compiler, but it is transparent for the developer who writes only normal code.

[1] B. Jacobs and F. Piessens, “Failboxes: Provably Safe Exception Handling,” in ECOOP 2009 – Object-Oriented Programming, vol. 5653, S. Drossopoulou, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 470–494. doi: 10.1007/978-3-642-03013-0_22.