\documentclass{seminar}

\include{macros}
\include{pmacros}

\begin{document}

% -------------------------------------------------- %

\begin{slide}
\stitle{CS156}{Topics}
\begin{itemize}
\item Verification of \emph{sequential} programs.
  \begin{itemize}
  \item No concurrency.
  \item Programs (should) always terminate.
  \item Observable at start (input) and end (output) of execution.
  \end{itemize}
\item Logical foundations:
  \begin{itemize}
  \item FOL.
  \item Invariants and ranking functions.
  \item Verification conditions.
  \item Decision procedures.
  \item Invariant generation.
  \item Induction.
  \end{itemize}
\end{itemize}

\vspace*{\fill}
\end{slide}

% -------------------------------------------------- %

\begin{slide}
\stitle{CS256}{Topics}
\begin{itemize}
\item Verification of \emph{reactive systems}.
  \begin{itemize}
  \item Highly concurrent. \\ 
    Concept of \emph{fairness}. \\
    Properties: \emph{mutual exclusion}, \emph{freedom from deadlock}.
  \item Programs need not terminate (\eg, OS, web server). \\
    But some components must terminate (\eg, IO handler).
  \item Observable throughout execution. \\
    And the environment affects execution.
  \end{itemize}
\item Logical foundations: Everything from CS156 {\it plus}
  \begin{itemize}
  \item \emph{temporal logics} \\
    linear (LTL), branching (CTL), alternating (ATL) time
  \item \emph{automata theory} and connection with temporal logics \\
    infinite strings (linear) and trees (branching, alternating)
  \end{itemize}
\end{itemize}

\vspace*{\fill}
\end{slide}

% -------------------------------------------------- %

\begin{slide}
\stitles{\sc prime}
\renewcommand{\arraystretch}{.9}
\[
\begin{array}{l} 
{\bf local}\ y:\ \hbox{\bf integer where}\ y=1 \\
\ell_0\colon\ \mbox{\bf loop forever do}  \\
\ \ \ \ \ \ \  \left[
\begin{array}{l}
\vdots\\
\ell_5:\,\hbox{\bf print}\ y\\
\ell_6:\,\\
\vdots\\
\ell_{10}:\, y \leftarrow y+1 \\
\vdots\\
\end{array} \right]
\end{array}
\]
Output: 2,3,5,7,11,13, $\ldots$
\newcommand{\atl}[1]{\*at\_\ell_{#1}}
\begin{itemize}
\item only primes: ~~~
$
\Box[ \atl{5} \rightarrow \mbox{prime}(y) ]
$
\item all primes: ~~~~~
$
\forall u\ (\mbox{prime}(u)\ \rightarrow\ \Diamond
                [\atl{5} \wedge y=u ])
$
\item monotonicity (correct order):
\[
\forall u\ [(\atl{6} \wedge y=u)\
        \rightarrow\
\Box(\atl{5} \rightarrow y>u)]
\]
\end{itemize}

\vspace*{\fill}
\end{slide}

% -------------------------------------------------- %

\begin{slide}
\stitles{\sc bakery[2]}

    \renewcommand{\arraystretch}{.9}
    \begin{program}
    \begin{tabular}{@{}lll@{}}
        \LOCAL & ${y_1}, {y_2}$
                                & : \INTEGER \WHERE ${y_1} = 0, 
                                                {y_2} = 0$
    \end{tabular} \\
    \\
    \begin{block}{P_1::}
       \LOOP \FOREVER \DO \\
            \begin{block}{}
            \Ll {\NONCRITICAL} \\
            \Ll {y_1} := {y_2}+1 \\
            \Ll \AWAIT {y_2}=0 \vee {y_1} \leq {y_2} \\
            \Ll {\CRITICAL} \\
            \Ll {y_1} := 0
            \end{block}
    \end{block} \\
    \ || \\
    \begin{block}{P_2::}
       \LOOP \FOREVER \DO \\
            \begin{block}{}
            \Lm {\NONCRITICAL} \\
            \Lm {y_2} := {y_1}+1 \\
            \Lm \AWAIT {y_1}=0 \vee {y_2}< {y_1} \\
            \Lm {\CRITICAL} \\
            \Lm {y_2} := 0
            \end{block}
    \end{block}
    \end{program}

\vspace*{\fill}
\end{slide}

% -------------------------------------------------- %

\newcommand\Sat[2]{\mbox{$#1_{#2}$}}
\newcommand\AND{\wedge}
\newcommand{\AImplies}{\mathop{\mbox{$\,\Rightarrow\,$}}}
\newcommand{\Awaits}{\mbox{$\:\cal W\:$}}

\begin{slide}
\stitles{Requirements for {\sc bakery[2]}}
\begin{itemize}

\item Mutual exclusion
\[
{\fbox{$\Box\neg(\Sat{\ell}{3} \ \AND \ \Sat{m}{3})$}}
\]
{The two processes are not in the critical section simultaneously.}

\item One-bounded overtaking
\[
{\fbox{$        \Sat{\ell}{2} \ \AImplies \ 
                \neg \Sat{m}{3} \Awaits
                   \Sat{m}{3} \Awaits
                        \neg \Sat{m}{3} \Awaits \Sat{\ell}{3}$}}
\]
{Once $P_1$ waits to get access, $P_2$ can enter its critical 
section at most once.}

\item Progress
\[
{\fbox{$\Sat{\ell}{1} \ \AImplies \Diamond \Sat{\ell}{3}$}}
\]
{Once $P_1$ shows interest in entering its critical section, it
eventually gets access to the critical section.}
\end{itemize}

\vspace*{\fill}
\end{slide}

% -------------------------------------------------- %

\begin{slide}
\stitle{CS256}{Administration}
\begin{itemize}

\item TTh 11:00-12:15, Gates B12

\item Instructor: Zohar Manna \\
  TA: Matteo Slanina

\item Text:
\begin{center}
{\it The Temporal Verification of Reactive Systems: Safety} \\
Zohar Manna and Amir Pnueli
\end{center}

\item Prerequisites: CS103, CS156, or equivalent background
\end{itemize}

\vspace*{\fill}
\end{slide}

% -------------------------------------------------- %

\end{document}
