\documentclass[12pt]{article}
\usepackage{amsmath}
\newcommand{\ignore}[1]{}
\newcommand{\Producer}{\mbox{\it Producer}}
\newcommand{\Consumer}{\mbox{\it Consumer}}
\newcommand{\GOTO}{{\sf goto}}
\newcommand{\IF}{{\sf if}}
\newcommand{\type}{\mbox{\it type}}
\newcommand{\Repeat}{{\rm repeat}}
\newcommand{\until}{{\rm until}}
\newcommand{\Value}{{\it Value}}
\newcommand{\Register}{{\it Register}}
\newcommand{\Val}{{\it Val}}
\newcommand{\PC}{\mbox{\it PC}}
\newcommand{\enq}{\mbox{\it enq}}
\newcommand{\deq}{\mbox{\it deq}}
\newcommand{\qed}{{$\hspace{2mm} q.e.d$}}
\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amstext}
\usepackage{amssymb}
\renewcommand{\mod}{\mbox{\rm \, mod\;}}
\def\newtheorems{\newtheorem{theorem}{Theorem}[section]
\newtheorem{cor}[theorem]{Corollary}
\newtheorem{prop}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{sublemma}[theorem]{Sublemma}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem{question}[theorem]{Question}}
\newtheorems
\title{A Concurrent Buffer}
\author{Uri Abraham \footnote{mathematical models for concurrency 2014,
Ben Gurion University of the Neguev.}}
\begin{document}
\maketitle
\begin{abstract}
Using the notions of state and history we analyze and reason about a two-process concurrent buffer
algorithm.
\end{abstract}
\section{Concurrent buffer queue specification}
\label{S1}
We repeat in this section some definitions that were made in a previous lecture about queues, but now the queue is assumed
to have a bounded capacity.
A queue is a FIFO data structure which supports two operations, enqueue and dequeue, so that the value of any dequeue operation $D$ is
the value of the earliest enqueue $E$ that precedes $D$ and whose value has not yet been dequeued. We want in this section to
answer the following specification problem. Suppose that we have a sequence of events $e_0,e_1,\ldots$ which may be infinite,
and is such that every event $e_i$ is either a dequeue event (we write $deq(e_i)$) or is an enqueue event (and we
write then $enq(e_i)$). Suppose moreover that we have a function $\Val^\ast$ defined over these events with value into some Data domain.
The question is this: under what conditions can we say that the sequence is a sequence of valid operations on a bounded fifo queue?
A queue-state is represented by a finite sequence $Q$ of $Data$ values. If $n=|Q|$ is the length of the sequence, then $Q[0],\ldots,Q[n-1]$
are the Data items of $Q$. We think of $Q[0]$ as being the ``head'' value of $Q$ and $Q[n-1]$ as its tail value. We assume a bound $K$ on the length of the queue, and so $0\leq |Q| \leq K$. The queue is said to be empty when $|Q|=0$
and full when $|Q|=K$. The concatenation operation on sequences is notated $^\frown$. So if $P$ and $Q$ are two sequences of length
$n=|P|$ and $m=|Q|$ then $P^\frown Q$ is the sequence $R$ of length $n+m$ defined by the following equations.
\begin{align}
R[i] &=P[i]\ \text{for } 0\leq i < n\ \text{and}\\
R[j] &= Q[j-n]\ \text{for } n\leq j < n+m.
\end{align}
When $d$ is some $Data$ value then $\langle d \rangle$ denotes the sequence of length $1$ whose sole entry is $d$,
and we can also write $Q^\frown d$ (or $d^\frown Q$) rather than $Q^\frown \langle d\rangle$ (or $\langle d\rangle ^\frown Q$).
\begin{definition}
\label{D1}
Let $\overline{e}=\langle e_0,e_1,\ldots \rangle$ be a sequence of events such that for every index $i$ of the sequence either $\enq(e_i)$
or else $\deq(e_i)$, and for every index $i$, $\Val^\ast(e_i)$ is some $Data$ value or else the empty value $\emptyset$. Then we say that $\overline{e}$ satisfies the ``state-based'' queue specifications
for a queue of capacity $K$ if there are queue states $pre(e_i)$ and $post(e_i)$ for every index $i$ of the sequence such that the following hold.
\end{definition}
\begin{enumerate}
\item
$pre(e_0)$ is the empty sequence. For every $i$ $pre(e_i)$ and $post(e_i)$ are sequences of length $\leq K$ of Data values.
\item For every index $i$ such that $i+1$ is also an index of the sequence $post(e_i)=pre(e_{i+1})$.
\item If $\deq(e_i)$ and $d=\Val^\ast(e_i)$ is a Data value, then $Q=pre(e_i)$ is nonempty and $Q= d^\frown post(e_i)$.
If $\deq(e_i)$ and $\Val^\ast(e_i)=\emptyset$, then $pre(e_i)$ is the empty sequence and $post(e_i)$ remains the empty sequence.
\item If $\enq(e_i)$ and $d=\Val^\ast(e_i)$, then $pre(e_i)^\frown d=post(e_i)$.
\end{enumerate}
A clear advantage of the state based queue specification is its simplicity. The regime of a queue is that items are added
at the tail and removed from its head.
\section{A bounded buffer algorithm}
We assume two processes a \Producer\ and a \Consumer\ that coordinate their actions with a bounded buffer $B$ that can
contain up-to $k\geq 1$ items. The buffer is full when it contains $k$ items, and it is empty when it contains no items.
The \Producer\ loads an item only when the buffer is not full, and the \Consumer\ unloads an item only when it is non-empty.
The role of the algorithm is to ensure that this is indeed the case. We assume that the buffer stores its
items in an array $B[0,\ldots,k-1]$ of items. We say that $B[i]$ is the $i$-th entry of $B$.
The algorithm uses two registers $s$ and $r$ that hold natural numbers. Register $s$ is written by the \Producer\
process. This variable records the number of items produced so far by the \Producer, and $s\pmod{k}=i$ is the index of the entry $B[i]$ into which \Producer\ is going to deposit
its $s$-th item.
Register $r$ records the number of items that were removed by the \Consumer, and $r \pmod{k}=j$ is the index of the entry $B[j]$ from which \Consumer\ is going to unload its $r$-th item.
Initially $r=s=0$.
The Bounded Buffer algorithm is in figure \ref{AP}\footnote{The algorithm appears in Abraham, {\em Models for Concurrency} Gordon and Breach 1999. A similar algorithm was discussed by Lamport in ``Proving the correctness of Multiprocess Programms, IEEE Transactions on Software Engineering, 1977.}.
The state variables include, in addition to $r$ and $s$, two program counter variables $PC_p$ and $PC_c$ which are the program
counters of the \Producer\ and \Consumer\ processes respectively. The value of the program counter indicates which instruction
is going to be executed next.
To sum-up, the set of state variables is \[V=\{ s,r, PC_p, PC_c, B\}.\]
The types of the variables is as follows. Variables $s$ and $r$ take values that are natural numbers. Variable $PC_p$ takes values in
$\{1_p,\ldots,4_p\}$, and $PC_c$ in $\{1_c,\ldots,4_c\}$. Variable
$B$ is an array of length $k$ (with enries $B[0],\ldots, B[k-1]$ of Data type).
A state is thus a function that assigns
to each of the variables in $V$ a value in its type\footnote{Type restrictions promote understanding of the algorithm and hence they are very useful. It is part of the proof obligations to ensure that the variables are indeed in their types. For this reason, when defining steps, one must
be very careful to note that the type restrictions are respected.}
If $\varphi$ is any statement about the state variables and $S$ is any state, then the satisfaction relation
$S\models \varphi$ says that $\varphi$ holds in $S$. For example, $S\models s-rj$ then $[i,\ccdot, j)_k= \langle i,\ldots, k-1\rangle^\frown \langle 0,\ldots, j-1\mod k\rangle$ (a sequence of
length $j-i \mod k$, that is $k-(i-j)$).
\end{enumerate}
\begin{lemma}
\label{LS}
Let $i,j\in [0,\ldots,k)$ be indices. If $[i,\ccdot, j)_k$ is of positive length $\ell>0$, then $[i+1\mod k,\ccdot,j)_k$
is the sequence of length $\ell-1$ obtained by removing the first member, $i$, of $[i,\ccdot, j)_k$.
If $[i,\ccdot, j)_k$
is of length $\ellj$, then $B\circ [i,\ccdot, j)_k$ is the sequence (of length $k-(i-j)$) $\langle B[i],\ldots, B[k-1],B[0],\ldots,B[j-1]\rangle$.
\end{enumerate}
For example, suppose that $B$ is the sequence (array) of length $7$: $B=\langle a,b,c,d,e,f,g\rangle$. So $B[0]=a,\ldots,B[6]=g$. Then
$B\circ [3,\ccdot,6)_7 = \langle d,e,f\rangle$ and $B\circ [6,\ccdot,3) = \langle g,a,b,c\rangle$.
The following is an immediate consequence of Lemma \ref{LS}.
\begin{lemma}
\label{LT}
If $R=B\circ[i,\ccdot, j)_k$ is of positive length $\ell>0$, and
$R' = B\circ[i+1\mod k,\ccdot, j)_k$, then $R'$ is the result of the dequeue operation on $R$,
and $B[i]$ is the value that this dequeue
operation returns.
Likewise, if $R= B\circ[i,\ccdot, j)_k$
is of length $\ell