\documentclass{beamer}

\setbeamertemplate{footline}
{
\begin{beamercolorbox}{section in foot}
\vskip-2mm \hskip 2mm\insertpagenumber
\end{beamercolorbox}
}

%\pause\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{\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{\CLASS}{\mbox{\sf\textcolor{lightblue}{class}}\;}
\newcommand{\SYNCHRONIZED}{\mbox{\sf\textcolor{lightblue}{synchronized}}\;}
\newcommand{\PUBLIC}{\mbox{\sf\textcolor{lightblue}{public}}\;}
\newcommand{\PRIVATE}{\mbox{\sf\textcolor{lightblue}{private}}\;}
\newcommand{\VOID}{\mbox{\sf\textcolor{lightblue}{void}}\;}
\newcommand{\WAIT}{\;\mbox{\sf\textcolor{lightblue}{wait}}}
\newcommand{\NOTIFY}{\;\mbox{\sf\textcolor{lightblue}{notify}}}
\newcommand{\NOTIFYALL}{\;\mbox{\sf\textcolor{lightblue}{notifyAll}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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 2] % (optional, use only with long paper titles)
{Concurrency 2}

\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{Solution to some of the exercises in previous lecture}
\subsection{Semaphores in Java}

\begin{frame}
  \frametitle{A few facts about Java (1/2)}
  \framesubtitle{Threads in Java}
  \begin{itemize}
    \item A thread is a single sequential line of control. It 
          may be execute in parallel/interleaving with other threads.
    \item The states of a live thread in Java:
    \vskip 1cm
    \begin{center}
    \hskip -1cm \includegraphics[height=3cm]{fig/threads.pdf}
    \end{center}
  \end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
  \frametitle{A few facts about Java (2/2)}
  \framesubtitle{Classes with synchronized methods}
{\scriptsize
  \begin{itemize}
    \item Class whose objects may be shared by different threads need synchronized methods 
    %\pause 
   \item  Example: A  bank account with two or more owners
   \begin{center}
\begin{columns}
\begin{column}{6.5cm}
    \begin{block}{Bank account}
    {
\ \\
\CLASS Account \{\\
\quad\quad \PRIVATE int balance;\\
\quad\quad \PUBLIC Account(int initialDeposit)\  \{\\
\quad\quad \quad \quad       balance = initialDeposit;\\
\quad\quad  \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID deposit(int amount)\  \{ \\
 \quad\quad \quad  \quad            balance = balance + amount;\\
\quad\quad  \}\\
\quad\quad  ...\\
   \}\\
    }
    \end{block}  
\end{column}
\end{columns}
   \end{center}
\vskip 2mm
%\pause
\item Synchronized methods are handled using a lock mechanism. 
\textcolor{purple}{\em A lock is per object}.
%\pause
\item When a thread suspends inside a synchronized method, it releases the lock.
  \end{itemize}
}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Definition of Semaphore (from previous lecture)}

{\small 
A \textcolor{purple}{generalized semaphore} $s$ is an integer variable with two 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
Example of use:
At beginning, $s = {\it max}$. Then 
$$[\cdots; \acquire(s) ;\; C_1; \; \release(s); \cdots] \;\para\;
 [\cdots; \acquire(s) ;\; C_2; \; \release(s); \cdots]$$
}
}
\end{frame}


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

\begin{frame}
  \frametitle{Use of a semaphore in Java}
{%\footnotesize   
\begin{center}
\begin{columns}
\begin{column}{5cm}
    \begin{block}{Creation of a Semaphore s}
    {s.Semaphore({\it max});}
    \end{block}  
\end{column}
\end{columns}
\begin{columns}
\begin{column}{4cm}
    \begin{block}{Thread 1}
    {
\ \\
...\\
s.acquire();\\
$C_1$;\\
s.release();\\
...\\
    }
    \end{block}  
\end{column}
\begin{column}{4cm}
    \begin{block}{Thread 2}
    {
\ \\
...\\
s.acquire();\\
$C_2$;\\
s.release();\\
...\\
    }
    \end{block}  
\end{column}
\end{columns}
   \end{center}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{Declaration of class Semaphore in Java}
{\scriptsize   
Use {\em sus} to indicate the number of suspended threads on the semaphore
\begin{center}
\begin{columns}
\begin{column}{8.5cm}
    \begin{block}{Semaphore}
    {
\ \\
\CLASS Semaphore \{\\
\quad\quad \PRIVATE int value, sus;\\
\quad\quad \PUBLIC Semaphore(int initial)\  \{\\
\quad\quad \quad \quad       value = initial; sus = 0;\\
\quad\quad  \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID acquire()\  \{ \\
 \quad\quad \quad  \quad            \IF (value == 0) \{ sus = sus + 1; \WAIT(); sus = sus - 1; \}\\
 \quad\quad \quad  \quad            \ELSE value = value - 1;\\
\quad\quad  \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID release()\  \{ \\
 \quad\quad \quad  \quad            \IF (sus > 0) \{ \NOTIFY(); \}\\
 \quad\quad \quad  \quad            \ELSE \{ value = value + 1; \}\\
\quad\quad  \}\\
   \}\\
    }
    \end{block}  
\end{column}
\end{columns}
   \end{center}
%\pause
However, this is not efficient \textcolor{purple}{(why?)} and it is not 
in the typical ``Java style''.
}
\end{frame}


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

\begin{frame}
  \frametitle{Semaphore in Java (typical Java solution)}
{\footnotesize   
\begin{center}
\begin{columns}
\begin{column}{6.5cm}
    \begin{block}{Semaphore}
    {
\ \\
\CLASS Semaphore \{\\
\quad\quad \PRIVATE int value;\\
\quad\quad \PUBLIC Semaphore(int initial)\  \{\\
\quad\quad \quad \quad       value = initial;\\
\quad\quad  \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID acquire()\  \{ \\
 \quad\quad \quad  \quad            \WHILE (value == 0) \WAIT();\\
 \quad\quad \quad  \quad            value = value - 1;\\
\quad\quad  \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID release()\  \{ \\
 \quad\quad \quad  \quad            \;value = value + 1;\\
 \quad\quad \quad  \quad             \NOTIFY();\\
\quad\quad  \}\\
   \}\\
    }
    \end{block}  
\end{column}
\end{columns}
   \end{center}
}
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Readers  and  Writers}

\begin{frame}
\textcolor{purple}{Problem}: A certain resource (for instance a file)
is shared by some readers and some writers.
The readers cannot modify the resource, while the writers can.
\\
\ 
\\
%\pause
We want that only one writer can access the resource at a time, while the readers are allowed to do it concurrently. 
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{Readers  and  Writers in Java}
\begin{center}
\begin{columns}
\begin{column}{4cm}
    \begin{block}{Reader}
    {
\ \\
...\\
r.acquireShared();   \\
{\em use r };\\
r.releaseShared();\\
...\\
}
    \end{block}  
\end{column}
\begin{column}{4cm}
    \begin{block}{Writer}
    {
\ \\
...\\
r.acquireExclusive();   \\
{\em use r};\\
r.releaseExclusive();\\
...\\
}
    \end{block}  
\end{column}

\end{columns}
   \end{center}
\end{frame}

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

\begin{frame}
  \frametitle{The class Resource}
{\footnotesize   
\begin{center}
\begin{columns}
\begin{column}{7.5cm}
    \begin{block}{Resource}
    {
\ \\
\CLASS Resource \{\\
\quad\quad \PRIVATE int readers, writers;\\
\quad\quad \PUBLIC Resource()\  \{\\
\quad\quad \quad \quad       readers = 0;\\
\quad\quad \quad \quad       writers = 0;\\
\quad\quad  \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID acquireShared()\  \{ ... \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID releaseShared()\  \{ ... \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID acquireExclusive()\  \{ ... \}\\
\quad\quad \PUBLIC \SYNCHRONIZED \VOID releaseExclusive()\  \{ ... \}\\
   \}\\
    }
    \end{block}  
\end{column}
\end{columns}
   \end{center}
}
\end{frame}



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

\begin{frame}
  \frametitle{The methods of Resource}
{\scriptsize   
\begin{center}
\begin{columns}
\begin{column}{4.5cm}
    \begin{block}{acquireShared()}
    {
\ \\
 \{ \\
 \quad           \WHILE (writers == 1)\;\{\\
 \quad\quad  \WAIT();\\
\quad \}\\
 \quad              readers = readers + 1;\\
 \}\\
}
\end{block}
    \begin{block}{releaseShared()}
    {
\ \\
  \{ \\
\quad      \;readers = readers - 1;\\
\quad            \NOTIFY();\\
 \}\\
}
\end{block}
\end{column}
\begin{column}{5cm}
    \begin{block}{acquireExclusive()}
   {
\ \\
  \{ \\
\quad \WHILE (writers == 1 || readers > 0) \;\{\\
\quad \quad  \WAIT();\\
\quad \}\\
\quad             writers = 1;\\
 \}\\
}
\end{block}
    \begin{block}{releaseExclusive()}
   {
\ \\
\{ \\
\quad              \;writers = 0;\\
\quad                \NOTIFYALL();\\
\}\\
    }
\end{block}
\end{column}
\end{columns}
   \end{center}
}
%\pause
However, this solution is not efficient. \textcolor{purple}{(Why?)}
\end{frame}

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

\begin{frame}
  \frametitle{A more efficient solution}
{\scriptsize  
  \begin{itemize}
\item Use suspension conditions {\em cR}, {\em cW}
\item Use {\em sR} to indicate the number of readers suspended. 
\end{itemize}

\begin{center}
\begin{columns}
\begin{column}{5cm}
    \begin{block}{acquireShared()}
    {
\ \\
 \{ \\
\quad  \WHILE (writers == 1) \{ \\
\quad    \quad     \;sR = sR + 1;\\
\quad    \quad     \WAIT(cR); \\
\quad    \quad     \;sR = sR - 1; \\
\quad \}\\
\quad  readers = readers + 1;\\
 \}\\
}
\end{block}
    \begin{block}{releaseShared()}
    {
\ \\
  \{ \\
\quad   \;readers = readers - 1;\\
\quad  \NOTIFY(cW);\\
 \}\\
}
\end{block}
\end{column}
\begin{column}{5cm}
    \begin{block}{acquireExclusive()}
   {
\ \\
  \{ \\
 \quad  \WHILE (writers == 1 || readers > 0) \; \{ \\
 \quad    \quad  \WAIT(cW);\\
 \quad  \}\\
 \quad writers = 1;\\
 \}\\
}
\end{block}
    \begin{block}{releaseExclusive()}
   {
\ \\
\{ \\
\quad            \;writers = 0;\\
\quad            \IF ( sR > 0) \{ \NOTIFYALL(cR);\;\}\\
\quad            \ELSE  \{ \NOTIFY(cW);\;\}\\
\}\\
    }
\end{block}
\end{column}
\end{columns}
\end{center}
\textcolor{purple}{Suspension conditions do not exist in Java, but  they exist in other languages}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Exercises}
\begin{itemize}
\item The "more efficient solution" for the Readers and Writers problem that we presented in this lecture is not starvation-free, because it
always gives priority to the readers. Modify the solution so to ensure that neither the writers nor the readers will starve.\\
\item About the first solution we presented for the Readers and Writers problem: it that one starvation-free? Justify your answer.
\end{itemize}
\end{frame}

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

\section{Verification of Concurrent Software (by Jean-Jacques L\'evy)}
\subsection{A case study: Ariane}
\begin{frame}
\end{frame}

\end{document}



