\documentclass{slides}
\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\begin{center}
{\huge \bf Concurrency 1}
\\ \bigskip
{\huge Shared Memory}
\\ \bigskip
{\tt Jean-Jacques.Levy@inria.fr} \\
INRIA -- Rocquencourt \\ 
\bigskip\bigskip
tel: +33-1-39-63-56-89
{\tt http://pauillac.inria.fr/$\sim$levy}
\end{center}

\end{slide}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
 Why concurrency?
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

\begin{enumerate}
\item Programs for multi-processors
\item Drivers for slow devices
\item Human users are concurrent
\item Distributed systems with multiple clients
\item Reduce lattency as an optimisation method
\end{enumerate}

\end{slide}

\newcommand{\ass}{:=}
\newcommand{\para}{\mid\mid}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Implicit Communication
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

Suppose $x$ is a global variable. 

At beginning, $x=0$

Consider\\[1ex]
 $S = [x \ass x+1; x \ass x+1  \para x\ass 2*x]$             \\ \\
 $T = [x \ass x+1; x \ass x+1  \para wait(x=1); x \ass 2*x]$ \\ \\

After $S$, then $x \in \{2,3,4\}$ \\
After $T$, then $x \in \{3,4\}$ \\[2ex]
$T$ may be blocked

\bigskip\bigskip

Conclusion

In $S$ and $T$, interaction via $x$ (shared memory)



\end{slide}




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Atomicity
\footnotesize\bigskip\bigskip\bigskip
\footnotesize


Suppose $x$ is a global variable. 

At beginning, $x=0$

Consider\\[1ex]
 $S = [x \ass x+1 \para x \ass x+1]$           

After $S$, then $x=2$.

\bigskip\bigskip

However if\\[1ex]
$[x \ass x+1]$ compiled into $[A \ass x+1; x \ass A]$

\bigskip\bigskip

Then \\
$S = [A \ass x+1; x \ass A] \para [A \ass x+1; x \ass A]$

and

After $S$, then $x \in \{1,2\}$.

\bigskip\bigskip

Conclusion
\begin{enumerate}
\item $[x \ass x+1]$ was firstly considered atomic
\item Atomicity is important
\end{enumerate}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\WHILE}{\mbox{\tiny\sf while}\;}
\newcommand{\DO}{\;\mbox{\tiny\sf do}\;}
\newcommand{\AND}{\;\mbox{\tiny\sf and}\;}
\newcommand{\OR}{\;\mbox{\tiny\sf or}\;}
\newcommand{\WAIT}{\;\mbox{\tiny\sf wait}\;}
\newcommand{\IF}{\;\mbox{\tiny\sf if}\;}
\newcommand{\THEN}{\;\mbox{\tiny\sf then}\;}
\newcommand{\ELSE}{\;\mbox{\tiny\sf else}\;}
\newcommand{\BEGIN}{\;\mbox{\tiny\sf begin}\;}
\newcommand{\END}{\;\mbox{\tiny\sf end}\;}
\newcommand{\turn}{\mbox{\em turn}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Critical section -- Mutual exclusion
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

Let
$P_1 = [\cdots; A; \cdots]$ and
$P_2 = [\cdots; B; \cdots]$

$A$ and $B$ are critical sections (ie should not be executed
simultaneously). Implementation?

\bigskip

{\bf Solution 1}
At beginning, $\turn = 1$.

$P_1 = [\cdots; \WHILE \turn = 2 \DO ; A; \turn \ass 2; \cdots]$ \\[1ex]
$P_2 = [\cdots; \WHILE \turn = 1 \DO ; B; \turn \ass 1; \cdots]$ \\[1ex]

\bigskip
$P_1$ privileged, not fair.

\bigskip\bigskip

{\bf Solution 2}
At beginning, $c_1 = 1$, $c_2 = 1$.

$P_1 = [\cdots; \WHILE c_2 = 0 \DO ; c_1 \ass 0; A; c_1 \ass 1; 
\cdots]$ \\[1ex]
$P_2 = [\cdots; \WHILE c_1 = 0 \DO ; c_2 \ass 0; B; c_2 \ass 1; 
\cdots]$ \\[1ex]


\bigskip
False.


{\bf Solution 3}
At beginning, $c_1 = 1$, $c_2 = 1$.

 
$P_1 = [\cdots; c_1 \ass 0; \WHILE c_2 = 0 \DO ; A; c_1 \ass 1; \cdots]$ 
\\[1ex]
$P_2 = [\cdots; c_2 \ass 0; \WHILE c_1 = 0 \DO ; B; c_2 \ass 1; \cdots]$ 
\\[1ex]


\bigskip
Deadlock. Both $P_1$ and $P_2$ are blocked.


\end{slide}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\tab}[3]{\multicolumn{#1}{l}{}&
                     \multicolumn{#2}{l}{{#3}}}

\begin{slide}{}
Dekker's Algorithm
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

{\bf Solution 4}
At beginning, $c_1 = 1$, $c_2 = 1$\\[1ex]

\begin{tabular}{rp{3ex}p{3ex}p{3ex}p{3ex}}
$P_1 = [$ &$\cdots$&&&  \\
\tab{1}{4}{$c_1 \ass 0;                  $}\\
\tab{1}{4}{$\WHILE c_2 = 0 \DO           $}\\
\tab{2}{3}{$\IF \turn = 2 \THEN \BEGIN   $}\\
\tab{3}{2}{$       c_1 \ass 1;   $}\\
\tab{3}{2}{$               \WHILE \turn = 2 \DO; $}\\
\tab{3}{2}{$               c_1 \ass 0;  $}\\
\tab{3}{2}{$               \END; $}\\
\tab{1}{4}{$         A;  $}\\
\tab{1}{4}{$         \turn \ass 2; c_1 \ass 1;$}\\
\tab{1}{4}{$         \cdots;    $}\\
$]$        & &&
\end{tabular}


\begin{tabular}{rp{3ex}p{3ex}p{3ex}p{3ex}}
$P_2 = [$ &$\cdots$&&&  \\
\tab{1}{4}{$c_2 \ass 0;                  $}\\
\tab{1}{4}{$\WHILE c_1 = 0 \DO           $}\\
\tab{2}{3}{$\IF \turn = 1 \THEN \BEGIN   $}\\
\tab{3}{2}{$       c_2 \ass 1;   $}\\
\tab{3}{2}{$               \WHILE \turn = 1 \DO; $}\\
\tab{3}{2}{$               c_2 \ass 0;  $}\\
\tab{3}{2}{$               \END; $}\\
\tab{1}{4}{$         A;  $}\\
\tab{1}{4}{$         \turn \ass 1; c_2 \ass 1;$}\\
\tab{1}{4}{$         \cdots;    $}\\
$]$        & &&
\end{tabular}


\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Peterson's Algorithm (IPL June 81)
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

At beginning, $c_1 = 0$, $c_2 = 0$\\[1ex]

\begin{tabular}{rp{3ex}p{3ex}p{3ex}p{3ex}}
$P_1 = [$ &$\cdots$&&&  \\
\tab{1}{4}{$c_1 \ass 1;                  $}\\
\tab{1}{4}{$turn \ass 1;                  $}\\
\tab{1}{4}{$\WAIT c_2 = 0 \OR turn = 2;      $}\\
\tab{1}{4}{$A;  $}\\
\tab{1}{4}{$c_1 \ass 0;$}\\
\tab{1}{4}{$\cdots;    $}\\
$]$        & &&
\end{tabular}


\begin{tabular}{rp{3ex}p{3ex}p{3ex}p{3ex}}
$P_1 = [$ &$\cdots$&&&  \\
\tab{1}{4}{$c_2 \ass 1;                  $}\\
\tab{1}{4}{$turn \ass 2;                  $}\\
\tab{1}{4}{$\WAIT c_1 = 0 \OR turn = 1;      $}\\
\tab{1}{4}{$B;  $}\\
\tab{1}{4}{$c_1 \ass 0;$}\\
\tab{1}{4}{$\cdots;    $}\\
$]$        & &&
\end{tabular}

Ex 01: prove it's correctness.


\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Dekker's Algorithm (cont'd)
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

Interested persons may look at

\bigskip

\begin{enumerate}
\item Lamport: barber, baker
\item Dijsktra (for $N$ processes $P_i$ for Dekker's)
\item Peterson is simpler and can be generalised to $N$ processes
\item proof in temporal logic (eg Lamport's TLA)
\item Dekker's algorithm is too complicated
\item Dekker's algorithm does busy waiting
\item Fairness acheived because of fair scheduling
\end{enumerate}

\bigskip

Need for higher constructs in concurrent programming languages.

\bigskip
Ex 1: Try to define fairness.

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Semaphores
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

A generalised semaphore $s$ is integer variable with 2 operations

$wait(s)$: If $s > 0$ then $s \ass s-1$\\
Otherwise be suspended on $s$. 

$signal(s)$: If some process is suspended on $s$, wake it up,
$s \ass s+1$.

\bigskip

Now mutual exclusion is easy:\\[1ex]

At beginning, $s = 1$. \\[1ex]
Then $P_1 \para P_2$ where\\[1ex]

$P_1 = [\cdots; wait(s) ;\; A; \; signal(s); \cdots]$ \\[1ex]
$P_2 = [\cdots; wait(s) ;\; B; \; signal(s); \cdots]$ 


\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\pair}[2]{\langle #1, #2 \rangle}
\newcommand{\red}{\rightarrow}
\newcommand{\SKIP}{\mbox{\tiny\sf skip}\;}
\newcommand{\TRUE}{\mbox{\tiny\sf true}\;}
\newcommand{\FALSE}{\mbox{\tiny\sf false}\;}
% \newcommand{\WAIT}{\mbox{\tiny\sf wait}\;}
\newcommand{\AWAIT}{\mbox{\tiny\sf await}\;}
\newcommand{\infrule}[2]{#1 \over #2}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Operational (micro-)semantics (sequential part)
\bigskip\bigskip\bigskip


\begin{center}
$\pair{\SKIP}{\sigma} \red \pair{\bullet}{\sigma}$

$\pair{x \ass e}{\sigma} \red \pair{\bullet}{\sigma[\sigma(e)/x]}$

$\infrule{\sigma(b) = \TRUE}{
     \pair{\IF b \THEN P \ELSE Q}{\sigma} \red \pair{P}{\sigma}}$

$\infrule{\sigma(b) = \FALSE}{
     \pair{\IF b \THEN P \ELSE Q}{\sigma} \red \pair{Q}{\sigma}}$


$\infrule{\pair{P}{\sigma} \red \pair{P'}{\sigma'}}{
   \pair{P;Q}{\sigma} \red \pair{P';Q}{\sigma'}}$

$\infrule{\pair{P}{\sigma} \red \pair{\bullet}{\sigma'}}{
   \pair{P;Q}{\sigma} \red \pair{Q}{\sigma'}}$

$\infrule{\sigma(b) = \TRUE}{
     \pair{\WHILE b \DO P}{\sigma} \red 
     \pair{P;\WHILE b \DO P}{\sigma}}$

$\infrule{\sigma(b) = \FALSE}{
     \pair{\WHILE b \DO P}{\sigma} \red 
     \pair{\bullet}{\sigma}}$




\end{center}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Operational semantics (parallel part)
\bigskip\bigskip\bigskip



\begin{center}
$\infrule{\pair{P}{\sigma} \red \pair{P'}{\sigma'}}{
   \pair{P \para Q}{\sigma} \red \pair{P' \para Q}{\sigma'}}$

$\infrule{\pair{Q}{\sigma} \red \pair{Q'}{\sigma'}}{
   \pair{P \para Q}{\sigma} \red \pair{P \para Q'}{\sigma'}}$

$\infrule{\sigma(b) = \TRUE}{
     \pair{\WAIT b}{\sigma} \red \pair{\bullet}{\sigma}}$

$\infrule{\sigma(b) = \TRUE \quad
          \pair{P}{\sigma} \red \pair{\bullet}{\sigma'}}{
     \pair{\AWAIT b \DO P}{\sigma} \red \pair{\bullet}{\sigma'}}$

$\infrule{\sigma(b) = \TRUE \quad
          \pair{P}{\sigma} \red \pair{P'}{\sigma'}}{
     \pair{\AWAIT b \DO P}{\sigma} \red \pair{P'}{\sigma'}}$
\end{center}

\bigskip


Ex 2: find SOS for boolean semaphores.

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
SOS executions
\bigskip\bigskip\footnotesize

$$
\pair{P_0}{\sigma_0} \red
\pair{P_1}{\sigma_1} \red
\pair{P_2}{\sigma_2} \red
\cdots
\pair{P_n}{\sigma_n} \red
$$

We write \\[1ex]
\begin{tabular}{l}
$\pair{P_0}{\sigma_0} \red^* \pair{P_n}{\sigma_n}$ when $n \geq 0$,\\
$\pair{P_0}{\sigma_0} \red^+ \pair{P_n}{\sigma_n}$ when $n > 0$.
\end{tabular}

\bigskip\bigskip

Remark that in our system, we have no rule such as


$$\infrule{\sigma(b) = \FALSE}{
     \pair{\WAIT b}{\sigma} \red \pair{\WAIT b}{\sigma}}$$

Ie no busy waiting. Reductions may block.
(Same remark for $\AWAIT b \DO P$).

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Atomic statements (Exercices)
\bigskip\bigskip\bigskip

Ex 3: What is the meaning of following rule?

$$\infrule{\pair{P}{\sigma} \red^+ \pair{\bullet}{\sigma'}}{
\pair{\{P\}}{\sigma} \red \pair{\bullet}{\sigma'}}$$


\bigskip
Ex 4: Show   $\AWAIT b \DO P  \equiv \{\WAIT B; P \}$

\bigskip
Ex 5: Meaning of $\{\WHILE \TRUE \DO \SKIP\}$  ???
Find simpler equivalent statement.

\bigskip
Ex 6: Try to add procedure calls to our SOS semantics.

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Producer - Consumer
\bigskip\bigskip\bigskip

\vspace{10cm}.


\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
 A typical thread package. Modula-3
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

\begin{verbatim}
INTERFACE Thread;

TYPE
  T <: ROOT;
  Mutex = MUTEX;
  Condition <: ROOT;

A Thread.T is a handle on a thread. A Mutex is
locked by some thread, or unlocked. A Condition
is a set of waiting threads. A newly-allocated
Mutex is unlocked; a newly-allocated Condition
is empty. It is a checked runtime error to pass
the NIL Mutex, Condition, or T to any procedure
in this interface.

TYPE Closure = OBJECT METHODS apply(): REFANY END;

PROCEDURE Fork(cl: Closure): T;

       Return a handle on a newly-created
       thread executing cl.apply().

PROCEDURE Join(t: T): REFANY;

       Wait until t has terminated and return
      its result. It is a checked runtime error to
      call this more than once for any t.
\end{verbatim}
\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}

\footnotesize
\begin{verbatim}
PROCEDURE Wait(m: Mutex; c: Condition);

       The calling thread must have m
       locked. Atomically unlocks m and
       waits on c. Then relocks m and
       returns.

PROCEDURE Acquire(m: Mutex);

       Wait until m is unlocked and then
       lock it.

PROCEDURE Release(m: Mutex);

       The calling thread must have m
       locked. Unlocks m.

PROCEDURE Broadcast(c: Condition);

       All threads waiting on c become
       eligible to run.

PROCEDURE Signal(c: Condition);

       One or more threads waiting on c
       become eligible to run.
\end{verbatim}
\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Lock
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

\begin{verbatim}
A LOCK statement has the form: 

    LOCK mu DO S END

where S is a statement and mu is an
expression. It is equivalent to:

    WITH m = mu DO
      Thread.Acquire(m);
      TRY S FINALLY Thread.Release(m) END
    END

where m stands for a variable that does
not occur in S.
\end{verbatim}
\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Try Finally
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

\begin{verbatim}
A statement of the form: 

    TRY S_1 FINALLY S_2 END

executes statement S_1 and then
statement S_2. If the outcome of S_1 is
normal, the TRY statement is equivalent
to S_1; S_2. If the outcome of S_1 is an
exception and the outcome of S_2 is
normal, the exception from S_1 is
re-raised after S_2 is executed. If both
outcomes are exceptions, the outcome of
the TRY is the exception from S_2.
\end{verbatim}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Concurrent stack
\footnotesize
\bigskip

Popping in a stack:

\begin{verbatim}
VAR nonEmpty := NEW(Thread.Condition);

LOCK m DO
    WHILE head = NIL DO Thread.Wait(m, nonEmpty) END;
    topElement := head;
    head := head.next;
END;
\end{verbatim}

Pushing into a stack:

\begin{verbatim}
LOCK m DO
    newElement.next := head;
    head := newElement;
    Thread.Signal (nonEmpty);
END;
\end{verbatim}

\bigskip
Caution: \verb+WHILE+ is safer than \verb+IF+ in Pop.


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Concurrent table
\footnotesize
\bigskip


\begin{verbatim}
VAR table := ARRAY [0..999] of REFANY {NIL, ...};
VAR i:[0..1000] := 0;

PROCEDURE Insert (r: REFANY) =
  BEGIN
    IF r <> NIL THEN

        table[i] := r;
        i := i+1;

  END;
END Insert;
\end{verbatim}

\bigskip
Caution: how not to loose values?


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Deadlocks
\footnotesize\bigskip\bigskip\bigskip

Thread $A$ locks mutex $m_1$\\
Thread $B$ locks mutex $m_2$\\
Thread $A$ trying to lock $m_2$\\
Thread $B$ trying to lock $m_1$

\bigskip
\bigskip

Simple technique
\bigskip

Respect a partial order between semaphores. For example, $A$ and $B$
uses $m_1$ and $m_2$ in same order.


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
Exercices (cont'd)
\footnotesize\bigskip\bigskip\bigskip
\footnotesize

Ex 7: Simulate conditions with semaphores. Hint: count number of
waiting processes on condition.

\bigskip

Ex 8: Readers and writers. A buffer may be read by several processes at
same time. But only one process may write in it. Write procedures
StartRead, EndRead, StartWrite, EndWrite.

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



 \end{document}

