Index: doc/theses/colby_parsons_MMAth/text/waituntil.tex
===================================================================
--- doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision c03c1acdd2e8c31fbdfeeb996f5f3d5de6b25aad)
+++ doc/theses/colby_parsons_MMAth/text/waituntil.tex	(revision 47b7142b40bf38fed2ced7fe498b771ae5633293)
@@ -477,5 +477,5 @@
 \end{tabular}
 \end{cquote}
-These examples are basically equivalence.
+These examples are basically equivalent.
 Here, the multiple timeouts are useful because the durations can change during execution and the separate clauses provide different code blocks if a timeout triggers.
 Multiple timeouts can also be used with @and@ to provide a minimal delay before proceeding.
@@ -499,6 +499,6 @@
 In either case, after the WUT unblocks it is safe to execute its the corresponding code block knowing access to the resource is protected by the lock or the read-only state of the future.
 Similarly, for channels, when an outside thread inserts a value into a channel, it must unblock the WUT.
-However, for channels, there is a race issue.
-If the outside thread inserts into the channel and unblocks the WUT, there is a race such that, another thread can remove the channel data, so after the WUT unblocks and attempts to remove from the buffer, it fails, and the WUT must reblock (busy waiting).
+However, for channels, there is a race condition that poses an issue.
+If the outside thread inserts into the channel and unblocks the WUT, there is a race where another thread can remove the channel data, so after the WUT unblocks and attempts to remove from the buffer, it fails, and the WUT must reblock (busy waiting).
 This scenario is a \gls{toctou} race that needs to be consolidated.
 To close the race, the outside thread must detect this case and insert directly into the left-hand side of the channel expression (@i << chan@) rather than into the channel, and then unblock the WUT.
@@ -522,32 +522,66 @@
 
 It was deemed important that exclusive-or semantics are maintained when only @or@ operators are 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.
-\PAB{explain how this is handled.}
-
-\PAB{I'm lost here to the end of the section. You have no example of the case you want to discuss so a made something up.}
+Consider the following example with three threads running concurrently.
+\begin{cfa}
+channel A, B; // zero size channels
+
+// Thread 1:
+waituntil( i << A ) {}
+or waituntil( i << B ) {}
+
+// Thread 2:
+waituntil( A << 1 ) {}
+
+// Thread 3:
+waituntil( B << 2 ) {}
+\end{cfa}
+
+For Thread 1 to have exclusive-or semantics, it must only consume from exactly one of @A@ or @B@.
+As such, Thread 2 and 3 must race to establish the winning clause of the @waituntil@ in Thread 1.
+This race is consolidated by Thread 2 and 3 each attempting to set a pointer to the winning clause's @select_node@ address using \gls{cas}.
+The winner will successfully \gls{cas} the address, insert the value and then signal Thread 1, whereas the loser will fail their \gls{cas}.
+If there is space in the channel, the losing thread may proceed with their channel operation and not signal, otherwise if there is no space they block as they would in a standard channel insert operation.
+It is important that threads race \emph{before} operating on the channel, since if they lose the race they may need to take a different action with respect to their channel operation.
+In the example case, the winner will handoff their value to Thread 1 and the loser will block.
+If the race was consolidated after the operation, both Thread 2 and 3 could potentially write into @i@ concurrently, which would be erroneous behaviour.
 
 Channels introduce another interesting consideration in their implementation.
-Supporting both reading and writing to a channel in a @waituntil@ means that one @waituntil@ clause may be the notifier by another @waituntil@ clause.
-\begin{cfa}
-waituntil( i << A ) { @B << i;@ }
-or waituntil( i << B ) { @A << i;@ }
-\end{cfa}
+Supporting both reading and writing to a channel in a @waituntil@ means that one @waituntil@ clause may be the notifier of another @waituntil@ clause.
 This poses a problem when dealing with the special-cased @or@ where the clauses need to win a race to operate on a channel.
-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@.
+
+Consider the following example, alongside a described ordering of events to highlight the race.
+Assume Thread 1 executes first, registers with channel @A@ and proceeds since it is empty and then is interrupted before registering with @B@.
+Thread 2 similarly registers with channel @B@, and proceeds since it doesn't have space to insert and then is interrupted before registering with @A@.
+At this point Thread 1 and 2 resume execution.
+There is now a race that must be dealt with on two fronts.
+If Thread 1 and 2 only race to \gls{cas} a winning clause for their own @waituntil@, Thread 1 may think that it successfully removed from @B@ and Thread 2 may think it successfully inserted into @A@, when only one of these operations can occur.
+\begin{cfa}
+channel A, B; // zero size channels
+
+// Thread 1:
+waituntil( i << A ) {}
+or waituntil( i << B ) {}
+
+// Thread 2:
+waituntil( B << 2 ) {}
+or waituntil( A << 1 ) {}
+\end{cfa}
 
 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 is held.
+This eliminates the race shown above since both Thread 1 and 2 cannot both be registering at the same time.
 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 outside thread first races to set its own race flag to be pending.
-If it succeeds, it then attempts to set the WUT's race flag to its success value.
-If the outside thread successfully sets the WUT's race flag, then the operation can proceed, if not the signalling threads set its own race flag back to the initial value.
-If any other threads attempt to set the producer's flag and see a pending value, they will wait until the value changes before proceeding to ensure that in the case that the producer fails, the signal will not be lost.
+This race case is detectable, and if detected, each thread first races to set its own @waituntil@ race pointer to be pending.
+If it succeeds, it then attempts to set the other thread's @waituntil@ race pointer to its success value.
+If either thread successfully sets the the other thread's @waituntil@ race pointer, then the operation can proceed, if not the signalling threads set its own race pointer back to the initial value and repeats.
+This retry mechanism can potentially introduce a livelock, but in practice a livelock here is highly unlikely.
+Furthermore, the likelihood of a livelock here is zero unless the program is in the niche case of having two or more exclusive-or waituntils with 2 or more clauses in reverse order of priority.
+This livelock case could be fully eliminated using locks like Go, or if a \gls{dcas} instruction is available.
+If any other threads attempt to set a WUT's race pointer and see a pending value, they will wait until the value changes before proceeding to ensure that in the case that the WUT fails, the signal will not be lost.
 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.
-These exception mechanisms were what brought in the @on_selected@ routine.
+These exception mechanisms are supported through 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 and an exception is thrown.