dhh1128 / intent

the intent formal language
https://intentlang.org
2 stars 1 forks source link

expose "critical line" concept from Kalb's exception safety preso #109

Open dhh1128 opened 9 years ago

dhh1128 commented 9 years ago

Must provide a way to declare and prove Kalb's "basic guarantee" (invariants are maintained and no resources are leaked). Also need to facilitate noexcept on dtors, swap, move. Also need to make it possible to very clearly create a "strong guarantee" (basically, ACID transactions--if an exception is thrown, there are no effects/changes in state). We do this by dividing function bodies into two sections using a "critical line". Everything above the line is exception-vulnerable; everything below the line is noexcept. So we do initial computation and save temp state. Then we use a series of noexcept swap calls to update the state. See https://youtu.be/UiZfODgB-Oc?t=48m, and also Kalb's website with more theory and slide decks: http://www.exceptionsafecode.com

dhh1128 commented 9 years ago

In C++, the compiler will call std::terminate if you throw from a noexcept function. It also doesn't do deep proof of noexcept at compile time by inspecting function body. That is, you could declare a function noexcept, and call a function that throws, and the compiler wouldn't complain. The reason for this is that you may have knowledge unavailable to the compiler, that tells you you are only calling the dangerous function in a way that avoids the codepath that throws. The compiler will trust you.

In intent, we can possibly do one better. If we declare a critical line in some formal way, we can enter a zone where we have to "reassure" the compiler that we're aware of throw possibilities; that is, the compiler could issue warnings about any potential code paths that might throw, that we invoke below the critical line. We might do this by implicitly adding a mark (say, +warnaboutthrow) (which could also be added explictly elsewhere if we want it) that tells the compiler to become pessimistic instead of optimistic. Resolving these warnings can be "sticky" -- that is, we can include with source a list of known reassurances that suppress the warnings (see http://codecraft.co/2014/08/06/in-which-warnings-evolve-wings/). If underlying code acquires a new path where exceptions can be thrown, we get warned anew about that specific path--but all our old suppressions remain in place, so we're only nagged each time our foundation shifts on us.