# HG changeset patch # User zhang # Date 1344607061 0 # Node ID e089ed1c3e2669bf2a193d16bcafe747ed916d5b # Parent 484c7b83f25145ceec28e4936e8e5c686b57a7d8 Slides modified diff -r 484c7b83f251 -r e089ed1c3e26 prio/Slides/Slides1.thy --- a/prio/Slides/Slides1.thy Fri Aug 10 13:54:21 2012 +0000 +++ b/prio/Slides/Slides1.thy Fri Aug 10 13:57:41 2012 +0000 @@ -45,22 +45,58 @@ \begin{frame} \frametitle{% \begin{tabular}{@ {}c@ {}} - \\[8mm] - \Large A Provably Correct Implementation\\[-3mm] - \Large of the Priority Inheritance Protocol\\[0mm] + \\[-3mm] + \Large Priority Inheritance Protocol \\[-3mm] + \Large Proved Correct \\[0mm] \end{tabular}} \begin{center} - \small Christian Urban\\ + \small Xingyuan Zhang \\ + \small \mbox{PLA University of Science and Technology} \\ + \small \mbox{Nanjing, China} \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} + \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{ + \begin{frame}[c] + \frametitle{\large Prioirty Inheritance Protocol (PIP)} + \large + + \begin{itemize} \large + \item Widely used in Real-Time OSs \pause + \item One solution of \textcolor{red}{`Priority Inversion'} problem \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}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -68,25 +104,83 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{Isabelle Theorem Prover} - My background: + \frametitle{Our Motivation} + \large \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) + \item Undergraduate OS course in our university \pause + \begin{itemize} + \item {\large Experiments using intrutional OSs } + \item {\large PINTOS (Stanford) is choosen } + \item {\large Core project: Implementing PIP in it} + \end{itemize} \pause + \item Understanding is crucial to implemention \pause + \item Little help was found in the literature \pause + \item Some mentioning the complication \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{\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{ + \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{ @@ -95,7 +189,8 @@ \large \begin{itemize} - \item Processes have priorities\\[5mm] + \item Purpose: gurantee the most urgent task be processed in time + \item Processes have priorities\\ \item Resources can be locked and unlocked \end{itemize} @@ -104,6 +199,7 @@ *} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -130,6 +226,23 @@ *} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Priority Inversion} + + \begin{center} + \includegraphics[scale=0.4]{PriorityInversion.png} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -138,7 +251,9 @@ \Large \begin{center} - \includegraphics[scale=0.26]{pathfinder.jpg} + \includegraphics[scale=0.2]{marspath1.png} + \includegraphics[scale=0.22]{marspath3.png} + \includegraphics[scale=0.4]{marsrover.png} \end{center} \end{frame}} @@ -168,29 +283,6 @@ *} -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 {* @@ -244,6 +336,29 @@ text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Event Abstraction} + + \begin{itemize}\large + \item Use Inductive Approch 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.45]{EventAbstract.png} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] @@ -258,10 +373,7 @@ 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{center}\medskip \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -276,7 +388,7 @@ \begin{center} \begin{tabular}{l} - @{thm preced_def[where thread="th"]} + @{thm preced_def[where thread="th"]} \end{tabular} \end{center} @@ -368,26 +480,43 @@ \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} - +(*<*) +context extend_highest_gen +begin +(*>*) text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{Theorem} - - \textcolor{gray}{``No indefinite priority inversion''}\bigskip + \frametitle{\mbox{\large Theorem: ``No indefinite priority inversion''}} - 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 + \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' \ running (t@s)"} and @{text "th' \ th"}} \pause + \end{center} + \fbox{ \hspace{1em} \pause + \begin{minipage}{0.95\textwidth} \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 + \item @{text "th'"} did not hold or wait for a resource in s: + \begin{center} + \textcolor{red}{@{text "\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 @@ -403,13 +532,13 @@ \begin{frame}[t] \frametitle{Implementation} - s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip + s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip - \alert{Create th prio}, \alert{Exit th} + When @{text "e"} = \alert{Create th prio}, \alert{Exit th} \begin{itemize} \item @{text "RAG s' = RAG s"} - \item precedences of descendants stay all the same + \item No precedence needs to recalculate \end{itemize} \end{frame}} @@ -421,14 +550,15 @@ \mode{ \begin{frame}[t] \frametitle{Implementation} + + s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip - s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip - \alert{Set th prio} + When @{text "e"} = \alert{Set th prio} \begin{itemize} \item @{text "RAG s' = RAG s"} - \item we have to recalculate the precedence of the direct descendants + \item No precedence needs to recalculate \end{itemize} \end{frame}} @@ -440,17 +570,19 @@ \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 + 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)} \ {(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 + \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)}"} @@ -467,17 +599,19 @@ \mode{ \begin{frame}[t] \frametitle{Implementation} - - s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip - \alert{Lock th cs} where cs is not locked + 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 \ {(C cs, T th')}"} \item no recalculation of precedences \end{itemize}\bigskip - \alert{Lock th cs} where cs is locked + \pause + + When @{text "e"} = \alert{Lock th cs} where cs is locked \begin{itemize} \item @{text "RAG s' = RAG s - {(T th, C cs)}"} @@ -489,35 +623,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} -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 {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -525,26 +630,27 @@ \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) + \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 researches \pause + \begin{itemize} \large + \item scheduler in RT-Linux\medskip + \item multiprocessor case\medskip + \item other ``nails'' ? (networks, \ldots) \pause + \item Refinement to real code and relation between implemenations + \end{itemize} \end{itemize} - - \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} + (*<*) end +end (*>*) \ No newline at end of file