Index: doc/theses/mike_brooks_MMath/array.tex
===================================================================
--- doc/theses/mike_brooks_MMath/array.tex	(revision bf8112b8e07cfd3becb83c79e4e3b5eee2d064de)
+++ doc/theses/mike_brooks_MMath/array.tex	(revision 5faa3a5390d1a4845f728030a7e3e373db2eaaac)
@@ -1766,5 +1766,5 @@
 it can also do these other cool checks, but watch how I can mess with its conservativeness and termination
 
-Two contemporary array-centric languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, contribute similar, restricted dependent types for tracking array length.
+Two contemporary array-centric languages, Dex~\cite{arr:dex:long} and Futhark~\cite{arr:futhark:tytheory}, contribute similar, restricted dependent types for tracking array length.
 Unlike \CFA, both are garbage-collected functional languages.
 Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary.
@@ -1936,5 +1936,5 @@
 \begin{itemize} 
 	\item
-	Alice holds and array and knows its size.
+	Alice holds an array and knows its size.
 	\item
 	Bob offers a service that can apply to an array of any size.
@@ -1955,5 +1955,5 @@
 \end{itemize}
 This interaction is the dual notion of existential polymorphism, working upon size information.
-Work\cite{arr:futhark:tytheory} accompanying the array-centric language Futhark has detailed its theory.
+Work~\cite{arr:futhark:tytheory} accompanying the array-centric language Futhark has detailed its theory.
 
 An existential size helps cope with unnecessary repetition that occurs as program size increases and more intermediaries separate an array producer and consumer.
@@ -1975,12 +1975,12 @@
 The intermediaries no longer need size information in scope to pass one along.
 @SchoolRef@ stops the polymorphism of @School@ from flowing farther outward.
-The final consumer need only open the box, discover what's inside, and proceed.
+The final consumer need only open the box, discover what is inside, and proceed.
 \begin{cfa}
 forall( [C], [S] ) static void process( School(C, S) * );
 void receive( SchoolRef r ) {
 	with( r ) {
-		classes; students; // are in scope
-		School( classes, students ) * s2 = school; // we can state the type
-		process( s2 ); // we can communicate the type
+		classes; students;				$\C{// are in scope}$
+		School( classes, students ) * s2 = school; $\C{// state the type}$
+		process( s2 );					$\C{// communicate the type}$
 	}
 }
@@ -1994,14 +1994,14 @@
 The programmer writes code in which it appears that a bound check ought to be unnecessary, but feedback about success or failure there is indirect.
 
-Dex\cite{arr:dex:long} is a contemporary array-centric language that follows in the Ada array tradition\cite{arr:ada:learn} of designating a type to be used for subscripting an array.
+Dex~\cite{arr:dex:long} is a contemporary array-centric language that follows in the Ada array tradition~\cite{arr:ada:learn} of designating a type to be used for subscripting an array.
 While \CFA has its new @[N]@ living in the type system, this @N@ is used to represent an array's size.
 An indexing type would be the type of @i@, in @ar[i]@.
 \begin{cfa}
 const size_t n = ask_the_user();
-typedef range(0, n) till_n_t; // does not exist in CFA yet
-till_n_t x = 42; // static reject
-till_n_t y = check(42); // static accept, dynamic check
+typedef @range(0, n)@ till_n_t; $\C{// does not exist in CFA yet}$
+till_n_t x = 42; $\C{// static reject}$
+till_n_t y = check(42); $\C{// static accept, dynamic check}$
 void f( array(int, n) & ar, till_n_t i ) {
-	sout | ar[ i ];  // bound check unnecessary
+	sout | ar[ i ];  $\C{// bound check unnecessary}$
 }
 \end{cfa}
@@ -2009,5 +2009,5 @@
 \begin{cfa}
 void f2( array(int, n) & ar, size_t i ) {
-	sout | ar[ i ];  // bound check necessary
+	sout | ar[ i ];  $\C{// bound check necessary}$
 }
 \end{cfa}
@@ -2019,5 +2019,5 @@
 If the user succeeds at needing no explicit bound checks, then the user is assured that there are no bound checks.
 
-Prior \CFA work\cite{Liang24} has touched upon this topic.
+Prior \CFA work~\cite{Liang24} has touched upon this topic.
 Therein, a user's enumeration type is adapted to serve as the domain of an array.
 However, this work progressed as far as inferring an array size from the enumeration type, \eg that @int happy_hours[ weekday_t ]@ should be a declaration with length seven.
Index: doc/theses/mike_brooks_MMath/background.tex
===================================================================
--- doc/theses/mike_brooks_MMath/background.tex	(revision bf8112b8e07cfd3becb83c79e4e3b5eee2d064de)
+++ doc/theses/mike_brooks_MMath/background.tex	(revision 5faa3a5390d1a4845f728030a7e3e373db2eaaac)
@@ -463,5 +463,5 @@
 however, it requires all dimensions except the first to be specified at compile time, \eg @m[][6]@, allowing all subscripting stride calculations to be generated with constants.
 Hence, every matrix passed to @fp1@ must have exactly 6 columns but the row size can vary.
-The variable-dimension approach (right) ignores (violates) the type system, \ie the parameter type has no suggestion of mutidimensionality and some acrobatics are required for a w\footnote{
+The variable-dimension approach (right) ignores (violates) the type system, \ie the parameter type has no suggestion of multidimensionality and some acrobatics are required for a w\footnote{
 	One may be tempted to phrase a call as \lstinline{fp2( 4, 4, vm1 )}, but this call is ill-typed.  Argument \lstinline{vm1} could match parameter declarations \lstinline{int m[][4]} or \lstinline{int (*m)[4]}.  But only the argument \lstinline{&vm1[0][0]}, or its equivalent, but confusing, \lstinline{vm1[0]}, relate \lstinline{vm1} to parameter type \lstinline{int*}.
 }, and subscripting is performed manually using pointer arithmetic in the macro @sub@.
@@ -534,5 +534,5 @@
 Nevertheless, the C array-of-array form is still important for special circumstances.
 
-\VRef[Figure]{f:ContiguousNon-contiguous} shows a powerful extension made in C99, for manipulating contiguous \vs non-contiguous arrays.\footnote{C90 also supported non-contiguous arrays.  Though GNU-flavoured C++ eventually got VLAs, it never got this enhancement for managing a multidimensionl VLA parameter. }
+\VRef[Figure]{f:ContiguousNon-contiguous} shows a powerful extension made in C99, for manipulating contiguous \vs non-contiguous arrays.\footnote{C90 also supported non-contiguous arrays.  Though GNU-flavoured C++ eventually got VLAs, it never got this enhancement for managing a multidimensional VLA parameter. }
 For contiguous-array arguments (including VLA), C99 conjoins one or more of the parameters as a downstream dimension(s), \eg @cols@, implicitly using this parameter to compute the row stride of @m@.
 Hence, if the declaration of @fc@ is changed to:
@@ -1184,5 +1184,5 @@
 \end{c++}
 It turns out that @TAILQ_REMOVE@ uses its ``which element to remove'' parameter at several places, importantly, one occurring after the removal's changes are in progress.
-When the second use encounters the macro substitution @TAILQ_LAST(reqs, reql)@, it obtains a different node than the first use got, with the removal's changes having alredy started.
+When the second use encounters the macro substitution @TAILQ_LAST(reqs, reql)@, it obtains a different node than the first use got, with the removal's changes having already started.
 This macro-induced phenomenon led to an invalid pointer dereference (safety violation), at a run-time well after the removal at issue (costly to resolve).
 
Index: doc/theses/mike_brooks_MMath/intro.tex
===================================================================
--- doc/theses/mike_brooks_MMath/intro.tex	(revision bf8112b8e07cfd3becb83c79e4e3b5eee2d064de)
+++ doc/theses/mike_brooks_MMath/intro.tex	(revision 5faa3a5390d1a4845f728030a7e3e373db2eaaac)
@@ -71,5 +71,5 @@
 Among the linked structures, the list's defining characteristic is maintaining a user-explicit total order (chain shape).
 Element search can be by position (as for array) or by value; it is sometimes presented as a subscript.
-In a more complex structure, the linked shape may be system managed (user impicit) by being a function of a designated ``key'' datum, \eg often for a hash table.
+In a more complex structure, the linked shape may be system managed (user implicit) by being a function of a designated ``key'' datum, \eg often for a hash table.
 Though such schemes often give better-than-$O(n)$ lookup, the linked list's user-explicit shape limits what the system can provide, to fast step/iteration for user-``nearby'' data, and slow exhaustive search/seek otherwise.
 Linked types are dynamically sized by adding and removing nodes using link fields internal or external to the list elements (nodes).
Index: doc/theses/mike_brooks_MMath/list.tex
===================================================================
--- doc/theses/mike_brooks_MMath/list.tex	(revision bf8112b8e07cfd3becb83c79e4e3b5eee2d064de)
+++ doc/theses/mike_brooks_MMath/list.tex	(revision 5faa3a5390d1a4845f728030a7e3e373db2eaaac)
@@ -1010,5 +1010,5 @@
 Therefore, the duration's response to size is not a steady worsening as size increases.
 Often, each size-independent configuration responds to size increases in steps of slowdown.
-Occasionally a slowdown step is followed by some perforamnce increase, where an incurred penalty begins to amortize away.
+Occasionally a slowdown step is followed by some performance increase, where an incurred penalty begins to amortize away.
 Hence, performance results can have interesting jitter as size increases.
 The analysis treats these behaviours as incidental.
@@ -1016,5 +1016,5 @@
 Rather, size zones are picked, specific effects inside of a zone are averaged away, and the story at one zone is compared to that at another.
 
-% It is true, but perhaps not obvious, that buildind and destroying long lists is slower than building and destroying short lists.
+% It is true, but perhaps not obvious, that building and destroying long lists is slower than building and destroying short lists.
 % Obviously, indeed, it takes longer to fuse and divide a hundred neighbours than five.
 % But the key metric in this work, AII, is about a single link--unlink.
@@ -1028,5 +1028,5 @@
 % So, duration's response to size is not a steady worsening as size increases.
 % Rather, each size-independent configuration often responds to size increases with leaps of worsening.
-% Occasionally a leap is even followed size-run of retrograde response, where a suddenly incurred penalty has a chance to ammortize away.
+% Occasionally a leap is even followed size-run of retrograde response, where a suddenly incurred penalty has a chance to amortize away.
 % The frameworks tend to leapfrog over each other, at different points, as size increases.
 % 
@@ -1046,5 +1046,5 @@
 	}
   \end{tabular}
-  \caption[Variety of IR duration responses to list length, at small--medium lengths]{Variety of IR duration responses to list length, at small--medium lengths.  Two example use cases are shown: I, stack movement with head-only access (plot a); IX, queue movement with element-oriented removal access (plot b); both use cases have insert-first polarity.  One example is run on each machine: UC-I on AMD (ploat a); UC-IX on Intel (plot b).  Lower is better.}
+  \caption[Variety of IR duration responses to list length, at small--medium lengths]{Variety of IR duration responses to list length, at small--medium lengths.  Two example use cases are shown: I, stack movement with head-only access (plot a); IX, queue movement with element-oriented removal access (plot b); both use cases have insert-first polarity.  One example is run on each machine: UC-I on AMD (plot a); UC-IX on Intel (plot b).  Lower is better.}
   \label{fig:plot-list-zoomin-abs}
 \end{figure}
@@ -1122,6 +1122,6 @@
 \subsubsection{Recap and Master Legend}
 
-For experiments performed in later sections, there are 12 use cases, which are all combinations of 2 movents, 2 polarities and 3 accessors.
-There are 4 pysical contexts, which are all combinations of 2 machines and 2 size (length) zones.
+For experiments performed in later sections, there are 12 use cases, which are all combinations of 2 movements, 2 polarities and 3 accessors.
+There are 4 physical contexts, which are all combinations of 2 machines and 2 size (length) zones.
 There are 3.25 frameworks.
 This accounting considers how LQ-list supports only the movement--polarity combination ``stack, insert first.''
@@ -1154,6 +1154,6 @@
 	}
   \end{tabular}
-  \caption[IR duration, transformed for general anaysis]{
-	IR duration, transformed for general anaysis.
+  \caption[IR duration, transformed for general analysis]{
+	IR duration, transformed for general analysis.
 	The analysis follows the single example setup of \VRef[Figure]{f:zoomin-abs-i-swift}, \ie Use Case I on AMD; there, IR is given as absolute duration.
 	Plot (a) transforms the source dataset by conditioning on specific size.
@@ -1180,5 +1180,5 @@
 
 The effect of conditioning on specific size erases the fact that \VRef[Figure]{fig:plot-list-zoomin-abs} shows, aside from the coarse hops, all frameworks getting smoothly slower as size increases.
-This effect is partiularly relevant \emph{within} a size zone, most noticeable as the data lines all going up across the Small box.
+This effect is particularly relevant \emph{within} a size zone, most noticeable as the data lines all going up across the Small box.
 Now, with size conditioned, \VRef[Figure]{f:zoomin-rel-i-swift} has the trends inside a zone box being flat.
 This flatness gives \subref*{f:histo-rel-i-swift} nicely separated histograms.
@@ -1186,9 +1186,9 @@
 Specific size is the only factor conditioned in this view.
 This choice was made to keep the relationship between \VRef[Figures]{f:zoomin-abs-i-swift} and \VRef[]{:zoomin-rel-i-swift} perceptible.
-By contrast, general comparisons like \VRef[Figure]{fig:plot-list-1ord} condition on more, generally, everyting not presented.
+By contrast, general comparisons like \VRef[Figure]{fig:plot-list-1ord} condition on more, generally, everything not presented.
 Its physical-factor breakdown conditions on use case and framework, but not on physical factors; its other two breakdowns are defined similarly.
 
 The noteworthy performance hop, in this example, is LQ-@list@, which \VRef[Figures]{f:zoomin-abs-i-swift} has as consistently slow in the Small range, and consistently fast in the Medium range.
-Therefore, in \VRef{f:zoomin-histo-i-swift}, its two per-size-zone histograms are far apart, and its cross-size-zone histogram is bimdal.
+Therefore, in \VRef{f:zoomin-histo-i-swift}, its two per-size-zone histograms are far apart, and its cross-size-zone histogram is bimodal.
 Hops and distribution contributions, like this one, are common.
 They are attention-grabbing curiosities when comparing nearly any pair of individual configurations.
@@ -1208,10 +1208,10 @@
 
 A condensed graphing style is used in subsequent plots to present this amount of data.
-\VRef[Figure]{fig:plot-list-rel} shows how the condensed graphing style is generated from indvidual-configuration measures.
+\VRef[Figure]{fig:plot-list-rel} shows how the condensed graphing style is generated from individual-configuration measures.
 \VRef[Figure]{f:zoomin-rel-i-swift} is formed from the data in \VRef[Figure]{f:zoomin-abs-i-swift}, transformed on the Y-axis to show duration relative to the mean across all four frameworks, at each specific size.
-\VRef[Figure]{f:zoomin-histo-i-swift} consenses the interesting data within the two boxes (Small/Medium) and their combination (Both).
+\VRef[Figure]{f:zoomin-histo-i-swift} condenses the interesting data within the two boxes (Small/Medium) and their combination (Both).
 This graph plots a vertical histogram for each of the 4 frameworks.
 A data point on \VRef[Figure]{f:zoomin-abs-i-swift} is one-to-one with a point on \VRef[Figure]{f:zoomin-rel-i-swift}; each gives one IC.
-Repeatability of the experimet being established previously, retry variance information (error bar on an individual-configuration point) is discarded, and only the expected performance of an IC (mean of its middle three out of five trials) is promoted into the histograms.
+Repeatability of the experiment being established previously, retry variance information (error bar on an individual-configuration point) is discarded, and only the expected performance of an IC (mean of its middle three out of five trials) is promoted into the histograms.
 Each histogram bin (light-shaded area) counts the number of ICs whose expected performance falls in the bin's range.
 A histogram's girth indicates the diversity of its qualifying configurations' performance expectations. 
@@ -1445,5 +1445,5 @@
 
 The second breakdown, movement and polarity (middle), the responses are more subdued.
-Note, LQ-list has no represntation in these comparisons because it only supports stacks that push and pop with the first element.
+Note, LQ-list has no representation in these comparisons because it only supports stacks that push and pop with the first element.
 \CFA is completely stable under movement and polarity changes.
 \uCpp and LQ show modest responses favouring queues and insertion at last.
@@ -1472,5 +1472,5 @@
 Speculation is that \CFA's increased data dependency, a result of the tagging scheme, pairs poorly with the aliasing implied by queue movement.
 The aliasing, at length 1, is: the head's first element is the head's last element.
-With stack movement, one of these names for the first element is reaused for both insert and remove.
+With stack movement, one of these names for the first element is reused for both insert and remove.
 While with queue movement, both names are used in alternation.
 
@@ -1479,19 +1479,19 @@
 The insight for contextualizing this issue was to inspect both length and width.
 
-The issue is seen as practically mitigated by noticing that the difficutly fades away as width increases.
+The issue is seen as practically mitigated by noticing that the difficulty fades away as width increases.
 This effect is seen both in \VRef[Figure]{fig:plot-list-short}'s easement across the top triangle rows, and, zoomed farther out, in \VRef[Figure]{fig:plot-list-wide}.
 
 Increasing the width matters to the aliasing hypothesis.
 In a narrow experiment, one element's insert and remove happen in rapid succession.
-So, the two aliases are exercied closer together, making a data hazard (that lacks ideal hardware treatment) stretch the instruction-pipeline schedule more significantly.
+So, the two aliases are exercised closer together, making a data hazard (that lacks ideal hardware treatment) stretch the instruction-pipeline schedule more significantly.
 Increasing the width adds harness-induced gaps between the uses of each alias, behind which a potential hazard can hide.
 
 In the practical scenario that judges length-1 performance as relevant, width 1 is contrived.
-A thread putting itself on an often-empty waiters' list is not doing so on one such list repeatedly, at least not without taking other situation-iduced pauses.
+A thread putting itself on an often-empty waiters' list is not doing so on one such list repeatedly, at least not without taking other situation-induced pauses.
 
 Thus, the congestion at low width + length comes from the harness using repetition (in order to obtain a measurable time).
 It does not reflect the situation that motivates the legitimate desire for good length-1 performance.
 
-There likely is a real hazard, unique to the \CFA framework, when a queue movement is repeated on a tiny list \emph{without other interventing action}.
+There likely is a real hazard, unique to the \CFA framework, when a queue movement is repeated on a tiny list \emph{without other intervening action}.
 Doing so is believed to occur only in contrived situations.
 
@@ -1574,8 +1574,8 @@
 
 From the perspective of assessing winning/losing frameworks, these physical effects are noise.
-So, subsequent analysis conditions on the phisical effects.
+So, subsequent analysis conditions on the physical effects.
 That is, it supposes you are put into an unknown physical situation (that is one of the four being tested), then presents all the ways your outcome could change as a result of non-physical factors, assuming that the physical situation is kept constant.
-It does do by presenting results relative to the mean of the physical quadrant (\VRef[fig]{fig:plot-list-mchn-szz} histogram) to which it belogs.
-With this adjustment, absolute duration values (in nonsecods) are lost.
+It does do by presenting results relative to the mean of the physical quadrant (\VRef[fig]{fig:plot-list-mchn-szz} histogram) to which it belongs.
+With this adjustment, absolute duration values (in nanoseconds) are lost.
 In return, the physical quadrants are re-combined, enabling assessment of the non-physical factors.
 \end{comment}
@@ -1630,5 +1630,5 @@
   This state is how LQ leaves a removed element; LQ does not offer an is-listed query.
 \item[no-iter(ation)] Removing support for well-terminating iteration.
-  The \CFA list uses bit-manipulation tagging on link poiters (rather than \eg null links) to express, ``No more elements this way.''
+  The \CFA list uses bit-manipulation tagging on link pointers (rather than \eg null links) to express, ``No more elements this way.''
   This tagging has the cost of submitting a retrieved value to the ALU, and awaiting this operation's completion, before dereferencing a link pointer.
   In some cases, the is-terminating bit is transferred from one link to another, or has a similar influence on a resulting link value; this logic adds register pressure and more data dependency.
