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

circular buffer --> ring buffer

parent 838a9b22
......@@ -60,7 +60,7 @@
\newcommand{\nl}{\texorpdfstring{\\}{}}
\title
{Formal Verification of a Concurrent Bounded Queue With a Circular Buffer}
{Formal Verification of a Concurrent Bounded Queue With a Ring Buffer}
\author{Glen Mével}
\affiliation{
......
% ------------------------------------------------------------------------------
% Overview of the implementation of the bounded queue with a circular buffer.
% Overview of the implementation of the bounded queue with a ring buffer.
\subsection{An Implementation of the Bounded MRMW Queue Using a Circular Buffer}
\subsection{An Implementation of the Bounded MRMW Queue Using a Ring Buffer}
\label{sec:queue:impl}
\input{figure-queue-impl}
......@@ -39,7 +39,7 @@ enqueuing either blocks or fails.
% ref: https://github.com/rigtorp/MPMCQueue
\fref{fig:queue:impl} shows the
implementation of the bounded MRMW queue in our \mocaml{} fragment. It uses a circular buffer of
implementation of the bounded MRMW queue in our \mocaml{} fragment. 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
......
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