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

group figures about spec

parent 4b6c1529
\begin{figure}
%\begin{figure}
\[\begin{array}{lcr}
\lahoareV
......@@ -17,4 +17,4 @@
\Description{A specification of the ``queue'' data structure under sequential consistency.}
\caption{A specification of the ``queue'' data structure under sequential consistency}
\label{fig:queue:specsc}
\end{figure}
%\end{figure}
\begin{figure}
%\begin{figure}
\[\begin{array}{lcr}
\hoareV
......@@ -17,4 +17,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:specseq}
\end{figure}
%\end{figure}
......@@ -7,8 +7,6 @@
\subsubsection{Specification in a sequential setting}
\input{figure-queue-spec-seq}
A queue is a first-in first-out container data~structure. At any time, it holds
an ordered list of items. It supports two main operations: \enqueue inserts
a provided item at one extremity of the queue (the \emph{head}); \dequeue extracts
......@@ -47,9 +45,12 @@ enqueued. % (by some other thread).
% queue de capacité bornée; dans ce cas il faut aussi que enqueue
% boucle quand la capacité est atteinte.
\subsubsection{Specification under sequential consistency}
\begin{figure}
\input{figure-queue-spec-seq}
\input{figure-queue-spec-sc}
\end{figure}
\input{figure-queue-spec-sc}
\subsubsection{Specification under sequential consistency}
We now allow for several threads to run concurrently. Let’s assume for now that
the memory model is sequentially consistent. % FP ajouter une référence?
......@@ -105,20 +106,6 @@ elements stored in the queue satisfy some predicate~$P$.
%
\[\begin{array}{lcr}
% \hoareV
% {\queueInv \isep \isQueueSC -}
% {\enqueue~\queue~\elem}
% {\Lam \Unit. \isQueueSC -}
%
%\qquad
%
% \hoareV
% {\queueInv \isep \isQueueSC -}
% {\dequeue~\queue}
% {\Lam \elem. \isQueueSC -}
%
%\\\\
\hoareV
{\queueInv \isep \isQueueSC P \isep P\,\elem}
{\enqueue~\queue~\elem}
......
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