\documentclass{beamer}
%% (C) Stephan Beyer, Dec 2006, All rights reserved.

%\includeonlyframes{inwork}
%% use [label=inwork] after \begin{frame}



\newenvironment{pcode}{\begin{list}{}{}}{\end{list}}

\mode<presentation>
{
  \usetheme{Warsaw}
  \setbeamercovered{transparent}
}

\usepackage{tikz}
\usepackage[german]{babel}
\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}

\title{Aufgabe 3: Algorithmusanalyse}

% \subtitle{Untertitel}

\author{Stephan Beyer (Team 3)}

\date[GvS]
{4. \"Ubung Grundlagen verteilter Systeme}
\subject{Informatik}

\begin{document}

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

\section{Einleitung}

\subsection{Problem}

\begin{frame}
\frametitle{Problem der speisenden Philosophen.}
\begin{itemize}
\uncover<2->{
\item Es sitzen $n\geq2$ hungrige Philosophen $c_1,\dots,c_n$} \uncover<3->{an einem runden Tisch.}
\uncover<4->{
\item Jeder hat vor sich einen Teller mit Essen.}
\uncover<5->{
\item Zwischen jedem Teller liegt eine Gabel\footnote{Oder ein Stäbchen.}.}
\uncover<6->{
	($\Rightarrow\,n$ Gabeln insgesamt).}
\uncover<7->{
\item Ein Philosoph braucht zwei Gabeln um essen zu können.}
\end{itemize}
\begin{center}
 \begin{tikzpicture}
   \visible<2->{
    \alert<8>{\draw (0,0) circle(6pt);}
    \alert<9>{\draw (2,0) circle(6pt);}
    \alert<10>{\draw (2,2) circle(6pt);}
    \alert<11>{\draw (0,2) circle(6pt);}
   }
   \visible<3->{\uncover<3-6>{
    \draw (1,1) circle(1);
   }}
   \visible<4->{\uncover<4-6>{
    \draw (0.5,0.5) circle(2pt);
    \draw (1.5,0.5) circle(2pt);
    \draw (0.5,1.5) circle(2pt);
    \draw (1.5,1.5) circle(2pt);
   }}
   \visible<5->{
    \alert<8,11>{\draw (0.2,1) -- (0.5,1);}
    \alert<8-9>{\draw (1,0.2) -- (1,0.5);}
    \alert<9-10>{\draw (1.8,1) -- (1.5,1);}
    \alert<10-11>{\draw (1,1.8) -- (1,1.5);}
   }
 \end{tikzpicture}
\end{center}
\end{frame}


\begin{frame}
\frametitle{Wo ist nun das Problem?}
\pause
Es gibt zu wenig Gabeln! D.\,h.
\begin{itemize}
\pause
\item Es können maximal nur 
	$\lfloor\frac{n}{2}\rfloor$ Philosophen gleichzeitig essen.
\pause
\item Die Anderen müssen warten, bis die jeweiligen Nachbarn ihre Gabeln
	nicht mehr benutzen. (\emph{Synchronisation})
\pause
\item Zwei Philosophen dürfen (können) nicht gleichzeitig die selbe Gabel 
	aufnehmen. (\emph{Koordination})
\pause
\item Philosophen \emph{verhungern},
	wenn sie nie ihre beiden Gabeln bekommen.
\pause
\item Nimmt jeder Philosoph eine freie Gabel in die
	Hand und wartet darauf, dass die zweite Gabel frei wird, so kann
	dies leicht zu \emph{Deadlocks} führen.
\end{itemize}
\end{frame}

\subsection{Algorithmus}

\begin{frame}
\frametitle{Und nun?}
\uncover<2->{Gegeben ist ein \emph{verteilter Algorithmus}}
\uncover<4->{im \emph{asynchronen Modell}}
\begin{block}{\uncover<5->{\textbf{Async} }\uncover<3->{\texttt{Philosophen}}\uncover<5->{ $c_i$}}
\vspace{1.5cm}
\begin{center}
\Huge{\uncover<6->\dots}
\end{center}
\vspace{1.5cm}
\end{block}
\end{frame}

\begin{frame}
\frametitle{Hilfsmittel}
\begin{description}
\item[\uncover<2->{Prioritätstoken {\tikz \fill[red] (1ex,1ex) circle (0.6ex);} --}]
	\uncover<4->{Inhaber hat erhöhte Priorität in Konfliktsituation,}
	\uncover<5->{Nachbarn tauschen es untereinander aus}
\item[\uncover<7->{"`\textsc{Hungry}"'-Event --}]
	\uncover<9->{ein Philosoph philosophiert über Hunger}
\item[\uncover<13->{Gedächtnis \raisebox{0.5ex}{\tikz \fill[cyan] (0.3ex,0.3ex) circle (0.3ex);} --}]
	\uncover<15->{jeder Philosoph merkt sich "`Hungerstatus"' seiner Nachbarn.}
\end{description}
  
\begin{block}{\uncover<3->{(Boolesche) Variablen für $c_i$}}
\begin{itemize}
\item \uncover<3->{\alert<3-6>{\texttt{holdspriotoken}$_{i,j}$}}
	\uncover<6->{-- $c_i$ besitzt Prioritätstoken, das er sich mit Nachbar $c_j$ teilt}
\item \uncover<8->{\alert<8-10>{\texttt{hungry}$_i$}}
	\uncover<10->{-- $c_i$ hat Hunger, will Essen, braucht Gabeln}
\item \uncover<11->{\alert<11-12>{\texttt{holdsfork}$_{i,j}$}}
	\uncover<12->{-- $c_i$ besitzt Gabel, die er sich mit Nachbar $c_j$ teilt}
\item \uncover<14->{\alert<14-16>{\texttt{needsfork}$_{i,j}$}}
	\uncover<16->{-- $c_i$ merkt sich, dass Nachbar $c_j$ hungrig ist}
\end{itemize}
\end{block}
\end{frame}


\begin{frame}
\frametitle{Initialisierung}
\pause
\begin{block}{\textbf{Async} \texttt{Philosophen} $c_i$}
Variablen:
\begin{itemize}
\item \alert<3-4>{\texttt{hungry}$_i$}
	\uncover<4->{$\;=\;$\texttt{false}}
\item \alert<5-6>{\texttt{holdsfork}$_{i,j}$}
	\uncover<6->{-- höchstens ein Nachbar hat die Gabel}
\item \alert<7-8>{\texttt{holdspriotoken}$_{i,j}$}
	\uncover<8->{-- höchstens ein Nachbar hat das Token}
\item \alert<9-10>{\texttt{needsfork}$_{i,j}$}
	\uncover<10->{$\;=\;$\texttt{false} für alle Nachbarn}
\end{itemize}
\uncover<11->{
	\vspace{0.3cm}
	\begin{center}
	\dots
	\end{center}
	\vspace{0.3cm}}
\end{block}
\end{frame}


\begin{frame}
%% erstes Inp-Actionpaar!
\frametitle{Algorithmusidee (1)}
\framesubtitle{Wir haben Hunger, Hunger, Hunger\dots}

\begin{block}{\textbf{Async} \texttt{Philosophen} $c_i$}
\textbf{Input:}	\alert<2>{\texttt{msg}$\;=\;$\texttt{nil}}
\textbf{Action \alert<2>{when} \alert<3>{not \texttt{hungry}$_i$} and 
	\alert<4>{\textsc{Hungry}-Event}:}
\begin{pcode}
\item
	\alert<5>{\texttt{hungry}$_i$ $:=$ \texttt{true}}
\item \alert<6>{\textbf{for} Nachbarn $c_j$} \textbf{do}
	\begin{pcode}
	\item
		\textbf{if} \alert<7>{\textbf{not} \texttt{holdsfork}$_{i,j}$}
		 \textbf{then}
			\alert<8>{send \texttt{request} to $(c_i,c_j)$}
	\end{pcode}
\end{pcode}
\end{block}

\begin{enumerate}
\item
	\uncover<2->{Immer wenn}
	\uncover<3->{Philosoph noch nicht hungrig ist}
	\uncover<4->{und Hunger-Event erhält,}
	\uncover<5->{wird er hungrig,}
\item
	\uncover<6->{schaut zu seinem linken und rechten Nachbarn,}
\item
	\uncover<7->{wenn dieser die Gabel jeweils nicht hält,}
	\uncover<8->{versucht er sie zu nehmen, d.\,h. fordert sie an.}
\end{enumerate}

\end{frame}


\begin{frame}
%% zweites Inp-Actionpaar!
\frametitle{Algorithmusidee (2)}
\framesubtitle{\texttt{request, request, request, request, request, request, request, request}}

\begin{block}{\textbf{Async} \texttt{Philosophen} $c_i$}
\textbf{Input:}
	\texttt{msg}$\;=\;$\alert<2>{\texttt{request}} with \texttt{origin(msg)}$=(c_j,c_i)\in In_i$ \\
\textbf{Action:}
\begin{pcode}
\item \textbf{if} \alert<3>{\textbf{not} \texttt{hungry}$_i$}
	\textbf{or} 
	\alert<5>{\textbf{not} \texttt{holdspriotoken}$_{i,j}$} 
	\textbf{then}
	\begin{pcode}
	\item \alert<4,6>{\texttt{holdsfork}$_{i,j}:=\;$\texttt{false}}
	\item \textbf{if not} \texttt{hungry}$_i$ \textbf{then}
		\begin{pcode}
		\item \alert<4>{send \texttt{fork(nil)} to $c_j$}
		\end{pcode}
	\textbf{else}
		\begin{pcode}
		\item \alert<6,7>{send} \alert<6>{\texttt{fork(\alert<7>{request})}} \alert<6,7>{to $c_j$}
		\end{pcode}
	\end{pcode}
	\alert<8>{\textbf{else}}
	 	\alert<9>{\texttt{needsfork}$_{i,j}:=\;$\texttt{true}}
\end{pcode}
\end{block}

\vbox{
\only<2>{Erhält ein Philosoph diesen \texttt{request}\dots}
\only<3>{\dots und ist nicht hungrig, \dots}
\only<4>{\dots so gibt er die Gabel dem \texttt{request}-Sender $c_j$.}
\only<5>{Ist er hungrig, hält aber nicht das Prioritätstoken, \dots}
\only<6>{\dots dann gibt er $c_j$ die Gabel, \dots}
\only<7>{\dots verlangt sie aber wieder zurück.}
\only<8>{Ist er hungrig \emph{und} hält das Prioritätstoken, \dots}
\only<9>{so merkt er sich lediglich, dass $c_j$ hungrig ist.}
}
\vbox{}
\end{frame}

\begin{frame}
%% drittes Inp-Actionpaar!
\frametitle{Algorithmusidee (3)}
\framesubtitle{Reichet die Gabel weiter\dots}

\begin{block}{\textbf{Async} \texttt{Philosophen} $c_i$}
\textbf{Input:} \alert<2>{\texttt{msg}$\;=\;$\texttt{fork(\alert<4,5>{param})}} 
	with \texttt{origin(msg)}$=(c_j,c_i) \in In_i$ \\
\textbf{Action:}
\begin{pcode}
\item \alert<3>{\texttt{holdsfork}$_{i,j}:=\;$\texttt{true}}
\item \textbf{if} \alert<4>{\texttt{param}$\;=\;$\texttt{priotoken}}
	\textbf{then}
	\alert<4>{\texttt{holdspriotoken}$_{i,j}:=\;$\texttt{true}}
\item \textbf{if} \alert<5>{\texttt{param}$\;=\;$\texttt{request}}
	\textbf{then}
	\alert<5>{\texttt{needsfork}$_{i,j}:=\;$\texttt{true}}
\item \textbf{if} \alert<6>{\texttt{holdsfork}$_{i,j}\;\forall$Nachbarn $c_k$} \textbf{then}
	\begin{pcode}
	\item \dots
	\end{pcode}
\end{pcode}
\end{block}
\vbox{
\only<2>{Erhält ein Philosoph die Gabel, \dots}
\only<3>{\dots so hat er sie. ;-)}
\only<4>{Manchmal wird das Prioritätstoken \dots}
\only<5>{\dots oder ein \texttt{request} mitgesendet.}
\only<6>{Hat er jetzt beide Gabeln, so kann er \dots}
}
\vbox{}
\end{frame}


\begin{frame}
%% drittes Inp-Actionpaar!
\frametitle{Algorithmusidee (4)}
\framesubtitle{Essen :-)}

\begin{block}{\textbf{if} {\texttt{holdsfork}$_{i,j}\;\forall$Nachbarn $c_k$} \textbf{then}}
\begin{pcode}
\item \alert<1>{eat}
\item \alert<2>{\texttt{hungry}$_i:=\;$\texttt{false}}
\item \textbf{for all} \alert<3>{Nachbarn $c_k$} \textbf{do}
	\begin{pcode}
	\item \textbf{if} \alert<4>{\texttt{holdspriotoken}$_{i,k}$} \textbf{then}
		\begin{pcode}
		\item \alert<5>{\texttt{holdspriotoken}$_{i,k}:=\;$\texttt{false}}
		\item \textbf{if} \alert<6>{\texttt{needsfork}$_{i,k}$} \textbf{then}
			\begin{pcode}
			\alert<7>{
			\item \texttt{needsfork}$_{i,k}:=\;$\texttt{false}
			\item \texttt{holdsfork}$_{i,k}:=\;$\texttt{false}
			\item \alert<5>{send} \texttt{fork(\alert<5>{priotoken})} \alert<5>{to $(c_i,c_k)$}}
			\end{pcode}
		\textbf{else}
			\begin{pcode}
			\item \alert<5>{send \texttt{priotoken} to $(c_i,c_k)$}
			\end{pcode}
		\end{pcode}
	\end{pcode}
\end{pcode}
\end{block}
\vbox{
\only<1>{Essen!}
\only<2>{Endlich satt.}
\only<3>{Nun kann er die Nachbarn wieder beachten.}
\only<4>{Besitzt er Prioritätstoken, \dots}
\only<5>{\dots, dann gibt er es dem jeweiligen Nachbarn.}
\only<6>{Benötigt ein Nachbar die Gabel, \dots}
\only<7>{\dots kriegt er sie jetzt.}
}
\vbox{}
\end{frame}

\begin{frame}
%% viertes (letztes) Inp-Actionpaar!
\frametitle{Algorithmusidee (5)}
\framesubtitle{Das berüchtigte Prioritätstoken}

\begin{block}{\textbf{Async} \texttt{Philosophen} $c_i$}
\textbf{Input:} \alert<2>{\texttt{msg}$\;=\;$\texttt{priotoken}} 
	with \texttt{origin(msg)}$=(c_j,c_i) \in In_i$ \\
\textbf{Action:}
\begin{pcode}
\item \alert<3>{\texttt{holdspriotoken}$_{i,j}:=$\texttt{true}}
\end{pcode}
\end{block}
\vbox{
\begin{itemize}
\item<2-> Erhält ein Philosoph das Prioritätstoken, \dots
\item<3> \dots dann hat er es.
\end{itemize}
}
\vbox{}
\end{frame}

\section{Aufgabe}
\subsection{Aufgabenstellung}

\begin{frame}
\frametitle{Aufgabenstellung}
Diskutieren Sie, ob der Algorithmus alle drei der folgenden 
Eigenschaften besitzt:
\begin{itemize}
\pause
\item Korrektheit
\pause
\item Lebendigkeit
\pause
\item Verhungerungsfreiheit
\end{itemize}
\pause
Diskutieren Sie ebenfalls die folgenden Eigenschaften:
\begin{itemize}
\pause
\item Botschaftenkomplexität
\pause
\item Adaptivität an wechselnd lange Denk- und Essperioden
\pause
\item Robustheit bei \emph{fail-stop}-Ausfällen
\end{itemize}
\end{frame}

\subsection{Lösung}

%\subsubsection{Korrektheit}

\begin{frame}
\frametitle{Korrektheit}
\framesubtitle{Wird eine Gabel zu jedem Zeitpunkt von höchstens einem 
Philosophen benutzt?}
\pause
Annahme:
\begin{itemize}
\item korrekte Initialisierung
\item keine Angreifer von au\ss{}en
\end{itemize}
\pause
Dann wird eine Gabel \emph{nie} von mehreren Philosophen gleichzeitig genutzt,
denn
\pause
eine Gabel wird immer losgelassen, bevor \texttt{fork($\cdot$)} gesendet wird.
\pause
$\Rightarrow\;$\emph{Korrekt!}
\pause
\begin{columns}[t]
\column{.5\textwidth}
\begin{block}{Code-Schnipsel \texttt{request}}
\alert{\texttt{holdsfork}$_{i,j}:=\;$\texttt{false}}\\
\textbf{if not} \texttt{hungry}$_i$ \textbf{then}
	\begin{pcode}
	\item \alert{send \texttt{fork(nil)} to $c_j$}
	\end{pcode}
\textbf{else}
	\alert{send \texttt{fork(request)} to $c_j$}
\end{block}
\pause
\column{.5\textwidth}
\begin{block}{Code-Schnipsel \texttt{fork(param)}}
\texttt{needsfork}$_{i,k}:=\;$\texttt{false}
\alert{
\texttt{holdsfork}$_{i,k}:=\;$\texttt{false}\\
send \texttt{fork(priotoken)} to $c_k$}
\end{block}
\end{columns}
\end{frame}


%\subsubsection{Einschub: formales Problem}

\begin{frame}
\frametitle{Ein kleines formales Problem}
\framesubtitle{$n=2$ verwirrt den Algorithmus}

\begin{columns}
\column{0.5\textwidth}\uncover<2->{Wunsch:}
\column{0.5\textwidth}\uncover<4->{Realität:}
\end{columns}
\begin{columns}
\column{0.5\textwidth}
\uncover<2->{
\begin{center}
 \begin{tikzpicture}
  \only<1-2>{
  \path	(0,1) node(a) [circle,draw] {\tiny $c_1$}
  	(2,1) node(b) [circle,draw] {\tiny $c_2$};}
  \only<3->{
  \path	(0,1) node(a) [circle,draw,fill=green] {\tiny $c_1$}
  	(2,1) node(b) [circle,draw] {\tiny $c_2$};}
  \draw[orange] (b) -- (1,0.45);
  \draw[orange] (b) -- (1,1.55);
  \draw[thick] (1,0.3) -- (1,0.6);
  \draw[thick] (1,1.7) -- (1,1.4);
  \visible<3->{\draw[thick,blue,->] (a) .. controls (1,2) .. node[above,sloped] {\texttt{request}} (b);
               \draw[thick,blue,->] (a) .. controls (1,0) .. node[below,sloped] {\texttt{request}} (b);}
 \end{tikzpicture}
\end{center}
}
\column{0.5\textwidth}
\uncover<4->{
\begin{center}
 \begin{tikzpicture}
  \only<1-2>{
  \path	(0,1) node(a) [circle,draw] {\tiny $c_1$}
  	(2,1) node(b) [circle,draw] {\tiny $c_2$};}
  \only<3->{
  \path	(0,1) node(a) [circle,draw,fill=green] {\tiny $c_1$}
  	(2,1) node(b) [circle,draw] {\tiny $c_2$};}
  \visible<5->{\draw[thick,blue,->] (a) -- node[above] {\texttt{request}} (b);}
  \draw[thick] (1,0.3) -- (1,0.6);
  \draw[thick] (1,1.7) -- (1,1.4);
  \draw[orange] (b) -- (1,0.45);
  \draw[orange] (b) -- (1,1.55);
 \end{tikzpicture}
\end{center}
}
\end{columns}
\begin{itemize}
\item<6-> $c_2$ wei\ss{} nur: \texttt{request} kam von $c_1$.
\item<7-> Wei\ss{} nicht: Kam der Request von \emph{links} oder \emph{rechts}?
\item<8-> Lösung: Einführung von "`Ports"'
 \begin{itemize}
 \item Port \texttt{0} für den jeweils linken Nachbarn,
 \item Port \texttt{1} für den jeweils rechten Nachbarn.
 \end{itemize}
\end{itemize}
\end{frame}




%\subsubsection{Lebendigkeit und Verhungerungsfreiheit}

\begin{frame}
\frametitle{Lebendigkeit und Verhungerungsfreiheit (1)}
\framesubtitle{Einführung}
\uncover<2->{Ist ein Philosoph hungrig, \dots}
\begin{description}
\item[\uncover<4->{Lebendigkeit}]
 \uncover<3->{\dots so erhält \emph{irgendein} Philosoph einmal seine Gabeln.}\uncover<7->{\footnote{"`Es tut sich was."'}}
\item[\uncover<6->{Verhungerungsfreiheit}]
 \uncover<5->{\dots so erhält \emph{dieser} Philosoph einmal seine Gabeln.}\uncover<8->{\footnote{eine reelle Chance auf Nahrung.}}
\end{description}

\vspace{5mm}
\uncover<9->{
\begin{block}{Fakt}
Ist der Algorithmus nicht \emph{lebendig}, so ist er auch nicht
\emph{verhungerungsfrei}.
\end{block}}
\vspace{5mm}
\uncover<10->{"`nicht lebendig"' bedeutet, dass Deadlocks existieren.}
\end{frame}



\begin{frame}
\frametitle{Lebendigkeit und Verhungerungsfreiheit (2)}
\framesubtitle{Analyse: zwei einfache Szenarien}
\begin{columns}
\column{0.5\textwidth}\uncover<2->{Szenario 1}
\column{0.5\textwidth}\uncover<7->{Szenario 2}
\end{columns}

\begin{columns}
\column{0.5\textwidth}
\uncover<2->{
\begin{center}
 \begin{tikzpicture}
 \only<1-2>{
  \path	(1,3) node(c1) [circle,draw] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw] {\tiny $c_4$};}
 \only<3->{
  \path	(1,3) node(c1) [circle,draw,fill=green] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};}
  \draw[orange] (c1) -- (2,3);
  \fill[red] (1.5,3) circle (0.6ex);
  \draw[orange] (c2) -- (3,2);
  \fill[red] (3,2.5) circle (0.6ex);
  \draw[orange] (c3) -- (2,1);
  \fill[red] (2.5,1) circle (0.6ex);
  \draw[orange] (c4) -- (1,2);
  \fill[red] (1,1.5) circle (0.6ex);
  \draw[thick] (2,3.3) -- (2,2.7);
  \draw[thick] (2.7,2) -- (3.3,2);
  \draw[thick] (2,1.3) -- (2,0.7);
  \draw[thick] (0.7,2) -- (1.3,2);
  
  \visible<4>{
  \draw[thick,blue,->] (c1) .. controls (0.5,2) .. node[left,near start] {\texttt{req}} (c4);
  \draw[thick,blue,->] (c2) .. controls (2,3.5) .. node[above,near start] {\texttt{req}} (c1);
  \draw[thick,blue,->] (c3) .. controls (3.5,2) .. node[right,near start] {\texttt{req}} (c2);
  \draw[thick,blue,->] (c4) .. controls (2,0.5) .. node[below,near start] {\texttt{req}} (c3);
  }
  \visible<5->{
  \fill[cyan] (1.5,3) circle (0.3ex);
  \fill[cyan] (3,2.5) circle (0.3ex);
  \fill[cyan] (2.5,1) circle (0.3ex);
  \fill[cyan] (1,1.5) circle (0.3ex);
  }
 \end{tikzpicture}
\end{center}
}
\column{0.5\textwidth}
\uncover<7->{
\begin{center}
 \begin{tikzpicture}
 \only<1-7>{
  \path	(1,3) node(c1) [circle,draw] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw] {\tiny $c_4$};}
 \only<8->{
  \path	(1,3) node(c1) [circle,draw,fill=green] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};}
  \draw[orange] (c1) -- (2,3);
  \fill[red] (1.5,3) circle (0.6ex);
  \draw[orange] (c1) -- (1,2);
  \fill[red] (1,2.5) circle (0.6ex);
  \draw[orange] (c3) -- (3,2);
  \fill[red] (3,1.5) circle (0.6ex);
  \draw[orange] (c3) -- (2,1);
  \fill[red] (2.5,1) circle (0.6ex);
  \draw[thick] (2,3.3) -- (2,2.7);
  \draw[thick] (2.7,2) -- (3.3,2);
  \draw[thick] (2,1.3) -- (2,0.7);
  \draw[thick] (0.7,2) -- (1.3,2);

  \visible<9>{
  \draw[thick,blue,->] (c4) .. controls (0.5,2) .. node[left,near start] {\texttt{req}} (c1);
  \draw[thick,blue,->] (c2) .. controls (2,3.5) .. node[above,near start] {\texttt{req}} (c1);
  \draw[thick,blue,->] (c2) .. controls (3.5,2) .. node[right,near start] {\texttt{req}} (c3);
  \draw[thick,blue,->] (c4) .. controls (2,0.5) .. node[below,near start] {\texttt{req}} (c3);
  }
  \visible<10->{
  \fill[cyan] (1.5,3) circle (0.3ex);
  \fill[cyan] (1,2.5) circle (0.3ex);
  \fill[cyan] (3,1.5) circle (0.3ex);
  \fill[cyan] (2.5,1) circle (0.3ex);
  }
 \end{tikzpicture}
\end{center}
}
\end{columns}
\begin{columns}
\column{0.5\textwidth}
 \uncover<6->{\begin{center}typische Verklemmung\end{center}}
\column{0.5\textwidth}
 \uncover<11->{\begin{center}Verklemmung aufgrund von Dummheit\end{center}}
\end{columns}
\end{frame}

\begin{frame}
\frametitle{Lebendigkeit und Verhungerungsfreiheit (3)}
\framesubtitle{Szenario 2: Dummheit statt Lebendigkeit?}
\uncover<2->{Nochmal Szenario 2:
\begin{center}
 \begin{tikzpicture}
 \only<1-2>{
  \path	(1,3) node(c1) [circle,draw] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw] {\tiny $c_4$};}
 \only<3-6>{
  \path	(1,3) node(c1) [circle,draw,fill=green] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};}
 \only<7-9>{
  \path	(1,3) node(c1) [circle,draw,fill=orange] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=orange] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};}
 \only<10-13>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};}
 \only<14>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=orange] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=orange] {\tiny $c_4$};}
 \only<15->{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$};}
 \only<19>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};}
 \only<20>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=orange] {\tiny $c_4$};}
 \only<21-22>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$};}
 \only<23>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=orange] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$};}
 \only<24>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$};}
	
  \visible<1-11>{
  \draw[orange] (c1) -- (2,3);
  \draw[orange] (c1) -- (1,2);
  \draw[orange] (c3) -- (3,2);
  \draw[orange] (c3) -- (2,1);
  }
  \visible<13-20,26->{
  \draw[orange] (c2) -- (2,3);
  \draw[orange] (c4) -- (1,2);
  \draw[orange] (c2) -- (3,2);
  \draw[orange] (c4) -- (2,1);
  }
  \visible<21,25>{
  \draw[orange] (c2) -- (2,3);
  \draw[orange] (c4) -- (1,2);
  }
  \visible<22-24>{
  \draw[orange] (c2) -- (2,3);
  \draw[orange] (c4) -- (1,2);
  \draw[orange] (c3) -- (3,2);
  \draw[orange] (c3) -- (2,1);
  }
  
  \draw[thick] (2,3.3) -- (2,2.7);
  \draw[thick] (2.7,2) -- (3.3,2);
  \draw[thick] (2,1.3) -- (2,0.7);
  \draw[thick] (0.7,2) -- (1.3,2);

  \visible<1-11,17-24>{
  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (3,1.5) circle (0.6ex);
  \fill[red] (2.5,1) circle (0.6ex);
  }
  \visible<13-15>{
  \fill[red] (2.5,3) circle (0.6ex);
  \fill[red] (1,1.5) circle (0.6ex);
  \fill[red] (3,2.5) circle (0.6ex);
  \fill[red] (1.5,1) circle (0.6ex);
  }
  \visible<25>{
  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  }
  \visible<26->{
  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (3,2.5) circle (0.6ex);
  \fill[red] (1.5,1) circle (0.6ex);
  }
  \visible<8>{
  \draw[thick,blue,->] (c4) .. controls (0.5,2) .. node[left,near start] {\texttt{req}} (c1);
  \draw[thick,blue,->] (c2) .. controls (2,3.5) .. node[above,near start] {\texttt{req}} (c1);
  \draw[thick,blue,->] (c2) .. controls (3.5,2) .. node[right,near start] {\texttt{req}} (c3);
  \draw[thick,blue,->] (c4) .. controls (2,0.5) .. node[below,near start] {\texttt{req}} (c3);
  }
  \visible<12>{
  \draw[thick,red,->] (c1) .. controls (0.5,2) .. node[left,near start] {\texttt{f(p)}} (c4);
  \draw[thick,red,->] (c1) .. controls (2,3.5) .. node[above,near start] {\texttt{f(p)}} (c2);
  \draw[thick,red,->] (c3) .. controls (3.5,2) .. node[right,near start] {\texttt{f(p)}} (c2);
  \draw[thick,red,->] (c3) .. controls (2,0.5) .. node[below,near start] {\texttt{f(p)}} (c4);
  }
  \visible<16>{
  \draw[thick,red,->] (c4) .. controls (0.5,2) .. node[left,near start] {\texttt{prio}} (c1);
  \draw[thick,red,->] (c2) .. controls (2,3.5) .. node[above,near start] {\texttt{prio}} (c1);
  \draw[thick,red,->] (c2) .. controls (3.5,2) .. node[right,near start] {\texttt{prio}} (c3);
  \draw[thick,red,->] (c4) .. controls (2,0.5) .. node[below,near start] {\texttt{prio}} (c3);
  }
  \visible<20>{
  \draw[thick,blue,->] (c3) .. controls (3.5,2) .. node[right,near start] {\texttt{req}} (c2);
  \draw[thick,blue,->] (c3) .. controls (2,0.5) .. node[below,near start] {\texttt{req}} (c4);
  }
  \visible<21>{
  \draw[thick,red,->] (c2) .. controls (3.5,2) .. node[right,near start] {\texttt{fork}} (c3);
  \draw[thick,red,->] (c4) .. controls (2,0.5) .. node[below,near start] {\texttt{fork}} (c3);
  }
  \visible<25>{
  \draw[thick,red,->] (c3) .. controls (3.5,2) .. node[right,near start] {\texttt{f(p)}} (c2);
  \draw[thick,red,->] (c3) .. controls (2,0.5) .. node[below,near start] {\texttt{f(p)}} (c4);
  }

  \visible<9-10>{
  \fill[cyan] (1.5,3) circle (0.3ex);
  \fill[cyan] (1,2.5) circle (0.3ex);
  \fill[cyan] (3,1.5) circle (0.3ex);
  \fill[cyan] (2.5,1) circle (0.3ex);
  }
 \end{tikzpicture}
\end{center}
}

\visible<4->{"`Warum essen $c_1$ und $c_3$ jetzt nicht?"'}
\visible<5->{-- "`Das steht nicht im Action-Teil für \texttt{msg=nil}."'}
\visible<6->{-- "`Sie sollen aber essen!"'}
\visible<7->{-- "`Ok\dots"'}
\visible<18->{-- "`Einwandfrei! :-)"'}
\end{frame}



\begin{frame}
\frametitle{Lebendigkeit und Verhungerungsfreiheit (4)}
\framesubtitle{Szenario 2: Die Lösung}

\begin{columns}
\column{.7\textwidth}
\uncover<2->{
\begin{block}{\textbf{if} {\texttt{holdsfork}$_{i,j}\;\forall$Nachbarn $c_k$} \textbf{then}}
eat ; \texttt{hungry}$_i:=\;$\texttt{false}\\
\textbf{for all} Nachbarn $c_k$ \textbf{do}
\begin{pcode}
\item \textbf{if} \texttt{holdspriotoken}$_{i,k}$ \textbf{then}
	\begin{pcode}
	\item \texttt{holdspriotoken}$_{i,k}:=\;$\texttt{false}
	\item \textbf{if} \texttt{needsfork}$_{i,k}$ \textbf{then}
		\begin{pcode}
		\item \texttt{needsfork}$_{i,k}:=\;$\texttt{false}
		\item \texttt{holdsfork}$_{i,k}:=\;$\texttt{false}
		\item send \texttt{fork(priotoken)} to $c_k$
		\end{pcode}
	\textbf{else}
		\begin{pcode}
		\item send \texttt{priotoken} to $c_k$
		\end{pcode}
	\end{pcode}
\end{pcode}
\end{block}}
\column{.3\textwidth}
\uncover<3->{Das ist der Code zum Essen aus \texttt{msg}$=$\texttt{fork(param)}.}
\uncover<4->{Den hängen wir an den Action-Teil zum Input \texttt{msg}$=$\texttt{nil} an.}
\end{columns}
\end{frame}



\begin{frame}
\frametitle{Lebendigkeit und Verhungerungsfreiheit (5)}
\framesubtitle{Fazit}

\begin{itemize}
\pause
\item bei einfachen Szenarien\footnote{Startbelegungen von Gabeln und Token}
	schon Verklemmungen am Anfang
\pause
\item Verklemmung bei \emph{Szenario 2} konnte mittels "`Copy\&Paste"' gelöst werden
\pause
\item Beobachtung: mit Startbelegung aus \emph{Szenario 2} kann typische Verklemmung
	wie in \emph{Szenario 1} nicht erreicht werden
	\begin{itemize}
	\pause
	\item mit Induktion und größerer Fallunterscheidung beweisbar
	\pause
	\item es entstehen zwei Klassen von Belegungen: \textsc{verklemmungsfrei}, \textsc{verhungerungsfrei}
	\end{itemize}
\pause
\item \alert{Lösung}: Initialisierung mit \emph{Szenario 2} erzwingen und der Algorithmus
	ist lebendig und verhungerungsfrei
\end{itemize}
\end{frame}

% (3)
% unterschlagen: was ist mit n=ungerade?
\begin{frame}
\frametitle{Lebendigkeit und Verhungerungsfreiheit (6)}
\framesubtitle{Startbelegung für ungerade $n$}
\uncover<2->{Beispiel $n=5$:
\begin{center}
 \begin{tikzpicture}
 \only<1-2>{
  \path	(1,3) node(c1) [circle,draw] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw] {\tiny $c_5$};}
 \only<3>{
  \path	(1,3) node(c1) [circle,draw,fill=green] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw,fill=green] {\tiny $c_5$};}
 \only<4-6>{
  \path	(1,3) node(c1) [circle,draw,fill=orange] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=orange] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw,fill=green] {\tiny $c_5$};}
 \only<7-9>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw,fill=green] {\tiny $c_5$};}
 \only<10>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=orange] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw,fill=orange] {\tiny $c_5$};}
 \only<11-13>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw,fill=white] {\tiny $c_5$};}
 \only<14>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=orange] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw,fill=white] {\tiny $c_5$};}
 \only<15->{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$}
	(4,2) node(c5) [circle,draw,fill=white] {\tiny $c_5$};}
	
  \visible<1-7>{
  \draw[orange] (c1) -- (2,3);
  \draw[orange] (c1) -- (1,2);
  \draw[orange] (c3) -- (2,1);
  
  \draw[orange] (c3) -- (4,1);
  \draw[orange] (c5) -- (4,3);
  }
  \visible<8>{
  \draw[orange] (c5) -- (4,3);
  }
  \visible<9-11>{
  \draw[orange] (c2) -- (2,3);
  \draw[orange] (c4) -- (1,2);
  \draw[orange] (c4) -- (2,1);
  \draw[orange] (c5) -- (4,3);
  \draw[orange] (c5) -- (4,1);
  }
  \visible<12>{
  \draw[orange] (c2) -- (2,3);
  \draw[orange] (c4) -- (1,2);
  \draw[orange] (c4) -- (2,1);
  \draw[orange] (c5) -- (4,1);
  }
  \visible<13->{
  \draw[orange] (c2) -- (2,3);
  \draw[orange] (c2) -- (4,3);
  \draw[orange] (c4) -- (1,2);
  \draw[orange] (c4) -- (2,1);
  \draw[orange] (c5) -- (4,1);
  }
  

  \draw[thick] (2,3.3) -- (2,2.7);
  \draw[thick] (2,1.3) -- (2,0.7);
  \draw[thick] (0.7,2) -- (1.3,2);
  \draw[thick] (4.2,0.8) -- (3.8,1.2);
  \draw[thick] (3.8,2.8) -- (4.2,3.2);

  \visible<1-7>{
  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (2.5,1) circle (0.6ex);

  \fill[red] (3.5,1) circle (0.6ex);
  \fill[red] (4,2.5) circle (0.6ex);
  }
  \visible<8>{
  \fill[red] (4,2.5) circle (0.6ex);
  }
  \visible<9-11>{
  \fill[red] (2.5,3) circle (0.6ex);
  \fill[red] (1,1.5) circle (0.6ex);
  \fill[red] (1.5,1) circle (0.6ex);

  \fill[red] (4,1.5) circle (0.6ex);
  \fill[red] (4,2.5) circle (0.6ex);
  }
  \visible<12>{
  \fill[red] (2.5,3) circle (0.6ex);
  }
  \visible<13-15>{
  \fill[red] (2.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (2.5,1) circle (0.6ex);

  \fill[red] (3.5,1) circle (0.6ex);
  \fill[red] (3.5,3) circle (0.6ex);
  }
  \visible<16>{
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (2.5,1) circle (0.6ex);
  \fill[red] (3.5,1) circle (0.6ex);
  }
  \visible<17>{
  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (2.5,1) circle (0.6ex);
  \fill[red] (3.5,1) circle (0.6ex);
  \fill[red] (4,2.5) circle (0.6ex);
  }

  \visible<5>{
  \draw[thick,blue,->] (c4) .. controls (0.5,2) .. node[left,near start] {\texttt{req}} (c1);
  \draw[thick,blue,->] (c2) .. controls (2,3.5) .. node[above,near start] {\texttt{req}} (c1);

  \draw[thick,blue,->] (c2) .. controls (3,2.5) .. node[left,near start] {\texttt{req}} (c5);
  \draw[thick,blue,->] (c5) .. controls (3,1.5) .. node[left,near start] {\texttt{req}} (c3);

  \draw[thick,blue,->] (c4) .. controls (2,0.5) .. node[below,near start] {\texttt{req}} (c3);
  }
  \visible<8>{
  \draw[thick,red,->] (c1) .. controls (0.5,2) .. node[left,near start] {\texttt{f(p)}} (c4);
  \draw[thick,red,->] (c1) .. controls (2,3.5) .. node[above,near start] {\texttt{f(p)}} (c2);
  \draw[thick,red,->] (c3) .. controls (2,0.5) .. node[below,near start] {\texttt{f(p)}} (c4);

  \draw[thick,red,->] (c3) .. controls (3,1.5) .. node[left,near start] {\texttt{f(p)}} (c5);
  }
  \visible<12>{
  \draw[thick,red,->] (c4) .. controls (0.5,2) .. node[left,near start] {\texttt{prio}} (c1);
  \draw[thick,red,->] (c4) .. controls (2,0.5) .. node[below,near start] {\texttt{prio}} (c3);
  \draw[thick,red,->] (c5) .. controls (3,1.5) .. node[left,near start] {\texttt{prio}} (c3);
  \draw[thick,red,->] (c5) .. controls (3,2.5) .. node[left,near start] {\texttt{f(p)}} (c2);
  }
  \visible<16>{
  \draw[thick,red,->] (c2) .. controls (2,3.5) .. node[above,near start] {\texttt{prio}} (c1);
  \draw[thick,red,->] (c2) .. controls (3,2.5) .. node[left,near start] {\texttt{prio}} (c5);
  }

  \visible<6-7>{
  \fill[cyan] (1.5,3) circle (0.3ex);
  \fill[cyan] (1,2.5) circle (0.3ex);
  \fill[cyan] (2.5,1) circle (0.3ex);
  \fill[cyan] (3.5,1) circle (0.3ex);
  \fill[cyan] (4,2.5) circle (0.3ex);
  }
  \visible<8-11>{
  \fill[cyan] (4,2.5) circle (0.3ex);
  }
 \end{tikzpicture}
\end{center}
}
\end{frame}

%\subsubsection{Botschaftenkomplexität}

\begin{frame}
\frametitle{Botschaftenkomplexität}
\framesubtitle{Worst-Case}
\pause
Wieviele Botschaften werden bei $n$ Philosophen und $r$ Essensrunden
maximal verschickt?
\begin{itemize}
\pause
\item $k_{\texttt{nil}} \leq 2$
\pause
\item $k_{\texttt{request}} \leq 1$
\pause
\item $k_{\texttt{fork}} \leq 2$
\pause
\item $k_{\texttt{prio}} = 0$
\pause
\item ein Philosoph wird hungrig: 
	$k_{c_i} \pause = k_{\texttt{nil}} \pause \cdot k_{\texttt{request}} 
	\pause + k_{\texttt{fork}} \pause + k_{\texttt{prio}} \pause \leq
	2\cdot1+2+0\pause =4$
\pause
\item alle Philosophen werden hungrig: $k_{c_1,\dots,c_n} \pause = 4 \cdot n$
\pause
\item alle Philosophen werden $r$-mal hungrig: $K\pause =4\,r\,n\pause =\alert{{\cal O}\left(r\,n\right)}$
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Adaptivität an wechselnd lange Denk- und Essperioden}
\begin{itemize}
\pause
\item Denkt ein Philosoph lange, \pause dann will er keine Gabeln
	\pause $\Rightarrow$ die anderen können essen
\pause
\item Isst ein Philosoph lange, \pause so kann es passieren, dass alle 
	auf diesen Philosophen warten müssen.
	\begin{itemize}
	\pause
	\item unabhängig von Prioritätstoken, weil Essvorgang \emph{atomar}
	\end{itemize}
\end{itemize}
\end{frame}



%\subsubsection{fail-stop-Ausfälle}

\begin{frame}
\frametitle{\emph{fail-stop}-Ausfälle (1)}
\framesubtitle{Ausfall beim Essen}

\uncover<2->{
\begin{center}
 \begin{tikzpicture}
  \path	(1,3) node(c1) [circle,draw,fill=orange] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=green] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=green] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};


  \draw[orange] (c1) -- (2,3);
  \draw[orange] (c1) -- (1,2);
  \draw[orange] (c2) -- (3,2);
  \draw[orange] (c4) -- (2,1);
  
  \draw[thick] (2,3.3) -- (2,2.7);
  \draw[thick] (2.7,2) -- (3.3,2);
  \draw[thick] (2,1.3) -- (2,0.7);
  \draw[thick] (0.7,2) -- (1.3,2);

  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (3,2.5) circle (0.6ex);
  \fill[red] (1.5,1) circle (0.6ex);

  \fill[cyan] (1.5,3) circle (0.3ex);
  \fill[cyan] (1,2.5) circle (0.3ex);
  \fill[cyan] (3,2.5) circle (0.3ex);
  \fill[cyan] (1.5,1) circle (0.3ex);
  
  \visible<3->{
  	\draw[thick] (0.7,2.7) -- (1.3,3.3);
	\draw[thick] (0.7,3.3) -- (1.3,2.7);
  	\draw[red] (0.7,2.7) -- (1.3,3.3);
	\draw[red] (0.7,3.3) -- (1.3,2.7);
  }
  \visible<4->{
  	\draw[thick] (1.4,2.8) -- (1.8,3.2);
	\draw[thick] (1.4,3.2) -- (1.8,2.8);
  	
	\draw[thick] (0.8,2.2) -- (1.2,2.6);
	\draw[thick] (0.8,2.6) -- (1.2,2.2);
  }
 \end{tikzpicture}
\end{center}
}
\begin{itemize}
\item<2-> $c_1$ isst gerade. $c_2,c_4$ warten auf ihn. $c_3$ wartet auf $c_2,c_4$.
\item<3-> $c_1$ fällt beim Essen aus.
\item<4-> Token und Gabeln sind ebenfalls weg.
\item<5-> Deadlock!
\end{itemize}
\end{frame}




\begin{frame}
\frametitle{\emph{fail-stop}-Ausfälle (2)}
\framesubtitle{Verlust von Botschaften}

\begin{columns}
\column{.5\textwidth}
\uncover<2->{
\begin{center}
 \begin{tikzpicture}
  \only<1-3>{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$};}
  \only<3->{
  \path	(1,3) node(c1) [circle,draw,fill=white] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=green] {\tiny $c_4$};}

  \draw[orange] (c1) -- (2,3);
  \draw[orange] (c1) -- (1,2);
  \draw[orange] (c2) -- (3,2);
  \draw[orange] (c4) -- (2,1);
  
  \draw[thick] (2,3.3) -- (2,2.7);
  \draw[thick] (2.7,2) -- (3.3,2);
  \draw[thick] (2,1.3) -- (2,0.7);
  \draw[thick] (0.7,2) -- (1.3,2);

  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (3,2.5) circle (0.6ex);
  \fill[red] (1.5,1) circle (0.6ex);
  
  \visible<4->{
   \draw[thick,blue,->] (c4) .. controls (0.5,2) .. node[left,near start] {\texttt{req}} (0.7,2.4);
   \draw[thick] (0.5,2.2) -- (0.9,2.6);
   \draw[thick] (0.5,2.6) -- (0.9,2.2);
  }
 \end{tikzpicture}
\end{center}
}
\column{.5\textwidth}
\uncover<5->{
\begin{center}
 \begin{tikzpicture}
  \only<1->{
  \path	(1,3) node(c1) [circle,draw,fill=green] {\tiny $c_1$}
  	(3,3) node(c2) [circle,draw,fill=white] {\tiny $c_2$}
	(3,1) node(c3) [circle,draw,fill=white] {\tiny $c_3$}
  	(1,1) node(c4) [circle,draw,fill=white] {\tiny $c_4$};}

  \draw[orange] (c1) -- (2,3);
  \only<1-5>{
  \draw[orange] (c4) -- (1,2);
  }
  \draw[orange] (c2) -- (3,2);
  \draw[orange] (c4) -- (2,1);
  
  \draw[thick] (2,3.3) -- (2,2.7);
  \draw[thick] (2.7,2) -- (3.3,2);
  \draw[thick] (2,1.3) -- (2,0.7);
  \draw[thick] (0.7,2) -- (1.3,2);

  \fill[red] (1.5,3) circle (0.6ex);
  \fill[red] (1,2.5) circle (0.6ex);
  \fill[red] (3,2.5) circle (0.6ex);
  \fill[red] (1.5,1) circle (0.6ex);
  
  \visible<6->{
   \draw[thick,red,->] (c4) .. controls (0.5,2) .. node[left,near start] {\texttt{fork}} (0.7,2.4);
   \draw[thick] (0.5,2.2) -- (0.9,2.6);
   \draw[thick] (0.5,2.6) -- (0.9,2.2);
  }
 \end{tikzpicture}
\end{center}
}
\end{columns}
\vspace{6mm}
\begin{itemize}
\item<7-> Keine erneuten \texttt{request}s bei Verlust.
\item<8-> Gabeln und Token verschwinden im Nirvana und werden nie wieder aufgesammelt.
\item<9-> Führt letztendlich zu Verhungerungen und Verklemmungen!
\end{itemize}
\end{frame}


%\section*{Ende}

\begin{frame}
\frametitle{Das war's!}
\framesubtitle{thx}
\begin{center}\Huge Vielen Dank für die Aufmerksamkeit!\end{center}
\end{frame}

\end{document}