
\documentclass{beamer}

%\includeonlyframes{title,outline,motivation}

\setbeamertemplate{footline}%[page number]
{
  \begin{beamercolorbox}{section in foot}
  \vskip-2mm\hskip2mm\insertpagenumber
  \end{beamercolorbox}
}


\usepackage{graphicx}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\colorlet{lightblue}{white!25!blue}
\newcommand{\WHILE}{\mbox{\sf \textcolor{lightblue}{while}}\;}
\newcommand{\DO}{\;\mbox{\sf\textcolor{lightblue}{do}}\;}
\newcommand{\AND}{\;\mbox{\sf\textcolor{lightblue}{and}}\;}
\newcommand{\OR}{\;\mbox{\sf\textcolor{lightblue}{or}}\;}
\newcommand{\WAIT}{\;\mbox{\sf\textcolor{lightblue}{wait}}\;}
\newcommand{\IF}{\;\mbox{\sf\textcolor{lightblue}{if}}\;}
\newcommand{\THEN}{\;\mbox{\sf\textcolor{lightblue}{then}}\;}
\newcommand{\ELSE}{\;\mbox{\sf\textcolor{lightblue}{else}}\;}
\newcommand{\BEGIN}{\;\mbox{\sf\textcolor{lightblue}{begin}}\;}
\newcommand{\END}{\mbox{\sf\textcolor{lightblue}{end}}\;}
\newcommand{\pair}[2]{\langle #1,\; #2 \rangle}
\newcommand{\SKIP}{\mbox{\sf\textcolor{lightblue}{skip}}\;}
\newcommand{\TRUE}{\mbox{\sf\textcolor{lightblue}{true}}\;}
\newcommand{\FALSE}{\mbox{\sf\textcolor{lightblue}{false}}\;}
\newcommand{\AWAIT}{\mbox{\sf\textcolor{lightblue}{await}}\;}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\turn}{\mbox{\em turn}}
\newcommand{\ass}{:=}
\newcommand{\para}{\mid\mid}
\newcommand{\tab}[3]{\multicolumn{#1}{l}{}&
                     \multicolumn{#2}{l}{{#3}}}
\newcommand{\pic}{$\pi$-calculus}
\newcommand{\acquire}{\mathop{\mathit{acquire}}}
\newcommand{\release}{\mathop{\mathit{release}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\assert}[1]{{\textcolor{violet}{\{#1\}}}}
\newcommand{\actif}{\mathop{\it actif}}
\newcommand{\tour}{\mathop{\it turn}}
\newcommand{\CO}{\mathit{pc}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>
{
  \usetheme{Darmstadt}  
  %\usetheme{Warsaw}
  % or ...

  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}

\usecolortheme{seahorse}


\usepackage[english]{babel}
% or whatever

\usepackage[latin1]{inputenc}
% or whatever

\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.


\title[Concurrency 1] % (optional, use only with long paper titles)
{Concurrency 1}

\subtitle{Shared Memory}

\author[Catuscia Palamidessi]{Catuscia Palamidessi\\
INRIA Futurs and LIX - Ecole Polytechnique}

%\institute[INRIA and LIX] % (optional, but mostly needed)
%{
%  INRIA Futurs and LIX - Ecole Polytechnique 
%}
% - Use the \inst command only if there are several affiliations.
% - Keep it simple, no one is interested in your street address.

\institute{The other lecturers for this course: }
\date{
Jean-Jacques L\'evy (PPS)\\
James Leifer (INRIA - Rocq)\\
Eric Goubault (CEA)\\ [2ex]
{\tt \scriptsize http://pauillac.inria.fr/\~{ }leifer/teaching/mpri-concurrency-2004/}
}
% - Either use conference name or its abbreviation.
% - Not really informative to the audience, more for people (including
%   yourself) who are reading the slides online

\subject{Course on Concurrency at MPRI}
% This is only inserted into the PDF information catalog. Can be left
% out. 



% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}


% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
\AtBeginSubsection[]
{
  \begin{frame}<beamer>
    \frametitle{Outline}
    \tableofcontents[currentsection,currentsubsection]
  \end{frame}
}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}


\begin{document}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[label=title]
  \titlepage
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[label=outline]
  \frametitle{Outline}
  \tableofcontents
  % You might wish to add the option [pausesections]
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Motivation}

\begin{frame}[label=motivation]
  \frametitle{Motivation}
  \framesubtitle{Why Concurrency?}
  \begin{itemize}
    \pause
    \item Programs for multi-processors
    \pause
    \item Drivers for slow devices
    \pause
    \item Human users are concurrent
    \pause
    \item Distributed systems with multiple clients
    \pause
    \item Reduce latency
    \pause
    \item Increase efficiency, but Amdahl's law\\
      $$ S= \frac{N}{b*N + (1-b)} $$ 
     ($S = \mbox{speedup}$, $b = \mbox{sequential part}$, $N$ processors)
  \end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Overview of the course}

\begin{frame}
  \frametitle{Overview of the course}

 {\tiny
 \begin{tabular}{lll}
 09-28  	&CP   & Shared memory: atomicity \\
 10-05 	&CP/JJL &	Shared memory: verification, report on Ariane 501\\
 10-12 	&CP    &	CCS: syntax and transitions, coinduction\\
 10-19 	&CP    & CCS: weak and strong bisimulations, axiomatization\\
 10-26 	&CP    & CCS: examples, Hennessy-Milner logic\\
 11-02 	&JL    & $\pi$-calculus: syntax; reduction, transitions, strong bisimulation\\
 11-09 	&JL    & $\pi$-calculus: sum, abstractions, data structures, bisimulation proofs\\
 11-16 	&JL    & $\pi$-calculus: bisimulation ``up to'', congruence, barbed bisimulation\\
 11-23 	& \textcolor{purple}{Review}\\
 11-30 	& \textcolor{purple}{MT exam}\\
 12-07  &JL    & $\pi$-calculus: comparison between equivalences\\
 12-14 	&JJL   &Expressivity of the pi-calculus and its variants\\
 12-21 	&\textcolor{green}{vacation}\\
 12-28 	&\textcolor{green}{vacation}\\
 01-04 	&JJL	&Distributed pi-calculus\\
 01-11 	&JJL	&Problems with distributed implementation\\
 01-18 	&EG 	&True concurrency versus interleaving semantics\\
 01-25 	&EG 	&Event structures and Petri nets\\
 02-01 	&EG 	&Application to the semantics of CCS\\
 02-08 	&EG 	&Comparison of the expressiveness of different models\\
 02-15 	&\textcolor{purple}{Review}\\
 02-22 	&\textcolor{purple}{Final exam}
 \end{tabular}
}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Concurrency in Shared Memory: Effects and Issues}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{Non-determinism}
\begin{itemize}
\pause
\item
Note: we assume that the update of a variable is {\em atomic}
\item
Let $x$ be a global variable. Assume that at the beginning $x=0$

\pause
\item
 Consider two simple processes\\[1ex]
 $S = [x \ass 1; ]$ \quad and \quad
 $T = [x \ass 2; ]$

\bigskip
\pause
\item
After the execution of $S\para T$, we have  $x \in \{1,2\}$ 

\bigskip

\pause
\item
Conclusion:
\begin{itemize}
\pause
\item
Result is not unique.
\pause
\item
Concurrent programs are not described by functions.
\end{itemize}

\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{Implicit Communication}
\begin{itemize}
\pause
\item Let $x$ be a global variable. Assume that at the beginning $x=0$

\pause
\item Consider the two  processes\\[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 ]$

\bigskip
\pause
\item After the execution of $S$, we have $x \in \{2,3,4\}$ 
\pause
\item After the execution of $T$, we have $x \in \{3,4\}$ 
\pause
\item $T$ may be blocked

\bigskip

\pause
\item Conclusion: The parallel subcomponents of a program may interact via their shared variables
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
  \frametitle{Input-output behavior}
\begin{itemize}
\pause
\item Let $x$ be a global variable. 

\pause
\item Consider the two processes \\[1ex]
 $S = [x \ass 1 ]$             \quad and \quad 
 $T = [x \ass 0; x \ass x+1 ]$

\bigskip
\pause
\item $S$ and $T$ are the same function on memory state.

\pause
\item However,
 $S \para S$ and 
 $T \para S$ are
different ``functions'' on memory state.


\bigskip

\pause
\item A process is an {\em atomic action}, followed by a process:
%
$$\mathcal{P} \simeq \mathop{\mathit{Null}} \;+\;
  2^{\mathop{\mathit{action}} \times \mathcal{P}}$$

\pause
\item Part of the concurrency course aims at giving sense to this equation.
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{Atomicity}
\begin{itemize}
\pause
\item Let $x$ be a global variable. Assume that at beginning $x=0$ 

\pause
\item Consider the process
 $S = [x \ass x+1 \para x \ass x+1]$           

\pause
\item After the execution of $S$ we have  $x=2$.

\bigskip

\pause
\item However
$[x \ass x+1]$ may be compiled into $[A \ass x+1; x \ass A]$

\pause
\item So,
$S$ may behave as $ [A \ass x+1; x \ass A] \para [B \ass x+1; x \ass B]$,\\ 
which, after execution, gives $x \in \{1,2\}$.

\bigskip

\pause
\item To avoid such effect, $[x \ass x+1]$ has to be  {\em atomic} 
\item Atomic statements, aka {\em critical sections} can be implemented via {\em mutual exclusion} 

\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Critical Sections and Mutual Exclusion}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Some attempts to implement a critical section}

\begin{frame}
  \frametitle{The problem}

\begin{itemize}

\item Let
$P_0 = [\cdots; C_0; \cdots]$ \quad and \quad $P_1 = [\cdots; C_1; \cdots]$

\bigskip 

\item We intent  $C_0$ and $C_1$ to be critical sections, i.e. they  should not be executed
simultaneously. 
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
  \frametitle{Attempt n.1}

\begin{itemize}
\item Use a variable $\turn$. At beginning, $\turn = 0$.
\begin{columns}
\begin{column}{4cm}
\begin{block}{P0}
{\scriptsize
\quad   ...;\\
\qquad  \WHILE turn != 0 \DO ;\\
\qquad   C0; \\
\qquad   turn := 1;\\
\qquad   ... \\ 
}
\end{block}
\end{column}
\begin{column}{4cm}
\begin{block}{P1}
{\scriptsize
\quad  ...;\\
\qquad   \WHILE turn != 1 \DO ;\\
\qquad   C1; \\
\qquad   turn := 0;\\
\qquad   ... \\ 
}
\end{block}
\end{column}
\end{columns}
\bigskip
\pause
\item However the method is unfair, because $P_0$ is privileged. 
Worse yet, until $P_0$ executes its critical section,  $P_1$ is blocked.

\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
  \frametitle{Attempt n.2}

\begin{itemize}
\item Use two boolean variables $a_0,a_1$. \\At beginning, $a_0 = a_1 = \FALSE$.

\begin{columns}
\begin{column}{4cm}
\begin{block}{P0}
{\scriptsize
\quad   ...;\\
\quad  \WHILE a1 \DO;\\
\quad   a0 := \TRUE;\\
\quad   C0;\\ 
\quad   a0 := \FALSE;\\
\quad   ...\\
}
\end{block}
\end{column}
\begin{column}{4cm}
\begin{block}{P1}
{\scriptsize
\quad  ...;\\
\quad  \WHILE a0 \DO;\\
\quad   a1 := \TRUE;\\
\quad   C1;\\ 
\quad   a1 := \FALSE;\\
\quad   ...\\
}
\end{block}
\end{column}
\end{columns}

\bigskip

\pause
\item Incorrect. It does not ensure mutual exclusion.
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
  \frametitle{Attempt n.3}

\begin{itemize}
\item Use two boolean variables $a_0, a_1$. \\At beginning,  $a_0 = a_1 = \FALSE$.

\begin{columns}
\begin{column}{4cm}
\begin{block}{P0}
{\scriptsize
\quad   ...;\\
\quad  a0 := \TRUE;\\
\quad  \WHILE a1 \DO ;\\
\quad   a0 := \TRUE;\\
\quad   C0;\\ 
\quad   a0 :=\FALSE;\\
\quad   ...\\
}
\end{block}
\end{column}
\begin{column}{4cm}
\begin{block}{P1}
{\scriptsize
\quad  ...;\\
\quad  a1 := \TRUE;\\
\quad  \WHILE a0 \DO ;\\
\quad   a1 := \TRUE;\\
\quad   C1;\\ 
\quad   a1 := \FALSE;\\
\quad   ...\\
}
\end{block}
\end{column}
\end{columns}

\bigskip

\pause
\item We may get a deadlock. Both $P_0$ and $P_1$ may block.
\end{itemize}
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Some famous algorithms}
\begin{frame}{}
\frametitle{Dekker's Algorithm (early Sixties)}

\begin{itemize}
\item The first correct mutual exclusion algorithm 

\item Use both the variable $\turn$ and the boolean variables $a_0$ and $a_1$. 
At beginning, $a_0 = a_1 = \FALSE$, $\turn\in\{0,1\}$

\begin{columns}
\begin{column}{4cm}\begin{block}{P0}{\scriptsize
\quad  ...;  \\
\quad  a0 := \TRUE;\\
\quad  \WHILE a1 \DO \\
\qquad  \IF turn != 0 \BEGIN\\
\qquad\qquad      a0 := \FALSE; \\
\qquad\qquad      \WHILE turn != 0 \DO ;\\
\qquad\qquad      a0 := \TRUE;\\
\qquad\qquad    \END;\\
\quad  C0; \\
\quad  turn := 1; a0 := \FALSE;\\
\quad  ...  \\
}
\end{block}\end{column}

\begin{column}{4cm}\begin{block}{P1}{\scriptsize
\quad  ...; \\
\quad  a1 := \TRUE;\\
\quad  \WHILE a0 \DO \\
\qquad  \IF turn != 1 \BEGIN\\
\qquad\qquad      a1 := \FALSE; \\
\qquad\qquad      \WHILE turn != 1 \DO ;\\
\qquad\qquad      a1 := \TRUE;\\
\qquad\qquad    \END;\\
\quad  C1; \\
\quad  turn := 0; a1 := \FALSE;\\
\quad  ...  \\
}
\end{block}\end{column}
\end{columns}

\bigskip
\pause
\item  
A variant of Dekker's algorithm for the case of $n$ processes 
was presented by Dijkstra (CACM 1965).
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Peterson's Algorithm (IPL 1981)}

\begin{itemize}
\item The simplest and most compact mutual exclusion algorithm in literature

\item Use both the variable $\turn$ and the boolean variables $a_0$ and $a_1$. 
At beginning, $a_0 = a_1 = \FALSE$, $\turn\in\{0,1\}$

\begin{columns}
\begin{column}{4cm}\begin{block}{P0}{\scriptsize
\quad  ...; \\  
\quad   a0 := \TRUE;\\
\quad  turn := 1;\\
\quad  \WHILE a1 \AND turn != 0 \DO ;\\
\quad  C0; \\
\quad  a0 := \FALSE;\\
\quad  ...  \\
}
\end{block}\end{column}

\begin{column}{4cm}\begin{block}{P1}{\scriptsize
\quad  ...; \\ 
\quad  a1 := \TRUE;\\
\quad  turn := 0;\\
\quad  \WHILE a0 \AND turn != 1 \DO ;\\
\quad  C1; \\
\quad  a1 := \FALSE;\\
\quad  ...  \\
}
\end{block}\end{column}
\end{columns}

\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Correctness of Peterson's Algorithm {\tiny (1/2)}}

\begin{itemize}

\item
To show the correctness 
it  is convenient to add two variables, $\CO_0$, $\CO_1$,
which represent a sort of 
 program counters for $P_0$ and $P_1$.\\
At beginning $\CO_0 = \CO_1 = 1$


\begin{columns}
\begin{column}{5.7cm}\begin{block}{P0}{\scriptsize
      ...;  \\
     $\assert{\neg a_0 \wedge \CO_0\neq 2 }$\\
        a0 := \TRUE; pc0 := 2;\\
     $\assert{a_0 \wedge \CO_0 = 2}$\\
         turn := 1; pc0 := 1;\\
      $\assert{a_0 \wedge \CO_0 \neq 2}$\\
         \WHILE a1 \AND turn != 0 \DO ;\\
     $\assert{a0 \wedge \CO_0\neq 2 \wedge (\neg a_1 \vee \tour = 0 \vee \CO_1 = 2)}$\\
         C0; \\
         a0 := \FALSE;\\
     $\assert{\neg a_0\wedge \CO_0\neq 2}$\\
      ... \\ 
}\end{block}\end{column}
\begin{column}{5.7cm}\begin{block}{P1}{\scriptsize
 ...;\\  
$\assert{\neg a_1 \wedge \CO_1\neq 2 }$\\
 a1 := \TRUE; pc1 := 2;\\
$\assert{a_1 \wedge \CO_1 = 2}$\\
 turn := 0; pc1 := 1;\\
$\assert{a_1 \wedge \CO_1 \neq 2}$\\
 \WHILE a0 \AND turn != 1 \DO  ;\\
$\assert{a1 \wedge \CO_1\neq 2 \wedge (\neg a_0 \vee \tour = 1 \vee \CO_0 = 2)}$\\
 C1; \\
 a1 := \FALSE;\\
$\assert{\neg a_1\wedge \CO_1\neq 2}$\\
 ... \\ 
}\end{block}\end{column}
\end{columns}

\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Correctness of Peterson's Algorithm  {\tiny (2/2)}}

We can prove the correctness by contradiction. 
If both programs were in their critical section, then the formulas
$\assert{a0 \wedge \CO_0\neq 2 \wedge (\neg a_1 \vee \tour = 0 \vee \CO_1 = 2)}$
and $\assert{a1 \wedge \CO_1\neq 2 \wedge (\neg a_0 \vee \tour = 1 \vee \CO_0 = 2)}$
should be true at the same time, but:

\textcolor{violet}
{
$$\begin{array}{ll}
 & a_0 \;\wedge\; \CO_0\neq 2 \;\wedge\; (\neg a_1 \vee \tour = 0 \vee \CO_1 = 2) \\
\wedge & a_1 \;\wedge\; \CO_1\neq 2 \;\wedge\; (\neg a_0 \vee \tour = 1 \vee \CO_0 = 2)\\ \\
\pause
\equiv & \tour = 0 \wedge \tour = 1\\
\end{array}
$$
}

\bigskip

\pause
\begin{center}\textcolor{purple}{\large Contradiction!}\end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Synchronization in Concurrent/Distributed algorithms
}

\begin{itemize}
\pause
\item Dekker's algorithm (early sixties). Quite complex.
\pause
\item Peterson is simpler and can be generalized to $N$ processes more easily
\pause
\item Both algorithms by Dekker and Peterson use busy waiting
\pause
\item Fairness relies on fair scheduling
\pause
\item Many other algorithms for mutual exclusion have been proposed in 
literature. Particularly by Lamport: barber, baker, \ldots
\pause
\item Proofs ? By model checking ?
With assertions ? In temporal logic (eg Lamport's TLA)?
\end{itemize}

\bigskip

\pause
Need for higher constructs in concurrent programming.
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Semaphores}
\begin{frame}
\frametitle{Semaphores}

{\small 
A \textcolor{purple}{generalized semaphore} $s$ is an integer variable with 2
operations

\begin{itemize}
\pause
\item
$\acquire(s)$: If $s > 0$ then $s \ass s-1$,
otherwise suspend on $s$. \ \ \ \textcolor{purple}{(atomically)}
\pause
\item
$\release(s)$: If some process is suspended on $s$, wake it up, 
otherwise $s \ass s+1$. \ \ \ \textcolor{purple}{(atomically)}
\end{itemize}

\bigskip

\pause
{\footnotesize
Now mutual exclusion is easy:
At beginning, $s = 1$. Then 
$$[\cdots; \acquire(s) ;\; C_0; \; \release(s); \cdots] \;\para\;
 [\cdots; \acquire(s) ;\; C_1; \; \release(s); \cdots]$$
}

\pause
\textcolor{purple}{Question} Consider another definition for semaphore:\\
\begin{tabular}{l}
$\acquire(s)$: If $s > 0$ then $s \ass s-1$. Otherwise restart. \\
$\release(s)$: Do $s \ass s+1$. \\
\end{tabular}

Are these definitions equivalent?
}
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The dining philosophers}
\begin{frame}
\frametitle{The dining philosophers}

{\small
\begin{itemize}
\pause
\item
Problem proposed by \textcolor{purple}{Dijkstra} for testing concurrency primitives

\pause
\item
5 philosophers spend their time around a table thinking  or eating  spaghetti. In order to eat, 
each philosopher needs two forks. However, there are only 5 forks on the table.

\begin{center}
\includegraphics<3->[height=2cm]{fig/philosophers.pdf}

\end{center}

\pause
\item
Desiderata
\begin{itemize}
\pause
\item if one philosopher gets hungry, some philosopher will eventually eat
(\textcolor{violet}{\em progress})
\pause
\item if one philosopher gets hungry, he will eventually eat
(\textcolor{violet}{\em starvation-freedom})
\end{itemize}
\end{itemize}
}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Exercises}
\begin{frame}
\frametitle{Exercises}
\begin{itemize}
\item (Difficult) Generalize Dekker's algorithm to the case of $n$ processes
\item Generalize Petersons's algorithm to the case of $n$ processes
\item Implement the Semaphore in Java
\item Write a program for the dining philosophers which ensure progress
\item Discuss how to modify the solution so to ensure starvation-freedom
\item Problem: A certain file is shared by some Reader and some Writer processes: 
we want that only one writer can write on the file at a time, while the readers 
are allowed to do it concurrently. Write the code for the  Reader and the Writer.
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}



