Commit a6956502 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Réorganisation implémentation.

parent 13e8bcc6
......@@ -7,7 +7,7 @@
\input{figure-lang-syntax}
The syntax of (an idealized fragment of) \mocaml{} is presented
The syntax of our idealized version \mocaml{} is presented
in~\fref{fig:syntax}. It is equipped with a standard call-by-value,
left-to-right evaluation. The parts of interest are the memory operations.
Their semantics have been described in our earlier paper~\citecosmo;
......
......@@ -5,29 +5,27 @@
\section{Implementation of a Bounded MRMW Queue Using a Ring Buffer}
\label{sec:queue:impl}
\input{lang}
\input{figure-queue-impl}
% TODO: find where this implementation was first described
% ref: https://github.com/rigtorp/MPMCQueue
We now present an implementation of a bounded MRMW queue, that satisfies the
specification devised in the previous section.
% TODO: \sref explicite ?
Its code appears in \fref{fig:queue:impl}; it is written in our \mocaml{} fragment.
We now present an implementation of a bounded MRMW queue, that satisfies the specification devised in \sref{sec:queue:spec}.
For the purpose of the formalization, it is written in an idealized version of the \mocaml{} language with a rigorously defined formal semantics, which we present in \sref{sec:lang} before showing its actual code (\sref{sec:queue:impl:presentation}, \sref{sec:queue:impl:code}) and giving intuitions about its mode of operation (\sref{sec:queue:impl:invariants}, \sref{sec:queue:impl:interactions}).
\input{lang}
\subsection{Presentation of the data stucture}
\label{sec:queue:impl:presentation}
\input{figure-queue-impl}
The queue uses a ring buffer of
fixed capacity~$\capacity \geq 1$. The buffer is represented by two arrays of
The code of the concurrent queue library we consider appears in \fref{fig:queue:impl}.
It uses a ring buffer of fixed capacity~$\capacity \geq 1$.
The buffer is represented by two arrays of
length~\capacity, \refstatuses and \refelements; in each slot (whose offset ranges from~$0$
included to~$\capacity$ excluded), the buffer thus stores a \emph{status} in an
atomic field and an \emph{item} in a nonatomic field. The data~structure also
has two integers stored in atomic references, \refhead and \reftail.
We now give an intuition as to how the code operates and why it is correct. We
state some properties, but the proof of these properties is deferred
until~\sref{sec:queue:proof}.
Items are identified by their \emph{rank} (starting at zero) in the queue
since its creation. The item of rank~\idx\ is stored in slot
``$\idx \mmod \capacity$'', which we denote as $\modcap\idx$.
......@@ -49,18 +47,14 @@ Each slot 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.%
%
\footnote{\label{fn:memleak}%
Technically, the slot stores a unit value~$\Unit$; indeed, keeping a stale
pointer could cause a memory leak.
}
%
In addition, for the concurrent queue operations to work properly, we must
remember for which rank each slot was last used.%
%
\footnote{%
Actually, we need not remember the full rank~\idx:
only the cycle, $\idx \div \capacity$, is needed.
}
%% \footnote{%
%% Actually, we need not remember the full rank~\idx:
%% only the cycle, $\idx \div \capacity$, is needed.
%% }
% JH : j'ai viré ce commentaire, qui ne me semble pas apporter d'information intéressante pour la compréhension de l'implémentation. Et c'est un peu confusant dans le flot du texte.
%
The status encodes this information in a single integer, as follows:
......@@ -78,44 +72,44 @@ Let~\head\ and~\tail\ be the value of references \refhead and \reftail,
respectively.
%
At any time, the ranks of items that are stored (or in the process of being stored)
in the queue range from~\tail\ included to~\head\ excluded. An invariant
in the queue range from~\tail\ included to~\head\ excluded. This, an invariant
property of the queue is:
%
\[
0 \leq \tail \leq \head \leq \tail+\capacity
\]
We say that the buffer is \emph{full} when slot~$\modcap\head$ has
a status less than $2\head$; in other words, the next slot at which to enqueue
is still in use for a rank less than~\head.%
\footnote{%
Either the slot has status $2(\head-\capacity)$ and some thread
is in the process of enqueuing the item of rank~$\head-\capacity$,
or it has status $2(\head-\capacity)+1$ and is occupied by that item.
}
%
This is implied by, but is weaker than, the equation $\head = \tail+\capacity$.%
\footnote{%
Some thread may have commited to dequeue the item of rank~$\head-\capacity$
without having completed that task yet; \reftail would be greater than
$\head-\capacity$ but the slot would still appear as occupied for that rank.
}
We say that the buffer is \emph{empty} when slot~$\modcap\tail$ has a status
less than $2\tail+1$; in other words, the next slot from which to dequeue is
still in use for a rank less than~\tail.%
\footnote{%
Either the slot has status $2(\tail-\capacity)+1$ and some thread
is in the process of dequeuing the item of rank~$\tail-\capacity$,
or it has status $2\tail$ and is available for a future item of rank~\tail.
}
%
This is implied by, but is weaker than, the equation $\head = \tail$.%
\footnote{%
Some thread may have commited to enqueue an item of rank~$\tail$
without having completed that task yet; \refhead would be greater than
$\tail$ but the slot would still appear as available.
}
%% We say that the buffer is \emph{full} when slot~$\modcap\head$ has
%% a status less than $2\head$; in other words, the next slot at which to enqueue
%% is still in use for a rank less than~\head.%
%% \footnote{%
%% Either the slot has status $2(\head-\capacity)$ and some thread
%% is in the process of enqueuing the item of rank~$\head-\capacity$,
%% or it has status $2(\head-\capacity)+1$ and is occupied by that item.
%% }
%% %
%% This is implied by, but is weaker than, the equation $\head = \tail+\capacity$.%
%% \footnote{%
%% Some thread may have commited to dequeue the item of rank~$\head-\capacity$
%% without having completed that task yet; \reftail would be greater than
%% $\head-\capacity$ but the slot would still appear as occupied for that rank.
%% }
%% We say that the buffer is \emph{empty} when slot~$\modcap\tail$ has a status
%% less than $2\tail+1$; in other words, the next slot from which to dequeue is
%% still in use for a rank less than~\tail.%
%% \footnote{%
%% Either the slot has status $2(\tail-\capacity)+1$ and some thread
%% is in the process of dequeuing the item of rank~$\tail-\capacity$,
%% or it has status $2\tail$ and is available for a future item of rank~\tail.
%% }
%% %
%% This is implied by, but is weaker than, the equation $\head = \tail$.%
%% \footnote{%
%% Some thread may have commited to enqueue an item of rank~$\tail$
%% without having completed that task yet; \refhead would be greater than
%% $\tail$ but the slot would still appear as available.
%% }
% GLEN: la terminologie "buffer vide/plein" est impropre: on dit que le buffer
......@@ -123,33 +117,9 @@ This is implied by, but is weaker than, the equation $\head = \tail$.%
% il se peut que d’autres cases plus loin aient déjà été vidées (idem pour
% "vide").
\subsection{Some invariants of the queue}
Once the queue has been created, the reference~\refhead is only accessed from
function~\tryenqueue. The only place where it is modified is the compare-and-set
operation in this function, which attempts to increment it by one, using
a compare-and-set operation. Hence this counter is strictly monotonic, and we
can regard a successful incrementation from~\head\ to~$\head+1$ as uniquely
attributing rank~\head\ to the candidate enqueuer. Only then it is allowed to
write into slot~$\modcap\head$.
Similarly, \reftail is only accessed from function~\trydequeue, is strictly
monotonic, and a successful incrementation from~\tail\ to~$\tail+1$ uniquely
attributes rank~\tail\ to the candidate dequeuer. Only then it is allowed to
write into slot~$\modcap\tail$.
The status of a given slot is strictly monotonic too. Indeed, there are two
places where it is updated.
As an enqueuer, when we write $2\head+1$, no other enqueuer updated the status
since we read it to be $2\head$, because only us have been attributed
rank~\head. In particular, it remained even, so no dequeuer tried to obtain
rank~\head\ and update the status of slot~$\modcap\head$. Hence, the status is
still $2\head$ when we overwrite it with $2\head+1$.
%
Symmetrically, the status is still $2\tail+1$ when a dequeuer overwrites it with
$2(\tail+\capacity)$.
\subsection{Explanation of the code}
\label{sec:queue:impl:code}
The function~\enqueue repeatedly calls \tryenqueue until it succeeds;
the latter can fail either because the buffer is full or because of a competing enqueuer.%
......@@ -163,24 +133,18 @@ When calling \tryenqueue, we start by reading the current value~\head\ of the
reference~\refhead. To check that slot~$\modcap\head$ is available for
rank~\head, we read its status.
%
If it differs from~$2\head$, we fail
%
(to be more precise,
a status less than~$2\head$ indicates that the buffer is full;
a status greater than~$2\head$ indicates interference from other threads and,
as explained later, this interference implies a competing enqueuer being
attributed rank~\head\ before we have).
If it differs from~$2\head$, we fail: a status less than~$2\head$ indicates that the buffer is full\footnote{Technically, the public state of the queue may contain less than $C$ elements in this case, so that we may consider it is not full. Here, by ``full'' we mean that next buffer slot is either not reclaimed by anyone or still in the process of being emptied by another thread. Even though the buffer is ``full'', it may have available slots if dequeing has completed more rapidly in these other slots.}, a status greater than~$2\head$ indicates interference from another competing enquing thread, which has been attributed rank~\head{} before we have.
If the status is $2\head$, then we try to increment \refhead from~\head\
to~$\head+1$.
%
If the CAS fails, we fail (it is again because of a competing enqueuer).
If the CAS fails, we fail: again, another competing enqueuer has been attributed rank~\head{}.
If the CAS succeeds, then we are attributed rank~\head\ and can proceed to
inserting an item into slot~$\modcap\head$. As explained earlier, its status has
inserting an item into slot~$\modcap\head$. As we will explain later, this implies that its status has
not changed since we read it: the slot is still available.
%
We write the new item, then we update the status accordingly. This update must
We write the new item, and then we update the status accordingly. This update must
come last, as it serves as a signal that the slot is now occupied with an item
and ready for dequeuers.
%
......@@ -195,15 +159,43 @@ the latter works analogously to \tryenqueue,%
%
\footnote{%
Overwriting the extracted value with a unit value~$\Unit$ is unnecessary for
functional correctness but, as mentioned in~\fnref{fn:memleak}, it prevents
memory leaks.
functional correctness but it prevents memory leaks.
}
%
and can fail either because the buffer is empty or because of a competing dequeuer.%
%
\footref{fn:distinguishfail}
\subsection{Monotonicity of the internal state of the queue}
\label{sec:queue:impl:invariants}
Once the queue has been created, the reference~\refhead is only accessed from
function~\tryenqueue. The only place where it is modified is the compare-and-set
operation in this function, which attempts to increment it by one, using
a compare-and-set operation. Hence this counter is strictly monotonic, and we
can regard a successful incrementation from~\head\ to~$\head+1$ as uniquely
attributing rank~\head\ to the candidate enqueuer. Only then it is allowed to
write into slot~$\modcap\head$.
Similarly, \reftail is only accessed from function~\trydequeue, is strictly
monotonic, and a successful incrementation from~\tail\ to~$\tail+1$ uniquely
attributes rank~\tail\ to the candidate dequeuer. Only then it is allowed to
write into slot~$\modcap\tail$.
The status of a given slot is strictly monotonic too. Indeed, there are two
places where it is updated.
As an enqueuer, when we write $2\head+1$, no other enqueuer updated the status
since we read it to be $2\head$, because only us have been attributed
rank~\head. In particular, it remained even, so no dequeuer tried to obtain
rank~\head\ and update the status of slot~$\modcap\head$. Hence, the status is
still $2\head$ when we overwrite it with $2\head+1$.
%
Symmetrically, the status is still $2\tail+1$ when a dequeuer overwrites it with
$2(\tail+\capacity)$.
\subsection{Interactions between threads}
\label{sec:queue:impl:interactions}
%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
......@@ -244,7 +236,7 @@ Possible situations are:
not done yet;
%
in that case the enqueuer continues unaffected,
and the candidate dequeuer fails because the buffer is empty;
and the candidate dequeuer fails because the buffer appears empty;
\item symmetrically, a candidate enqueuer checking whether slot~$\modcap\head$
is available for storing an item of rank~\head\ while a dequeuer is still in
......
......@@ -19,9 +19,9 @@ Ghost state in Iris takes values from algebraic structures called CMRAs.
For the purpose of this paper, it is enough to think of a CMRA as a set
equipped with a binary composition operation $(\mtimes)$ that is partial,
associative and commutative.%
\footnote{%
CMRAs are also step-indexed, but this is out of the scope of this paper.
}
%% \footnote{%
%% CMRAs are also step-indexed, but this is out of the scope of this paper.
%% }
Ghost state values are assigned to ghost variables.
The separation logic assertion~$\ownGhost\gname{a}$, where $a$ is an element of
some CMRA, intuitively means that we own a fragment of the ghost variable
......
Supports Markdown
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