diff -r 000000000000 -r 110247f9d47e Slides/Slides1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/Slides1.thy Thu Dec 06 15:11:21 2012 +0000 @@ -0,0 +1,669 @@ +(*<*) +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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{Priority Inversion} + + \begin{center} + \includegraphics[scale=0.4]{PriorityInversion.png} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ + \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{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{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{ + \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{ + \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}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} +(*<*) +context extend_highest_gen +begin +(*>*) +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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' \ running (t@s)"} and @{text "th' \ 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 "\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{ + \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{ + \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{ + \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)} \ {(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{ + \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 \ {(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{ + \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{ + \begin{frame}[c] + \frametitle{Questions?} + + \begin{itemize} \large + \item Thank you for listening! + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +(*<*) +end +end +(*>*) \ No newline at end of file