\documentclass[a4paper,twoside,12pt]{article}
%\usepackage [reqno] {amsmath}
\usepackage{amsfonts,amstext}
\usepackage{amsmath}
\usepackage{german}
\usepackage{graphicx}
\usepackage{fullpage}

\newcommand{\ZETTELNUMMER}{5}
\newcommand{\ABGABEDATUM}{am 25. Mai 2018 bis 12 Uhr in die
Tutorenf\"acher}

\newcounter{AUFGNR}
\setcounter{AUFGNR}{1}
\newcommand{\AUFGABE}[2]{\vspace{0.3cm}\item[Aufgabe~\arabic{AUFGNR}]\stepcounter{AUFGNR} #1\hfill\emph{#2}}


\newcommand{\floor}[1]{\left\lfloor{#1}\right\rfloor}
\newcommand{\ceil}[1]{\left\lceil{#1}\right\rceil}
\newcommand{\half}[1]{\frac{#1}{2}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}



\renewcommand{\labelenumi}{(\alph{enumi})}
\renewcommand{\labelenumii}{(\roman{enumii})}


\begin{document}
\pagestyle{empty}
\hrule\medskip
\rule{0ex}{0ex}\\[-1ex]
\ZETTELNUMMER. Aufgabenblatt zur Vorlesung

\smallskip
\noindent
\large
\textbf{Nichtsequentielle und Verteilte Programmierung}\hfill SoSe 
2018 \\[0.5ex]
\normalsize
Wolfgang Mulzer, Katinka Wolter

\medskip\hrule

\smallskip
\noindent
\textbf{Abgabe} \ABGABEDATUM

\vskip 0.5cm

\begin{description}

\AUFGABE{Algorithmus von Dekker}{10 Punkte}

Der Algorithmus von Dekker  lautete folgenderma\ss{}en:
\begin{verbatim}
======================================================
  global adrin = false, bdrin = false, dran = a
a1: U                        | b1: U
a2: adrin  <- true           | b2: bdrin  <- true
a3: while bdrin do           | b3: while adrin do 
a4:    if dran = b then      | b4:    if dran = a then
a5:       adrin <- false     | b5:       bdrin <- false 
a6:       while dran != a do | b6:       while dran != b do
a7:          NOP             | b7:          NOP
a8:       adrin <- true      | b8:       bdrin <- true 
a9: K                        | b9: K
a10:dran <- b                | b10:dran <- a
a11:adrin <- false           | b11:bdrin <- false 
\end{verbatim}

\begin{enumerate}
\item Beweisen Sie, dass der Algorithmus von Dekker die folgenden
  Invarianten erf\"ullt:
  \begin{enumerate}
      \item $\Box (\texttt{dran} = a \vee \texttt{dran} = b)$,
      \item $\Box (a_3 \vee a_4 \vee a_5 \vee a_9 \vee a_{10} \vee 
        a_{11} \Leftrightarrow \texttt{adrin})$, und
      \item $\Box (b_3 \vee b_4 \vee b_5 \vee b_9 \vee b_{10} \vee 
        b_{11} \Leftrightarrow \texttt{bdrin})$.
  \end{enumerate}
  \item Der individuelle Fortschritt f\"ur \texttt{a} war 
    folgenderma\ss{}en spezifiziert: F\"ur jede m\"ogliche 
    Zustandsfolge gilt
    \[
        \Box (a_2 \Rightarrow \lozenge a_9) \tag{*}
    \]
    Zeigen Sie, dass (*) auch dann gilt, wenn \texttt{a} oder 
    \texttt{b} in ihren unkritischen Abschnitten h\"angenbleiben 
    k\"onnen, d..h., es gelten nur  
    $\Box (a_1 \Rightarrow \lozenge (a_2 \vee a_\perp))$ und 
    $\Box(b_1 \Rightarrow \lozenge (b_2 \vee b_\perp))$ statt
    $\Box (a_1 \Rightarrow \lozenge a_2 )$ und 
   $\Box(b_1 \Rightarrow \lozenge b_2)$.
\end{enumerate}

\AUFGABE{Pr\"afixsummen}{10 Punkte}

Sei $A$ ein Feld mit $n$ Zahlen. Unser Ziel ist es,
ein Feld $B$ mit den \emph{Pr\"afixsummen} von $A$ zu berechnen,
d.h., es soll gelten: $B[i] = \sum_{j = 0}^i A[j]$, f\"ur 
$i = 0, \dots, n-1$.

Nehmen Sie an, Sie haben $n$ Prozesse zur Verf\"ugung, genau einen
Prozess f\"ur jedes Element von $A$. In einer \emph{Runde} kann jeder
Prozess genau zwei Elemente aus $A$ oder $B$ lesen und genau ein
Element in $A$ oder $B$ schreiben.

\begin{enumerate}
\item 
  Beschreiben Sie ein Verfahren, das $B$ berechnet und 
  dazu $O(\log n)$ Runden ben\"otigt. 
  Beweisen Sie, dass Ihr Verfahren korrekt ist.

\item Informieren Sie sich \"uber das Java-Interface 
\texttt{ExecutorService} (insbesondere die Methode 
\texttt{submit}) und verwenden Sie dieses Interface,
um Ihre Methode aus (a) zu implementieren.
\end{enumerate}

\AUFGABE{Semaphoren}{10 Punkte}

In einer Hundeschule gelten die folgenden Regeln zur Beaufsichtigung
von Welpen:
\begin{enumerate}
\item Pro Aufsichtsperson d\"urfen maximal 10 Welpen aufgenommen werden;
\item Neue Welpen d\"urfen nur angenommen werden, wenn schon gen\"ugend
  Aufsichtspersonen anwesend sind; 
\item Aufsichtspersonen d\"urfen nur gehen, wenn gen\"ugend
Aufsichtspersonen f\"ur die anwesenden Welpen verbleiben.
\end{enumerate}

Definieren Sie in Java eine Klasse \texttt{DogSchool}, welche
mit Hilfe von Java-Semaphoren Methoden zur Simulation des Kommens
und Gehens von Welpen und Aufsichtspersonen bereit stellt.
Sowohl die Welpen als auch die Aufsichtspersonen sollen 
mit Hilfe von Threads simuliert
werden.
Testen Sie Ihre Klasse, indem Sie die Hundeschule mit zuf\"alligen
Ereignissen und Wartezeiten simulieren. 
\end{description}
\end{document}
