Index: doc/theses/colby_parsons_MMAth/text/waituntil.tex
===================================================================
--- doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision dbf5e1890699a4755af129c8750ab720f60fcc8c)
+++ doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision 7ed01beaf08420e95646081115fb8219edfed5d7)
@@ -15,5 +15,5 @@
 
 Now the problem is extended.
-Some stalls are wheelchair accessible and some stalls have specific sexual orientation.
+Some stalls are wheelchair accessible and some stalls have specific gender identification.
 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.
@@ -44,5 +44,5 @@
 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 not in the set of resources being waited on.
-If all guards are false, the ALT does nothing and the thread continues.
+If all guards are false, the ALT, Occam's \gls{synch_multiplex} statement, 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]
@@ -377,5 +377,5 @@
 
 \section{\lstinline{waituntil} Implementation}
-The @waituntil@ statement is not inherently complex, and the pseudo code in presented in Figure~\ref{f:WU_Impl}.
+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.
 The basic steps of the @waituntil@ statement are:
@@ -388,18 +388,12 @@
 while ( statement predicate not satisfied ) {	$\C{// check predicate}$
 	// block
-	for ( resource in waituntil statement )		$\C{// run true code blocks}$
+	for ( resource in waituntil statement ) {	$\C{// run true code blocks}$
+        if ( statement predicate is satisfied ) break;
 		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.
-
+	if ( unregister_select( resource, node ) ) run code block
+\end{cfa}
 \caption{\lstinline{waituntil} Implementation}
 \label{f:WU_Impl}
@@ -416,6 +410,7 @@
 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.
+If clauses becomes satisfied, the thread unblocks, and for each satisfied clause the block fails and the thread proceeds, otherwise the block succeeds (like a semaphore where a block is a @P()@ and a satisfied clause is a @V()@).
 After proceeding past the block all clauses are checked for completion and the completed clauses have their code blocks run.
+While checking clause completion, if enough clauses have been run such that the statement predicate is satisfied, the loop exits early.
 In the case where the block succeeds, the thread will be woken by the thread that marks one of the resources as available.
 
@@ -423,5 +418,4 @@
 Once the thread escapes the loop, the @select_nodes@ are unregistered from the resources.
 \end{enumerate}
-Pseudocode detailing these steps is presented in the following code block.
 
 These steps give a basic overview of how the statement works.
@@ -445,5 +439,5 @@
 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
+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.
@@ -510,5 +504,5 @@
 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.
+This race case is detectable, and if detected, producer will first race to set its own race flag to be pending.
 If it succeeds, it then attempts to set the consumer's race flag to its success value.
 If the producer successfully sets the consumer race flag, then the operation can proceed, if not the signalling thread will set its own race flag back to the initial value.
@@ -518,5 +512,5 @@
 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 and an exception is thrown.
 
 \subsection{Guards and Statement Predicate}\label{s:wu_guards}