\documentclass{beamer}

\setbeamertemplate{footline}
{
\begin{beamercolorbox}{section in foot}
\vskip-2mm \hskip 2mm\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 (INRIA Rocquencourt)\\
James Leifer (INRIA Rocquencourt)\\
Eric Goubault (CEA)\\ [2ex]
{\tt \scriptsize http://pauillac.inria.fr/\~{ }leifer/teaching/mpri-concurrency-2005/}
}
% - 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}}


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

%\beamerdefaultoverlayspecification{<+->}


\begin{document}

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

\begin{frame}
  \titlepage
\end{frame}

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

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

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

\section{Motivation}

\begin{frame}
  \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

%\pausees

\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[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}



