Commit d191abb9 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: don’t force figures for seq spec and SC spec to remain together

parent 9c5bf12d
%\begin{figure}
\begin{figure}
\begin{mathpar}
\infer{~}{\persistent{\queueInv}}
\and
......@@ -26,4 +26,4 @@
\Description{A specification of the ``queue'' data structure in a sequentially consistent model.}
\caption{A specification of the ``queue'' data structure in a sequentially consistent memory model}
\label{fig:queue:spec:sc}
%\end{figure}
\end{figure}
%\begin{figure}
\begin{figure}
\begin{mathpar}
\hoareV
{\TRUE}
......@@ -18,4 +18,4 @@
\Description{A specification of the ``queue'' data structure in a sequential setting.}
\caption{A specification of the ``queue'' data structure in a sequential setting}
\label{fig:queue:spec:seq}
%\end{figure}
\end{figure}
\subsection{Specification under sequential consistency}
\label{sec:queue:spec:sc}
\input{figure-queue-spec-sc}
We now consider a situation where several threads can access the queue concurrently.
Let us assume for now that the memory model is sequentially consistent~\cite{lamport-79}.
%
......
\subsection{Specification in a sequential setting}
\label{sec:queue:spec:seq}
\input{figure-queue-spec-seq}
Let us start by assuming a sequential setting. We can then use standard
\SL~\cite{reynolds-02} to reason about programs and the resources they manipulate.
%
......@@ -48,9 +50,3 @@ enqueued.
This specification also applies to bounded queues, where (somewhat analogously)
\enqueue loops when the capacity is reached ($\nbelems = \capacity$), waiting
until room becomes available.
\begin{figure}
\input{figure-queue-spec-seq}
\bigskip
\input{figure-queue-spec-sc}
\end{figure}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment