\documentclass[semlcmss,sem-a4]{seminar}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{../include/mon-seminar}
\input{../include/mon-color}
\input{../include/mon-dvipdf}
\usepackage{eurosym}
\usepackage{superpose}
\usepackage{colortbl}


\usepackage{hyperref}
% \usepackage {pstcol,color,pst-node}
\usepackage{advi}
\usepackage{advi-annot}
\usepackage{advi-graphicx}
\usepackage{superpose}

\newcommand{\urlter}[3]{\advirecord{#1}{%
\adviembed[name=netscape; height=0mm]{%
netscape -remote openFile(#2)}}%
\advianchor[click]{#1}{#3}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\newif\ifFrenchItemizeSpacing \FrenchItemizeSpacingfalse
%hevea \bfseries\blueSky
\blueSky
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\WHILE}{\mbox{\sf\colorKeyword while}\;}
\newcommand{\DO}{\;\mbox{\sf\colorKeyword do}\;}
\newcommand{\AND}{\;\mbox{\sf\colorKeyword and}\;}
\newcommand{\OR}{\;\mbox{\sf\colorKeyword or}\;}
\newcommand{\WAIT}{\;\mbox{\sf\colorKeyword wait}\;}
\newcommand{\IF}{\;\mbox{\sf\colorKeyword if}\;}
\newcommand{\THEN}{\;\mbox{\sf\colorKeyword then}\;}
\newcommand{\ELSE}{\;\mbox{\sf\colorKeyword else}\;}
\newcommand{\BEGIN}{\;\mbox{\sf\colorKeyword begin}\;}
\newcommand{\END}{\;\mbox{\sf\colorKeyword end}\;}
\newcommand{\pair}[2]{\langle #1,\; #2 \rangle}
\newcommand{\SKIP}{\mbox{\sf\colorKeyword skip}\;}
\newcommand{\TRUE}{\mbox{\sf\colorKeyword true}\;}
\newcommand{\FALSE}{\mbox{\sf\colorKeyword false}\;}
\newcommand{\AWAIT}{\mbox{\sf\colorKeyword 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]{{\orchidBis \{#1\}}}
\newcommand{\actif}{\mathop{\it actif}}
\newcommand{\tour}{\mathop{\it turn}}
\newcommand{\CO}{\mathit{c}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \bfseries
\blueSky
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\begin{center}
{\blueBis \large \bf Concurrency 2 \\[1ex]
\Large
\colorbox{monyellow}{From shared memory}\\
\colorbox{monyellow}{to synchronization}\\
\colorbox{monyellow}{by communication on}\\
\colorbox{monyellow}{channels}\\[.3ex]
}
\bigskip
{\red Jean-Jacques Lévy (INRIA - Rocq)}\\[2ex]


% {\small\ahref{http://jeanjacqueslevy.net/dea}{jeanjacqueslevy.net/dea}}\\[2ex]

\small
{\blueBis MPRI concurrency course with:}\\[1ex]
Pierre-Louis Curien (PPS)\\
Eric Goubault (CEA)\\
James Leifer (INRIA - Rocq)\\
Catuscia Palamidessi (INRIA - Futurs)

\end{center}

\end{slide}
\blueSky
\centerslidesfalse
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Plan}

\bigskip

\begin{itemize}

\item exercises (followup)

\item readers and writers

\item the five philosophers

\item synchronous communication channels

\item CML

\item coding semaphores

\end{itemize}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[21.5cm,16.5cm]
\heading{Readers and Writers (1/6)}

\bigskip
A shared resource is concurrently {\red read} or {\DarkOrange
modified}.  

\begin{itemize}

\itemW Several processes may concurrently read the shared resource.

\item A single process (the writer) may modify the resource.

\item When readers are running, no writer can be executed. 

\item When a writer is running, no other writer, nor a reader
can run concurrently. 


\bigskip

\begin{tabular}{@{\hspace{-4ex}}l@{\hspace{6ex}}l}
\adviwait
\begin{lstlisting}{}
PROCEDURE Read() = 
BEGIN
  AcquireShared();
  (* read shared data *)
  ReleaseShared();
END Read;
\end{lstlisting} &
\adviwait
\begin{lstlisting}{}
PROCEDURE Write() = 
BEGIN
  AcquireExclusive();
  (* write shared data *)
  ReleaseExclusive();
END Write;
\end{lstlisting}
\end{tabular}
\end{itemize}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[21.5cm,16.5cm]\blueSky
\heading{Les lecteurs et les écrivains (2/6)}

En {\red lecture}, on a $\mathit{nReaders}$  simultanés
($\mathit{nReaders} > 0$).

En {\red écriture}, on a $\mathit{nReaders} = -1$.

 
\begin{tabular}{@{\hspace{0ex}}l@{\hspace{6em}}l}
\adviwait
\begin{lstlisting}{} 
PROCEDURE AcquireShared() =
BEGIN
  LOCK m DO
    WHILE nReaders = -1 DO
      Thread.Wait(m, c);
    END;
    ++ nReaders;
  END;
END AcquireShared;

PROCEDURE ReleaseShared() =
BEGIN
  LOCK m DO
    -- nReaders;
    IF nReaders = 0 THEN
      Thread.Signal(c);
  END:
END ReleaseShared;
\end{lstlisting} & \adviwait
\begin{lstlisting}{}
PROCEDURE AcquireExclusive() =
BEGIN
  LOCK m DO
    WHILE nReaders != 0 DO
      Thread.Wait(m, c);
    END;
    nReaders := -1;
  END;
END AcquireExclusive;

PROCEDURE ReleaseExclusive() =
BEGIN
  LOCK m DO
   nReaders := 0;
   `{\red Thread.Broadcast(c);}`
  END;
END ReleaseExclusive;
` `
\end{lstlisting}
\end{tabular}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[21.5cm,16.5cm]

\blueSky
\heading{Les lecteurs et les écrivains (3/6)}

{\it Broadcast\/} réveille trop de processus se retrouvant
immédiatement bloqués.  Avec deux conditions \lstinline|cR| et
\lstinline|cW|, on a un contrôle plus fin:

\begin{tabular}{@{\hspace{0ex}}l@{\hspace{6em}}l}
\begin{lstlisting}{}
PROCEDURE AcquireShared() =
BEGIN
  LOCK m DO
    ++ nWaitingReaders;
    WHILE nReaders = -1 DO
      Thread.Wait(m, cR);
    END;
    -- nWaitingReaders;
    ++ nReaders;
  END;
END AcquireShared;

PROCEDURE ReleaseShared() =
BEGIN
  LOCK m DO
    -- nReaders;
    IF nReaders = 0 THEN
      Thread.Signal(cW);
  END:
END ReleaseShared;
\end{lstlisting} &
\begin{lstlisting}{}
PROCEDURE AcquireExclusive() =
BEGIN
  LOCK m DO
    WHILE nReaders != 0 DO
      Thread.Wait(m, cW);
    END;
    nReaders := -1;
  END;
END AcquireExclusive;

PROCEDURE ReleaseExclusive() =
BEGIN
  LOCK m DO
   nReaders := 0;
   IF nWaitingReaders > 0 THEN
     `{\red Thread.Broadcast(cR);}`
   ELSE
     `{\red Thread.Signal(cW);}`
  END;
END ReleaseExclusive;
\end{lstlisting}
\end{tabular}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[21.5cm,16.5cm]\blueSky
\heading{Les lecteurs et les écrivains (4/6)}

Exécuter {\it signal} à l'intérieur d'une section critique n'est pas
très efficace. Avec un seul processeur, ce n'est pas un problème car
les réveillés passent dans l'état prêt attendant la disponibilité
du processeur. 

Avec plusieurs processeurs, le processus réveillé peut retomber
rapidement dans l'état bloqué, tant que le verrou n'est pas relaché.

Il vaut mieux faire {\red{\it signal} à l'extérieur} de la section
critique.\\
(Ce qu'on ne fait jamais !!)
\bigskip

\begin{lstlisting}{}
PROCEDURE ReleaseShared() =
BEGIN
  VAR doSignal: BOOLEAN;
  LOCK m DO
    -- nReaders;
    doSignal := nReaders = 0;
  END:
  IF doSignal THEN
    `{\red Thread.Signal(cW);`
END ReleaseShared;
\end{lstlisting}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[21.5cm,16.5cm]\blueSky
\heading{Les lecteurs et les écrivains (5/6)}

Des blocages inutiles sont possibles (avec plusieurs
processeurs) sur le {\it Broadcast} de fin d'écriture.

Comme avant, on peut le sortir de la section critique. 

Si plusieurs lecteurs sont réveillés, {\red un seul} prend le
verrou. Mieux vaut faire {\it signal} en fin d'écriture,
puis refaire {\it signal} en fin d'accès partagé pour relancer les
autres lecteurs.

\bigskip
\begin{tabular}{@{\hspace{0ex}}l@{\hspace{6em}}l}
\begin{lstlisting}{}
PROCEDURE AcquireShared() =
BEGIN
  LOCK m DO
    ++ nWaitingReaders;
    WHILE nReaders = -1 DO
      Thread.Wait(m, cR);
    END;
    -- nWaitingReaders;
    ++ nReaders;
  END;
  `{\red Thread.Signal(cR)}`;
END AcquireShared;
\end{lstlisting} &
\begin{lstlisting}{}
PROCEDURE ReleaseExclusive() =
BEGIN
  LOCK m DO
   nReaders := 0;
   IF nWaitingReaders > 0 THEN
     `{\red Thread.Signal(cR);}`
   ELSE
     `{\red Thread.Signal(cW);}`
  END;
END ReleaseExclusive;
` `
` `
\end{lstlisting}
\end{tabular}


 
\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[21.5cm,16.5cm]\blueSky
\heading{Les lecteurs et les écrivains (6/6)}

{\DarkOrange Famine} possible {\DarkOrange d'un écrivain} en attente
de fin de lecture. La politique d'ordonnancement des processus peut
aider. On peut aussi logiquement imposer le passage d'un écrivain.

\bigskip
\begin{tabular}{@{\hspace{0ex}}l@{\hspace{2em}}l}
\begin{lstlisting}{}
PROCEDURE AcquireShared() =
BEGIN
  LOCK m DO
    ++ nWaitingReaders;
    IF nWaitingWriters > 0 THEN
      Thread.Wait(m, cR);
    WHILE nReaders = -1 DO
      Thread.Wait(m, cR);
    END;
    -- nWaitingReaders;
    ++ nReaders;
  END;
  `{\red Thread.Signal(cR)}`;
END AcquireShared;
\end{lstlisting} &
\begin{lstlisting}{}
PROCEDURE AcquireExclusive() =
BEGIN
  LOCK m DO
    ++nWaitingWriters;
    WHILE nReaders != 0 DO
      Thread.Wait(m, cW);
    END;
    --nWaitingWriters;
    nReaders := -1;
  END;
END AcquireExclusive;
` `
` `
` `
\end{lstlisting}
\end{tabular}

\bigskip
{\red Contrôler finement la synchronisation peut être complexe.}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}\blueSky
\heading{Les 5 philosophes (1/7)}

\bigskip
\begin{itemize}
\itemW
Problème de {\red\tt [Dijkstra]} pour tester les primitives
concurrentes: verrous, conditions, sémaphores, sémaphores
généralisés, etc.

\itemW
5 moines philosophes $\Phi_i$ pensent et mangent. Pour manger, ils
vont dans la salle commune, où ils dégustent un plat de spaghettis.

\itemW
il faut {\red deux} fourchettes pour manger les spaghettis.  Mais, le
monastère ne dispose que de 5 fourchettes.

\begin{center}
\epsfig{file=fig/philosophes.eps,scale=.35}

\end{center}

\itemW
Comment arriver à ce qu'aucun moine ne meure de faim? 

\end{itemize}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}\blueSky
\heading{Les 5 philosophes (2/7)}

\bigskip
\begin{lstlisting}
  (* `\rm -------------------- Première solution --------------` *)

  VAR s: ARRAY [0..4] OF MUTEX;

  PROCEDURE Philosophe (i: CARDINAL) =
  BEGIN
    (* penser *)
    Thread.Acquire(s[i]);
    Thread.Acquire(s[(i+1) MOD 5]);
    (* manger *)
    Thread.Release(s[i]);
    Thread.Release(s[(i+1) MOD 5]);
  END Philosophe;
\end{lstlisting}

Sureté, mais interblocage.

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}\blueSky
\heading{Les 5 philosophes (3/7)}

\bigskip
\begin{lstlisting}
(* `\rm -------------------- Deuxième solution --------------` *)

  VAR f: ARRAY 0..4 OF CARDINAL = {2, 2, 2, 2, 2};
      manger: ARRAY 0..4 OF Thread.Condition; 

  PROCEDURE Philosophe (i: CARDINAL) = 
  BEGIN
    WHILE true DO
      (* penser *)
      PrendreFourchettes(i);
      (* manger *)
      RelacherFourchettes(i);
    END;
  END Philosophe;
\end{lstlisting}

\bigskip

\begin{itemize}
\item $f[i]$ est le nombre de fourchettes disponibles pour $\Phi_i$
\end{itemize}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}\blueSky
\heading{Les 5 philosophes (4/7)}

\vspace*{1ex}
\bigskip
\begin{lstlisting}
  PROCEDURE PrendreFourchettes (i: CARDINAL) =
  BEGIN
    LOCK m DO
      WHILE f[i] != 2 DO
        Thread.Wait (m, manger[i]);
      END;
      -- f[(i-1) MOD 5]; -- f[(i+1) MOD 5];
    END:
  END PrendreFourchettes;
`\adviwait`
  PROCEDURE RelacherFourchettes (i: CARDINAL) =
  BEGIN
    VAR g := (i-1) MOD 5, d := (i+1) MOD 5;
    LOCK m DO
      ++ f[g]; ++ f[d];
      IF f[d] = 2 THEN
        Thread.Signal (manger[d]);
      IF f[g] = 2 THEN
        Thread.Signal (manger[g]);
    END;
  END RelacherFourchettes;
\end{lstlisting}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}\blueSky
\heading{Les 5 philosophes (5/7)}

\begin{itemize}
\itemW L'invariant suivant est vérifié
%
$$ \sum_{i=0}^{4} f[i] = 10 - 2 \times \mathit{mangeurs}
$$

\itemW interblocage $\;\Rightarrow\;\mathit{mangeurs} = 0$\\
$\;\Rightarrow\;f[i] = 2$ pour tout $i$ ($0 \leq i < 5$)\\
$\;\Rightarrow\;$ pas d'interblocage pour le dernier à demander à manger.

\itemW famine, si, par exemple, les philosophes 1 et 3 complottent
  contre le philosophe 2, qui mourra de faim.

\end{itemize}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}\blueSky
\heading{Les 5 philosophes (6/7)}

\bigskip
\begin{itemize}
\itemW On reprend la première solution $+$ sémaphore généralisé
  $\mathit{salle}$\\
  Au début $\mathit{salle} = 4$

\begin{itemize}
\itemBW Pour manger, les philosophes rentrent  dans la salle;
\itemBW il y a au plus 4 philosophes dans la salle; 
\itemBW ils sortent de la salle après le repas;
\itemBW et retournent penser dans leur cellule.
\end{itemize}
\vspace*{1ex}

\adviwait
\begin{lstlisting}
  (* `\rm -------------------- Troisième solution --------------` *)
  PROCEDURE Philosophe (i: CARDINAL) =
  BEGIN
    (* penser *)
    `\tt\orchidBis SemaphoreGen.P(salle);`   (* `\rm --------- début zone critique ------` *)    
    Thread.Acquire(s[i]);
    Thread.Acquire(s[(i+1) MOD 5]);
    (* manger *)
    Thread.Release(s[i]);
    Thread.Release(s[(i+1) MOD 5]);
    `\tt\orchidBis SemaphoreGen.V(salle);` (* `\rm --------- fin zone critique  --------` *)
  END Philosophe; 
\end{lstlisting}

\end{itemize}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}\blueSky
\heading{Les 5 philosophes (7/7)}

\begin{itemize}

\itemW 4 philosophes au plus dans la salle $\Rightarrow$ pas d'interblocage.

\itemW l'invariant suivant est vérifié
$$\mathit{salle} + \mbox{nombre de processus dans la zone critique} = 4$$

\itemW Si $\Phi_i$ exécute \lstinline|P(s[i])|, alors il finira cette
instruction.

\itemW Si $\Phi_i$ attend indéfiniment sur \lstinline|P(s[(i+1)%5])|,
alors $\Phi_{i+1}$ attend indéfiniment sur \lstinline|P(s[(i+2)%5])|.

\itemW Si $\Phi_i$ exécute \lstinline|P(s[(i+1)%5])|, alors il finira
  cette instruction.

\itemW $\Rightarrow$ Pas de famine.
\end{itemize}

\bigskip

\adviwait
\exercice Programmer cette solution des 5 philosophes avec
les seuls \lstinline|Thread.Wait|, \lstinline|Thread.Signal| et
\lstinline|Thread.Broadcast|.

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Communication channels (1/2)}

\begin{itemize}

\item shared memory is not structured (see Ariane 502 on-board
software)
$\Rightarrow$ restricted communication between processes

\item network of processes 

\item channels as FIFOs {\tt\red[Kahn, Macqueen]} \\
eg Eratosthenes sieve\\
\vfill



\end{itemize}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Communication channels (2/2)}

\newcommand{\send}{\mathop{\mathit{send}}}
\newcommand{\receive}{\mathop{\mathit{receive}}}

\begin{itemize}

\item channels just contains scalars\\
communication by rendez-vous (Occam, Ada, etc)

\item in
$$[P ; \send(c, x) ; P'] \;\para\; [Q ; \receive(c) ; Q']$$
$P$ and $Q$ get synchronized by the communication on $c$. \\
Then
$Q$ and $Q'$ may start concurrently.

\item basic model $\Rightarrow$ 
CSP {\tt\red[Hoare, 78]}, 
CCS {\tt\red[Milner, 80]}, 
$\pi$-calcul {\tt\red[Milner, Parrow, Walker, 90]}, 

\item CCS and $\pi$-calculus are easily implementable on top of shared
memory. Much more difficult for distributed environments, since one
has to fight with the global consensus problem. 

See at end of MPRI concurrency course.

$\Rightarrow$ join-calculus {\red\tt[Fournet, Gonthier, 96]}, 
$\pi 1$-calculus {\red\tt[Amadio, 97]}, nomadic-pic
{\red\tt[Sewell, Wojciechowski, 00]}, \ldots\ 
polyphonic C$\#$ {\red\tt[MSR, 03]}.

\end{itemize}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\lstset{
  language=[Objective]Caml,
  basicstyle=\ttfamily,
  keywordstyle=\tt\colorKeyword,
  identifierstyle=,
  commentstyle=\DarkOrange\it,
  stringstyle=\ttfamily\color{orchidBis},
  showstringspaces=false,
  lineskip=-.6ex,
  xleftmargin=0ex,
  extendedchars=true,
  columns=fullflexible,
  basewidth={.45em},
  fontadjust=true,
  escapechar=`}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Concurrent ML}

The Event library in Ocaml implements {\tt\red[Reppy]} SML library.
\bigskip

\begin{lstlisting}{}
sig
  type 'a channel
  val new_channel : unit -> 'a Event.channel
  type 'a event
  val send : 'a Event.channel -> 'a -> unit Event.event
  val receive : 'a Event.channel -> 'a Event.event
  val choose : 'a Event.event list -> 'a Event.event
  val wrap : 'a Event.event -> ('a -> 'b) -> 'b Event.event
  val guard : (unit -> 'a Event.event) -> 'a Event.event
  val sync : 'a Event.event -> 'a
  val select : 'a Event.event list -> 'a
  ...
end
\end{lstlisting}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Updatable storage cell (1/4)}

\begin{lstlisting}{}
open Event;;
`\adviwait`
type 'a request =  GET | PUT of 'a;;

type 'a cell = {
  reqCh: 'a request channel;
  replyCh: 'a channel;
  }  ;;
`\adviwait`
let send1 c msg = sync (send c msg) ;;
let receive1 c =  sync (receive c) ;;

let `\red\tt get` c =   send1 c.reqCh GET; receive1 c.replyCh ;;
let `\red\tt put` c x = send1 c.reqCh (PUT x) ;;
`\adviwait`
let `\red\tt cell` x = 
  let reqCh = new_channel() in
  let replyCh = new_channel() in
  let rec loop x = match (receive1 reqCh) with
    GET -> send1 replyCh x ; loop x
  | PUT x' -> loop x'
  in `\adviwait`
  Thread.create loop x ;
  {reqCh = reqCh; replyCh = replyCh} ;;
\end{lstlisting}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Updatable storage cell (2/4)}

\begin{lstlisting}{}
open Event;;

type 'a cell = {
  getCh: 'a channel;
  putCh: 'a channel;
  }  ;;

let get c = 
  sync (receive c.getCh);;

let put c x =
  sync (send c.putCh x);;

let cell x = 
  let getCh = new_channel() in
  let putCh = new_channel() in
  let rec loop x = select [
    wrap (send getCh x) (function () -> loop x);
    wrap (receive putCh) loop
  ] 
  in
  Thread.create loop x ;
  {getCh = getCh; putCh = putCh} ;;
\end{lstlisting}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Updatable storage cell (3/4)}

\begin{lstlisting}{}
open Event;;

type 'a sem = {
  getCh: 'a channel;
  putCh: 'a channel;
  }  ;; 

let get c =  sync (receive c.getCh);;
let put c x =  sync (send c.putCh x);;

let sem () = 
  let getCh = new_channel() in
  let putCh = new_channel() in
  let rec loop x = 
    let putEvt = wrap (receive putCh) (function y -> loop (Some y)) in
    match x with
      None ->  sync putEvt
    | Some y -> 
      let getEvt = wrap (send getCh y) (function () -> loop x) in
      select [ getEvt; putEvt ]
  in
  Thread.create loop None ;
  {getCh = getCh; putCh = putCh} ;;
\end{lstlisting}

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Updatable storage cell (4/4)}

\newcommand{\eqdef}{\stackrel{\hbox{\tiny def}}{=}}
\newcommand{\Loop}{\mathop{\mathit{loop}}}
\newcommand{\None}{\mathop{\mathit{None}}}
\newcommand{\Some}{\mathop{\mathit{Some}}}
\newcommand{\Out}[1]{\overline{#1}}
\newcommand{\Get}{\mathit{Get}}
\newcommand{\Put}{\mathop{\mathit{Put}}}
\newcommand{\Sem}{\mathop{\mathit{Sem}}}
$$
\begin{array}{rcl}
\Loop(\None) &=& \Put(y) \cdot \Loop(\Some y)\\
\Loop(\Some y) &=& \Out{\Get} {\langle y \rangle}
                    \cdot \Loop(\None) \\
              &+& \Put (z) \cdot \Loop(\Some z) \\
\\
\Sem(x) &\eqdef& \Loop(\Some x)\\
\\
&\Downarrow&\\
\\
\Sem(x) &=& 
\Out{\Get} \cdot \Put(y) \cdot \Sem(y) \\
              &+& \Put(y) \cdot \Sem(y) 
\end{array}
$$

\bigskip
\exercice Give a program and equations for generalized semaphores. 

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Conclusion}

\begin{itemize}

\item What are the equations of interactions?

\item Simplify by considering just interaction.

\item Find a logic for interaction.

\item Is there an interesting denotational semantics?

\item Find new/correct paradigms for programming.

\item What's about distribution ?

\item Mobility ?

\item Security ?

\vfill

\item \Large $\Rightarrow$ next lectures in MPRI Concurrency course.

\end{itemize}

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


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