Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Glen Mével
cosmo
Commits
86021dc5
Commit
86021dc5
authored
Feb 26, 2021
by
POTTIER Francois
Browse files
A few typos and comments.
parent
295a0eda
Changes
1
Hide whitespace changes
Inline
Side-by-side
papers/icfp2021/queue-impl.tex
View file @
86021dc5
...
...
@@ -9,7 +9,7 @@
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
a
n
item at one extremity of the queue (the
\emph
{
head
}
);
\dequeue
extracts
an item ---~if there is one~--- from the other extremity (the
\emph
{
tail
}
).
In a concurrent setting, a legitimate question is whether several threads can
...
...
@@ -34,6 +34,10 @@ more frequently than they are dequeued; in this situation, a bounded queue has n
exhausting system memory; instead, if the maximum size is reached,
enqueuing either blocks or fails.
% TODO: ref for bounded pools/queues: Herlihy & Shavit 10.1
% FP ce n'est pas seulement une question de limiter l'occupation mémoire
% de la file, mais aussi une façon de forcer les producteurs à attendre
% une fois que la file est pleine; donc c'est un mécanisme de contrôle
% de flux.
% TODO: find where this implementation was first described
% ref: https://github.com/rigtorp/MPMCQueue
...
...
@@ -46,8 +50,8 @@ 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
k
now give an intuition as to how the code operates and why it is correct. We
state some properties, but the
full
proof of the
m being invariant
is deferred
We now give an intuition as to how the code operates and why it is correct. We
state some properties, but the proof of the
se properties
is deferred
until~
\sref
{
sec:queue:proof
}
.
Items are identified by their
\emph
{
rank
}
(starting at zero) in the queue
...
...
@@ -117,6 +121,10 @@ is still in use for a rank less than~\head\
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).
%
% FP ces remarques techniques entre parenthèses sont intéressantes
% mais un peu difficiles à absorber en première lecture. Elles
% seraient mieux en footnote?
%
This implies that
$
\head
=
\tail
+
\capacity
$
.
We say that the buffer is
\emph
{
empty
}
when slot~
$
\modcap\tail
$
has a status
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment