\documentclass[12pt]{article}

\newcommand{\R}{{\sf R}}


\newcommand{\GOTO}{{\sf goto}}
\newcommand{\IF}{{\sf if}}

\newcommand{\type}{\mbox{\it type}}
\newcommand{\Copier}{{\it Copier}}
\newcommand{\Repeat}{{\rm repeat}}
\newcommand{\until}{{\rm until}}

\newcommand{\Value}{{\it Value}}
\newcommand{\Register}{{\it Register}}
\newcommand{\Val}{{\it Val}}
\newcommand{\COPY}{{\it COPY}}
\newcommand{\Changer}{{\it Changer}}
\newcommand{\val}{{\it value}}
\newcommand{\Pcopy}{\mbox{$P_{cpy}$}}
\newcommand{\Pchange}{\mbox{$P_{chg}$}}

\newcommand{\Rcopy}{\mbox{$\R_{cpy}$}}
\newcommand{\itRcopy}{\mbox{$R_{cpy}$}}

\newcommand{\Rchange}{\mbox{$\R_{chg}$}}
\newcommand{\itRchange}{\mbox{$R_{chg}$}}
\newcommand{\tcopy}{\mbox{$t_{cpy}$}}
\newcommand{\PCchange}{\mbox{$PC_{chg}$}}
\newcommand{\PC}{\mbox{\it PC}}
\newcommand{\PCcopy}{\mbox{$PC_{cpy}$}}

\newcommand{\qed}{{$\hspace{2mm} q.e.d$}}
\newcommand{\tchange}{\mbox{$t_{chg}$}}

\usepackage{amsmath} 
\usepackage{latexsym}
\usepackage{amstext}
\usepackage{amssymb}



\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{On States for concurrency}
\author{Uri Abraham \footnote{Mathematical models for concurrency 2014}\\
Ben Gurion University of the Neguev.}

\begin{document}
\maketitle

\begin{abstract}
The notions of state and history can be used not only to analyze and reason about a sequential program but also
about concurrent programs that involve two or more processes.
As an example to accompany this introduction we take the back-and-forth algorithm which is a very simple mutual exclusion
algorithm for two processes. It is a simplified version of the Peterson--Fischer algorithm which will be dealt with in
a later lecture.
\end{abstract}

 

\section{States and histories}
\label{SectionStatesandhistories}

The notion of {\em state} is one of the most important in this course. What is a state?
A state is a description of a system as if frozen in time. It is a snapshot: a picture taken at the highest possible shutter speed.
Is reality a sequence of states (like a movie is a sequence of frames)? or perhaps reality is the primitive notion and a state is an idealized derivative? The mathematical definition of a state is first given in its simplest (a function defined on a set of variables) and is then developed into a structure with its corresponding satisfaction relation definition. 

Suppose a set $V$ (members of $V$ are called state variables) 
and a map \type\ which assigns to every variable
$v \in V$ a set of possible values: $\type(v)$.
A {\em state} (over $V$ and \type) 
is a map $S$ defined on $V$ such that 
\begin{equation}
\label{E}
S(v)\in \type(v)\ \mbox{for every}\ v \in V.
\end{equation}


A protocol is a program designed to be executed by two or more processors
concurrently. We shall not give a formal definition of this notion here, but the
example of the Back-And-forth Protocol should clarify it, and we shall use this example
in order to exemplify states. 


Any protocol is associated with a set of variables. These are the local
variables of the involved processes, as well as the communication means
(registers, queues etc.) which are shared variables. In addition, we need
special variables, ``program counters'', which point to the enabled instructions
of each process. Let $V$ be the set of variables thus obtained, with $\type(v)$
defined for each $v\in V$. A state is a function over $V$ that respects the type of each variable.

A pair of states (over $V$) is called a ``step'' when it describes an atomic change of the system. 
 The possibility
that the two states in a step are equal is not excluded.
Any instruction of the
protocol corresponds to a set of steps: those steps that represent an execution of the instruction.

Special states are defined to be ``initial states'' of the protocol.

 A {\em history} (for a given protocol with variable set $V$) 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 such
that step $\langle S_i, S_{i+1}\rangle$ is an execution of $R$.
A history contains steps by  different processors, and thus their
steps  are ``interleaved'' in a history.

The collection of all resulting histories describes the possible
executions of the given protocol, and in order to prove that a protocol satisfies
a certain property $\varphi$ 
(such as mutual-exclusion) we have to prove that each of
the resulting histories satisfies this property. The problem with this approach is that the relation ``$H$ satisfies $\varphi$'' remains to be defined. Yet, at this stage of our lectures we leave this issue at the informal level and rely on our intuitions. We will return to this important question later on.

It turns out to be convenient to allow two consecutive states in a history that are equal: $S_{i+1} = S_i$. 
Step $\langle S_i, S_{i+1}\rangle$ is called in this case (by Lamport) a ``stuttering step''. 
Stuttering steps are natural in the following situation. Suppose
that $V_1$ and $V_2$ are sets of variables and $X_1$, $X_2$ are collections
of states over $V_1$ and $V_2$ (respectively). Suppose that $\pi : X_2 \to
X_1$ is a map from the state space $X_2$ to $X_1$.  A simple example of such a map is
when $V_1 \subseteq V_2$ and for every state $S \in X_2$, $\pi(S) = S
\restriction V_1$ (namely restriction of $S$ to the variables in $V_1$).
It is possible that $S \not = S'$ and yet $\pi(S)=\pi(S')$. If $H= \langle
S_i\mid i\in \omega\rangle$ is a history over $X_2$ (namely $S_i\in X_2$
for every $i\in \omega$) then we may define $\pi(H)=H'$ by the
equation $H' = \langle \pi(S_i)\mid i\in \omega\rangle$.
There are many situations in which it is natural and useful to view $H'$ as a history sequence. But
since it is possible that $S'_i = S'_{i+1}$ we must accept the possibility of stuttering steps in histories. 


\section{The back-and-forth Protocol}

This section  introduces the back-and-forth Protocol and uses it to illustrate the
 notions defined above: state, steps, and histories.
There are two (serial) processes: $\Pcopy$ (also known as the \Copier) and $\Pchange$ (aka the 
\Changer). They communicate with two single-writer, 
single-reader serial registers, $\Rcopy$ owned by $\Pcopy$,
 and $\Rchange$ owned by $\Pchange$. 
The owner of the register is its sole writer, and the other
process can read it.
The registers  are boolean, and their initial values are arbitrary.
The boolean values 0 and 1 will be called ``colors'' here.

The algorithms (or protocol) are presented in Figure \ref{AP}. In order to analyze this algorithm with
finer granularity we rewrite it in Figure \ref{BP} and replace the repeat--until instruction with an
explicit checking and go-to instruction.

\begin{figure}
\begin{tabular}{|l|l|}\hline
 \begin{minipage}[t]{53mm} 
 \vspace{1mm}

$\Pcopy$

 \vspace{2mm}
RepeatForever
\begin{enumerate}
\item[$1_0$.] \Repeat\ $\tcopy := \Rchange$\\
\until\ $\tcopy\not =\Rcopy$
\item[$2_0$.] $CS$
\item[$3_0$.] $\Rcopy := \tcopy$.
\end{enumerate}
\end{minipage}
&
\begin{minipage}[t]{53mm}
\vspace{1mm}
$\Pchange$

\vspace{2mm}

RepeatForever
\begin{enumerate}
\item[$1_1$.] \Repeat\ $\tchange := \Rcopy$\\
\until\ $\tchange = \Rchange$

\item[$2_1$.] $CS$

\item[$3_1$.] $\Rchange := 1 -\tchange.$
\end{enumerate}
\vspace{1mm}
\end{minipage}\\
\hline
\end{tabular}
\caption{The back-and-forth Protocol. Variables $\tchange$ and $\tcopy$ are local to the processes. they
hold binary values $\{ 0 , 1 \}$. Registers $\Rcopy$ and $\Rchange$ are serial.}
\label{AP}
\end{figure}  


\begin{figure}
\begin{tabular}{|l|l|}\hline
 \begin{minipage}[t]{53mm} 
 \vspace{1mm}
$\Pcopy$

\vspace{2mm}
RepeatForever

\begin{enumerate}
\item[$0_0$.]$\tcopy := \Rchange$;
\item[$1_0$.]  \IF\  $\tcopy =\Rcopy$ \GOTO\ $0_0$;

\item[$2_0$.] $CS$
\item[$3_0$.] $\Rcopy := \tcopy$.
\end{enumerate}
\end{minipage}
&
\begin{minipage}[t]{53mm}
\vspace{1mm}
$\Pchange$

\vspace{2mm}

RepeatForever

\begin{enumerate}

\item[$0_1$.] $\tchange := \Rcopy$
\item[$1_1$.] \IF\  $\tchange\not = \Rchange$ \GOTO\ $0_1$;

\item[$2_1$.] $CS$

\item[$3_1$.] $\Rchange := 1 -\tchange.$
\end{enumerate}
\vspace{1mm}
\end{minipage}\\
\hline
\end{tabular}
\caption{The explicit back-and-forth Protocol.}
\label{BP}
\end{figure}  

\subsubsection{States and histories of the back-and-forth Protocol}

Our aim now is to define histories 
of the back-and-forth Protocol, 
in the fashion outlined in the previous section. For this, we first
define the set \[Var=\{ \Rcopy, \Rchange, \tcopy, \tchange, \PCcopy, \PCchange\}\] of variables associated with the protocol, and for each variable $x\in V$ we also define $\type(x)$, the set of possible values
of $x$.
\begin{enumerate}
\item \Rcopy\ and \Rchange are the registers owned by $\Pcopy$ and $\Pchange$. The possible values of these registers are
$0$ and $1$. So $\type(\Rcopy)=\type(\Rchange)=\{0,1\}$.
\item $\tcopy$ and $\tchange$  are the local boolean variables of
$\Pcopy$ and $\Pchange$ respectively. 
$\type(t_0)= \type(t_1) = \{ 0, 1 \}$.
\item  \PCcopy\ and \PCchange\  are the program counters of $\Pcopy$ and $\Pchange$
respectively. 
$\type(\PCchange)= \{ 0_1, 1_1, 2_1,  3_1 \}$ refers to these lines 
in the \PCchange\  protocol. Similarly
$\type(\PCcopy)=\{0_0,1_0,2_0, 3_0\}$
refers to lines in the \Pcopy\ operation. For example, $\PCchange
= 3_1$ indicate that the write on \Rchange\  is enabled and \Changer\ is ready to execute ``$\Rchange := 1 -\tchange$''.
\end{enumerate}


A state of the back-and-forth protocol is a function defined on $Var$ which gives to every variable a value in its type.
Note that any such function is a state. We do not require that a state actually appears in one of the possible executions 
of the algorithm. The number of states is $2^4\times 4^2$.

An initial state is a state $S$ such that $S(\PCcopy)=0_0$ and $S(\PCchange)=0_1$ (so there are no restriction on the
values of the other variables). 
We define next the set of program steps.

A {\em program step}  is a pair of states $\langle S_1,S_2\rangle$ over $V$ that
represents an execution of an instruction (a line) of the protocol. In details we have the following.
 
Steps by $\Pcopy$:
\begin{enumerate}
\item 
A pair of states $s=\langle S_1,S_2\rangle$ constitutes a reading step of register \Rchange\ by $\Pcopy$ 
corresponding to line 0 of its code when the following conditions hold:
\begin{enumerate}
\item $S_1(\PCcopy)=0_0$, 
\item $S_2(\PCcopy)=1_0$, $S_2(\tcopy)  = S_1(\Rchange)$, and 
 for any state variable
$X$ other than $\PCcopy$ and $\tcopy$, $S_2(X)=S_1(X)$ (we will say ``and no other variable changes'').
\end{enumerate}
We say that these are $(0_0,1_0)$ steps.

\item 
A pair of states $s=\langle S_1,S_2\rangle$ 
forms a ``CS entry'' step when 

\[ S_1(\PCcopy)=1_0,\ S_1(\tcopy) \not = S_1(\Rcopy),\ S_2(\PCcopy)= 2_0,\]

and no  variable other than $\PCcopy$ changes. 

These steps are denoted $(1_0,2_0)$ steps. 

\item  
A pair of states $\langle S_1,S_2)$ is a ``failed check'' 
if $S_1(\PCcopy)=1_0$,
$S_1(\tcopy) = S_1(\Rcopy)$, $S_2(\PCcopy)= 0_0$, 
and no other variable changes. 

These are called $(1_0,0_0)$ steps.

\item A pair of states $\langle S_1,S_2)$ is a ``CS stay'' step when $S_2=S_1$. It is a ``CS exit'' step when
$S_1(\PCcopy)=2_0$, $S_2(\PCcopy)=3_0$, and no other variable changes.

These are $(2_0,2_0)$ and (respectively) $(2_0,3_0)$ steps.

\item We say that $\langle S_1,S_2\rangle$ is a write step (on register \Rcopy\ by $\Pcopy$) 
corresponding to line $3_0$ of the \Pcopy\ operation if
$S_1(\PCcopy)=3_0$, $S_2(\PCcopy)=0_0$, $S_2(\Rcopy)= S_1(\tcopy)$, and
no other variable changes.

These are said to be $(3_0,0_0)$ steps.
\end{enumerate}


\begin{exercise}
Write in details the steps of $\Pchange$.
\end{exercise}

A {\em history} is defined as a sequence $R = \langle S_i\mid i\in I\rangle$ where the index set $I$ is either $\omega$ (the set of natural numbers) or else a finite initial segment of $\omega$ such that $S_0$ is an initial state and for every $i$ the pair $(S_i,S_{i+1})$ is a program step by one of the processes. For simplicity of expression we will assume henceforth that $I=\omega$. 

\subsubsection{The assertional argument}
We shall argue that in any history $R = \langle S_i\mid i\in \omega \rangle$, every state $S_i$ satisfies the mutual exclusion property: it is not the case that $S_i(\PCcopy)=2_0$ and $S_i(\PCchange)=2_1$.
We begin with an intuitively appealing argument, of the type that is sometimes said to be ``behavioral''. This intuitive argument refers
to the algorithm of Figure \ref{AP}.

 Consider the steps by $\Pcopy$. An execution of the protocol consists of several reads of $\Rchange$ until a successful read is obtained (a read for which $\tcopy\not= \Rcopy$ holds). Then, if indeed a successful read is obtained, it is followed by a $CS$ event and then a write on $\Rcopy$. Similarly, a successful read for \Pchange\ is one in which condition 
$\tchange=\Rcopy$ holds, which indicates that the two registers had different values (when $\Rchange$ was read).
 There are two types of initial states, one in which $\Rchange=\Rcopy$ and another for which  $\Rchange\not = \Rcopy$. The argument is very much the same for both types. Assume for example that initially $\Rchange=\Rcopy$ holds. As long as this condition remains, \Pcopy\ will not be able to end the repeat loop of line 1 and to satisfy the \until\ $\tcopy\not = \Rcopy$ condition. Process \Pchange, however, will read register $\Rcopy$ and immediately satisfy its 
 ``\until\ $\tchange = \Rchange$'' condition and enter its $CS$. Then, assuming that at some stage \Pchange\ exits its critical section, it executes the write $\Rchange := 1 -\tchange$ for line 3, and reverses the situation. Now it is \Pchange\ that remains with $\PCchange =1_1$ and cannot satisfy its \until\ condition. Only when \Pcopy\ has a successful read, it can enter its critical section, and then when it exits its critical section it brings back the condition $\Rchange=\Rcopy$. Then and only then the ``door'' for \Pchange\ is opened again and it can enter its critical section.
 Continuing this way, we see that the critical sections of the two processes alternate with each process enabling the entry of the other process to its critical section.
 
 This argument, especially if accompanied with a picture is surely very convincing, and investigating concurrent algorithms
 in terms of such ``behavioral reasoning'' is very common. The reader may not immediately see why these behavioral arguments
 are not considered ``formal''. Indeed, the back-and-forth algorithm is so simple (not to say trivial)
  that it is not obvious to see what a formal proof could add. Experience of many researchers however has shown that this 
  type of behavioral argument, in
more complex situations, has lead to grave errors.

 One feature of formal arguments which should alert the reader to possible pitfalls when it is not present in the proof is the following. A mathematical proof is proving some property of some objects. Now you should always ask yourselves the following questions when reading an informal argument: are the objects that appear in the argument well defined? Can you locate in the proof the places where the exact definitions of these objects appear? If the answer to one of these question is negative, then there is a danger that the proof is too informal. In our case, the basic objects are the states and the steps defined above.
So the answer to the first question is ``yes''. We do have precise definition of the objects we deal with. But for the second question we have to admit that the answer is negative. Nowhere in this behavioral argument did we refer to the exact definition of the steps. So the behavioral argument fails to pass our formality test.

Yet behavioral arguments {\em are} attractive and natural and we do not want to prohibit their usage.
 In this course we want to study the tension between the formal and informal and between the behavioral 
 and state-based correctness proofs. A main aim of this course is to learn how to transform behavioral correctness arguments 
 into more formal correctness proofs. 

We describe in our course two approaches to concurrency. The invariant proof approach is based on the state and history notions, and the Tarskian models approach is based on relational structures. 
We begin with the invariant method which is almost universally accepted as the ``right'' approach to concurrency, and only
after learning some basic logic and investigating the notion of time will we be able to define Tarskian system executions with which behavioral arguments can be formalized.


An {\em invariant} is a statement $\varphi$ about states such that
\begin{enumerate}
\item $\varphi$ holds in every initial state. 

\item If $(S,T)$ is any step and $\varphi$ holds in $S$ then it holds in $T$ as well.

\end{enumerate}


We shall prove that the conjunction of the following four statements A, B, C, D is an invariant of the back-and-forth algorithm.
\begin{description}
\item[A:]  $\Rchange = \Rcopy \rightarrow \PCcopy = 0_0, 1_0$.


\item[B:] $\Rchange \not = \Rcopy \rightarrow \PCchange = 0_1, 1_1$.

\item[C:] If $\PCchange = 1_1\ \text{and}\ $(\tchange = \Rchange)$,\ \text{then}\ \Rchange = \Rcopy$.

\item[D:] If 
$\PCcopy = 1_0\ \text{and}\ (\tcopy\not= \Rcopy), \text{then}\ \Rcopy \not = \Rchange$.

\end{description}
Here, condition $\PCchange = 1_1, 2_1,3_1$, for example, is a shorthand for the disjunction $\PCchange=1_1 \vee \PCchange=2_1\vee\cdots$.

We also note that the constants $0_0,\ldots,3_0,0_1,\ldots,3_1$ are all different. Formally,
this statement is also an invariant. The proof that indeed this is an invariant does not
depend on the program that we analyze, but on the fact that no instruction can change the
value of a program constant. So, although we may use this fact in our proof, we do not need
to justify it.

Language: In any implication $\alpha = (X\ implies\ Y)$ we say that $X$ is the premiss ($X=prem(\alpha)$)
and $Y$ the conclusion ($Y=conc(\alpha)$). Recall that an implication holds (is true) in a state if the premiss is false
or the conclusion is true.

\begin{exercise}Prove that the conjunction (which we call $\varphi$) $A\wedge B\wedge C\wedge D$ is an invariant.

\end{exercise}
Directions. First prove that $\varphi$ holds in any initial state.

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

\item $s$ is some $(1_0,0_0)$ step.

\item $s$ is some $(1_0,2_0)$ step.

\item $s$ is some $(2_0,2_0)$ step.
\item $s$ is some $(2_0,3_0)$ step.

\item $s$ is some $(3_0,0_0)$ step.

\item $s$ is some $(0_1,1_1)$ step. 

\item $s$ is some $(1_1,0_1)$ step.

\item $s$ is some $(1_1,2_1)$ step.

\item $s$ is some $(2_1,2_1)$ step.
\item $s$ is some $(2_1,3_1)$ step.

\item $s$ is some $(3_1,0_1)$ step.

\end{enumerate}

Let $ME$ be the mutual-exclusion statement: $\PCcopy=2_0\rightarrow \PCchange\not= 2_1$.
\begin{exercise} Prove that the invariant implies $ME$.\end{exercise}

\begin{exercise} Prove that the following statement E is an invariant.
\[ E: \ \PCcopy = 2_0,3_0\rightarrow \tcopy\not = \Rcopy.\]

Then show that this statement is not a consequence of the invariant $A\wedge B \wedge C\wedge D$. For this you have to find a state $S$ that satisfies $A\wedge B \wedge C\wedge D$ but does
not satisfy $E$. This example shows that the invariant $A\wedge B \wedge C\wedge D$ is true
in some states that never appear in any history execution of the algorithm. That is, our
invariant does not characterize those states that appear in histories. 
\end{exercise}


\end{document}

