source: doc/theses/andrew_beach_MMath/features.tex @ e3984a68

\chapter{Exception Features}
\label{c:features}

This chapter covers the design and user interface of the \CFA EHM
and begins with a general overview of EHMs. It is not a strict
definition of all EHMs nor an exhaustive list of all possible features.
However it does cover the most common structure and features found in them.

\section{Overview of EHMs}
% We should cover what is an exception handling mechanism and what is an
% exception before this. Probably in the introduction. Some of this could
% move there.
\subsection{Raise / Handle}
An exception operation has two main parts: raise and handle.
These terms are sometimes known as throw and catch but this work uses
throw/catch as a particular kind of raise/handle.
These are the two parts that the user writes and may
be the only two pieces of the EHM that have any syntax in a language.

\paragraph{Raise}
The raise is the starting point for exception handling,
by raising an exception, which passes it to
the EHM.

Some well known examples include the @throw@ statements of \Cpp and Java and
the \code{Python}{raise} statement of Python. In real systems, a raise may
perform some other work (such as memory management) but for the
purposes of this overview that can be ignored.

\paragraph{Handle}
The primary purpose of an EHM is to run some user code to handle a raised
exception. This code is given, along with some other information,
in a handler.

A handler has three common features: the previously mentioned user code, a
region of code it guards and an exception label/condition that matches
against the raised exception.
Only raises inside the guarded region and raising exceptions that match the
label can be handled by a given handler.
If multiple handlers could can handle an exception,
EHMs define a rule to pick one, such as ``best match" or ``first found".

The @try@ statements of \Cpp, Java and Python are common examples. All three
also show another common feature of handlers, they are grouped by the guarded
region.

\subsection{Propagation}
After an exception is raised comes what is usually the biggest step for the
EHM: finding and setting up the handler for execution.
The propagation from raise to
handler can be broken up into three different tasks: searching for a handler,
matching against the handler and installing the handler.

\paragraph{Searching}
The EHM begins by searching for handlers that might be used to handle
the exception.
The search will find handlers that have the raise site in their guarded
region.
The search includes handlers in the current function, as well as any in
callers on the stack that have the function call in their guarded region.

\paragraph{Matching}
Each handler found is with the raised exception. The exception
label defines a condition that is used with the exception and decides if
there is a match or not.
%
In languages where the first match is used, this step is intertwined with
searching; a match check is performed immediately after the search finds
a handler.

\paragraph{Installing}
After a handler is chosen, it must be made ready to run.
The implementation can vary widely to fit with the rest of the
design of the EHM. The installation step might be trivial or it could be
the most expensive step in handling an exception. The latter tends to be the
case when stack unwinding is involved.

If a matching handler is not guaranteed to be found, the EHM needs a
different course of action for this case.
This situation only occurs with unchecked exceptions as checked exceptions
(such as in Java) can make the guarantee.
The unhandled action is usually very general, such as aborting the program.

\paragraph{Hierarchy}
A common way to organize exceptions is in a hierarchical structure.
This pattern comes from object-orientated languages where the
exception hierarchy is a natural extension of the object hierarchy.

Consider the following exception hierarchy:
\begin{center}
\input{exception-hierarchy}
\end{center}
A handler labeled with any given exception can handle exceptions of that
type or any child type of that exception. The root of the exception hierarchy
(here \code{C}{exception}) acts as a catch-all, leaf types catch single types
and the exceptions in the middle can be used to catch different groups of
related exceptions.

This system has some notable advantages, such as multiple levels of grouping,
the ability for libraries to add new exception types and the isolation
between different sub-hierarchies.
This design is used in \CFA even though it is not a object-orientated
language; so different tools are used to create the hierarchy.

% Could I cite the rational for the Python IO exception rework?

\subsection{Completion}
After the handler has finished, the entire exception operation has to complete
and continue executing somewhere else. This step is usually simple,
both logically and in its implementation, as the installation of the handler
is usually set up to do most of the work.

The EHM can return control to many different places, where
the most common are after the handler definition (termination)
and after the raise (resumption).

\subsection{Communication}
For effective exception handling, additional information is often passed
from the raise to the handler and back again.
So far, only communication of the exceptions' identity is covered.
A common communication method for adding information to an exception
is putting fields into the exception instance
and giving the handler access to them.
% You can either have pointers/references in the exception, or have p/rs to
% the exception when it doesn't have to be copied.
Passing references or pointers allows data at the raise location to be
updated, passing information in both directions.

\section{Virtuals}
\label{s:virtuals}
Virtual types and casts are not part of \CFA's EHM nor are they required for
an EHM.
However, one of the best ways to support an exception hierarchy
is via a virtual hierarchy and dispatch system.
Ideally, the virtual system would have been part of \CFA before the work
on exception handling began, but unfortunately it was not.
Hence, only the features and framework needed for the EHM were
designed and implemented for this thesis.
Other features were considered to ensure that
the structure could accommodate other desirable features in the future
but are not implemented.
The rest of this section only discusses the implemented subset of the
virtual system design.

The virtual system supports multiple ``trees" of types. Each tree is
a simple hierarchy with a single root type. Each type in a tree has exactly
one parent -- except for the root type which has zero parents -- and any
number of children.
Any type that belongs to any of these trees is called a virtual type.
% A type's ancestors are its parent and its parent's ancestors.
% The root type has no ancestors.
% A type's descendants are its children and its children's descendants.

For the purposes of illistration, a proposed -- but unimplemented syntax --
will be used. Each virtual type is repersented by a trait with an annotation
that makes it a virtual type. This annotation is empty for a root type, which
creates a new tree:
\begin{cfa}
trait root_type(T) virtual() {}
\end{cfa}
The annotation may also refer to any existing virtual type to make this new
type a child of that type and part of the same tree. The parent may itself
be a child or a root type and may have any number of existing children.
\begin{cfa}
trait child_a(T) virtual(root_type) {}
trait grandchild(T) virtual(child_a) {}
trait child_b(T) virtual(root_type) {}
\end{cfa}
\todo{Update the diagram in vtable.fig to show the new type tree.}

Every virtual type also has a list of virtual members and a unique id,
both are stored in a virtual table.
Every instance of a virtual type also has a pointer to a virtual table stored
in it, although there is no per-type virtual table as in many other languages.

The list of virtual members is built up down the tree. Every virtual type
inherits the list of virtual members from its parent and may add more
virtual members to the end of the list which are passed on to its children.
Again, using the unimplemented syntax this might look like:
\begin{cfa}
trait root_type(T) virtual() {
        const char * to_string(T const & this);
        unsigned int size;
}

trait child_type(T) virtual(root_type) {
        char * irrelevant_function(int, char);
}
\end{cfa}
% Consider adding a diagram, but we might be good with the explanation.

As @child_type@ is a child of @root_type@ it has the virtual members of
@root_type@ (@to_string@ and @size@) as well as the one it declared
(@irrelivant_function@).

It is important to note that these are virtual members, and may contain   
arbitrary fields, functions or otherwise.
The names ``size" and ``align" are reserved for the size and alignment of the
virtual type, and are always automatically initialized as such.
The other special case are uses of the trait's polymorphic argument
(@T@ in the example), which are always updated to refer to the current
virtual type. This allows functions that refer to to polymorphic argument
to act as traditional virtual methods (@to_string@ in the example), as the
object can always be passed to a virtual method in its virtual table.

Up until this point the virtual system is similar to ones found in
object-oriented languages but this is where \CFA diverges.
Objects encapsulate a single set of methods in each type,
universally across the entire program,
and indeed all programs that use that type definition.
The only way to change any method is to inherit and define a new type with
its own universal implementation. In this sense,
these object-oriented types are ``closed" and cannot be altered.
% Because really they are class oriented.

In \CFA, types do not encapsulate any code.
Whether or not satisfies any given assertion, and hence any trait, is
context sensitive. Types can begin to satisfy a trait, stop satisfying it or
satisfy the same trait at any lexical location in the program.
In this sense, an type's implementation in the set of functions and variables
that allow it to satisfy a trait is ``open" and can change
throughout the program.
This capability means it is impossible to pick a single set of functions
that represent a type's implementation across a program.

\CFA side-steps this issue by not having a single virtual table for each
type. A user can define virtual tables that are filled in at their
declaration and given a name. Anywhere that name is visible, even if it is
defined locally inside a function (although in this case the user must ensure
it outlives any objects that use it), it can be used.
Specifically, a virtual type is ``bound" to a virtual table that
sets the virtual members for that object. The virtual members can be accessed
through the object.

While much of the virtual infrastructure is created, it is currently only used
internally for exception handling. The only user-level feature is the virtual
cast, which is the same as the \Cpp \code{C++}{dynamic_cast}.
\label{p:VirtualCast}
\begin{cfa}
(virtual TYPE)EXPRESSION
\end{cfa}
Note, the syntax and semantics matches a C-cast, rather than the function-like
\Cpp syntax for special casts. Both the type of @EXPRESSION@ and @TYPE@ must be
a pointer to a virtual type.
The cast dynamically checks if the @EXPRESSION@ type is the same or a sub-type
of @TYPE@, and if true, returns a pointer to the
@EXPRESSION@ object, otherwise it returns @0p@ (null pointer).

\section{Exception}
% Leaving until later, hopefully it can talk about actual syntax instead
% of my many strange macros. Syntax aside I will also have to talk about the
% features all exceptions support.

Exceptions are defined by the trait system; there are a series of traits, and
if a type satisfies them, then it can be used as an exception. The following
is the base trait all exceptions need to match.
\begin{cfa}
trait is_exception(exceptT &, virtualT &) {
        // Numerous imaginary assertions.
};
\end{cfa}
The trait is defined over two types, the exception type and the virtual table
type. Each exception type should have a single virtual table type.
There are no actual assertions in this trait because the trait system
cannot express them yet (adding such assertions would be part of
completing the virtual system). The imaginary assertions would probably come
from a trait defined by the virtual system, and state that the exception type
is a virtual type, is a descendant of @exception_t@ (the base exception type)
and allow the user to find the virtual table type.

% I did have a note about how it is the programmer's responsibility to make
% sure the function is implemented correctly. But this is true of every
% similar system I know of (except Agda's I guess) so I took it out.

There are two more traits for exceptions defined as follows:
\begin{cfa}
trait is_termination_exception(
                exceptT &, virtualT & | is_exception(exceptT, virtualT)) {
        void defaultTerminationHandler(exceptT &);
};

trait is_resumption_exception(
                exceptT &, virtualT & | is_exception(exceptT, virtualT)) {
        void defaultResumptionHandler(exceptT &);
};
\end{cfa}
Both traits ensure a pair of types are an exception type, its virtual table
type
and defines one of the two default handlers. The default handlers are used
as fallbacks and are discussed in detail in \vref{s:ExceptionHandling}.

However, all three of these traits can be tricky to use directly.
While there is a bit of repetition required,
the largest issue is that the virtual table type is mangled and not in a user
facing way. So these three macros are provided to wrap these traits to
simplify referring to the names:
@IS_EXCEPTION@, @IS_TERMINATION_EXCEPTION@ and @IS_RESUMPTION_EXCEPTION@.

All three take one or two arguments. The first argument is the name of the
exception type. The macro passes its unmangled and mangled form to the trait.
The second (optional) argument is a parenthesized list of polymorphic
arguments. This argument is only used with polymorphic exceptions and the
list is be passed to both types.
In the current set-up, the two types always have the same polymorphic
arguments so these macros can be used without losing flexibility.

For example consider a function that is polymorphic over types that have a
defined arithmetic exception:
\begin{cfa}
forall(Num | IS_EXCEPTION(Arithmetic, (Num)))
void some_math_function(Num & left, Num & right);
\end{cfa}

\section{Exception Handling}
\label{s:ExceptionHandling}
As stated,
\CFA provides two kinds of exception handling: termination and resumption.
These twin operations are the core of \CFA's exception handling mechanism.
This section covers the general patterns shared by the two operations and
then goes on to cover the details each individual operation.

Both operations follow the same set of steps.
First, a user raises an exception.
Second, the exception propagates up the stack, searching for a handler.
Third, if a handler is found, the exception is caught and the handler is run.
After that control continues at a raise-dependent location.
As an alternate to the third step,
if a handler is not found, a default handler is run and, if it returns,
then control
continues after the raise.

The differences between the two operations include how propagation is
performed, where excecution after an exception is handler
and which default handler is run.

\subsection{Termination}
\label{s:Termination}
Termination handling is the familiar kind of handling
and used in most programming
languages with exception handling.
It is a dynamic, non-local goto. If the raised exception is matched and
handled, the stack is unwound and control (usually) continues in the function
on the call stack that defined the handler.
Termination is commonly used when an error has occurred and recovery is
impossible locally.

% (usually) Control can continue in the current function but then a different
% control flow construct should be used.

A termination raise is started with the @throw@ statement:
\begin{cfa}
throw EXPRESSION;
\end{cfa}
The expression must return a reference to a termination exception, where the
termination exception is any type that satisfies the trait
@is_termination_exception@ at the call site.
Through \CFA's trait system, the trait functions are implicitly passed into the
throw code for use by the EHM.
A new @defaultTerminationHandler@ can be defined in any scope to
change the throw's behaviour when a handler is not found (see below).

The throw copies the provided exception into managed memory to ensure
the exception is not destroyed if the stack is unwound.
It is the user's responsibility to ensure the original exception is cleaned
up whether the stack is unwound or not. Allocating it on the stack is
usually sufficient.

% How to say propagation starts, its first sub-step is the search.
Then propagation starts with the search. \CFA uses a ``first match" rule so
matching is performed with the copied exception as the search key.
It starts from the raise site and proceeds towards base of the stack,
from callee to caller.
At each stack frame, a check is made for termination handlers defined by the
@catch@ clauses of a @try@ statement.
\begin{cfa}
try {
        GUARDED_BLOCK
} catch (EXCEPTION_TYPE$\(_1\)$ * [NAME$\(_1\)$]) {
        HANDLER_BLOCK$\(_1\)$
} catch (EXCEPTION_TYPE$\(_2\)$ * [NAME$\(_2\)$]) {
        HANDLER_BLOCK$\(_2\)$
}
\end{cfa}
When viewed on its own, a try statement simply executes the statements
in the \snake{GUARDED_BLOCK} and when those are finished,
the try statement finishes.

However, while the guarded statements are being executed, including any
invoked functions, all the handlers in these statements are included in the
search path.
Hence, if a termination exception is raised, these handlers may be matched
against the exception and may handle it.

Exception matching checks the handler in each catch clause in the order
they appear, top to bottom. If the representation of the raised exception type
is the same or a descendant of @EXCEPTION_TYPE@$_i$, then @NAME@$_i$
(if provided) is
bound to a pointer to the exception and the statements in @HANDLER_BLOCK@$_i$
are executed. If control reaches the end of the handler, the exception is
freed and control continues after the try statement.

If no termination handler is found during the search, then the default handler
(\defaultTerminationHandler) visible at the raise statement is called.
Through \CFA's trait system the best match at the raise statement is used.
This function is run and is passed the copied exception.
If the default handler finishes, control continues after the raise statement.

There is a global @defaultTerminationHandler@ that is polymorphic over all
termination exception types.
The global default termination handler performs a cancellation
(as described in \vref{s:Cancellation})
on the current stack with the copied exception.
Since it is so general, a more specific handler can be defined,
overriding the default behaviour for the specific exception types.

\subsection{Resumption}
\label{s:Resumption}

Resumption exception handling is less familar form of exception handling,
but is
just as old~\cite{Goodenough75} and is simpler in many ways.
It is a dynamic, non-local function call. If the raised exception is
matched, a closure is taken from up the stack and executed,
after which the raising function continues executing.
The common uses for resumption exceptions include
potentially repairable errors, where execution can continue in the same
function once the error is corrected, and
ignorable events, such as logging where nothing needs to happen and control
should always continue from the raise site.

Except for the changes to fit into that pattern, resumption exception
handling is symmetric with termination exception handling, by design
(see \autoref{s:Termination}).

A resumption raise is started with the @throwResume@ statement:
\begin{cfa}
throwResume EXPRESSION;
\end{cfa}
\todo{Decide on a final set of keywords and use them everywhere.}
It works much the same way as the termination raise, except the
type must satisfy the \snake{is_resumption_exception} that uses the
default handler: \defaultResumptionHandler.
This can be specialized for particular exception types.

At run-time, no exception copy is made. Since
resumption does not unwind the stack nor otherwise remove values from the
current scope, there is no need to manage memory to keep the exception
allocated.

Then propagation starts with the search,
following the same search path as termination,
from the raise site to the base of stack and top of try statement to bottom.
However, the handlers on try statements are defined by @catchResume@ clauses.
\begin{cfa}
try {
        GUARDED_BLOCK
} catchResume (EXCEPTION_TYPE$\(_1\)$ * [NAME$\(_1\)$]) {
        HANDLER_BLOCK$\(_1\)$
} catchResume (EXCEPTION_TYPE$\(_2\)$ * [NAME$\(_2\)$]) {
        HANDLER_BLOCK$\(_2\)$
}
\end{cfa}
Note that termination handlers and resumption handlers may be used together
in a single try statement, intermixing @catch@ and @catchResume@ freely.
Each type of handler only interacts with exceptions from the matching
kind of raise.
Like @catch@ clauses, @catchResume@ clauses have no effect if an exception
is not raised.

The matching rules are exactly the same as well.
The first major difference here is that after
@EXCEPTION_TYPE@$_i$ is matched and @NAME@$_i$ is bound to the exception,
@HANDLER_BLOCK@$_i$ is executed right away without first unwinding the stack.
After the block has finished running control jumps to the raise site, where
the just handled exception came from, and continues executing after it,
not after the try statement.

\subsubsection{Resumption Marking}
\label{s:ResumptionMarking}
A key difference between resumption and termination is that resumption does
not unwind the stack. A side effect is that, when a handler is matched
and run, its try block (the guarded statements) and every try statement
searched before it are still on the stack. There presence can lead to
the recursive resumption problem.
\todo{Is there a citation for the recursive resumption problem?}

The recursive resumption problem is any situation where a resumption handler
ends up being called while it is running.
Consider a trivial case:
\begin{cfa}
try {
        throwResume (E &){};
} catchResume(E *) {
        throwResume (E &){};
}
\end{cfa}
When this code is executed, the guarded @throwResume@ starts a
search and matches the handler in the @catchResume@ clause. This
call is placed on the stack above the try-block.
Now the second raise in the handler searches the same try block,
matches again and then puts another instance of the
same handler on the stack leading to infinite recursion.

While this situation is trivial and easy to avoid, much more complex cycles
can form with multiple handlers and different exception types.
To prevent all of these cases, each try statement is ``marked" from the
time the exception search reaches it to either when a handler completes
handling that exception or when the search reaches the base
of the stack.
While a try statement is marked, its handlers are never matched, effectively
skipping over it to the next try statement.

\begin{center}
\input{stack-marking}
\end{center}

There are other sets of marking rules that could be used,
for instance, marking just the handlers that caught the exception,
would also prevent recursive resumption.
However, the rules selected mirrors what happens with termination,
so this reduces the amount of rules and patterns a programmer has to know.

The marked try statements are the ones that would be removed from
the stack for a termination exception, \ie those on the stack
between the handler and the raise statement.
This symmetry applies to the default handler as well, as both kinds of
default handlers are run at the raise statement, rather than (physically
or logically) at the bottom of the stack.
% In early development having the default handler happen after
% unmarking was just more useful. We assume that will continue.

\section{Conditional Catch}
Both termination and resumption handler clauses can be given an additional
condition to further control which exceptions they handle:
\begin{cfa}
catch (EXCEPTION_TYPE * [NAME] ; CONDITION)
\end{cfa}
First, the same semantics is used to match the exception type. Second, if the
exception matches, @CONDITION@ is executed. The condition expression may
reference all names in scope at the beginning of the try block and @NAME@
introduced in the handler clause. If the condition is true, then the handler
matches. Otherwise, the exception search continues as if the exception type
did not match.

The condition matching allows finer matching by checking
more kinds of information than just the exception type.
\begin{cfa}
try {
        handle1 = open( f1, ... );
        handle2 = open( f2, ... );
        handle3 = open( f3, ... );
        ...
} catch( IOFailure * f ; fd( f ) == f1 ) {
        // Only handle IO failure for f1.
} catch( IOFailure * f ; fd( f ) == f3 ) {
        // Only handle IO failure for f3.
}
// Handle a failure relating to f2 further down the stack.
\end{cfa}
In this example the file that experienced the IO error is used to decide
which handler should be run, if any at all.

\begin{comment}
% I know I actually haven't got rid of them yet, but I'm going to try
% to write it as if I had and see if that makes sense:
\section{Reraising}
\label{s:Reraising}
Within the handler block or functions called from the handler block, it is
possible to reraise the most recently caught exception with @throw@ or
@throwResume@, respectively.
\begin{cfa}
try {
        ...
} catch( ... ) {
        ... throw;
} catchResume( ... ) {
        ... throwResume;
}
\end{cfa}
The only difference between a raise and a reraise is that reraise does not
create a new exception; instead it continues using the current exception, \ie
no allocation and copy. However the default handler is still set to the one
visible at the raise point, and hence, for termination could refer to data that
is part of an unwound stack frame. To prevent this problem, a new default
handler is generated that does a program-level abort.
\end{comment}

\subsection{Comparison with Reraising}
In languages without conditional catch, that is no ability to match an
exception based on something other than its type, it can be mimicked
by matching all exceptions of the right type, checking any additional
conditions inside the handler and re-raising the exception if it does not
match those.

Here is a minimal example comparing both patterns, using @throw;@
(no argument) to start a re-raise.
\begin{center}
\begin{tabular}{l r}
\begin{cfa}
try {
    do_work_may_throw();
} catch(exception_t * exc ;
                can_handle(exc)) {
    handle(exc);
}



\end{cfa}
&
\begin{cfa}
try {
    do_work_may_throw();
} catch(exception_t * exc) {
    if (can_handle(exc)) {
        handle(exc);
    } else {
        throw;
    }
}
\end{cfa}
\end{tabular}
\end{center}
At first glance catch-and-reraise may appear to just be a quality of life 
feature, but there are some significant differences between the two
stratagies.

A simple difference that is more important for \CFA than many other languages
is that the raise site changes, with a re-raise but does not with a
conditional catch.
This is important in \CFA because control returns to the raise site to run
the per-site default handler. Because of this only a conditional catch can
allow the original raise to continue.

The more complex issue comes from the difference in how conditional
catches and re-raises handle multiple handlers attached to a single try
statement. A conditional catch will continue checking later handlers while
a re-raise will skip them.
If the different handlers could handle some of the same exceptions,
translating a try statement that uses one to use the other can quickly
become non-trivial:

\noindent
Original, with conditional catch:
\begin{cfa}
...
} catch (an_exception * e ; check_a(e)) {
        handle_a(e);
} catch (exception_t * e ; check_b(e)) {
        handle_b(e);
}
\end{cfa}
Translated, with re-raise:
\begin{cfa}
...
} catch (exception_t * e) {
        an_exception * an_e = (virtual an_exception *)e;
        if (an_e && check_a(an_e)) {
                handle_a(an_e);
        } else if (check_b(e)) {
                handle_b(e);
        } else {
                throw;
        }
}
\end{cfa}
(There is a simpler solution if @handle_a@ never raises exceptions,
using nested try statements.)

% } catch (an_exception * e ; check_a(e)) {
%     handle_a(e);
% } catch (exception_t * e ; !(virtual an_exception *)e && check_b(e)) {
%     handle_b(e);
% }
%
% } catch (an_exception * e)
%   if (check_a(e)) {
%     handle_a(e);
%   } else throw;
% } catch (exception_t * e)
%   if (check_b(e)) {
%     handle_b(e);
%   } else throw;
% }
In similar simple examples translating from re-raise to conditional catch
takes less code but it does not have a general trivial solution either.

So, given that the two patterns do not trivially translate into each other,
it becomes a matter of which on should be encouraged and made the default.
From the premise that if a handler that could handle an exception then it
should, it follows that checking as many handlers as possible is preferred.
So conditional catch and checking later handlers is a good default.

\section{Finally Clauses}
\label{s:FinallyClauses}
Finally clauses are used to preform unconditional clean-up when leaving a
scope and are placed at the end of a try statement after any handler clauses:
\begin{cfa}
try {
        GUARDED_BLOCK
} ... // any number or kind of handler clauses
... finally {
        FINALLY_BLOCK
}
\end{cfa}
The @FINALLY_BLOCK@ is executed when the try statement is removed from the
stack, including when the @GUARDED_BLOCK@ finishes, any termination handler
finishes or during an unwind.
The only time the block is not executed is if the program is exited before
the stack is unwound.

Execution of the finally block should always finish, meaning control runs off
the end of the block. This requirement ensures control always continues as if
the finally clause is not present, \ie finally is for cleanup not changing
control flow.
Because of this requirement, local control flow out of the finally block
is forbidden. The compiler precludes any @break@, @continue@, @fallthru@ or
@return@ that causes control to leave the finally block. Other ways to leave
the finally block, such as a long jump or termination are much harder to check,
and at best requiring additional run-time overhead, and so are only
discouraged.

Not all languages with unwinding have finally clauses. Notably \Cpp does
without it as destructors, and the RAII design pattern, serve a similar role.
Although destructors and finally clauses can be used for the same cases,
they have their own strengths, similar to top-level function and lambda
functions with closures.
Destructors take more work to create, but if there is clean-up code
that needs to be run every time a type is used, they are much easier
to set-up for each use. % It's automatic.
On the other hand finally clauses capture the local context, so is easy to
use when the clean-up is not dependent on the type of a variable or requires
information from multiple variables.

\section{Cancellation}
\label{s:Cancellation}
Cancellation is a stack-level abort, which can be thought of as as an
uncatchable termination. It unwinds the entire current stack, and if
possible forwards the cancellation exception to a different stack.

Cancellation is not an exception operation like termination or resumption.
There is no special statement for starting a cancellation; instead the standard
library function @cancel_stack@ is called passing an exception. Unlike a
raise, this exception is not used in matching only to pass information about
the cause of the cancellation.
Finally, as no handler is provided, there is no default handler.

After @cancel_stack@ is called the exception is copied into the EHM's memory
and the current stack is unwound.
The behaviour after that depends on the kind of stack being cancelled.

\paragraph{Main Stack}
The main stack is the one used by the program main at the start of execution,
and is the only stack in a sequential program.
After the main stack is unwound there is a program-level abort. 

The first reason for this behaviour is for sequential programs where there
is only one stack, and hence to stack to pass information to.
Second, even in concurrent programs, the main stack has no dependency
on another stack and no reliable way to find another living stack.
Finally, keeping the same behaviour in both sequential and concurrent
programs is simple and easy to understand.

\paragraph{Thread Stack}
A thread stack is created for a \CFA @thread@ object or object that satisfies
the @is_thread@ trait.
After a thread stack is unwound, the exception is stored until another
thread attempts to join with it. Then the exception @ThreadCancelled@,
which stores a reference to the thread and to the exception passed to the
cancellation, is reported from the join to the joining thread.
There is one difference between an explicit join (with the @join@ function)
and an implicit join (from a destructor call). The explicit join takes the
default handler (@defaultResumptionHandler@) from its calling context while
the implicit join provides its own; which does a program abort if the
@ThreadCancelled@ exception cannot be handled.

The communication and synchronization are done here because threads only have
two structural points (not dependent on user-code) where
communication/synchronization happens: start and join.
Since a thread must be running to perform a cancellation (and cannot be
cancelled from another stack), the cancellation must be after start and
before the join, so join is used.

% TODO: Find somewhere to discuss unwind collisions.
The difference between the explicit and implicit join is for safety and
debugging. It helps prevent unwinding collisions by avoiding throwing from
a destructor and prevents cascading the error across multiple threads if
the user is not equipped to deal with it.
It is always possible to add an explicit join if that is the desired behaviour.

With explicit join and a default handler that triggers a cancellation, it is
possible to cascade an error across any number of threads,
alternating between the resumption (possibly termination) and cancellation,
cleaning up each
in turn, until the error is handled or the main thread is reached.

\paragraph{Coroutine Stack}
A coroutine stack is created for a @coroutine@ object or object that
satisfies the @is_coroutine@ trait.
After a coroutine stack is unwound, control returns to the @resume@ function
that most recently resumed it. @resume@ reports a
@CoroutineCancelled@ exception, which contains a references to the cancelled
coroutine and the exception used to cancel it.
The @resume@ function also takes the \defaultResumptionHandler{} from the
caller's context and passes it to the internal report.

A coroutine only knows of two other coroutines,
its starter and its last resumer.
The starter has a much more distant connection, while the last resumer just
(in terms of coroutine state) called resume on this coroutine, so the message
is passed to the latter.

With a default handler that triggers a cancellation, it is possible to
cascade an error across any number of coroutines,
alternating between the resumption (possibly termination) and cancellation,
cleaning up each in turn,
until the error is handled or a thread stack is reached.