pip: Slides/Slides1.thy@045371bde100

(*<*)
theory Slides1
imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
begin

notation (latex output)
  set ("_") and
  Cons  ("_::/_" [66,65] 65) 

ML {*
  open Printer;
  show_question_marks_default := false;
  *}

notation (latex output)
  Cons ("_::_" [78,77] 73) and
  vt ("valid'_state") and
  runing ("running") and
  birthtime ("last'_set") and
  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
  Prc ("'(_, _')") and
  holding ("holds") and
  waiting ("waits") and
  Th ("T") and
  Cs ("C") and
  readys ("ready") and
  depend ("RAG") and 
  preced ("prec") and
  cpreced ("cprec") and
  dependents ("dependants") and
  cp ("cprec") and
  holdents ("resources") and
  original_priority ("priority") and
  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

(*>*)



text_raw {*
  \renewcommand{\slidecaption}{Nanjing, P.R. China, 1 August 2012}
  \newcommand{\bl}[1]{#1}                        
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\[-3mm]
  \Large Priority Inheritance Protocol \\[-3mm] 
  \Large Proved Correct \\[0mm]
  \end{tabular}}
  
  \begin{center}
  \small Xingyuan Zhang \\
  \small \mbox{PLA University of Science and Technology} \\
  \small \mbox{Nanjing, China}
  \end{center}

  \begin{center}
  \small joint work with \\
  Christian Urban \\
  Kings College, University of London, U.K.\\
  Chunhan Wu \\
  My Ph.D. student now working for Christian\\
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\large Prioirty Inheritance Protocol (PIP)}
  \large

  \begin{itemize} 
  \item Widely used in Real-Time OSs \pause
  \item One solution of \textcolor{red}{`Priority Inversion'} \pause
  \item A flawed manual correctness proof (1990)\pause
        \begin{itemize} \large
          \item {Notations with no precise definition}
          \item {Resorts to intuitions}
        \end{itemize} \pause
  \item Formal treatments using model-checking \pause
        \begin{itemize} \large
          \item {Applicable to small size system models}
          \item { Unhelpful for human understanding } 
        \end{itemize} \pause
  \item Verification of PCP in PVS (2000)\pause
        \begin{itemize} \large
           \item {A related protocol}
           \item {Priority Ceiling Protocol}
        \end{itemize}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Our Motivation}
  \large

  \begin{itemize}
  \item Undergraduate OS course in our university \pause
        \begin{itemize}
           \item {\large Experiments using instrutional OSs }
           \item {\large PINTOS (Stanford) is chosen }
           \item {\large Core project: Implementing PIP in it}
        \end{itemize} \pause
  \item Understanding is crucial for the implemention \pause
  \item Existing literature of little help \pause
  \item Some mention the complication
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\mbox{Some excerpts}}
  
  \begin{quote}
  ``Priority inheritance is neither ef$\!$ficient nor reliable. 
  Implementations are either incomplete (and unreliable) 
  or surprisingly complex and intrusive.''
  \end{quote}\medskip

  \pause

  \begin{quote}
  ``I observed in the kernel code (to my disgust), the Linux 
  PIP implementation is a nightmare: extremely heavy weight, 
  involving maintenance of a full wait-for graph, and requiring 
  updates for a range of events, including priority changes and 
  interruptions of wait operations.''
  \end{quote}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Our Aims}
  \large

  \begin{itemize}
  \item Formal specification at appropriate abstract level,
        convenient for:
  \begin{itemize} \large
    \item Constructing interactive proofs
    \item Clarifying the underlying ideas
  \end{itemize} \pause
  \item Theorems usable to guide implementation, critical point:
    \begin{itemize} \large
      \item Understanding the relationship with real OS code \pause
      \item Not yet formalized
    \end{itemize}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}




text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Real-Time OSes}
  \large

  \begin{itemize}
  \item Purpose: gurantee the most urgent task to be processed in time
  \item Processes have priorities\\
  \item Resources can be locked and unlocked
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Problem}
  \Large

  \begin{center}
  \begin{tabular}{l}
  \alert{H}igh-priority process\\[4mm]
  \onslide<2->{\alert{M}edium-priority process}\\[4mm]
  \alert{L}ow-priority process\\[4mm]
  \end{tabular}
  \end{center}

  \onslide<3->{
  \begin{itemize}
  \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L}
  \item<4> avoid indefinite priority inversion
  \end{itemize}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Priority Inversion}

  \begin{center}
  \includegraphics[scale=0.4]{PriorityInversion.png}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Mars Pathfinder Mission 1997}
  \Large

  \begin{center}
  \includegraphics[scale=0.2]{marspath1.png}
  \includegraphics[scale=0.22]{marspath3.png}
  \includegraphics[scale=0.4]{marsrover.png}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Solution}
  \Large

  \alert{Priority Inheritance Protocol (PIP):}

  \begin{center}
  \begin{tabular}{l}
  \alert{H}igh-priority process\\[4mm]
  \textcolor{gray}{Medium-priority process}\\[4mm]
  \alert{L}ow-priority process\\[21mm]
  {\normalsize (temporarily raise its priority)}
  \end{tabular}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}




text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{A Correctness ``Proof'' in 1990}
  \Large

  \begin{itemize}
  \item a paper$^\star$ 
  in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm]
  \end{itemize}

  \normalsize
  \begin{quote}
  \ldots{}after the thread (whose priority has been raised) completes its 
  critical section and releases the lock, it ``returns to its original 
  priority level''.
  \end{quote}\bigskip

  \small
  $^\star$ in IEEE Transactions on Computers
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{}
  \Large

  \begin{center}
  \begin{tabular}{l}
  \alert{H}igh-priority process 1\\[2mm]
  \alert{H}igh-priority process 2\\[8mm]
  \alert{L}ow-priority process
  \end{tabular}
  \end{center}

  \onslide<2->{
  \begin{itemize}
  \item Solution: \\Return to highest \alert{remaining} priority
  \end{itemize}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Event Abstraction}

  \begin{itemize}\large
     \item Use Inductive Approach of L. Paulson \pause
     \item System is event-driven \pause
     \item A \alert{state} is a list of events 
  \end{itemize}

  \pause

  \begin{center}
  \includegraphics[scale=0.4]{EventAbstract.png}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Events}
  \Large

  \begin{center}
  \begin{tabular}{l}
  Create \textcolor{gray}{thread priority}\\
  Exit \textcolor{gray}{thread}\\
  Set \textcolor{gray}{thread priority}\\
  Lock \textcolor{gray}{thread cs}\\
  Unlock \textcolor{gray}{thread cs}\\
  \end{tabular}
  \end{center}\medskip

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Precedences}
  \large

  \begin{center}
  \begin{tabular}{l}
  @{thm preced_def[where thread="th"]} 
  \end{tabular}
  \end{center}

  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{RAGs}

\begin{center}
  \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
  \begin{tikzpicture}[scale=1]
  %%\draw[step=2mm] (-3,2) grid (1,-1);

  \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
  \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};

  \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);
  \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);
  \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);
  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);
  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);
  \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);
  \end{tikzpicture}
  \end{center}\bigskip

  \begin{center}
  \begin{minipage}{0.8\linewidth}
  \raggedleft
  @{thm cs_depend_def}
  \end{minipage}
  \end{center}\pause

  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Good Next Events}
  %%\large

  \begin{center}
  @{thm[mode=Rule] thread_create[where thread=th]}\bigskip

  @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip

  @{thm[mode=Rule] thread_set[where thread=th]}
  \end{center}

  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Good Next Events}
  %%\large

  \begin{center}
  @{thm[mode=Rule] thread_P[where thread=th]}\bigskip
  
  @{thm[mode=Rule] thread_V[where thread=th]}\bigskip
  \end{center}

  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}
(*<*)
context extend_highest_gen
begin
(*>*)
text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\mbox{\large Theorem: ``No indefinite priority inversion''}}

  \pause

  Theorem $^\star$: If th is the thread with the highest precedence in state 
  @{text "s"}: \pause
  \begin{center}
  \textcolor{red}{@{thm highest})}
  \end{center}
  \pause
  and @{text "th"} is blocked by a thread @{text "th'"} in 
  a future state @{text "s'"} (with @{text "s' = t@s"}): \pause
  \begin{center}
  \textcolor{red}{@{text "th' \<in> running (t@s)"} and @{text "th' \<noteq> th"}} \pause
  \end{center}
  \fbox{ \hspace{1em} \pause
  \begin{minipage}{0.95\textwidth}
  \begin{itemize}
  \item @{text "th'"} did not hold or wait for a resource in s:
  \begin{center}
  \textcolor{red}{@{text "\<not>detached s th'"}}  
  \end{center} \pause
  \item @{text "th'"} is running with the precedence of @{text "th"}:
  \begin{center}
  \textcolor{red}{@{text "cp (t@s) th' = preced th s"}} 
  \end{center} 
  \end{itemize}
  \end{minipage}}
  \pause
  \small
  $^\star$ modulo some further assumptions\bigskip\pause
  It does not matter which process gets a released lock.

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{Implementation}
  
  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip

  When @{text "e"} = \alert{Create th prio}, \alert{Exit th} 
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s"}
  \item No precedence needs to be recomputed
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{Implementation}

  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
  

  When @{text "e"} = \alert{Set th prio}
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s"}
  \item No precedence needs to be recomputed
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{Implementation}

  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip

  When @{text "e"} = \alert{Unlock th cs} where there is a thread to take over
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"}
  \item we have to recalculate the precedence of the direct descendants
  \end{itemize}\bigskip

  \pause

  When @{text "e"} =  \alert{Unlock th cs} where no thread takes over
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s - {(C cs, T th)}"}
  \item no recalculation of precedences
  \end{itemize}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{Implementation}

  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip

  When @{text "e"} = \alert{Lock th cs} where cs is not locked
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"}
  \item no recalculation of precedences
  \end{itemize}\bigskip

  \pause

  When @{text "e"} = \alert{Lock th cs} where cs is locked
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s - {(T th, C cs)}"}
  \item we have to recalculate the precedence of the descendants
  \end{itemize}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Conclusion}
  
  \begin{itemize} \large
  \item Aims fulfilled \medskip \pause
  \item Alternative way \pause
       \begin{itemize} 
           \item using Isabelle/HOL in OS code development \medskip
           \item through the Inductive Approach
       \end{itemize} \pause
  \item Future research \pause
       \begin{itemize}
           \item scheduler in RT-Linux\medskip
           \item multiprocessor case\medskip
           \item other ``nails'' ? (networks, \ldots) \medskip \pause
           \item Refinement to real code and relation between implementations
        \end{itemize}
  \end{itemize}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Questions?}
  
  \begin{itemize} \large
  \item Thank you for listening!
  \end{itemize}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


(*<*)
end
end
(*>*)
author	Christian Urban <urbanc@in.tum.de>
	Fri, 05 May 2017 14:26:00 +0100 (2017-05-05)
changeset 167	045371bde100
parent 4	9d667d545e32
permissions	-rw-r--r--