\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-r<k$ means that
$S(s)-S(r)<k$. States can thus be considered to be structures with a well defined satisfaction relation.

An initial state for the buffer algorithm is a state $S$ such that $S(s)=S(r)=0$, $S(PC_p)=1_p$ and $S(P_c)=1_c$. And $S(B)$ is
an arbitrary array of length $k$ of Data values.

A pair of states (over $V$) is called a ``step'' when it describes an atomic change of the system (a detailed definition
is given below).
 
There are two kind of steps in our buffer system: steps of the \Producer\ process and steps of the \Consumer.
Any instruction of the
protocol corresponds to a set of steps: those steps that represent an execution of the instruction.


 A {\em history} (for our protocol) is
a sequence of states  over $V$,
 $$H= \langle S_i \mid i \in \omega \rangle,$$ where $\omega$ is the set of natural
 numbers (we assume for simplicity that $H$ is infinite),
  such that $S_0$ is an initial state and for every $i\in \omega$ 
there is an instruction $R$ in the protocol (of one of the two processes) such
that step $\langle S_i, S_{i+1}\rangle$ is an execution of $R$.
A history contains steps by  the two processes, and thus the
execution is said to ``interleave'' the actions of the processes in a history.

The collection of all resulting histories describes the possible
executions of the given protocol, and in order to prove that all protocol executions satisfy
a certain property $\varphi$ 
we have to prove that each of
the resulting histories satisfies this property.


\begin{figure}
\fbox{
\begin{tabular}{l|l}

 \begin{minipage}[t]{70mm} 
 \vspace{1mm}
\Producer

\begin{enumerate}
\item[$1_p$.] \IF\ $s-r = k \ \GOTO\ 1_p$;

\item[$2_p$.] produce a Data value $d$ and\\ $B[s\pmod{k}]:= d$;
\item[$3_p$.] $s:= s+1 $;
\item[$4_p$.] \GOTO\ $1_p$
\end{enumerate}

\end{minipage}
&
\begin{minipage}[t]{60mm}
\vspace{1mm}
\Consumer

\begin{enumerate}
\item[$1_c$.] \IF\ $s=r$ \GOTO\ $1_c$;


\item[$2_c$.] consume $B[r\pmod{k}]$;

\item[$3_c$.] $r:= r+1 $;

\item[$4_c$.] \GOTO\ $1_c$;
\end{enumerate}


\vspace{1mm}
\end{minipage}

\end{tabular}
}%%%%%%
\caption{The bounded concurrent buffer algorithm for two processes.}
\label{AP}
\end{figure}  

The steps of the buffer algorithm can be given names by reference to the change of the program counter. So, for example
a $(1_p,1_p)$ step is an execution of instruction $1_p$ by the \Producer\ process in which condition $(s-r=k $) holds.
And a $(1_p,2_p)$ step is an execution of this instruction in which the condition does not hold.
A $(2_p,3_p)$ step is said to be a loading step, and a $(2_c,3_c)$ step is an unloading step.



\begin{exercise}
Write in details the steps of the buffer algorithm.
\end{exercise}
As an example we bring the following. 
\begin{definition}
\label{DE}
A $(2_p,3_p)$ step is a pair of states $(S,T)$ such that the following holds.
\begin{enumerate}
\item $S(PC_p)=2_p$, $T(PC_p)=3_p$,

\item for every buffer index $0\leq i < k$, if $i\not= S(s)\pmod{k}$ then $T(B)[i]=S(B)[i]$.
For $i=S(s)\pmod{k}$, $T(B)[i]$ is an arbitrary message. Every state
variable other than  $B$ and  $PC_p$ has the same value in $T$ as in $S$.
\end{enumerate}
If $e=(S,T)$ is a $(2_p,3_p)$ step, then we say that $e$ is an enqueue step (we can write $enq(e)$) and we define
$\Val(e)=T(B)[T(S(s) \pmod{k}]$ as the value of this step\footnote{This is {\em not} the $\Val^\ast$ function defined
in Section \ref{S1}.}.

Similarly, if $e=(S,T)$ is a $(2_c.3_c)$ step, then we say that $e$ is a dequeue step (we can write $deq(e)$) and we define
$\Val(e)=T(B)[T(r) \pmod{k}]$ as the value of this step.
\end{definition}


\subsection{The assertional argument}

Recall that an assertion is a statement about states, and an invariant is an assertion $\varphi$ which holds in every initial state and which
has the following property. If $(S,T)$ is any step such that $\varphi$ holds in $S$, then $\varphi$ holds in $T$ as well.

We have proved the following simple but important theorem.
If $\varphi$ is an invariant and $R$ a history as above, then $\varphi$ holds in every state of $R$.

\begin{exercise}
\label{E2} Prove that the following conjunction of A, B, and C is an invariant.
\begin{enumerate}
\item[A.]
Every state variable is in its type. In particular $B$ is an array of Data values.
\item[B.] $0\leq s-r\leq k$.
\item[C.]
If $PC_p=2_p,3_p$ then $s-r < k$. If $PC_c=2_c,3_c$ then $0<s-r$.


\end{enumerate}
\end{exercise}
Directions. First prove that it holds in any initial state.

Then consider in turn each of the following ten kinds of steps. For each kind and for every step $st=(S,T)$ of that kind, assume that $S\models A\wedge B\wedge C$, and then prove that $T\models X$ for each of $X=A,B,C$.
\begin{enumerate}
\item $st$ is some $(1_p,1_p)$ step. 

\item $st$ is some $(1_p,2_p)$ step.

\item $st$ is some $(2_p,3_p)$ step.

\item $st$ is some $(3_p,4_p)$ step.
\item $st$ is some $(4_p,1_p)$ step.

\item $st$ is some $(1_c,1_c)$ step. 

\item $st$ is some $(1_c,2_c)$ step.

\item $st$ is some $(2_c,3_c)$ step.

\item $st$ is some $(3_c,4_c)$ step.
\item $st$ is some $(4_c,1_c)$ step.


\end{enumerate}

\section{A queue is implemented}
Exercise \ref{E2} does not yet establish that our algorithm implements a queue. In order to prove this main result
we need to introduce a new variable $Q$ whose values are Data sequences. This variable is not to be found in the algorithm text of Figure
\ref{AP}--it is an artificially introduced data structure which behaves as a queue should behave (that is as specified in Section \ref{S1}).
The correctness proof then has to show that the values of the dequeue steps in a history are equal to the values of the corresponding
dequeues of the hypothetical queue $Q$. So now we will have two functions that give values to enqueue and dequeue steps. The \Val\ function
which was defined above in Definition \ref{DE}, and the $\Val^\ast$ which is defined in Section \ref{S1} and the correctness proof has
to establish that these two functions are equal. This is going to be clearer with the additional details that follow.

We add a new state variable $Q$ whose values are sequences of Data items. So now the set of variables is redefined as:
\[ V= \{ s,r, PC_p, PC_c,B, Q\}.\]
An initial state is a state $S$ such that $S(s)=S(r)=0$, and $S(PC_p)=1_p, S(PC_c)=1_c$, and $S(B)$ is an array of length $k$ of Data
values, as before, and the additional requirement now is that $S(Q)$ is the empty sequence $\emptyset$. That is, the queue is initially
empty.

Steps are defined as before but with additional requirements for the enqueue and dequeue steps (that is, the $(2_p,3_p)$ and $(2_c,3_c)$
steps). 
\begin{enumerate}
\item {\em Enqueue steps.} The additional requirement for a $(2_p,3_p)$ step $(S,T)$ is that $T(Q)=S(Q)^\frown \langle T(d)\rangle$. That is, the queue $Q$
is extended with the newly produced Data value added to its tail.  And if $e = (S,T)$ is some $(2_p,3_p)$ step then in addition to the
$\Val$ function that was defined in \ref{DE}, we define $\Val^\ast(e) = T(d)$. (So $\Val^\ast(e)=\Val(e)$, and the two functions agree by definition on the enqueue steps.)
\item {\em Dequeue steps.}
If $e=(S,T)$ is a $(2_c,3_c)$ step, then in addition to the requirements of Definition \ref{DE} we ask the following.
If $S(Q)=\emptyset$, then $T(Q)=\emptyset$ and we define $\Val^\ast(e)=\emptyset$. That is, if the queue is empty then
the queue remains empty in a dequeue step and the value$^\ast$ of the step is the empty value $\emptyset$. But if
$S(Q)\not=\emptyset$ and $x$ is the head value of the queue (that is $x= S(Q)(0)$) then we define $\Val^\ast(e)=x$
and $\langle x\rangle^\frown S(Q) = T(Q)$ (or in simple words, $T(Q)$ is obtained from $S(Q)$ by removing the first item
$x$ of $S(Q)$).
\end{enumerate}
Now consider an execution history of our buffer algorithm, $R = \langle S_i\mid i\in \omega \rangle$,
 where the states $S_i$ are states with the added variable $Q$. If we prove that the length of $Q$ never succeed $k$ (that is
$|S_i(Q)|\leq k$ for every index $i$) and that for every dequeue step $e_i=(S_i,S_{i+1})$ $\Val^\ast(e_i)=\Val(e_i)$ then
we have proven that the algorithm implements a queue. With this aim in mind, we first introduce definitions and notations.

\newcommand{\ccdot}{\cdot\cdot}

The set $[0,\ldots,k) = \{i\mid 0\leq i < k\}$ is supplied with the $\mod k$ successor function that takes $i$ to $i+1\mod k$.
 For indices $i,j\in [0,\ldots, k)$, we denote with
 $[i,\ccdot ,j)_k$ the sequence that goes in a circular way from $i$ to $j-1 \pmod{k}$. 
So, for example, if $k=7$ then the $\mod 7$ successor of $6$ is $0$, $[3,\ccdot.6)_7$ is the sequence
$\langle 3,4,5\rangle$, and  $[6,\ccdot,3)_7$ is the sequence $\langle 6,0,1,2\rangle$. Note also that
$[5,\ccdot,0)$ is the sequence $\langle 5,6\rangle$. The formal definition is the following.
\begin{enumerate}
\item If $i=j$ then $[i,\ccdot, j)_k = \emptyset$.

\item If $i<j$ then $[i,\ccdot, j)_k$ is the sequence of length $j-i$ that enumerates the interval $[i,\ldots,j)$.
That is, $(i,\ccdot, j)_k= \langle i,\ldots, j-1\rangle$.
\item If $i>j$ 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 $\ell<k$, then $[i,\ccdot, j+1\mod k)_k$ is the sequence of length $\ell+1$ obtained by adding $j$ to
$[i\ccdot j)_k$. That is $[i,\ccdot, j+1\mod k)_k =[i\ccdot j)_k^\frown \langle j \rangle $.
 \end{lemma}

For example, for $k=7$, $[6,\ccdot,0)_7 = \langle 6\rangle$ and $[6+1 \mod 7,\ccdot,0)_7= \emptyset$. And 
$[3,\ccdot, 6+1\mod 7)_7  = \langle 3,4,5,6\rangle = [3,\ccdot,6)_7^\frown 6$.

If $B$ is an array of length $ k$ of Data values and $0\leq i,j<k$ are indices, then $B\circ [i,\ccdot, j)_k$ denotes the 
sequence of Data values obtained as the composition of the functions $B$ and $[i,\ccdot, j)_k$. 
Following an intuitive image, we can say that $B\circ [i,\ccdot, j)_k$ is the {\em arc} of $B$ that extends from index
$i$ and up-to (but not including) index $j$.  In details, the definition is
the following.
\begin{enumerate}
\item If $i=j$ then  $B\circ [i,\ccdot, j)_k$ is the empty sequence.
 

\item If $i<j$, then  $B\circ [i,\ccdot, j)_k$ is the sequence (of length $j-i$) 
\[B[i],\ldots, B[j-1].\] (or, in another notation
the sequence $\langle B[\ell]\mid i\leq \ell < j\rangle$). 

\item If $i>j$, 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<k$, if $B'$ is an array of length $k$ with the same entries as $B$ 
except possibly that  $d=B'[j]$ is some given Data value and we define  $R' = B'\circ[i ,\ccdot, j+1\mod k)$, then $R'$ is obtained 
by enqueueing the value $d$ to $R$.
\end{lemma}

For example, if $B$ is the array of length $7$ as above, and $R= B\circ [3,\ccdot, 6)_7 = \langle d,e,f\rangle$, then after executing 
$B[6] : = h$, $B\circ [3,\ccdot, 0)_7$ is equal to $\langle e,f,g,,h\rangle$.

In the following theorem we consider equation $(B\circ[m\mod{k},\ccdot, n\mod{k})_k) = Q$; using the arc imagery we can say that
 it holds in state $S$ iff the  sequence
$S(Q)$ is equal to the arc of $S(B)$ that extends from index $S(i)$ and up-to (but not including) index $S(j)$.
\begin{theorem} Let $m$ and $n$ be natural numbers and $\varphi(m,n)$ be the statement 
\begin{equation}
\label{EE} (B\circ[i,\ccdot,j)_k) = Q,\end{equation}
\end{theorem}
where $i = m\mod{k}$ and $j = n\mod{k}$. 
The following conjunction $\alpha = E_1\wedge E_2\wedge E_3\wedge E_4$ is an invariant of our buffer algorithm.

\begin{enumerate}
\item[$E_1$] If $PC_p\not = 3_p$ and $PC_c\not = 3_c$ then $\varphi(r, s)$.
\item[$E_2$] If $PC_p=3_p$ and $PC_c=3_c$ then $\varphi(r+1, s+1 )$.
\item[$E_3$] If $PC_p\not = 3_p$ and $PC_c=3_c$ then $\varphi(r+1 , s )$.
\item[$E_4$] If $PC_p=3_p$ and $PC_c\not = 3_c$ then $\varphi(r, s+1)$.

\end{enumerate}

It is convenient to use the following notation. If $\tau$ is any expression that involves state variables, if $S$ is
any state, then $\tau^S$ denotes the value of $\tau$ as it is evaluated in state $S$. For example, expression
$B\circ[r+1\mod{k},\ccdot, s\mod{k})_k$ involves variables $B$, $r$ and $s$, and so 
\[(B\circ[r+1\mod{k},\ccdot, s\mod{k})_k)^S= S(B)\circ [S(r)+1\mod{k},\ccdot, S(s)\mod{k})_k.\]

We sketch some steps of the proof and let the reader complete the rest. We first have to prove
that our invariant $\alpha$ holds in every initial state.
If $S$ is an initial state then $S\models Q=\emptyset\wedge r=0\wedge s=0$. But $[0,\ccdot,0)_k=\emptyset$ and hence $\varphi(0,0)$
 is obvious. (Since the antecedents\footnote{In an implication $X\rightarrow Y$, $X$ is the antecedent and $Y$ the subsequent
of the implication.} of $E_2,E_3$ and $E_4$ are false in the initial state $S$, these statements are true.)
 
Now we have to deal with each type of step. As an example we take $(S,T)$ to be some $(2_p,3_p)$ step
and assume that $\alpha$ holds in $S$. We have to prove that $\alpha$ holds in $T$ as well.
Recall the definition of $(2_p,3_p)$ steps for states with the additional variable $Q$:
a $(2_p,3_p)$ step is a pair of states $(S,T)$ such that the following holds.
\begin{enumerate}
\item $S(PC_p)=2_p$, $T(PC_p)=3_p$,

\item for every buffer index $0\leq i < k$, if $i\not= S(s)\pmod{k}$ then $T(B)[i]=S(B)[i]$.
For $i=S(s)\pmod{k}$, $T(B)[i] = T(d)$ is an arbitrary Data value. Every state
variable other than  $B$, $d$ and  $PC_p$ has the same value in $T$ as in $S$.

\item  $T(Q)=S(Q)^\frown \langle T(d)\rangle$.

\end{enumerate}



Since $T\models PC_p=3_p$, there are two cases that we have to consider: $T\models PC_c=3_c$ and $T\models PC_c\not = 3_c$.
\begin{enumerate}
\item $T\models PC_c=3_c$. In this case the antecedent of $E_2$ holds and we have to prove that $T\models \varphi(r+1, s+1 )$ (note that
statements $E_1,E_3,E_4$ hold trivially in $T$ since their antecedents are false). In state $S$, $PC_p=2_p$ and $PC_c=3_c$ (as the value of
$PC_c$ does not change in this step). As $\alpha$ holds in $S$, $S\models E_3$ and so $S\models
\varphi(r+1 , s )$. That is
\[S\models  (B\circ[r+1\mod{k},\ccdot, s\mod{k})_k) = Q.\]
And we have to prove that
\begin{equation}
\label{Eq} T\models (B\circ[r+1\mod{k},\ccdot, s+1\mod{k})_k) = Q.\end{equation}
	How $Q$ is changed in this step? $T(Q)=S(Q)^\frown\langle T(d)\rangle$ by definition of this step.
	
	How $B$ is changed in this step? If $0\leq i <k$ and
 $i\not=T(s)\mod k$ then $T(B)[i]=S(B)[i]$, and, for $i=T(s)\mod k$, $T(B)[i]=T(d)$. Note that by Exercise \ref{E2} (itec $C$)
$S\models 0<s-r<k$, and hence $T\models 0<s-r<k$ (as these variables do not change). So $T\models 0\leq s-(r+1)<k$. Thus the length of 
$([r+1\mod{k},\ccdot, s\mod{k})_k)^S$  is $s-(r+1)<k$, and (the second statement of) Lemma \ref{LT} says then that 
$(B\circ[r+1\mod{k},\ccdot, s+1\mod{k})_k)^T$ is obtained from $(B\circ[r+1\mod{k},\ccdot, s\mod{k})_k)^S$ by enqueing $T(d)$.
Thus proving (\ref{Eq}).

\item The second case is when $T\models PC_c \not = 3_c$. 
\begin{exercise}
\label{LE}: complete this case.
\end{exercise}
\end{enumerate}

For the next example we consider a $(3_p,4_p)$ step $(S,T)$. That is, an execution of instruction $s:=s+1$.
 Suppose that $\alpha$ holds in $S$ and we have to prove that it holds
in $T$ as well. Again there are two cases, depending on whether $T\models PC_c=3_c$ or not. Suppose for example that
in state $T$ $PC_c\not = 3_c$. Hence our obligation is to prove that $E_1$ holds in $T$ since the antecedent of all other
conjuncts of $\alpha$ are false in $T$. 
in state $T$ $PC_c\not = 3_c$,
 it follows that $S\models PC_c\not = 3_c \wedge PC_p=3_p$. So by $E_4$, $\varphi(r,s+1)$
holds in $S$.  Statement $\varphi(r,s+1)$ involves variables $B$, $Q$, $r$ which do not change in this step, and variable
$s$ which does, as $T(s)=S(s)+1$. Hence $T$ satisfies $\varphi(r,s)$ as required. 




We ask the interested student to complete the proof that $\alpha$ is an invariant, and we continue with the correctness proof
assuming that we already know that $\alpha$ holds in every state of the given history.

Recall that the main issue in proving that the algorithm implements a queue is in proving that for every dequeue step $e$ in
the history $\Val(e)=\Val^\ast(e)$. So let $e = (S,T)$ be one of the dequeue steps in the history (i.e. a $(2_c,3_c)$ step).
By Definition \ref{DE},
 \begin{equation}
\label{Ev1} \Val(e) = T(B)[T(r) \pmod{k}]
\end{equation} is the value of this step. 

In state $S$, $PC_c=2_c$ and hence (by Exercise \ref{E2}) $0<s-r$ holds in $S$. If $S(PC_p)=3_p$ then $\varphi(r,s+1)$ holds in $S$
by $E_4$, and if $S(PC_p)\not = 3_p$ then $\varphi(r,s)$ holds by $E_1$. 
Hence  $S(Q)$ is either  $(B\circ[r\mod{k},\ccdot, s+1\mod{k})_k)^S$ or $(B\circ[r\mod{k},\ccdot, s\mod{k})_k)^S$.
In both cases, since $r<s$ in $S$, these arcs are nonempty, and hence $S(Q)$ is non-empty, and the first member of $S(Q)$
 (the one at its tail) is defined to be
$\Val^\ast(e)$. So $\Val^\ast(e) = \Val(e)$ follows.

\end{document}

