Index: doc/theses/colby_parsons_MMAth/glossary.tex
===================================================================
--- doc/theses/colby_parsons_MMAth/glossary.tex	(revision 60c3d87e3c00f8e5303153bdaebe7088085c2e8e)
+++ doc/theses/colby_parsons_MMAth/glossary.tex	(revision 6d18ddbed6ac65a32f450a83b04e3c6ddc7058f5)
@@ -37,37 +37,36 @@
 \newabbreviation{toctou}{TOCTOU}{\Newterm{time-of-check to time-of-use}}
 
-\newglossaryentry{actor}
-{
+\newglossaryentry{actor}{
 name=actor,
 description={A basic unit of an actor system that can store local state and send messages to other actors.}
 }
 
-\newglossaryentry{gulp}
-{
-name=gulp,
+\newglossaryentry{gulp}{
+name={gulp},
+first={\Newterm{gulp}},
 description={Move the contents of message queue to a local queue of the executor thread using a single atomic instruction.}
 }
 
-\newglossaryentry{impl_concurrency}
-{
+\newglossaryentry{impl_concurrency}{
 name=implicit concurrency,
+first={\Newterm{implicit concurrency}},
 description={A class of concurrency features that abstract away explicit thread synchronization and mutual exclusion.}
 }
 
-\newglossaryentry{actor_model}
-{
+\newglossaryentry{actor_model}{
 name=actor model,
+first={\Newterm{actor model}},
 description={A concurrent computation model, where tasks are broken into units of work that are distributed to actors in the form of messages.}
 }
 
-\newglossaryentry{actor_system}
-{
+\newglossaryentry{actor_system}{
 name=actor system,
+first={\Newterm{actor system}},
 description={An implementation of the actor model.}
 }
 
-\newglossaryentry{synch_multiplex}
-{
+\newglossaryentry{synch_multiplex}{
 name=synchronous multiplexing,
+first={\Newterm{synchronous multiplexing}},
 description={synchronization on some subset of a set of resources.}
 }
Index: doc/theses/colby_parsons_MMAth/text/actors.tex
===================================================================
--- doc/theses/colby_parsons_MMAth/text/actors.tex	(revision 60c3d87e3c00f8e5303153bdaebe7088085c2e8e)
+++ doc/theses/colby_parsons_MMAth/text/actors.tex	(revision 6d18ddbed6ac65a32f450a83b04e3c6ddc7058f5)
@@ -21,7 +21,7 @@
 An actor is executed by an underlying \Newterm{executor} (kernel thread-pool) that fairly invokes each actor, where an actor invocation processes one or more messages from its mailbox.
 The default number of executor threads is often proportional to the number of computer cores to achieve good performance.
-An executor is often tunable with respect to the number of kernel threads and its scheduling algorithm, which optimize for specific actor applications and workloads \see{end of Section~\ref{s:CFAActorSyntax}}.
-
-\section{Classic Actor System}
+An executor is often tunable with respect to the number of kernel threads and its scheduling algorithm, which optimize for specific actor applications and workloads \see{end of Section~\ref{s:CFAActor}}.
+
+\subsection{Classic Actor System}
 An implementation of the actor model with a community of actors is called an actor system.
 Actor systems largely follow the actor model, but can differ in some ways.
@@ -45,5 +45,5 @@
 \end{figure}
 
-\section{\CFA Actors}
+\subsection{\CFA Actor System}
 Figure~\ref{f:standard_actor} shows an actor system designed as \Newterm{actor-centric}, where a set of actors are scheduled and run on underlying executor threads~\cite{CAF,Akka,ProtoActor}.
 The simplest design has a single global queue of actors accessed by the executor threads, but this approach results in high contention as both ends of the queue by the executor threads.
@@ -92,5 +92,5 @@
 \end{enumerate}
 
-\section{\CFA Actor Syntax}\label{s:CFAActorSyntax}
+\section{\CFA Actor}\label{s:CFAActor}
 \CFA is not an object oriented language and it does not have \gls{rtti}.
 As such, all message sends and receives among actors can only occur using static type-matching, as in Typed-Akka~\cite{AkkaTyped}.
@@ -146,47 +146,50 @@
 // messages
 struct str_msg {
-	@inline message;@						$\C{// Plan-9 C nominal inheritance}$
 	char str[12];
+	@inline message;@						$\C{// Plan-9 C inheritance}$
 };
 void ?{}( str_msg & this, char * str ) { strcpy( this.str, str ); }  $\C{// constructor}$
 struct int_msg {
-	@inline message;@						$\C{// Plan-9 C nominal inheritance}$
 	int i;
+	@inline message;@						$\C{// Plan-9 C inheritance}$
 };
-void ?{}( int_msg & this, int i ) { this.i = i; }	$\C{// constructor}$
 // behaviours
-allocation receive( my_actor &, @str_msg & msg@ ) {
-	sout | "string message \"" | msg.str | "\"";
+allocation receive( my_actor &, @str_msg & msg@ ) with(msg) {
+	sout | "string message \"" | str | "\"";
 	return Nodelete;						$\C{// actor not finished}$
 }
-allocation receive( my_actor &, @int_msg & msg@ ) {
-	sout | "integer message" | msg.i;
+allocation receive( my_actor &, @int_msg & msg@ ) with(msg) {
+	sout | "integer message" | i;
 	return Nodelete;						$\C{// actor not finished}$
 }
 int main() {
+	str_msg str_msg{ "Hello World" };		$\C{// constructor call}$
+	int_msg int_msg{ 42 };					$\C{// constructor call}$
 	start_actor_system();					$\C{// sets up executor}$
 	my_actor actor;							$\C{// default constructor call}$
-	str_msg str_msg{ "Hello World" };		$\C{// constructor call}$
-	int_msg int_msg{ 42 };					$\C{// constructor call}$
-	@actor << str_msg << int_msg;@			$\C{// cascade sends}$
-	@actor << int_msg;@						$\C{// send}$
-	@actor << finished_msg;@				$\C{// send => terminate actor (deallocation deferred)}$
+	@actor | str_msg | int_msg;@			$\C{// cascade sends}$
+	@actor | int_msg;@						$\C{// send}$
+	@actor | finished_msg;@					$\C{// send => terminate actor (deallocation deferred)}$
 	stop_actor_system();					$\C{// waits until actors finish}\CRT$
 } // deallocate int_msg, str_msg, actor
 \end{cfa}
 \caption{\CFA Actor Syntax}
-\label{f:CFAActorSyntax}
-\end{figure}
-
-Figure~\ref{f:CFAActorSyntax} shows a complete \CFA actor example starting with the actor type @my_actor@ created by defining a @struct@ that inherits from the base @actor@ @struct@ via the @inline@ keyword.
-This inheritance style is the Plan-9 C-style nominal inheritance discussed in Section~\ref{s:Inheritance}.
+\label{f:CFAActor}
+\end{figure}
+
+Figure~\ref{f:CFAActor} shows a complete \CFA actor example starting with the actor type @my_actor@ created by defining a @struct@ that inherits from the base @actor@ @struct@ via the @inline@ keyword.
+This inheritance style is the Plan-9 C-style inheritance discussed in Section~\ref{s:Inheritance}.
 Similarly, the message types @str_msg@ and @int_msg@ are created by defining a @struct@ that inherits from the base @message@ @struct@ via the @inline@ keyword.
-Both message types have constructors to set the message value.
+Only @str_msg@ needs a constructor to copy the C string;
+@int_msg@ is initialized using its \CFA auto-generated constructors.
 There are two matching @receive@ (behaviour) routines that process the corresponding typed messages.
-The program main begins by calling @start_actor_system@ to start the actor implementation, including executor threads to run the actors.
-An actor and two messages are created on the stack, and four messages are sent to the actor using operator @<<@.
-The last message is the builtin @finish_msg@, which returns @Finished@ to an executor thread, which removes the actor from the actor system \see{Section~\ref{s:ActorBehaviours}}.
-The call to @stop_actor_system@ blocks program main until all actors are finished and removed from the actor system.
-The program main ends by deleting the actor and messages from the stack.
+Both @receive@ routines use a @with@ clause so message fields are not qualified and return @Nodelete@ indicating the actor is not finished.
+Also, all messages are marked with @Nodelete@ as their default allocation state.
+The program main begins by creating two messages on the stack.
+Then the executor system is started by calling @start_actor_system@.
+Now an actor is created on the stack and four messages are sent it using operator @?|?@.
+The last message is the builtin @finish_msg@, which returns @Finished@ to an executor thread, causing it to removes the actor from the actor system \see{Section~\ref{s:ActorBehaviours}}.
+The call to @stop_actor_system@ blocks the program main until all actors are finished and removed from the actor system.
+The program main ends by deleting the actor and two messages from the stack.
 The output for the program is:
 \begin{cfa}
@@ -237,4 +240,24 @@
 Note, it is safe to construct an actor or message with a status other than @Nodelete@, since the executor only examines the allocation action after a behaviour returns.
 
+\subsection{Actor Envelopes}\label{s:envelope}
+As stated, each message, regardless of where it is allocated, can be sent to an arbitrary number of actors, and hence, appear on an arbitrary number of message queues.
+Because a C program manages message lifetime, messages cannot be copied for each send, otherwise who manages the copies.
+Therefore, it up to the actor program to manage message life-time across receives.
+However, for a message to appear on multiple message queues, it needs an arbitrary number of associated destination behaviours.
+Hence, there is the concept of an envelop, which is dynamically allocated on each send, that wraps a message with any extra implementation fields needed to persist between send and receive.
+Managing the envelop is straightforward because it is created at the send and deleted after the receive, \ie there is 1:1 relationship for an envelop and a many to one relationship for a message.
+
+% In actor systems, messages are sent and received by actors.
+% When a actor receives a message it executes its behaviour that is associated with that message type.
+% However the unit of work that stores the message, the receiving actor's address, and other pertinent information needs to persist between send and the receive.
+% Furthermore the unit of work needs to be able to be stored in some fashion, usually in a queue, until it is executed by an actor.
+% All these requirements are fulfilled by a construct called an envelope.
+% The envelope wraps up the unit of work and also stores any information needed by data structures such as link fields.
+
+% One may ask, "Could the link fields and other information be stored in the message?".
+% This is a good question to ask since messages also need to have a lifetime that persists beyond the work it delivers.
+% However, if one were to use messages as envelopes then a message would not be able to be sent to multiple actors at a time.
+% Therefore this approach would just push the allocation into another location, and require the user to dynamically allocate a message for every send, or require careful ordering to allow for message reuse.
+
 \subsection{Actor System}\label{s:ActorSystem}
 The calls to @start_actor_system@, and @stop_actor_system@ mark the start and end of a \CFA actor system.
@@ -258,55 +281,94 @@
 All actors must be created \emph{after} calling @start_actor_system@ so the executor can keep track of the number of actors that have entered the system but not yet terminated.
 
-% All message sends are done using the left-shift operator, @<<@, similar to the syntax of \CC's stream output.
-% \begin{cfa}
-% allocation ?<<?( my_actor & receiver, my_msg & msg )
-% \end{cfa}
-% Notice this signature is the same as the @receive@ routine, which is no coincidence.
-% The \CFA compiler generates a @?<<?@ routine definition and forward declaration for each @receive@ routine that has the appropriate signature.
-% The generated routine packages the message and actor in an \hyperref[s:envelope]{envelope} and adds it to the executor's queues via an executor routine.
-% As part of packaging the envelope, the @?<<?@ routine sets a routine pointer in the envelope to point to the appropriate receive routine for given actor and message types.
-
-\subsection{Actor Send}\label{s:ActorSend} % C_TODO: rework this paragraph based on discussion with Mike, see ~/cfa-cc/actor_poly.tex for notes (and fangren's resolver changes)
-All message sends are done using the left-shift operator, @<<@, similar to the syntax of \CC's stream output.
+\subsection{Actor Send}\label{s:ActorSend}
+All message sends are done using the vertical-bar (bit-or) operator, @?|?@, similar to the syntax of the \CFA stream I/O.
+Hence, programmers must write a matching @?|?@ routine for each @receive@ routine, which is awkward and generates a maintenance problem That must be solved.
+The currently supported approach to creating a generic @?|?@ routine requires users to create specific routines for their actor and message types that access the base type.
+Since these routines are not complex, they can be generated using macros that the user can add following their message and actor types.
+This works, but is not much better than asking users to write the @?|?@ routine themselves.
+
 As stated, \CFA does not have named inheritance with RTTI.
 \CFA does have a preliminary form of virtual routines, but it is not mature enough for use in this work.
-Therefore, there is no mechanism to write a generic @<<@ routine taking a base actor and message type, and then dynamically selecting the @receive@ routine from the actor argument.
-(For messages, the Plan-9 inheritance is sufficient because only the inherited fields are needed during the message send.)
-Hence, programmers must write a matching @<<@ routine for each @receive@ routine, which is awkward and generates a maintenance problem.
-Therefore, I chose to use a template-like approach, where the compiler generates a matching @<<@ routine for each @receive@ routine it finds with an actor/message type-signature.
-Then, \CFA uses the type from the left-hand side of an assignment to select the matching receive routine.
+Virtuals would provide a clean mechanism to write a single generic @?|?@ routine taking a base actor and message type, and then dynamically selecting the @receive@ routine from the actor argument.
+Note, virtuals are not needed for the send; Plan-9 inheritance is sufficient because only the inherited fields are needed during the message send (only upcasting is needed).
+
+Therefore, a template-like approach was chosen, where the compiler generates a matching @?|?@ routine for each @receive@ routine it finds with the correct actor/message type-signature.
+This approach requires no annotation or additional code to be written by users, thus it resolves the maintenance problem.
 (When the \CFA virtual routines mature, it should be possible to seamlessly transition to it from the template approach.)
 
-% Funneling all message sends through a single @allocation ?<<?(actor &, message &)@ routine is not feasible since the type of the actor and message would be erased, making it impossible to acquire a pointer to the correct @receive@.
-% As such a @?<<?@ routine per @receive@ provides type information needed to write the correct "address" on the envelope.
-
-% The left-shift operator routines are generated by the compiler.
-An example of a receive routine and its corresponding generated operator routine is shown in Figure~\ref{f:actor_gen}.
-Notice the parameter signature of @?<<?@ is the same as the @receive@ routine.
-A @?<<?@ routine is generated per @receive@ routine with a matching signature.
-The @?<<?@ routine packages the message and actor in an \hyperref[s:envelope]{envelope} and adds it to the executor's queues via the executor routine @send@.
-The envelope is conceptually "addressed" to a behaviour, which is stored in the envelope as a function pointer to a @receive@ routine.
-The @?<<?@ routines ensure that messages are sent to the right address, \ie sent to the right @receive@ routine based on actor and message type.
+Figure~\ref{f:send_gen} shows the generated send routine for the @int_msg@ receive in Figure~\ref{f:CFAActor}.
+Operator @?|?@ has the same parameter signature as the corresponding @receive@ routine and returns an @actor@ so the operator can be cascaded.
+The routine sets @rec_fn@ to the matching @receive@ routine using the left-hand type to perform the selection.
+Then the routine packages the base and derived actor and message and actor, along with the receive routine into an \hyperref[s:envelope]{envelope}.
+Finally, the envelop is added to the executor queue designated by the actor using the executor routine @send@.
 
 \begin{figure}
 \begin{cfa}
-$\LstCommentStyle{// from Figure~\ref{f:CFAActorSyntax}}$
-struct my_actor { inline actor; }; 					$\C[3.5in]{// actor}$
-struct int_msg { inline message; int i; }; 			$\C{// message}$
-void ?{}( int_msg & this, int i ) { this.i = i; }	$\C{// constructor}$
-allocation receive( @my_actor &, int_msg & msg@ ) {	$\C{// receiver}$
-	sout | "integer message" | msg.i;
-	return Nodelete;
-}
-
-// compiler generated operator
-#define RECEIVER( A, M ) (allocation (*)(actor &, message &))(allocation (*)( A &, M & ))receive
-my_actor & ?<<?( @my_actor & receiver, int_msg & msg@ ) {
-	send( receiver, (request){ &receiver, &msg, RECEIVER( my_actor, int_msg ) } );
+$\LstCommentStyle{// from Figure~\ref{f:CFAActor}}$
+struct my_actor { inline actor; }; 						$\C[3.75in]{// actor}$
+struct int_msg { inline message; int i; }; 				$\C{// message}$
+allocation receive( @my_actor &, int_msg & msg@ ) {...}	$\C{// receiver}$
+
+// compiler generated send operator
+typedef allocation (*receive_t)( actor &, message & );
+actor & ?|?( @my_actor & receiver, int_msg & msg@ ) {
+	allocation (*rec_fn)( my_actor &, int_msg & ) = @receive@; // deduce receive routine
+	request req{ &receiver, (actor *)&receiver, &msg, (message *)&msg, (receive_t)rec_fn };
+	send( receiver, req ); 								$\C{// queue message for execution}\CRT$
 	return receiver;
 }
 \end{cfa}
 \caption{Generated Send Operator}
-\label{f:actor_gen}
+\label{f:send_gen}
+\end{figure}
+
+\subsection{Actor Termination}\label{s:ActorTerm}
+As discussed in Section~\ref{s:ActorSend}, during a message send, the derived type of the actor and message is erased, and then recovered later by calling the receive routine.
+After the receive routine is done, the executor must clean up the actor and message according to their allocation status.
+If the allocation status is @Delete@ or @Destroy@, the appropriate destructor must be called by the executor.
+This poses a problem; the type of the actor or message is not available to the executor, but it needs to call the right destructor!
+This requires down-casting from the base type to derived type, which requires a virtual system.
+Thus, a rudimentary destructor-only virtual system was added to \CFA as part of this work.
+This virtual system is used via Plan-9 inheritance of the @virtual_dtor@ type.
+The @virtual_dtor@ type maintains a pointer to the start of the object, and a pointer to the correct destructor.
+When a type inherits the @virtual_dtor@ type, the compiler adds code to its destructor to make sure that whenever any destructor along inheritance tree is called, the destructor call is intercepted, and restarts at the appropriate destructor for that object.
+
+\begin{figure}
+\begin{cfa}
+struct base_type { inline virtual_dtor; };
+struct intermediate_type { inline base_type; };
+struct derived_type { inline intermediate_type; };
+
+int main() {
+    derived_type d1, d2, d3;
+    intermediate_type & i = d2;
+    base_type & b = d3;
+    ^d1{}; ^i{}; ^b{}; // all of these will call the destructors in the correct order
+}
+
+\end{cfa}
+\caption{\CFA Virtual Destructor}
+\label{f:VirtDtor}
+\end{figure}
+
+This virtual destructor system was built for this work, but is general and can be used in any type in \CFA.
+Actors and messages opt into this system by inheriting the @virtual_dtor@ type, which allows the executor to call the right destructor without knowing the derived actor or message type.
+
+Figure~\ref{f:ConvenienceMessages} shows three builtin convenience messages and receive routines used to terminate actors, depending on how an actor is allocated: @Delete@, @Destroy@ or @Finished@.
+For example, in Figure~\ref{f:CFAActor}, the builtin @finished_msg@ message and receive are used to terminate the actor because the actor is allocated on the stack, so no deallocation actions are performed by the executor.
+
+\begin{figure}
+\begin{cfa}
+message __base_msg_finished $@$= { .allocation_ : Finished }; // no auto-gen constructors
+struct __delete_msg_t { inline message; } delete_msg = __base_msg_finished;
+struct __destroy_msg_t { inline message; } destroy_msg = __base_msg_finished;
+struct __finished_msg_t { inline message; } finished_msg = __base_msg_finished;
+
+allocation receive( actor & this, __delete_msg_t & msg ) { return Delete; }
+allocation receive( actor & this, __destroy_msg_t & msg ) { return Destroy; }
+allocation receive( actor & this, __finished_msg_t & msg ) { return Finished; }
+\end{cfa}
+\caption{Builtin Convenience Messages}
+\label{f:ConvenienceMessages}
 \end{figure}
 
@@ -319,5 +381,4 @@
 The goal is to achieve better performance and scalability for certain kinds of actor applications by reducing executor locking.
 Note, lock-free queues do not help because busy waiting on any atomic instruction is the source of the slowdown whether it is a lock or lock-free.
-Work steal now becomes queue stealing, where an entire actor/message queue is stolen, which trivially preserves message ordering in a queue \see{Section~\ref{s:steal}}.
 
 \begin{figure}
@@ -330,35 +391,26 @@
 
 Each executor thread iterates over its own message queues until it finds one with messages.
-At this point, the executor thread atomically \gls{gulp}s the queue, meaning move the contents of message queue to a local queue of the executor thread using a single atomic instruction.
-This step allows the executor threads to process the local queue without any atomics until the next gulp, while other executor threads are adding in parallel to the end of one of the message queues.
-In detail, an executor thread performs a test-and-gulp, non-atomically checking if a queue is non-empty before gulping it.
-If a test fails during a message add, the worst-case is cycling through all the message queues.
-However, the gain is minimizing costly lock acquisitions.
+At this point, the executor thread atomically \gls{gulp}s the queue, meaning it moves the contents of message queue to a local queue of the executor thread using a single atomic instruction.
 An example of the queue gulping operation is shown in the right side of Figure \ref{f:gulp}, where a executor threads gulps queue 0 and begins to process it locally.
-
-Processing a local queue involves removing a unit of work from the queue and executing it.
+This step allows an executor thread to process the local queue without any atomics until the next gulp.
+Other executor threads can continue adding to the ends of executor thread's message queues.
+In detail, an executor thread performs a test-and-gulp, non-atomically checking if a queue is non-empty, before attempting to gulp it.
+If an executor misses an non-empty queue due to a race, it eventually finds the queue after cycling through its message queues.
+This approach minimizes costly lock acquisitions.
+
+Processing a local queue involves: removing a unit of work from the queue, dereferencing the actor pointed-to by the work-unit, running the actor's behaviour on the work-unit message, examining the returned allocation status from the @receive@ routine for the actor and internal status in the delivered message, and taking the appropriate actions.
 Since all messages to a given actor are in the same queue, this guarantees atomicity across behaviours of that actor since it can only execute on one thread at a time.
-After running a behaviour, the executor thread examines the returned allocation status from the @receive@ routine for the actor and internal status in the delivered message, and takes the appropriate action.
-Once all actors have marked themselves as being finished the executor initiates shutdown by inserting a sentinel value into the message queues. % C_TODO: potentially change if I keep shutdown flag change
-Once a executor threads sees a sentinel it stops running.
-After all executors stop running the actor system shutdown is complete.
-
-\section{Envelopes}\label{s:envelope}
-As stated, each message, regardless of where it is allocated, can be sent to an arbitrary number of actors, and hence, appear on an arbitrary number of message queues.
-Because a C program manages message lifetime, messages cannot be copied for each send, otherwise who manages the copies.
-Therefore, it up to the actor program to manage message life-time across receives.
-However, for a message to appear on multiple message queues, it needs an arbitrary number of associated destination behaviours.
-Hence, there is the concept of an envelop, which is dynamically allocated on each send, that wraps a message with any extra implementation fields needed to persist between send and receive.
-Managing the envelop is straightforward because it is created at the send and deleted after the receive, \ie there is 1:1 relationship for an envelop and a many to one relationship for a message.
-
-Unfortunately, this frequent allocation of envelopes for each send results in heavy contention on the memory allocator.
-As such, a way to alleviate contention on the memory allocator would result in a performance improvement.
-Contention is reduced using a novel data structure, called a \Newterm{copy queue}.
+As each actor is created or terminated by an executor thread, it increments/decrements a global counter.
+When an executor decrements the counter to zero, it sets a global boolean variable that is checked by each executor thread when it has no work.
+Once a executor threads sees the flag is set it stops running.
+After all executors stop, the actor system shutdown is complete.
 
 \subsection{Copy Queue}\label{s:copyQueue}
+Unfortunately, the frequent allocation of envelopes for each send results in heavy contention on the memory allocator.
+This contention is reduced using a novel data structure, called a \Newterm{copy queue}.
 The copy queue is a thin layer over a dynamically sized array that is designed with the envelope use case in mind.
-A copy queue supports the typical queue operations of push/pop but in a different way than a typical array based queue.
-The copy queue is designed to take advantage of the \gls{gulp}ing pattern.
-As such, the amortized runtime cost of each push/pop operation for the copy queue is $O(1)$.
+A copy queue supports the typical queue operations of push/pop but in a different way from a typical array-based queue.
+
+The copy queue is designed to take advantage of the \gls{gulp}ing pattern, giving an amortized runtime cost for each push/pop operation of $O(1)$.
 In contrast, a na\"ive array-based queue often has either push or pop cost $O(n)$ and the other cost $O(1)$ since one of the operations requires shifting the elements of the queue.
 Since the executor threads gulp a queue to operate on it locally, this creates a usage pattern where all elements are popped from the copy queue without any interleaved pushes.
@@ -372,5 +424,5 @@
 For many workload, the copy queues grow in size to facilitate the average number of messages in flight and there is no further dynamic allocations.
 One downside of this approach that more storage is allocated than needed, \ie each copy queue is only partially full.
-Comparatively, the individual envelope allocations of a list based queue mean that the actor system always uses the minimum amount of heap space and cleans up eagerly.
+Comparatively, the individual envelope allocations of a list-based queue mean that the actor system always uses the minimum amount of heap space and cleans up eagerly.
 Additionally, bursty workloads can cause the copy queues to allocate a large amounts of space to accommodate the peaks of the throughput, even if most of that storage is not needed for the rest of the workload's execution.
 
@@ -378,72 +430,76 @@
 Initially, the memory reclamation na\"ively reclaims one index of the array per \gls{gulp}, if the array size is above a low fixed threshold.
 However, this approach has a problem.
-The high memory usage watermark nearly doubled!
-The issue can easily be highlighted with an example.
+The high memory watermark nearly doubled!
+The issue is highlighted with an example.
 Assume a fixed throughput workload, where a queue never has more than 19 messages at a time.
 If the copy queue starts with a size of 10, it ends up doubling at some point to size 20 to accommodate 19 messages.
 However, after 2 gulps and subsequent reclamations the array size is 18.
 The next time 19 messages are enqueued, the array size is doubled to 36!
-To avoid this issue a second check is added.
-Each copy queue now tracks the utilization of its array size.
+To avoid this issue, a second check is added.
 Reclamation only occurs if less than half of the array is utilized.
-In doing this, the reclamation scheme is able to achieve a lower high-watermark and a lower overall memory utilization compared to the non-reclamation copy queues.
-However, the use of copy queues still incurs a higher memory cost than list-based queueing.
-With the inclusion of a memory reclamation scheme the increase in memory usage is reasonable considering the performance gains and is discussed further in Section~\ref{s:actor_perf}.
+This check achieves a lower total storage and overall memory utilization compared to the non-reclamation copy queues.
+However, the use of copy queues still incurs a higher memory cost than list-based queueing, but the increase in memory usage is reasonable considering the performance gains \see{Section~\ref{s:actor_perf}}.
 
 \section{Work Stealing}\label{s:steal}
-Work stealing is a scheduling strategy that attempts to load balance, and increase resource utilization by having idle threads steal work.
-There are many parts that make up a work stealing actor scheduler, but the two that will be highlighted in this work are the stealing mechanism and victim selection.
-
-% C_TODO enter citation for langs
+Work stealing is a scheduling strategy to provide \Newterm{load balance}.
+The goal is to increase resource utilization by having idle threads steal work from working threads.
+While there are multiple parts in work-stealing scheduler, the two important components are victim selection and the stealing mechanism.
+
 \subsection{Stealing Mechanism}
-In this discussion of work stealing the worker being stolen from will be referred to as the \textbf{victim} and the worker stealing work will be called the \textbf{thief}.
-The stealing mechanism presented here differs from existing work stealing actor systems due the inverted actor system.
-Other actor systems such as Akka \cite{} and CAF \cite{} have work stealing, but since they use an classic actor system that is actor-centric, stealing work is the act of stealing an actor from a dequeue.
-As an example, in CAF, the sharded actor queue is a set of double ended queues (dequeues).
-Whenever an actor is moved to a ready queue, it is inserted into a worker's dequeue.
+In work stealing, the stealing worker is called the \Newterm{thief} and the stolen-from worker is called the \Newterm{victim}.
+The stealing mechanism presented here differs from existing work-stealing actor-systems because of the message-centric (inverted) actor-system.
+Other actor systems, such as Akka~\cite{Akka} and CAF~\cite{CAF}, have work stealing, but use an actor-centric system where stealing is dequeuing from a non-empty ready-queue to an empty ready-queue.
+As an example, in CAF, the sharded actor queue is a set of double-ended queues (dequeues).
+When an actor has messages, it is inserted into a worker's dequeue (ready queue).
 Workers then consume actors from the dequeue and execute their behaviours.
 To steal work, thieves take one or more actors from a victim's dequeue.
-This action creates contention on the dequeue, which can slow down the throughput of the victim.
-The notion of which end of the dequeue is used for stealing, consuming, and inserting is not discussed since it isn't relevant.
-By the pigeon hole principle there are three dequeue operations (push/victim pop/thief pop) that can occur concurrently and only two ends to a dequeue, so work stealing being present in a dequeue based system will always result in a potential increase in contention on the dequeues.
+By the pigeon hole principle, there are three dequeue operations (push/victim pop/thief pop) that can occur concurrently and only two ends to a dequeue, so work stealing in a dequeue-based system always results in a potential increase in contention on the dequeues.
+This contention can slows down the victim's throughput.
+Note, which end of the dequeue is used for stealing, consuming, and inserting is not discussed since the largest cost is the mutual exclusion and its duration for safely performing the queue operations.
+
+Work steal now becomes queue stealing, where an entire actor/message queue is stolen, which trivially preserves message ordering in a queue \see{Section~\ref{s:steal}}.
 
 % C_TODO: maybe insert stealing diagram
 
-In \CFA, the actor work stealing implementation is unique.
-While other systems are concerned with stealing actors, the \CFA actor system steals queues.
-This is a result of \CFA's use of the inverted actor system.
-The goal of the \CFA actor work stealing mechanism is to have a zero-victim-cost stealing mechanism.
-This does not means that stealing has no cost.
-This goal is to ensure that stealing work does not impact the performance of victim workers.
-This means that thieves can not contend with victims, and that victims should perform no stealing related work unless they become a thief.
-In theory this goal is not achieved, but results will be presented that show the goal is achieved in practice.
-In \CFA's actor system workers own a set of sharded queues which they iterate over and gulp.
-If a worker has iterated over the queues they own twice without finding any work, they try to steal a queue from another worker.
-Stealing a queue is done wait-free with a few atomic instructions that can only create contention with other stealing workers.
-To steal a queue a worker does the following:
+In \CFA, the actor work-stealing implementation is unique because of the message-centric system.
+In this system, it is impractical to steal actors because an actor's messages are distributed in temporal order along the message queue.
+To ensure sequential actor execution and FIFO message delivery, actor stealing requires finding and removing all of an actor's messages, and inserting them consecutively in another message queue.
+This operation is $O(N)$ with a non-trivial constant.
+The only way for work stealing to become practical is to shard the message queue, which also reduces contention, and steal queues to eliminate queue searching.
+
+Given queue stealing, the goal is to have a zero-victim-cost stealing mechanism, which does not mean stealing has no cost.
+It means work stealing does not affect the performance of the victim worker.
+The implication is that thieves cannot contend with a victim, and that a victim should perform no stealing related work unless it becomes a thief.
+In theory, this goal is not achievable, but results show the goal is achieved in practice.
+
+In \CFA's actor system, workers own a set of sharded queues, which they iterate over and gulp.
+If a worker has iterated over its message queues twice without finding any work, it tries to steal a queue from another worker.
+Stealing a queue is done wait-free with a few atomic instructions that can only create contention with other stealing workers, not the victim.
+To steal a queue, a worker does the following:
 \begin{enumerate}[topsep=5pt,itemsep=3pt,parsep=0pt]
 \item
-The thief chooses a victim.
+The thief chooses a victim, which is trivial because all workers are stored in a shared array.
 
 \item
 The thief starts at a random index in the array of the victim's queues and searches for a candidate queue.
-A candidate queue is any queue that is not empty, is not being stolen by another thief, and is not being processed by the victim.
-These are not strictly enforced rules.
-The candidate is identified non-atomically and as such queues that do not satisfy these rules may be stolen.
-However, steals that do not meet these requirements do not affect correctness so they are allowed and do not constitute failed steals as the queues will still be swapped.
-
-
-\item
-Once a candidate queue is chosen, the thief attempts a wait-free swap of the victim's queue and a random on of the thief's queues.
-This swap can fail.
-If the swap is successful the thief swaps the two queues.
-If the swap fails, another thief must have attempted to steal one of the two queues being swapped.
-Failing to steal is good in this case since stealing a queue that was just swapped would likely result in stealing an empty queue.
+A candidate queue is any non-empty queue not being processed by the victim and not being stolen by another thief.
+These rules are not strictly enforced.
+A candidate is identified non-atomically, and as such, queues that do not satisfy these rules may be stolen.
+However, steals not meeting the rules do not affect correctness and do not constitute failed steals as the queue is always swapped.
+
+\item
+Once a candidate queue is chosen, the thief attempts a wait-free swap of a victim's queue to a random empty thief queue.
+If the swap successes, the steal is completed.
+If the swap fails, the victim may have been gulping that message queue or another thief must have attempted to steal the victim's queue.
+In either case, that message queue is highly likely to be empty.
+
+\item
+Once a thief fails or succeeds in stealing a queue, it iterates over its messages queues again because new messages may have arrived during stealing.
+Stealing is only repeated after two consecutive iterations over its owned queues without finding work.
 \end{enumerate}
 
-Once a thief fails or succeeds in stealing a queue, it goes back to its own set of queues and iterates over them again.
-It will only try to steal again once it has completed two consecutive iterations over its owned queues without finding any work.
 The key to the stealing mechanism is that the queues can still be operated on while they are being swapped.
-This eliminates any contention between thieves and victims.
+This functionality eliminates any contention among thieves and victims.
+
 The first key to this is that actors and workers maintain two distinct arrays of references to queues.
 Actors will always receive messages via the same queues.
@@ -594,6 +650,4 @@
 
 \subsection{Stealing Guarantees}
-
-% C_TODO insert graphs for each proof
 Given that the stealing operation can potentially fail, it is important to discuss the guarantees provided by the stealing implementation.
 Given a set of $N$ swaps a set of connected directed graphs can be constructed where each vertex is a queue and each edge is a swap directed from a thief queue to a victim queue.
@@ -737,4 +791,6 @@
 Since the @Finished@ allocation status is unused for messages, it is used internally to detect if a message has been sent.
 Deallocating a message without sending it could indicate to a user that they are touching freed memory later, or it could point out extra allocations that could be removed.
+\item Detection of messages sent but not received
+As discussed in Section~\ref{s:executor}, once all actors have terminated shutdown is communicated to executor threads via a status flag. Upon termination the executor threads check their queues to see if any contain messages. If they do, an error is reported. Messages being sent but not received means that their allocation action did not occur and their payload was not delivered. Missing the allocation action can lead to memory leaks and missed payloads can cause unpredictable behaviour. Detecting this can indicate a race or logic error in the user's code.
 \end{itemize}