(*<*)
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}{London, 28 June 2012}
  \newcommand{\bl}[1]{#1}                        
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\[8mm]
  \Large A Provably Correct Implementation\\[-3mm] 
  \Large of the Priority Inheritance Protocol\\[0mm]
  \end{tabular}}
  
  \begin{center}
  \small Christian Urban\\
  \end{center}

  \begin{center}
  \small joint work with Xingyuan Zhang and Chunhan Wu\medskip \\
  \small \mbox{from the PLA University of Science and Technology in Nanjing}
  \end{center}

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

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Isabelle Theorem Prover}
  My background:

  \begin{itemize}
  \item mechanical reasoning about languages with binders (Nominal)\medskip
  \item Barendregt's variable convention can lead to \alert{false}\medskip
  \item found a bug in a proof by Bob Harper and Frank Pfenning (CMU) on
  LF (ACM TOCL, 2005)
  \end{itemize}

  \begin{textblock}{6}(6.5,12.5)
  \includegraphics[scale=0.28]{isabelle1.png}
  \end{textblock}

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

*}

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

  \begin{itemize}
  \item Processes have priorities\\[5mm]
  \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{Mars Pathfinder Mission 1997}
  \Large

  \begin{center}
  \includegraphics[scale=0.26]{pathfinder.jpg}
  \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{\mbox{}}
  
  \begin{quote}
  ``Priority inheritance is neither ef$\!$ficient nor reliable. 
  Implementations are either incomplete (and unreliable) 
  or surprisingly complex and intrusive.''
  \end{quote}\medskip

  \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{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{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}\pause\medskip

  \large
  A \alert{state} is a list of events (that happened so far).

  \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}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Theorem}
  
  \textcolor{gray}{``No indefinite priority inversion''}\bigskip

  Theorem:$^\star$ If th is the thread with the highest precedence in state s,
  then in every future state @{text "s'"} in which th is still
  alive\smallskip


  \begin{itemize}
  \item th is blocked by a thread @{text "th'"} that was alive in s 
  \item @{text "th'"} held a resource in s, and
  \item @{text "th'"} is running with the precedence of th.\bigskip
  \end{itemize}

  \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\bigskip\bigskip

  \alert{Create th prio}, \alert{Exit th} 
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s"}
  \item precedences of descendants stay all the same
  \end{itemize}

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

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

  \alert{Set th prio}
  
  \begin{itemize}
  \item @{text "RAG s' = RAG s"}
  \item we have to recalculate the precedence of the direct descendants
  \end{itemize}

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

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

  \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

  \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\bigskip\bigskip

  \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

  \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{PINTOS}

  \begin{itemize}
  \item \ldots{}small operating system developed at Stanford for teaching;
  written in C\bigskip 
  \end{itemize}
  
  \begin{center}
  \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
  \hline
  {\bf Event} & {\bf PINTOS function} \\
  \hline
  @{text Create} & @{text "thread_create"}\\
  @{text Exit}   & @{text "thread_exit"}\\
  @{text Set}    & @{text "thread_set_priority"}\\
  @{text Lock}   & @{text "lock_acquire"}\\
  @{text Unlock} & @{text "lock_release"}\\ 
  \hline
  \end{tabular}
  \end{center}


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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Conclusion}
  
  \begin{itemize}
  \item surprised how pleasant the experience was\medskip

  \item no real specification existed for PIP\medskip

  \item general technique (a ``hammer''):\\[2mm]
  events, separation of good and bad configurations\medskip

  \item scheduler in RT-Linux\medskip

  \item multiprocessor case\medskip

  \item other ``nails'' ? (networks, \ldots)
  \end{itemize}


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

(*<*)
end
(*>*)