move remarks to footnotes

papers/icfp2021/main.tex

@@ -18,6 +18,7 @@
 % \usepackage{extpfeil} % fancy long arrows (has to be sourced before stmaryrd)
 % \usepackage{stmaryrd}
 \usepackage{xspace}
+\usepackage{footmisc} % recall a footnote with \footref
 % Respect the order of papers inside a \cite command.
 \setcitestyle{nosort}
 

papers/icfp2021/notations.tex

 % References to sections, lemmas, theorems, etc.
 \newcommand{\sref}[1]{\S\ref{#1}}
 \newcommand{\fref}[1]{Figure~\ref{#1}}
+\newcommand{\fnref}[1]{Footnote~\ref{#1}}
 
 % Abbreviations.
 \def\etal.{\emph{et al.}}

papers/icfp2021/queue-impl.tex

@@ -33,11 +33,23 @@ In other words, it is the rank of the next item to be dequeued.
 
 Each cell in the buffer is in one of two states: either it is \emph{occupied},
 meaning that it stores some item of the queue; or it is \emph{available},
-meaning that the value it stores is irrelevant (in that case, we store a unit
-value $\Unit$ in that cell; indeed, keeping a stale pointer could cause a
-space leak). In addition, for the concurrent queue operations to work
-properly, we must remember at which rank each offset was last used. The status
-encodes this information in a single integer, as follows:
+meaning that the value it stores is irrelevant.%
+%
+\footnote{\label{fn:memleak}%
+  In that case, we store a unit value $\Unit$ in that cell; indeed, keeping
+  a stale pointer could cause a space leak.
+}
+%
+In addition, for the concurrent queue operations to work properly, we must
+remember at which rank each offset was last used.%
+\footnote{%
+  % FP je pense qu'on peut supprimer cette remarque technique?
+  % Glen: je la passe en footnote.
+  Actually, we need not remember the full rank~\idx:
+  only the cycle, $\idx \div \capacity$, is needed.
+}
+%
+The status encodes this information in a single integer, as follows:
 
 \begin{itemize}%
 
@@ -49,19 +61,19 @@ encodes this information in a single integer, as follows:
 
 \end{itemize}%
 
-% FP je pense qu'on peut supprimer cette remarque technique?
-% (Actually, the status need not encode the full rank~\idx. Only the cycle,
-% $\idx \div \capacity$, is needed.)
-
 The function~\enqueue repeatedly calls \tryenqueue until it succeeds.
 \tryenqueue can fail either because the buffer is full or because of a race
-with another enqueuer. (We currently do not distinguish between these two
-causes, but this is feasible.)
+with another enqueuer.%
+%
+\footnote{\label{fn:distinguishfail}%
+  We currently do not distinguish between these two causes, but this is feasible.
+}
 
 Similarly, \dequeue repeatedly calls \trydequeue untils it succeeds.
 \trydequeue can fail either because the buffer is empty or because of a race
-with another dequeuer. (Again, we currently do not distinguish between these
-two causes, but this is feasible).
+with another dequeuer.%
+%
+\footref{fn:distinguishfail}
 
 A noteworthy feature of this implementation is that the head and tail are
 independent of each other, so that an enqueuer and a dequeuer never race
@@ -118,6 +130,10 @@ nonatomic write to \refelements has taken place. Thus, a thread which dequeues t
 (after reading its status) is certain to read a correct value from the array \refelements.
 This is a typical release/acquire idiom.
 
-Function~\trydequeue works analogously. (Overwriting the extracted value with
-the unit value~$\Unit$ is unnecessary for functional correctness, but doing this
-avoids keeping a stale pointer.)
+Function~\trydequeue works analogously.%
+%
+\footnote{%
+  Overwriting the extracted value with a unit value~$\Unit$ is unnecessary for
+  functional correctness but, as mentioned in~\fnref{fn:memleak}, it prevents
+  space leaks.
+}

papers/icfp2021/queue-spec.tex

@@ -226,10 +226,10 @@ a dequeuer to an enqueuer.%
 %
 \footnote{%
   This is not entirely true: the implementation that we show later does create
-  a happens-before relation from the dequeuer of rank~$\idx$ to the enqueuer of
+  a happens-before relationship from the dequeuer of rank~$\idx$ to the enqueuer of
   rank~$\idx+\capacity$ (hence also to all enqueuers of subsequent ranks).
   We choose to not reveal this in the specification.
-}%
+}
 %
 Hence, by contrast with a sequential queue that would
 be guarded by a lock, the concurrent queue is not linearizable, even though it