diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/Slides1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/Slides1.thy Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,550 @@ +(*<*) +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{ + \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{ + \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{ + \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{ + \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 "\"} \alert{H $<$ L} + \item<4> avoid indefinite priority inversion + \end{itemize}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Mars Pathfinder Mission 1997} + \Large + + \begin{center} + \includegraphics[scale=0.26]{pathfinder.jpg} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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)} \ {(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{ + \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 \ {(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{ + \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{ + \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 +(*>*) \ No newline at end of file