Index: doc/theses/colby_parsons_MMAth/text/waituntil.tex
===================================================================
--- doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision 7ed01beaf08420e95646081115fb8219edfed5d7)
+++ doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision c2c171747f6a76789fe7e2861bf8ed06b7f0d080)
@@ -368,7 +368,7 @@
 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.
+When a resource becomes available, @on_selected@ is run, and if it returns false, the corresponding code block is not run.
 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 register/unregister routines in the trait also 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.
@@ -379,4 +379,7 @@
 The @waituntil@ statement is not inherently complex, and the pseudo code is presented in Figure~\ref{f:WU_Impl}.
 The complexity comes from the consideration of race conditions and synchronization needed when supporting various primitives.
+Figure~\ref{f:WU_Impl} aims to introduce the reader to the rudimentary idea and control flow of the @waituntil@.
+The following sections then use examples to fill in details that Figure~\ref{f:WU_Impl} does not provide.
+Finally, the full pseudocode of the waituntil is presented in Figure~\ref{f:WU_Full_Impl}.
 The basic steps of the @waituntil@ statement are:
 
@@ -422,5 +425,5 @@
 Digging into parts of the implementation will shed light on the specifics and provide more detail.
 
-\subsection{Locks}
+\subsection{Locks}\label{s:wu_locks}
 
 The \CFA runtime supports a number of spinning and blocking locks, \eg semaphore, MCS, futex, Go mutex, spinlock, owner, \etc.
@@ -566,5 +569,55 @@
 Operators inside clauses in \CFA could potentially be implemented with careful circumvention of the problems involved, but it was not deemed an important feature when taking into account the runtime cost that would need to be paid to handle these situations.
 The problem of operators inside clauses also becomes a difficult issue to handle when supporting channels.
-If internal operators were supported, it would require some way to ensure that channels used with internal operators are modified on if and only if the corresponding code block is run, but that is not feasible due to reasons described in the exclusive-or portion of Section~\ref{s:wu_chans}. 
+If internal operators were supported, it would require some way to ensure that channels used with internal operators are modified on if and only if the corresponding code block is run, but that is not feasible due to reasons described in the exclusive-or portion of Section~\ref{s:wu_chans}.
+
+\subsection{The full \lstinline{waituntil} picture}
+Now that the details have been discussed, the full pseudocode of the waituntil is presented in Figure~\ref{f:WU_Full_Impl}.
+
+\begin{figure}
+\begin{cfa}
+bool when_conditions[N];
+for ( node in s )								 $\C{// evaluate guards}$
+    if ( node has guard ) 
+        when_conditions[node] = node_guard;
+    else 
+        when_conditions[node] = true;
+
+select_nodes s[N];								 $\C[3.25in]{// declare N select nodes}$
+try {
+    for ( node in s )								 $\C{// register nodes}$
+        if ( when_conditions[node] )
+            register_select( resource, node );
+
+    // ... set statuses for nodes with when_conditions[node] == false ...
+
+    while ( statement predicate not satisfied ) {	$\C{// check predicate}$
+        // block
+        for ( resource in waituntil statement ) {	$\C{// run true code blocks}$
+            if ( statement predicate is satisfied ) break;
+            if ( resource is avail ) {
+                try {
+                    if( on_selected( resource ) )              $\C{// conditionally run block}$
+                        run code block
+                } finally {                                    $\C{// for exception safety}$
+                    unregister_select( resource, node );       $\C{// immediate unregister}$
+                } 
+            }
+        }
+    }
+} finally {                                                     $\C{// for exception safety}$
+    for ( registered nodes in s )								$\C{// deregister nodes}$
+        if ( when_conditions[node] && unregister_select( resource, node ) && on_selected( resource ) ) 
+            run code block $\C{// conditionally run code block upon unregister}\CRT$
+}
+\end{cfa}
+\caption{Full \lstinline{waituntil} Pseudocode Implementation}
+\label{f:WU_Full_Impl}
+\end{figure}
+
+In comparison to Figure~\ref{f:WU_Impl}, this pseudocode now includes the specifics discussed in this chapter.
+Some things to note are as follows:
+The @finally@ blocks provide exception-safe RAII unregistering of nodes, and in particular, the @finally@ inside the innermost loop performs the immediate unregistering required for deadlock-freedom that was mentioned in Section~\ref{s:wu_locks}.
+The @when_conditions@ array is used to store the boolean result of evaulating each guard at the beginning of the @waituntil@, and it is used to conditionally omit operations on resources with @false@ guards.
+As discussed in Section~\ref{s:wu_chans}, this pseudocode includes code blocks conditional on the result of both @on_selected@ and @unregister_select@, which allows the channel implementation to ensure that all available channel resources will have their corresponding code block run.
 
 \section{Waituntil Performance}