Index: doc/theses/colby_parsons_MMAth/text/waituntil.tex
===================================================================
--- doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision bcc56c93e6f5177376fcef0b7fdab47f0538672f)
+++ doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision 847ab8f8121e19ac3b7f0aa27361926c67b12c62)
@@ -6,106 +6,259 @@
 
 Consider the following motivating problem.
-There are @N@ stalls (resources) in a bathroom and there are @M@ people (threads).
+There are $N$ stalls (resources) in a bathroom and there are $M$ people (threads) using the bathroom.
 Each stall has its own lock since only one person may occupy a stall at a time.
-Humans tend to solve this problem in the following way.
+Humans solve this problem in the following way.
 They check if all of the stalls are occupied.
-If not they enter and claim an available stall.
-If they are all occupied, the people queue and watch the stalls until one is free and then enter and lock the stall.
-This solution can be implemented on a computer easily if all threads are waiting on all stalls and agree to queue.
+If not, they enter and claim an available stall.
+If they are all occupied, people queue and watch the stalls until one is free, and then enter and lock the stall.
+This solution can be implemented on a computer easily, if all threads are waiting on all stalls and agree to queue.
+
 Now the problem is extended.
-Some stalls are wheelchair accessible, some stalls are dirty and other stalls are clean.
-Each person (thread) may choose some subset of dirty, clean and accessible stalls that they want to wait for.
-Immediately the problem becomes much more difficult.
-A single queue no longer fully solves the problem: What happens when there is a stall available that the person at the front of the queue will not choose?
-The naive solution to this problem has each thread to spin indefinitely continually checking the stalls until an suitable one is free.
-This is not good enough since this approach wastes cycles and results in no fairness among threads waiting for stalls as a thread will jump in the first stall available without any regard to other waiting threads.
-Waiting for the first stall (resource) available without spinning is an example of \gls{synch_multiplex}, the ability to wait synchronously for a resource or set of resources.
+Some stalls are wheelchair accessible and some stalls have specific sexual orientation.
+Each person (thread) may be limited to only one kind of stall or may choose among different kinds of stalls that match their criteria.
+Immediately, the problem becomes more difficult.
+A single queue no longer fully solves the problem.
+What happens when there is a stall available that the person at the front of the queue cannot choose?
+The na\"ive solution has each thread spin indefinitely continually checking the every matching kind of stall(s) until a suitable one is free.
+This approach is insufficient since it wastes cycles and results in unfairness among waiting threads as a thread can acquire the first matching stall without regard to the waiting time of other threads.
+Waiting for the first appropriate stall (resource) that becomes available without spinning is an example of \gls{synch_multiplex}: the ability to wait synchronously for one or more resources based on some selection criteria.
 
 \section{History of Synchronous Multiplexing}
 There is a history of tools that provide \gls{synch_multiplex}.
-Some well known \gls{synch_multiplex} tools include unix system utilities: select(2)\cite{linux:select}, poll(2)\cite{linux:poll}, and epoll(7)\cite{linux:epoll}, and the select statement provided by Go\cite{go:selectref}.
-
-The theory surrounding \gls{synch_multiplex} was largely introduced by Hoare in his 1985 CSP book \cite{Hoare85} and his later work with Roscoe on the theoretical language Occam\cite{Roscoe88}.
-The work on Occam in \cite{Roscoe88} calls their \gls{synch_multiplex} primitive ALT, which waits for one resource to be available and then executes a corresponding block of code.
-Waiting for one resource out of a set of resources can be thought of as a logical exclusive-or over the set of resources.
-Both CSP and Occam include \Newterm{guards} for communication channels and the ability to wait for a single channel to be ready out of a set of channels.
+Some well known \gls{synch_multiplex} tools include Unix system utilities: @select@~\cite{linux:select}, @poll@~\cite{linux:poll}, and @epoll@~\cite{linux:epoll}, and the @select@ statement provided by Go~\cite{go:selectref}, Ada~\cite[\S~9.7]{Ada16}, and \uC~\cite[\S~3.3.1]{uC++}.
+The concept and theory surrounding \gls{synch_multiplex} was introduced by Hoare in his 1985 book, Communicating Sequential Processes (CSP)~\cite{Hoare85},
+\begin{quote}
+A communication is an event that is described by a pair $c.v$ where $c$ is the name of the channel on which the communication takes place and $v$ is the value of the message which passes.~\cite[p.~113]{Hoare85}
+\end{quote}
+The ideas in CSP were implemented by Roscoe and Hoare in the language Occam~\cite{Roscoe88}.
+
+Both CSP and Occam include the ability to wait for a \Newterm{choice} among receiver channels and \Newterm{guards} to toggle which receives are valid.
+For example,
+\begin{cfa}[mathescape]
+(@G1@(x) $\rightarrow$ P @|@ @G2@(y) $\rightarrow$ Q )
+\end{cfa}
+waits for either channel @x@ or @y@ to have a value, if and only guards @G1@ and @G2@ are true;
+if only one guard is true, only one channel receives, and if both guards are false, no receive occurs.
+% extended CSP with a \gls{synch_multiplex} construct @ALT@, which waits for one resource to be available and then executes a corresponding block of code.
+In detail, waiting for one resource out of a set of resources can be thought of as a logical exclusive-or over the set of resources.
 Guards are a conditional operator similar to an @if@, except they apply to the resource being waited on.
-If a guard is false then the resource it guards is considered to not be in the set of resources being waited on.
-Guards can be simulated using if statements, but to do so requires \[2^N\] if statements, where @N@ is the number of guards.
-The equivalence between guards and exponential if statements comes from an Occam ALT statement rule~\cite{Roscoe88}, which is presented in \CFA syntax in Figure~\ref{f:wu_if}.
-Providing guards allows for easy toggling of waituntil clauses without introducing repeated code.
-
-\begin{figure}
-\begin{cfa}
-// CFA's guards use the keyword 'when'
-when( predicate ) waituntil( A ) {} 
-or waituntil( B ) {}
-// ===
-if ( predicate ) {
-    waituntil( A ) {}
-    or waituntil( B ) {}
-} else {
-    waituntil( B ) {}
+If a guard is false, then the resource it guards is not in the set of resources being waited on.
+If all guards are false, the ALT does nothing and the thread continues.
+Guards can be simulated using @if@ statements as shown in~\cite[rule~2.4, p~183]{Roscoe88}
+\begin{lstlisting}[basicstyle=\rm,mathescape]
+ALT( $b$ & $g$ $P$, $G$ ) = IF ( $b$ ALT($\,g$ $P$, $G$ ), $\neg\,$b ALT( $G$ ) )			 (boolean guard elim).
+\end{lstlisting}
+but require $2^N-1$ @if@ statements, where $N$ is the number of guards.
+The exponential blowup comes from applying rule 2.4 repeatedly, since it works on one guard at a time.
+Figure~\ref{f:wu_if} shows an example of applying rule 2.4 for three guards.
+Also, notice the additional code duplication for statements @S1@, @S2@, and @S3@.
+
+\begin{figure}
+\centering
+\begin{lrbox}{\myboxA}
+\begin{cfa}
+when( G1 )
+	waituntil( R1 ) S1 
+or when( G2 )
+	waituntil( R2 ) S2
+or when( G3 )
+	waituntil( R3 ) S3
+
+
+
+
+
+
+
+\end{cfa}
+\end{lrbox}
+
+\begin{lrbox}{\myboxB}
+\begin{cfa}
+if ( G1 )
+	if ( G2 )
+		if ( G3 ) waituntil( R1 ) S1 or waituntil( R2 ) S2 or waituntil( R3 ) S3
+		else waituntil( R1 ) S1 or waituntil( R2 ) S2
+	else
+		if ( G3 ) waituntil( R1 ) S1 or waituntil( R3 ) S3
+		else waituntil( R1 ) S1
+else
+	if ( G2 )
+		if ( G3 ) waituntil( R2 ) S2 or waituntil( R3 ) S3
+		else waituntil( R2 ) S2
+	else
+		if ( G3 ) waituntil( R3 ) S3
+\end{cfa}
+\end{lrbox}
+
+\subfloat[Guards]{\label{l:guards}\usebox\myboxA}
+\hspace*{5pt}
+\vrule
+\hspace*{5pt}
+\subfloat[Simulated Guards]{\label{l:simulated_guards}\usebox\myboxB}
+\caption{\CFA guard simulated with \lstinline{if} statement.}
+\label{f:wu_if}
+\end{figure}
+
+When discussing \gls{synch_multiplex} implementations, the resource being multiplexed is important.
+While CSP wait on channels, the earliest known implementation of synch\-ronous multiplexing is Unix's @select@~\cite{linux:select}, multiplexing over file descriptors.
+The @select@ system-call is passed three sets of file descriptors (read, write, exceptional) to wait on and an optional timeout.
+@select@ blocks until either some subset of file descriptors are available or the timeout expires.
+All file descriptors that are ready are returned by modifying the argument sets to only contain the ready descriptors.
+
+This early implementation differs from the theory presented in CSP: when the call from @select@ returns it may provide more than one ready file descriptor.
+As such, @select@ has logical-or multiplexing semantics, whereas the theory described exclusive-or semantics.
+It is possible to achieve exclusive-or semantics with @select@ by arbitrarily operating on only one of the returned descriptors.
+@select@ passes the interest set of file descriptors between application and kernel in the form of a worst-case sized bit-mask, where the worst-case is the largest numbered file descriptor.
+@poll@ reduces the size of the interest sets changing from a bit mask to a linked data structures, independent of the file-descriptor values.
+@epoll@ further reduces the data passed per call by keeping the interest set in the kernel, rather than supplying it on every call.
+
+These early \gls{synch_multiplex} tools interact directly with the operating system and others are used to communicate among processes.
+Later, \gls{synch_multiplex} started to appear in applications, via programming languages, to support fast multiplexed concurrent communication among threads.
+An early example of \gls{synch_multiplex} is the @select@ statement in Ada~\cite[\S~9.7]{Ichbiah79}.
+The @select@ statement in Ada allows a task object, with their own threads, to multiplex over a subset of asynchronous calls its methods.
+The Ada @select@ statement has the same exclusive-or semantics and guards as Occam ALT;
+however, it multiplexes over methods rather than channels.
+
+\begin{figure}
+\begin{lstlisting}[language=ada,literate=]
+task type buffer is -- thread
+	... -- buffer declarations
+	count : integer := 0;
+begin -- thread starts here
+	loop
+		select
+			when count < Size => -- guard
+			accept insert( elem : in ElemType ) do  -- method
+				... -- add to buffer
+				count := count + 1;
+			end;
+			-- executed if this accept called
+		or
+			when count > 0 => -- guard
+			accept remove( elem : out ElemType ) do  -- method
+				... --remove and return from buffer via parameter
+				count := count - 1;
+			end;
+			-- executed if this accept called
+		or delay 10.0;  -- unblock after 10 seconds without call
+		or else -- do not block, cannot appear with delay
+		end select;
+	end loop;
+end buffer;
+var buf : buffer; -- create task object and start thread in task body
+\end{lstlisting}
+\caption{Ada Bounded Buffer}
+\label{f:BB_Ada}
+\end{figure}
+
+Figure~\ref{f:BB_Ada} shows the outline of a bounded buffer implemented with Ada task.
+Note, a task method is associated with the \lstinline[language=ada]{accept} clause of the \lstinline[language=ada]{select} statement, rather than being a separate routine.
+The thread executing the loop in the task body blocks at the \lstinline[language=ada]{select} until a call occurs to @insert@ or @remove@.
+Then the appropriate \lstinline[language=ada]{accept} method is run with the called arguments.
+Hence, the @select@ statement provides rendezvous points for threads, rather than providing channels with message passing.
+The \lstinline[language=ada]{select} statement also provides a timeout and @else@ (nonblocking), which changes synchronous multiplexing to asynchronous.
+Now the thread polls rather than blocks.
+
+Another example of programming-language \gls{synch_multiplex} is Go using a @select@ statement with channels~\cite{go:selectref}.
+Figure~\ref{l:BB_Go} shows the outline of a bounded buffer implemented with a Go routine.
+Here two channels are used for inserting and removing by client producers and consumers, respectively.
+(The @term@ and @stop@ channels are used to synchronize with the program main.)
+Go's @select@ has the same exclusive-or semantics as the ALT primitive from Occam and associated code blocks for each clause like ALT and Ada.
+However, unlike Ada and ALT, Go does not provide guards for the \lstinline[language=go]{case} clauses of the \lstinline[language=go]{select}.
+Go also provides a timeout via a channel and a @default@ clause like Ada @else@ for asynchronous multiplexing.
+
+\begin{figure}
+\centering
+
+\begin{lrbox}{\myboxA}
+\begin{lstlisting}[language=go,literate=]
+func main() {
+	insert := make( chan int, Size )
+	remove := make( chan int, Size )
+	term := make( chan string )
+	finish := make( chan string )
+
+	buf := func() {
+		L: for {
+			select { // wait for message
+			  case i = <- buffer:
+			  case <- term: break L
+			}
+			remove <- i;
+		}
+		finish <- "STOP" // completion
+	}
+	go buf() // start thread in buf
 }
-\end{cfa}
-\caption{Occam's guard to if statement equivalence shown in \CFA syntax.}
-\label{f:wu_if}
-\end{figure}
-
-When discussing \gls{synch_multiplex} implementations, one must discuss the resources being multiplexed.
-While the aforementioned theory waits on channels, the earliest known implementation of a synchronous multiplexing tool, Unix's select(2)\cite{linux:select}, is multiplexed over file descriptors.
-The select(2) system call is passed three sets of file descriptors (read, write, exceptional) to wait on and an optional timeout.
-Select(2) will block until either some subset of file descriptors are available or the timeout expires.
-All file descriptors that are ready will be returned by modifying the argument sets to only contain the ready descriptors.
-This early implementation differs from the theory presented in Occam and CSP; when the call from select(2) returns it may provide more than one ready file descriptor.
-As such, select(2) has logical-or multiplexing semantics, whereas the theory described exclusive-or semantics.
-This is not a drawback.
-A user can easily achieve exclusive-or semantics with select by arbitrarily choosing only one of the returned descriptors to operate on.
-Select(2) was followed by poll(2), which was later followed by epoll(7), with each successor improving upon drawbacks in their predecessors.
-The syscall poll(2) improved on select(2) by allowing users to monitor descriptors with numbers higher than 1024 which was not supported by select.
-Epoll(7) then improved on poll(2) to return the set of file descriptors; when one or more descriptors became available poll(2) would return the number of availables descriptors, but would not indicate which descriptors were ready.
-
-It is worth noting these \gls{synch_multiplex} tools mentioned so far interact directly with the operating system and are often used to communicate between processes.
-Later, \gls{synch_multiplex} started to appear in user-space to support fast multiplexed concurrent communication between threads.
-An early example of \gls{synch_multiplex} is the select statement in Ada~\cite[\S~9.7]{Ichbiah79}.
-The select statement in Ada allows a task to multiplex over some subset of its own methods that it would like to @accept@ calls to.
-Tasks in Ada are essentially objects that have their own thread, and as such have methods, fields, etc.
-The Ada select statement has the same exclusive-or semantics and guards as ALT from Occam, however it multiplexes over methods on rather than multiplexing over channels.
-A code block is associated with each @accept@, and the method that is accepted first has its corresponding code block run after the task unblocks.
-In this way the select statement in Ada provides rendezvous points for threads, rather than providing some resource through message passing.
-The select statement in Ada also supports an optional timeout with the same semantics as select(2), and provides an @else@.
-The @else@ changes the synchronous multiplexing to asynchronous multiplexing.
-If an @else@ clause is in a select statement and no calls to the @accept@ed methods are immediately available the code block associated with the @else@ is run and the task does not block.
-
-A popular example of user-space \gls{synch_multiplex} is Go with their select statement~\cite{go:selectref}.
-Go's select statement operates on channels and has the same exclusive-or semantics as the ALT primitive from Occam, and has associated code blocks for each clause like ALT and Ada.
-However, unlike Ada and ALT, Go does not provide any guards for their select statement cases.
-Go provides a timeout utility and also provides a @default@ clause which has the same semantics as Ada's @else@ clause.
-
-\uC provides \gls{synch_multiplex} over futures with their @_Select@ statement and Ada-style \gls{synch_multiplex} over monitor and task methods with their @_Accept@ statement~\cite{uC++}.
-Their @_Accept@ statement builds upon the select statement offered by Ada, by offering both @and@ and @or@ semantics, which can be used together in the same statement.
-These semantics are also supported for \uC's @_Select@ statement.
-This enables fully expressive \gls{synch_multiplex} predicates.
-
-There are many other languages that provide \gls{synch_multiplex}, including Rust's @select!@ over futures~\cite{rust:select}, OCaml's @select@ over channels~\cite{ocaml:channel}, and C++14's @when_any@ over futures~\cite{cpp:whenany}.
-Note that while C++14 and Rust provide \gls{synch_multiplex}, their implementations leave much to be desired as they both rely on busy-waiting polling to wait on multiple resources.
+
+
+
+
+\end{lstlisting}
+\end{lrbox}
+
+\begin{lrbox}{\myboxB}
+\begin{lstlisting}[language=uC++=]
+_Task BoundedBuffer {
+	... // buffer declarations
+	int count = 0;
+  public:
+	void insert( int elem ) {
+		... // add to buffer
+		count += 1;
+	}
+	int remove() {
+		... // remove and return from buffer
+		count -= 1;
+	}
+  private:
+	void main() {
+		for ( ;; ) {
+			_Accept( ~buffer ) break;
+			or _When ( count < Size ) _Accept( insert );
+			or _When ( count > 0 ) _Accept( remove );
+		}
+	}
+};
+buffer buf; // start thread in main method
+\end{lstlisting}
+\end{lrbox}
+
+\subfloat[Go]{\label{l:BB_Go}\usebox\myboxA}
+\hspace*{5pt}
+\vrule
+\hspace*{5pt}
+\subfloat[\uC]{\label{l:BB_uC++}\usebox\myboxB}
+
+\caption{Bounded Buffer}
+\label{f:AdaMultiplexing}
+\end{figure}
+
+Finally, \uC provides \gls{synch_multiplex} with Ada-style @select@ over monitor and task methods with the @_Accept@ statement~\cite[\S~2.9.2.1]{uC++}, and over futures with the @_Select@ statement~\cite[\S~3.3.1]{uC++}.
+The @_Select@ statement extends the ALT/Go @select@ by offering both @and@ and @or@ semantics, which can be used together in the same statement.
+Both @_Accept@ and @_Select@ statements provide guards for multiplexing clauses, as well as, timeout, and @else@ clauses.
+
+There are other languages that provide \gls{synch_multiplex}, including Rust's @select!@ over futures~\cite{rust:select}, OCaml's @select@ over channels~\cite{ocaml:channel}, and C++14's @when_any@ over futures~\cite{cpp:whenany}.
+Note that while C++14 and Rust provide \gls{synch_multiplex}, the implementations leave much to be desired as both rely on polling to wait on multiple resources.
 
 \section{Other Approaches to Synchronous Multiplexing}
-To avoid the need for \gls{synch_multiplex}, all communication between threads/processes has to come from a single source.
-One key example is Erlang, in which each process has a single heterogenous mailbox that is the sole source of concurrent communication, removing the need for \gls{synch_multiplex} as there is only one place to wait on resources.
-In a similar vein, actor systems circumvent the \gls{synch_multiplex} problem as actors are traditionally non-blocking, so they will never block in a behaviour and only block when waiting for the next message.
+
+To avoid the need for \gls{synch_multiplex}, all communication among threads/processes must come from a single source.
+For example, in Erlang each process has a single heterogeneous mailbox that is the sole source of concurrent communication, removing the need for \gls{synch_multiplex} as there is only one place to wait on resources.
+Similar, actor systems circumvent the \gls{synch_multiplex} problem as actors only block when waiting for the next message never in a behaviour.
 While these approaches solve the \gls{synch_multiplex} problem, they introduce other issues.
-Consider the case where a thread has a single source of communication (like erlang and actor systems) wants one of a set of @N@ resources.
-It requests @N@ resources and waits for responses.
-In the meantime the thread may receive other communication, and may either has to save and postpone the related work or discard it.
-After the thread receives one of the @N@ resources, it will continue to receive the other ones it requested, even if it does not need them.
-If the requests for the other resources need to be retracted, the burden falls on the programmer to determine how to synchronize appropriately to ensure that only one resource is delivered.
+Consider the case where a thread has a single source of communication and it wants a set of @N@ resources.
+It sequentially requests the @N@ resources and waits for each response.
+During the receives for the @N@ resources, it can receive other communication, and has to save and postpone these communications, or discard them.
+% If the requests for the other resources need to be retracted, the burden falls on the programmer to determine how to synchronize appropriately to ensure that only one resource is delivered.
 
 \section{\CFA's Waituntil Statement}
+
 The new \CFA \gls{synch_multiplex} utility introduced in this work is the @waituntil@ statement.
 There is a @waitfor@ statement in \CFA that supports Ada-style \gls{synch_multiplex} over monitor methods, so this @waituntil@ focuses on synchronizing over other resources.
-All of the \gls{synch_multiplex} features mentioned so far are monomorphic, only supporting one resource to wait on: select(2) supports file descriptors, Go's select supports channel operations, \uC's select supports futures, and Ada's select supports monitor method calls.
-The waituntil statement in \CFA is polymorphic and provides \gls{synch_multiplex} over any objects that satisfy the trait in Figure~\ref{f:wu_trait}.
-No other language provides a synchronous multiplexing tool polymorphic over resources like \CFA's waituntil.
+All of the \gls{synch_multiplex} features mentioned so far are monomorphic, only waiting on one kind of resource: Unix @select@ supports file descriptors, Go's @select@ supports channel operations, \uC's @select@ supports futures, and Ada's @select@ supports monitor method calls.
+The \CFA @waituntil@ is polymorphic and provides \gls{synch_multiplex} over any objects that satisfy the trait in Figure~\ref{f:wu_trait}.
+No other language provides a synchronous multiplexing tool polymorphic over resources like \CFA's @waituntil@.
 
 \begin{figure}
@@ -113,20 +266,22 @@
 forall(T & | sized(T))
 trait is_selectable {
-    // For registering a waituntil stmt on a selectable type
-    bool register_select( T &, select_node & );
-
-    // For unregistering a waituntil stmt from a selectable type
-    bool unregister_select( T &, select_node & );
-
-    // on_selected is run on the selecting thread prior to executing the statement associated with the select_node
-    bool on_selected( T &, select_node & );
+	// For registering a waituntil stmt on a selectable type
+	bool register_select( T &, select_node & );
+
+	// For unregistering a waituntil stmt from a selectable type
+	bool unregister_select( T &, select_node & );
+
+	// on_selected is run on the selecting thread prior to executing
+	// the statement associated with the select_node
+	bool on_selected( T &, select_node & );
 };
 \end{cfa}
-\caption{Trait for types that can be passed into \CFA's waituntil statement.}
+\caption{Trait for types that can be passed into \CFA's \lstinline{waituntil} statement.}
 \label{f:wu_trait}
 \end{figure}
 
-Currently locks, channels, futures and timeouts are supported by the waituntil statement, but this will be expanded as other use cases arise.
-The @waituntil@ statement supports guarded clauses, like Ada, and Occam, supports both @or@, and @and@ semantics, like \uC, and provides an @else@ for asynchronous multiplexing. An example of \CFA waituntil usage is shown in Figure~\ref{f:wu_example}. In Figure~\ref{f:wu_example} the waituntil statement is waiting for either @Lock@ to be available or for a value to be read from @Channel@ into @i@ and for @Future@ to be fulfilled. 
+Currently locks, channels, futures and timeouts are supported by the @waituntil@ statement, and can be expanded through the @is_selectable@ trait as other use-cases arise.
+The @waituntil@ statement supports guarded clauses, both @or@ and @and@ semantics, and provides an @else@ for asynchronous multiplexing.
+Figure~\ref{f:wu_example} shows a \CFA @waituntil@ usage, which is waiting for either @Lock@ to be available \emph{or} for a value to be read from @Channel@ into @i@ \emph{and} for @Future@ to be fulfilled \emph{or} a timeout of one second. 
 
 \begin{figure}
@@ -140,4 +295,6 @@
 or when( i == 0 ) waituntil( i << Channel ) { ... }
 and waituntil( Future ) { ... }
+or waituntil( timeout( 1`s ) ) { ... }
+// else { ... }
 \end{cfa}
 \caption{Example of \CFA's waituntil statement}
@@ -146,81 +303,120 @@
 
 \section{Waituntil Semantics}
-There are two parts of the waituntil semantics to discuss, the semantics of the statement itself, \ie @and@, @or@, @when@ guards, and @else@ semantics, and the semantics of how the waituntil interacts with types like channels, locks and futures.
-
-\subsection{Waituntil Statement Semantics}
-The @or@ semantics are the most straightforward and nearly match those laid out in the ALT statement from Occam, the clauses have an exclusive-or relationship where the first one to be available will be run and only one clause is run.
-\CFA's @or@ semantics differ from ALT semantics in one respect, instead of randomly picking a clause when multiple are available, the clause that appears first in the order of clauses will be picked.
-\eg in the following example, if @foo@ and @bar@ are both available, @foo@ will always be selected since it comes first in the order of @waituntil@ clauses.
-\begin{cfa}
-future(int) bar;
-future(int) foo;
+
+The @waituntil@ semantics has two parts: the semantics of the statement itself, \ie @and@, @or@, @when@ guards, and @else@ semantics, and the semantics of how the @waituntil@ interacts with types like channels, locks and futures.
+
+\subsection{Statement Semantics}
+
+The @or@ semantics are the most straightforward and nearly match those laid out in the ALT statement from Occam.
+The clauses have an exclusive-or relationship where the first available one is run and only one clause is run.
+\CFA's @or@ semantics differ from ALT semantics: instead of randomly picking a clause when multiple are available, the first clause in the @waituntil@ that is available is executed.
+For example, in the following example, if @foo@ and @bar@ are both available, @foo@ is always selected since it comes first in the order of @waituntil@ clauses.
+\begin{cfa}
+future(int) bar, foo;
+
 waituntil( foo ) { ... }
 or waituntil( bar ) { ... }
 \end{cfa}
 
-The @and@ semantics match the @and@ semantics used by \uC.
-When multiple clauses are joined by @and@, the @waituntil@ will make a thread wait for all to be available, but will run the corresponding code blocks \emph{as they become available}.
-As @and@ clauses are made available, the thread will be woken to run those clauses' code blocks and then the thread will wait again until all clauses have been run. 
-This allows work to be done in parallel while synchronizing over a set of resources, and furthermore gives a good reason to use the @and@ operator.
-If the @and@ operator waited for all clauses to be available before running, it would not provide much more use that just acquiring those resources one by one in subsequent lines of code.
-The @and@ operator binds more tightly than the @or@ operator.
-To give an @or@ operator higher precedence brackets can be used.
-\eg the following waituntil unconditionally waits for @C@ and one of either @A@ or @B@, since the @or@ is given higher precendence via brackets.
-\begin{cfa}
-(waituntil( A ) { ... }
-or waituntil( B ) { ... } )
+The \CFA @and@ semantics match the @and@ semantics of \uC \lstinline[language=uC++]{_Select}.
+When multiple clauses are joined by @and@, the @waituntil@ makes a thread wait for all to be available, but still runs the corresponding code blocks \emph{as they become available}.
+When an @and@ clause becomes available, the waiting thread unblocks and runs that clause's code-block, and then the thread waits again for the next available clause or the @waituntil@ statement is now true.
+This semantics allows work to be done in parallel while synchronizing over a set of resources, and furthermore, gives a good reason to use the @and@ operator.
+If the @and@ operator waited for all clauses to be available before running, it would be the same as just acquiring those resources consecutively by a sequence of @waituntil@ statements.
+
+As for normal C expressions, the @and@ operator binds more tightly than the @or@.
+To give an @or@ operator higher precedence, parenthesis are used.
+For example, the following @waituntil@ unconditionally waits for @C@ and one of either @A@ or @B@, since the @or@ is given higher precedence via parenthesis.
+\begin{cfa}
+@(@ waituntil( A ) { ... }		// bind tightly to or
+or waituntil( B ) { ... } @)@
 and waituntil( C ) { ... }
 \end{cfa}
 
-The guards in the waituntil statement are called @when@ clauses.
-Each the boolean expression inside a @when@ is evaluated once before the waituntil statement is run.
-The guards in Occam's ALT effectively toggle clauses on and off, where a clause will only be evaluated and waited on if the corresponding guard is @true@.
-The guards in the waituntil statement operate the same way, but require some nuance since both @and@ and @or@ operators are supported.
-This will be discussed further in Section~\ref{s:wu_guards}.
-When a guard is false and a clause is removed, it can be thought of as removing that clause and its preceding operator from the statement.
-\eg in the following example the two waituntil statements are semantically the same.
-\begin{cfa}
-when(true) waituntil( A ) { ... }
-or when(false) waituntil( B ) { ... }
+The guards in the @waituntil@ statement are called @when@ clauses.
+Each boolean expression inside a @when@ is evaluated \emph{once} before the @waituntil@ statement is run.
+Like Occam's ALT, the guards toggle clauses on and off, where a @waituntil@ clause is only evaluated and waited on if the corresponding guard is @true@.
+In addition, the @waituntil@ guards require some nuance since both @and@ and @or@ operators are supported \see{Section~\ref{s:wu_guards}}.
+When a guard is false and a clause is removed, it can be thought of as removing that clause and its preceding operation from the statement.
+For example, in the following, the two @waituntil@ statements are semantically equivalent.
+
+\begin{lrbox}{\myboxA}
+\begin{cfa}
+when( true ) waituntil( A ) { ... }
+or when( false ) waituntil( B ) { ... }
 and waituntil( C ) { ... }
-// === 
+\end{cfa}
+\end{lrbox}
+
+\begin{lrbox}{\myboxB}
+\begin{cfa}
 waituntil( A ) { ... }
 and waituntil( C ) { ... }
-\end{cfa}
-
-The @else@ clause on the waituntil has identical semantics to the @else@ clause in Ada.
-If all resources are not immediately available and there is an @else@ clause, the @else@ clause is run and the thread will not block.
-
-\subsection{Waituntil Type Semantics}
-As described earlier, to support interaction with the waituntil statement a type must support the trait shown in Figure~\ref{f:wu_trait}.
-The waituntil statement expects types to register and unregister themselves via calls to @register_select@ and @unregister_select@ respectively.
+
+\end{cfa}
+\end{lrbox}
+
+\begin{tabular}{@{}lcl@{}}
+\usebox\myboxA & $\equiv$ & \usebox\myboxB
+\end{tabular}
+
+The @else@ clause on the @waituntil@ has identical semantics to the @else@ clause in Ada.
+If all resources are not immediately available and there is an @else@ clause, the @else@ clause is run and the thread continues.
+
+\subsection{Type Semantics}
+
+As mentioned, to support interaction with the @waituntil@ statement a type must support the trait in Figure~\ref{f:wu_trait}.
+The @waituntil@ statement expects types to register and unregister themselves via calls to @register_select@ and @unregister_select@, respectively.
 When a resource becomes available, @on_selected@ is run.
-Many types do not need @on_selected@, but it is provided since some types may need to perform some work or checks before the resource can be accessed in the code block.
+Many types do not need @on_selected@, but it is provided if a type needs to perform work or checks before the resource can be accessed in the code block.
 The register/unregister routines in the trait return booleans.
-The return value of @register_select@ is @true@ if the resource is immediately available, and @false@ otherwise.
-The return value of @unregister_select@ is @true@ if the corresponding code block should be run after unregistration and @false@ otherwise.
-The routine @on_selected@, and the return value of @unregister_select@ were needed to support channels as a resource.
-More detail on channels and their interaction with waituntil will be discussed in Section~\ref{s:wu_chans}.
-
-\section{Waituntil Implementation}
-The waituntil statement is not inherently complex, and can be described as a few steps.
-The complexity of the statement comes from the consideration of race conditions and synchronization needed when supporting various primitives.
-The basic steps of the waituntil statement are the following:
-
-\begin{enumerate}[topsep=5pt,itemsep=3pt,parsep=0pt]
-
+The return value of @register_select@ is @true@, if the resource is immediately available and @false@ otherwise.
+The return value of @unregister_select@ is @true@, if the corresponding code block should be run after unregistration and @false@ otherwise.
+The routine @on_selected@ and the return value of @unregister_select@ are needed to support channels as a resource.
+More detail on channels and their interaction with @waituntil@ appear in Section~\ref{s:wu_chans}.
+
+\section{\lstinline{waituntil} Implementation}
+The @waituntil@ statement is not inherently complex, and the pseudo code in presented in Figure~\ref{f:WU_Impl}.
+The complexity comes from the consideration of race conditions and synchronization needed when supporting various primitives.
+The basic steps of the @waituntil@ statement are:
+
+\begin{figure}
+\begin{cfa}
+select_nodes s[N];								 $\C[3.25in]{// declare N select nodes}$
+for ( node in s )								 $\C{// register nodes}$
+	register_select( resource, node );
+while ( statement predicate not satisfied ) {	$\C{// check predicate}$
+	// block
+	for ( resource in waituntil statement )		$\C{// run true code blocks}$
+		if ( resource is avail ) run code block
+}
+for ( resource in waituntil statement ) {
+	if ( statement predicate is run-satisfied ) break;
+	if ( resource is avail ) run code block
+}
+for ( node in s )								$\C{// deregister nodes}\CRT$
+	if (unregister_select( resource, node ) ) run code block
+\end{cfa}
+Each clause has a couple of statuses, UNSAT when not available, SAT when available and not run and RUN when it is available and the associated code block was run.
+The first while ( statement predicate not satisfied) waits until the predicate is satisfied, where UNSAT = false and SAT = true and RUN = true.
+The if ( statement predicate is run-satisfied ) considers a status of RUN = true and all other statuses to be false.
+
+\caption{\lstinline{waituntil} Implementation}
+\label{f:WU_Impl}
+\end{figure}
+
+\begin{enumerate}
 \item
-First the waituntil statement creates a @select_node@ per resource that is being waited on.
-The @select_node@ is an object that stores the waituntil data pertaining to one of the resources.
+The @waituntil@ statement declares $N$ @select_node@s, one per resource that is being waited on, which stores any @waituntil@ data pertaining to that resource.
 
 \item
-Then, each @select_node@ is then registered with the corresponding resource.
+Each @select_node@ is then registered with the corresponding resource.
 
 \item
-The thread executing the waituntil then enters a loop that will loop until the @waituntil@ statement's predicate is satisfied.
-In each iteration of the loop the thread attempts to block.
-If any clauses are satified the block will fail and the thread will proceed, otherwise the block succeeds.
+The thread executing the @waituntil@ then loops until the statement's predicate is satisfied.
+In each iteration, if the predicate is unsatisfied, the thread blocks.
+If clauses becomes satisfied, the thread unblocks, and for each satisfied the block fails and the thread proceeds, otherwise the block succeeds.
 After proceeding past the block all clauses are checked for completion and the completed clauses have their code blocks run.
-In the case where the block suceeds, the thread will be woken by the thread that marks one of the resources as available.
+In the case where the block succeeds, the thread will be woken by the thread that marks one of the resources as available.
 
 \item
@@ -228,24 +424,26 @@
 \end{enumerate}
 Pseudocode detailing these steps is presented in the following code block.
-\begin{cfa}
-select_nodes s[N]; // N select nodes
-for ( node in s )
-    register_select( resource, node );
-while( statement predicate not satisfied ) {
-    // try to block
-    for ( resource in waituntil statement )
-        if ( resource is avail ) run code block
-}
-for ( node in s )
-    unregister_select( resource, node );
-\end{cfa}
+
 These steps give a basic overview of how the statement works.
 Digging into parts of the implementation will shed light on the specifics and provide more detail.
 
 \subsection{Locks}
-Locks are one of the resources supported by the @waituntil@ statement.
-When a thread waits on multiple locks via a waituntil, it enqueues a @select_node@ in each of the lock's waiting queues.
-When a @select_node@ reaches the front of the queue and gains ownership of a lock, the blocked thread is notified.
-The lock will be held until the node is unregistered.
+
+The \CFA runtime supports a number of spinning and blocking locks, \eg semaphore, MCS, futex, Go mutex, spinlock, owner, \etc.
+Many of these locks satisfy the @is_selectable@ trait, and hence, are resources supported by the @waituntil@ statement.
+For example, the following waits until the thread has acquired lock @l1@ or locks @l2@ and @l3@.
+\begin{cfa}
+owner_lock l1, l2, l3;
+waituntil ( l1 ) { ... }
+or waituntil( l2 ) { ... }
+and waituntil( l3 ) { ... }
+\end{cfa}
+Implicitly, the @waituntil@ is calling the lock acquire for each of these locks to establish a position in the lock's queue of waiting threads.
+When the lock schedules this thread, it unblocks and performs the @waituntil@ code to determine if it can proceed.
+If it cannot proceed, it blocks again on the @waituntil@ lock, holding the acquired lock.
+
+In detail, when a thread waits on multiple locks via a @waituntil@, it enqueues a @select_node@ in each of the lock's waiting queues.
+When a @select_node@ reaches the front of the lock's queue and gains ownership, the thread blocked on the @waituntil@ is unblocked.
+Now, the lock is temporarily held by the @waituntil@ thread until the node is unregistered, versus the thread waiting on the lock
 To prevent the waiting thread from holding many locks at once and potentially introducing a deadlock, the node is unregistered right after the corresponding code block is executed.
 This prevents deadlocks since the waiting thread will never hold a lock while waiting on another resource.
@@ -253,5 +451,6 @@
 
 \subsection{Timeouts}
-Timeouts in the waituntil take the form of a duration being passed to a @sleep@ or @timeout@ call.
+
+Timeouts in the @waituntil@ take the form of a duration being passed to a @sleep@ or @timeout@ call.
 An example is shown in the following code.
 
@@ -262,17 +461,17 @@
 \end{cfa}
 
-The timeout implementation highlights a key part of the waituntil semantics, the expression inside a @waituntil()@ is evaluated once at the start of the @waituntil@ algorithm.
+The timeout implementation highlights a key part of the @waituntil@ semantics, the expression inside a @waituntil()@ is evaluated once at the start of the @waituntil@ algorithm.
 As such, calls to these @sleep@ and @timeout@ routines do not block, but instead return a type that supports the @is_selectable@ trait.
-This feature leverages \CFA's ability to overload on return type; a call to @sleep@ outside a waituntil will call a different @sleep@ that does not return a type, which will block for the appropriate duration.
+This feature leverages \CFA's ability to overload on return type; a call to @sleep@ outside a @waituntil@ will call a different @sleep@ that does not return a type, which will block for the appropriate duration.
 This mechanism of returning a selectable type is needed for types that want to support multiple operations such as channels that allow both reading and writing.
 
 \subsection{Channels}\label{s:wu_chans}
-To support both waiting on both reading and writing to channels, the operators @?<<?@ and @?>>?@ are used read and write to a channel respectively, where the lefthand operand is the value being read into/written and the righthand operand is the channel.
+To support both waiting on both reading and writing to channels, the operators @?<<?@ and @?>>?@ are used read and write to a channel respectively, where the left-hand operand is the value being read into/written and the right-hand operand is the channel.
 Channels require significant complexity to synchronously multiplex on for a few reasons.
 First, reading or writing to a channel is a mutating operation;
 If a read or write to a channel occurs, the state of the channel has changed.
 In comparison, for standard locks and futures, if a lock is acquired then released or a future is ready but not accessed, the state of the lock and the future is not permanently modified.
-In this way, a waituntil over locks or futures that completes with resources available but not consumed is not an issue.
-However, if a thread modifies a channel on behalf of a thread blocked on a waituntil statement, it is important that the corresponding waituntil code block is run, otherwise there is a potentially erroneous mismatch between the channel state and associated side effects.
+In this way, a @waituntil@ over locks or futures that completes with resources available but not consumed is not an issue.
+However, if a thread modifies a channel on behalf of a thread blocked on a @waituntil@ statement, it is important that the corresponding @waituntil@ code block is run, otherwise there is a potentially erroneous mismatch between the channel state and associated side effects.
 As such, the @unregister_select@ routine has a boolean return that is used by channels to indicate when the operation was completed but the block was not run yet.
 When the return is @true@, the corresponding code block is run after the unregister.
@@ -281,5 +480,5 @@
 It was deemed important that exclusive-or semantics were maintained when only @or@ operators were used, so this situation has been special-cased, and is handled by having all clauses race to set a value \emph{before} operating on the channel.
 This approach is infeasible in the case where @and@ and @or@ operators are used.
-To show this consider the following waituntil statement.
+To show this consider the following @waituntil@ statement.
 
 \begin{cfa}
@@ -288,6 +487,6 @@
 \end{cfa}
 
-If exclusive-or semantics were followed, this waituntil would only run the code blocks for @A@ and @B@, or the code blocks for @C@ and @D@.
-However, to race before operation completion in this case introduces a race whose complexity increases with the size of the waituntil statement.
+If exclusive-or semantics were followed, this @waituntil@ would only run the code blocks for @A@ and @B@, or the code blocks for @C@ and @D@.
+However, to race before operation completion in this case introduces a race whose complexity increases with the size of the @waituntil@ statement.
 In the example above, for @i@ to be inserted into @C@, to ensure the exclusive-or it must be ensured that @i@ can also be inserted into @D@.
 Furthermore, the race for the @or@ would also need to be won.
@@ -297,5 +496,5 @@
 This would incur a high cost for signalling threads and heavily increase contention on internal channel locks.
 Furthermore, the @waituntil@ statement is polymorphic and can support resources that do not have internal locks, which also makes this approach infeasible.
-As such, the exclusive-or semantics are lost when using both @and@ and @or@ operators since they can not be supported without significant complexity and hits to waituntil statement performance.
+As such, the exclusive-or semantics are lost when using both @and@ and @or@ operators since they can not be supported without significant complexity and hits to @waituntil@ statement performance.
 
 Channels introduce another interesting consideration in their implementation.
@@ -304,10 +503,10 @@
 When both a special-case @or@ is inserting to a channel on one thread and another thread is blocked in a special-case @or@ consuming from the same channel there is not one but two races that need to be consolidated by the inserting thread.
 (This race can also occur in the mirrored case with a blocked producer and signalling consumer.)
-For the producing thread to know that the insert succeeded, they need to win the race for their own waituntil and win the race for the other waituntil.
+For the producing thread to know that the insert succeeded, they need to win the race for their own @waituntil@ and win the race for the other @waituntil@.
 
 Go solves this problem in their select statement by acquiring the internal locks of all channels before registering the select on the channels.
 This eliminates the race since no other threads can operate on the blocked channel since its lock will be held.
-This approach is not used in \CFA since the waituntil is polymorphic.
-Not all types in a waituntil have an internal lock, and when using non-channel types acquiring all the locks incurs extra uneeded overhead.
+This approach is not used in \CFA since the @waituntil@ is polymorphic.
+Not all types in a @waituntil@ have an internal lock, and when using non-channel types acquiring all the locks incurs extra unneeded overhead.
 Instead this race is consolidated in \CFA in two phases by having an intermediate pending status value for the race.
 This race case is detectable, and if detected the thread attempting to signal will first race to set the race flag to be pending.
@@ -317,7 +516,7 @@
 This protocol ensures that signals will not be lost and that the two races can be resolved in a safe manner.
 
-Channels in \CFA have exception based shutdown mechanisms that the waituntil statement needs to support.
+Channels in \CFA have exception based shutdown mechanisms that the @waituntil@ statement needs to support.
 These exception mechanisms were what brought in the @on_selected@ routine.
-This routine is needed by channels to detect if they are closed upon waking from a waituntil statement, to ensure that the appropriate behaviour is taken.
+This routine is needed by channels to detect if they are closed upon waking from a @waituntil@ statement, to ensure that the appropriate behaviour is taken.
 
 \subsection{Guards and Statement Predicate}\label{s:wu_guards}
@@ -332,9 +531,9 @@
 To support statement guards in \uC, the tree prunes a branch if the corresponding guard is false.
 
-The \CFA waituntil statement blocks a thread until a set of resources have become available that satisfy the underlying predicate.
-The waiting condition of the waituntil statement can be represented as a predicate over the resources, joined by the waituntil operators, where a resource is @true@ if it is available, and @false@ otherwise.
-In \CFA, this representation is used as the mechanism to check if a thread is done waiting on the waituntil.
-Leveraging the compiler, a predicate routine is generated per waituntil that when passed the statuses of the resources, returns @true@ when the waituntil is done, and false otherwise.
-To support guards on the \CFA waituntil statement, the status of a resource disabled by a guard is set to a boolean value that ensures that the predicate function behaves as if that resource is no longer part of the predicate.
+The \CFA @waituntil@ statement blocks a thread until a set of resources have become available that satisfy the underlying predicate.
+The waiting condition of the @waituntil@ statement can be represented as a predicate over the resources, joined by the @waituntil@ operators, where a resource is @true@ if it is available, and @false@ otherwise.
+In \CFA, this representation is used as the mechanism to check if a thread is done waiting on the @waituntil@.
+Leveraging the compiler, a predicate routine is generated per @waituntil@ that when passed the statuses of the resources, returns @true@ when the @waituntil@ is done, and false otherwise.
+To support guards on the \CFA @waituntil@ statement, the status of a resource disabled by a guard is set to a boolean value that ensures that the predicate function behaves as if that resource is no longer part of the predicate.
 
 \uC's @_Select@, supports operators both inside and outside of the clauses.
@@ -348,6 +547,6 @@
 \end{cfa}
 
-This is more expressive that the waituntil statement in \CFA.
-In \CFA, since the waituntil statement supports more resources than just futures, implementing operators inside clauses was avoided for a few reasons.
+This is more expressive that the @waituntil@ statement in \CFA.
+In \CFA, since the @waituntil@ statement supports more resources than just futures, implementing operators inside clauses was avoided for a few reasons.
 As a motivating example, suppose \CFA supported operators inside clauses and consider the code snippet in Figure~\ref{f:wu_inside_op}.
 
@@ -362,11 +561,11 @@
 \end{figure}
 
-If the waituntil in Figure~\ref{f:wu_inside_op} works with the same semantics as described and acquires each lock as it becomes available, it opens itself up to possible deadlocks since it is now holding locks and waiting on other resources.
+If the @waituntil@ in Figure~\ref{f:wu_inside_op} works with the same semantics as described and acquires each lock as it becomes available, it opens itself up to possible deadlocks since it is now holding locks and waiting on other resources.
 Other semantics would be needed to ensure that this operation is safe.
 One possibility is to use \CC's @scoped_lock@ approach that was described in Section~\ref{s:DeadlockAvoidance}, however the potential for livelock leaves much to be desired.
 Another possibility would be to use resource ordering similar to \CFA's @mutex@ statement, but that alone is not sufficient if the resource ordering is not used everywhere.
-Additionally, using resource ordering could conflict with other semantics of the waituntil statement.
+Additionally, using resource ordering could conflict with other semantics of the @waituntil@ statement.
 To show this conflict, consider if the locks in Figure~\ref{f:wu_inside_op} were ordered @D@, @B@, @C@, @A@.
-If all the locks are available, it becomes complex to both respect the ordering of the waituntil in Figure~\ref{f:wu_inside_op} when choosing which code block to run and also respect the lock ordering of @D@, @B@, @C@, @A@ at the same time.
+If all the locks are available, it becomes complex to both respect the ordering of the @waituntil@ in Figure~\ref{f:wu_inside_op} when choosing which code block to run and also respect the lock ordering of @D@, @B@, @C@, @A@ at the same time.
 One other way this could be implemented is to wait until all resources for a given clause are available before proceeding to acquire them, but this also quickly becomes a poor approach.
 This approach won't work due to TOCTOU issues; it is not possible to ensure that the full set resources are available without holding them all first.
@@ -376,8 +575,8 @@
 
 \section{Waituntil Performance}
-The two \gls{synch_multiplex} utilities that are in the realm of comparability with the \CFA waituntil statement are the Go @select@ statement and the \uC @_Select@ statement.
+The two \gls{synch_multiplex} utilities that are in the realm of comparability with the \CFA @waituntil@ statement are the Go @select@ statement and the \uC @_Select@ statement.
 As such, two microbenchmarks are presented, one for Go and one for \uC to contrast the systems.
 The similar utilities discussed at the start of this chapter in C, Ada, Rust, \CC, and OCaml are either not meaningful or feasible to benchmark against.
-The select(2) and related utilities in C are not comparable since they are system calls that go into the kernel and operate on file descriptors, whereas the waituntil exists solely in userspace.
+The select(2) and related utilities in C are not comparable since they are system calls that go into the kernel and operate on file descriptors, whereas the @waituntil@ exists solely in user space.
 Ada's @select@ only operates on methods, which is done in \CFA via the @waitfor@ utility so it is not meaningful to benchmark against the @waituntil@, which cannot wait on the same resource.
 Rust and \CC only offer a busy-wait based approach which is not comparable to a blocking approach.
@@ -386,5 +585,5 @@
 
 \subsection{Channel Benchmark}
-The channel multiplexing microbenchmarks compare \CFA's waituntil and Go's select, where the resource being waited on is a set of channels.
+The channel multiplexing microbenchmarks compare \CFA's @waituntil@ and Go's select, where the resource being waited on is a set of channels.
 The basic structure of the microbenchmark has the number of cores split evenly between producer and consumer threads, \ie, with 8 cores there would be 4 producer threads and 4 consumer threads.
 The number of clauses @C@ is also varied, with results shown with 2, 4, and 8 clauses.
@@ -394,7 +593,7 @@
 
 \begin{cfa}
-    for (;;)
-        waituntil( val << chans[0] ) {} or waituntil( val << chans[1] ) {} 
-        or waituntil( val << chans[2] ) {} or waituntil( val << chans[3] ) {}
+	for (;;)
+		waituntil( val << chans[0] ) {} or waituntil( val << chans[1] ) {} 
+		or waituntil( val << chans[2] ) {} or waituntil( val << chans[3] ) {}
 \end{cfa}
 A successful consumption is counted as a channel operation, and the throughput of these operations is measured over 10 seconds.
@@ -404,5 +603,5 @@
 \begin{figure}
 	\centering
-    \captionsetup[subfloat]{labelfont=footnotesize,textfont=footnotesize}
+	\captionsetup[subfloat]{labelfont=footnotesize,textfont=footnotesize}
 	\subfloat[AMD]{
 		\resizebox{0.5\textwidth}{!}{\input{figures/nasus_Contend_2.pgf}}
@@ -411,5 +610,5 @@
 		\resizebox{0.5\textwidth}{!}{\input{figures/pyke_Contend_2.pgf}}
 	}
-    \bigskip
+	\bigskip
 
 	\subfloat[AMD]{
@@ -419,5 +618,5 @@
 		\resizebox{0.5\textwidth}{!}{\input{figures/pyke_Contend_4.pgf}}
 	}
-    \bigskip
+	\bigskip
 
 	\subfloat[AMD]{
@@ -427,5 +626,5 @@
 		\resizebox{0.5\textwidth}{!}{\input{figures/pyke_Contend_8.pgf}}
 	}
-	\caption{The channel synchronous multiplexing benchmark comparing Go select and \CFA waituntil statement throughput (higher is better).}
+	\caption{The channel synchronous multiplexing benchmark comparing Go select and \CFA \lstinline{waituntil} statement throughput (higher is better).}
 	\label{f:select_contend_bench}
 \end{figure}
@@ -433,5 +632,5 @@
 \begin{figure}
 	\centering
-    \captionsetup[subfloat]{labelfont=footnotesize,textfont=footnotesize}
+	\captionsetup[subfloat]{labelfont=footnotesize,textfont=footnotesize}
 	\subfloat[AMD]{
 		\resizebox{0.5\textwidth}{!}{\input{figures/nasus_Spin_2.pgf}}
@@ -440,5 +639,5 @@
 		\resizebox{0.5\textwidth}{!}{\input{figures/pyke_Spin_2.pgf}}
 	}
-    \bigskip
+	\bigskip
 
 	\subfloat[AMD]{
@@ -448,5 +647,5 @@
 		\resizebox{0.5\textwidth}{!}{\input{figures/pyke_Spin_4.pgf}}
 	}
-    \bigskip
+	\bigskip
 
 	\subfloat[AMD]{
@@ -456,5 +655,5 @@
 		\resizebox{0.5\textwidth}{!}{\input{figures/pyke_Spin_8.pgf}}
 	}
-	\caption{The asynchronous multiplexing channel benchmark comparing Go select and \CFA waituntil statement throughput (higher is better).}
+	\caption{The asynchronous multiplexing channel benchmark comparing Go select and \CFA \lstinline{waituntil} statement throughput (higher is better).}
 	\label{f:select_spin_bench}
 \end{figure}
@@ -464,5 +663,5 @@
 The AMD machine has been observed to have higher caching contention cost, which creates on a bottleneck on the channel locks, which results in similar scaling between \CFA and Go.
 At low cores, Go has significantly better performance, which is likely due to an optimization in their scheduler.
-Go heavily optimizes thread handoffs on their local runqueue, which can result in very good performance for low numbers of threads which are parking/unparking eachother~\cite{go:sched}.
+Go heavily optimizes thread handoffs on their local run-queue, which can result in very good performance for low numbers of threads which are parking/unparking each other~\cite{go:sched}.
 In the Intel benchmarks, \CFA performs better than Go as the number of cores scale and as the number of clauses scale.
 This is likely due to Go's implementation choice of acquiring all channel locks when registering and unregistering channels on a @select@.
@@ -491,9 +690,9 @@
 \label{t:pathGo}
 \begin{tabular}{*{5}{r|}r}
-    & \multicolumn{1}{c|}{\CFA} & \multicolumn{1}{c@{}}{Go} \\
-    \hline
-    AMD		& \input{data/nasus_Order} \\
-    \hline
-    Intel	& \input{data/pyke_Order}
+	& \multicolumn{1}{c|}{\CFA} & \multicolumn{1}{c@{}}{Go} \\
+	\hline
+	AMD		& \input{data/nasus_Order} \\
+	\hline
+	Intel	& \input{data/pyke_Order}
 \end{tabular}
 \end{table}
@@ -505,5 +704,5 @@
 
 \subsection{Future Benchmark}
-The future benchmark compares \CFA's waituntil with \uC's @_Select@, with both utilities waiting on futures.
+The future benchmark compares \CFA's @waituntil@ with \uC's @_Select@, with both utilities waiting on futures.
 Both \CFA's @waituntil@ and \uC's @_Select@ have very similar semantics, however @_Select@ can only wait on futures, whereas the @waituntil@ is polymorphic. 
 They both support @and@ and @or@ operators, but the underlying implementation of the operators differs between @waituntil@ and @_Select@.
@@ -520,6 +719,6 @@
 		\label{f:futureIntel}
 	}
-	\caption{\CFA waituntil and \uC \_Select statement throughput synchronizing on a set of futures with varying wait predicates (higher is better).}
-    \caption{}
+	\caption{\CFA \lstinline{waituntil} and \uC \lstinline{_Select} statement throughput synchronizing on a set of futures with varying wait predicates (higher is better).}
+	\caption{}
 	\label{f:futurePerf}
 \end{figure}
@@ -529,5 +728,5 @@
 Results of this benchmark are shown in Figure~\ref{f:futurePerf}.
 Each set of columns is marked with a name representing the predicate for that set of columns.
-The predicate name and corresponding waituntil statement is shown below:
+The predicate name and corresponding @waituntil@ statement is shown below:
 
 \begin{cfa}
@@ -554,5 +753,5 @@
 \end{cfa}
 
-In Figure~\ref{f:futurePerf}, the @OR@ column for \CFA is more performant than the other \CFA predicates, likely due to the special-casing of waituntil statements with only @or@ operators.
+In Figure~\ref{f:futurePerf}, the @OR@ column for \CFA is more performant than the other \CFA predicates, likely due to the special-casing of @waituntil@ statements with only @or@ operators.
 For both \uC and \CFA the @AND@ column is the least performant, which is expected since all three futures need to be fulfilled for each statement completion, unlike any of the other operators.
 Interestingly, \CFA has lower variation across predicates on the AMD (excluding the special OR case), whereas \uC has lower variation on the Intel.
