41   \renewcommand{\slidecaption}{Nanjing, P.R. China, 1 August 2012}

    43   \renewcommand{\slidecaption}{Leicester, 7 December 2012}

    49   \Large Priority Inheritance Protocol \\[-3mm] 

    51   \LARGE A Provably Correct\\[-1mm] 

    50   \Large Proved Correct \\[0mm]

    52   \LARGE Priority Inheritance Protocol\\[-3mm] 

    54   \small Xingyuan Zhang \\

    56    Christian Urban\\

    55   \small \mbox{PLA University of Science and Technology} \\

    57   \small King's College London

    56   \small \mbox{Nanjing, China}

    58   \end{center}\bigskip

    57   \end{center}

    59  

    58 

    60   \begin{center}

    59   \begin{center}

    61   \small joint work with Xingyuan Zhang and Chunhan Wu from the PLA

    60   \small joint work with \\

    62   University of Science and Technology in Nanjing

    61   Christian Urban \\

    63   \end{center}

    62   Kings College, University of London, U.K.\\

    64 

    63   Chunhan Wu \\

    65   \end{frame}}

    64   My Ph.D. student now working for Christian\\

    66   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    65   \end{center}

    67 *}

    66 

    68 

    67   \end{frame}}

    69 text_raw {*

    68   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    70   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    69 *}

    71   \mode<presentation>{

    70 

    72   \begin{frame}[c]

    71 text_raw {*

    73   \frametitle{Interactive Theorem Proving}

    72   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    74 

    73   \mode<presentation>{

    75   \begin{center}

    74   \begin{frame}[c]

    76   \includegraphics[scale=0.23]{isabelle.png}

    75   \frametitle{\large Prioirty Inheritance Protocol (PIP)}

    77   \end{center}  

    76   \large

    78 

    77 

    79   \only<2>{

    78   \begin{itemize} 

    80   \begin{textblock}{12}(2,13.6)

    79   \item Widely used in Real-Time OSs \pause

    81   \begin{tikzpicture}

    80   \item One solution of \textcolor{red}{`Priority Inversion'} \pause

    82   \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

    81   \item A flawed manual correctness proof (1990)\pause

    83   {\normalsize\color{darkgray}

    82         \begin{itemize} \large

    84   \begin{minipage}{10cm}\raggedright

    83           \item {Notations with no precise definition}

    85   \ldots more often than not, thinking is only Plan B

    84           \item {Resorts to intuitions}

    86 

    85         \end{itemize} \pause

    87   \end{minipage}};

    86   \item Formal treatments using model-checking \pause

    88   \end{tikzpicture}

    87         \begin{itemize} \large

    89   \end{textblock}}

    88           \item {Applicable to small size system models}

    90 

    89           \item { Unhelpful for human understanding } 

    91 

    90         \end{itemize} \pause

    92   \end{frame}}

    91   \item Verification of PCP in PVS (2000)\pause

    93   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    92         \begin{itemize} \large

    94 

    93            \item {A related protocol}

    95 *}

    94            \item {Priority Ceiling Protocol}

    96 

    95         \end{itemize}

    97 text_raw {*

    96   \end{itemize}

    98   \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

    97 

    99   \tikzstyle{node1}=[rectangle, minimum size=8mm, rounded corners=3mm, very thick, 

    98   \end{frame}}

   100                      draw=black!50, top color=white, bottom color=black!20]

    99   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   101   \tikzstyle{node2}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   100 

   102                      draw=red!70, top color=white, bottom color=red!50!black!20]

   101 *}

   103   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   102 

   104   \mode<presentation>{

   103 text_raw {*

   105   \begin{frame}[c]

   104   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   106   \frametitle{}

   105   \mode<presentation>{

   107 

   106   \begin{frame}[c]

   108   \begin{tabular}{@ {}c@ {\hspace{2mm}}c}

   107   \frametitle{Our Motivation}

   109   \\[6mm]

   108   \large

   110   \begin{tabular}{c}

   109 

   111   \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

   110   \begin{itemize}

   112   {\footnotesize Bob Harper}\\[-2.5mm]

   111   \item Undergraduate OS course in our university \pause

   113   {\footnotesize (CMU)}

   112         \begin{itemize}

   114   \end{tabular}

   113            \item {\large Experiments using instrutional OSs }

   115   \begin{tabular}{c@ {}}

   114            \item {\large PINTOS (Stanford) is chosen }

   116   \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

   115            \item {\large Core project: Implementing PIP in it}

   117   {\footnotesize Frank Pfenning}\\[-2.5mm]

   116         \end{itemize} \pause

   118   {\footnotesize (CMU)}

   117   \item Understanding is crucial for the implemention \pause

   119   \end{tabular} &

   118   \item Existing literature of little help \pause

   120 

   119   \item Some mention the complication

   121   \begin{tabular}{@ {\hspace{-3mm}}p{7cm}}

   120   \end{itemize}

   122   \begin{tikzpicture}[remember picture, scale=0.5]

   121 

   123   \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

   122   \end{frame}}

   124   { \& \& \node (desc) {\makebox[0mm]{\begin{tabular}{l}published in a journal\\ 

   123   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   125     \small (ACM ToCL, 31 pages, 2005)\\[3mm]\end{tabular}}};\\

   124 

   126     \&[-10mm] 

   125 *}

   127     \node (def1)   [node1] {\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

   126 

   128     \node (proof1) [node1] {Proof}; \&

   127 

   129     \node (alg1)   [node1] {\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

   128 text_raw {*

   130   };

   129   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   131   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   130   \mode<presentation>{

   132   \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

   131   \begin{frame}[c]

   133   \draw[<-,black,line width=0.5mm] (proof1) -- (desc);

   132   \frametitle{\mbox{Some excerpts}}

   134   \end{tikzpicture}

   133   

   135   \end{tabular}\\

   134   \begin{quote}

   135   ``Priority inheritance is neither ef$\!$ficient nor reliable. 

   136   Implementations are either incomplete (and unreliable) 

   137   or surprisingly complex and intrusive.''

   138   \end{quote}\medskip

   141 

   138   \\[0mm]

   142   \begin{quote}

   139   

   143   ``I observed in the kernel code (to my disgust), the Linux 

   140   \multicolumn{2}{c}{

   144   PIP implementation is a nightmare: extremely heavy weight, 

   141   \begin{tabular}{p{6cm}}

   145   involving maintenance of a full wait-for graph, and requiring 

   142   \raggedright

   146   updates for a range of events, including priority changes and 

   143   \color{black}{relied on their proof in a\\ {\bf security} critical application}

   147   interruptions of wait operations.''

   144   \end{tabular}

   148   \end{quote}

   145   

   149 

   146   \begin{tabular}{c}

   150   \end{frame}}

   147   \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

   151   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   148   {\footnotesize Andrew Appel}\\[-2.5mm]

   152 *}

   149   {\footnotesize (Princeton)}

   153 

   150   \end{tabular}}

   154 

   151   \end{tabular} 

   155 text_raw {*

   152 

   156   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   153   \end{frame}}

   157   \mode<presentation>{

   154   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   158   \begin{frame}[c]

   155 

   159   \frametitle{Our Aims}

   156 *}

   160   \large

   157 

   161 

   158 text_raw {*

   162   \begin{itemize}

   159   \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

   163   \item Formal specification at appropriate abstract level,

   160   \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   164         convenient for:

   161                      draw=black!50, top color=white, bottom color=black!20]

   165   \begin{itemize} \large

   162   \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   166     \item Constructing interactive proofs

   163                      draw=red!70, top color=white, bottom color=red!50!black!20]

   167     \item Clarifying the underlying ideas

   164   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   168   \end{itemize} \pause

   165   \mode<presentation>{

   169   \item Theorems usable to guide implementation, critical point:

   166   \begin{frame}<2->[squeeze]

   170     \begin{itemize} \large

   167   \frametitle{} 

   171       \item Understanding the relationship with real OS code \pause

   168   

   172       \item Not yet formalized

   169   \begin{columns}

   173     \end{itemize}

   170   

   174   \end{itemize}

   171   \begin{column}{0.8\textwidth}

   175 

   172   \begin{textblock}{0}(1,2)

   176   \end{frame}}

   173 

   177   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   174   \begin{tikzpicture}

   178 

   175   \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

   179 *}

   176   { \&[-10mm] 

   180 

   177     \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

   178     \node (proof1) [node1] {\large Proof}; \&

   179     \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

   180     

   181     \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   182     \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

   183     \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

   184     \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   185      

   186     \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   187     \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   188     \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

   189     \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

   190 

   191     \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   192     \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   193     \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

   194     \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   195   };

   196 

   197   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   198   \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

   199   

   200   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}

   201   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

   202 

   203   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}

   204   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}

   205   

   206   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}

   207   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

   208 

   209   \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 

   210   \end{tikzpicture}

   211 

   212   \end{textblock}

   213   \end{column}

   214   \end{columns}

   215 

   216 

   217   \begin{textblock}{3}(12,3.6)

   218   \onslide<4->{

   219   \begin{tikzpicture}

   220   \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

   221   \end{tikzpicture}}

   222   \end{textblock}

   223 

   224   \end{frame}}

   225   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   226 *}

   192   \item Purpose: gurantee the most urgent task to be processed in time

   238   \item Purpose of a general OS:\\ 

   193   \item Processes have priorities\\

   239   give access to various resources\\

   194   \item Resources can be locked and unlocked

   240   $\Rightarrow$ access needs to be moderated by\\ 

   195   \end{itemize}

   241   $\phantom{\Rightarrow}$ locking and unlocking\medskip \\

   196 

   242 

   197   \end{frame}}

   243   \item Purpose of a real-time OS:\\

   198   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   244   gurantee tasks to be completed in time\medskip\pause

   199 

   245 

   200 *}

   246   \item \alert{this already results into a surprisingly non-trivial scheduling problem}

   201 

   247   \end{itemize}

   202 

   248 

   203 text_raw {*

   249   \end{frame}}

   204   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   250   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   205   \mode<presentation>{

   251 

   206   \begin{frame}[c]

   252 *}

   207   \frametitle{Problem}

   253 

   254 

   255 text_raw {*

   256   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   257   \mode<presentation>{

   258   \begin{frame}[c]

   259   \frametitle{The Problem}

   212   \alert{H}igh-priority process\\[4mm]

   264   \alert{H}igh-priority process (waits)\\[4mm]

   214   \alert{L}ow-priority process\\[4mm]

   266   \alert{L}ow-priority process (has a lock)\\[4mm]

   220   \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L}

   272   \item \alert{priority inversion}\\ \hspace{2cm}@{text "\<equiv>"} H waits for a process\\ 

   221   \item<4> avoid indefinite priority inversion

   273   \mbox{}\hfill with lower priority

   274   \item<4> avoid \alert{indefinite} priority inversion

   253   \begin{center}

   312   \alert{Priority Inheritance Protocol (PIP):}\bigskip

   254   \includegraphics[scale=0.2]{marspath1.png}

   255   \includegraphics[scale=0.22]{marspath3.png}

   256   \includegraphics[scale=0.4]{marsrover.png}

   257   \end{center}

   258 

   259   \end{frame}}

   260   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   261 *}

   262 

   263 text_raw {*

   264   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   265   \mode<presentation>{

   266   \begin{frame}[c]

   267   \frametitle{Solution}

   268   \Large

   269 

   270   \alert{Priority Inheritance Protocol (PIP):}

   276   \alert{L}ow-priority process\\[21mm]

   318   \alert{L}ow-priority process\\[15mm]

   277   {\normalsize (temporarily raise its priority)}

   319   {\normalsize (temporarily raise the priority of \alert{L})}

   278   \end{tabular}

   320   \end{tabular}

   279   \end{center}

   321   \end{center}

   280 

   322 

   281   \end{frame}}

   323   \end{frame}}

   282   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   324   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   283 *}

   325 *}

   284 

   326 

   285 

   327 

   286 

   328 

   287 

   329 

   288 text_raw {*

   330 text_raw {*

   289   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   331   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   290   \mode<presentation>{

   332   \mode<presentation>{

   291   \begin{frame}[c]

   333   \begin{frame}[c]

   292   \frametitle{A Correctness ``Proof'' in 1990}

   334   \frametitle{A First Correctness ``Proof''}

   296   \item a paper$^\star$ 

   338   \item the paper$^\star$ first describing  PIP ``proved'' also its 

   297   in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm]

   339   correctness:\\[5mm]

   308   $^\star$ in IEEE Transactions on Computers

   350   $^\star$ in IEEE Transactions on Computers in 1990 by Sha et al.

   322   \alert{H}igh-priority process 1\\[2mm]

   364   \alert{H}igh-priority process 1 (waits)\\[2mm]

   323   \alert{H}igh-priority process 2\\[8mm]

   365   \alert{H}igh-priority process 2 (waits)\\[8mm]

   324   \alert{L}ow-priority process

   366   \alert{L}ow-priority process (has a lock)

   330   \item Solution: \\Return to highest \alert{remaining} priority

   372   \item Solution: return to the highest

   373   \phantom{Solution:} \alert{remaining} priority\\

   337 

   380 text_raw {*

   338 text_raw {*

   381   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   339   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   382   \mode<presentation>{

   340   \mode<presentation>{

   383   \begin{frame}[c]

   341   \begin{frame}[c]

   384   \frametitle{Specification}

   342   \frametitle{Event Abstraction}

   343 

   344   \begin{itemize}\large

   345      \item Use Inductive Approach of L. Paulson \pause

   346      \item System is event-driven \pause

   347      \item A \alert{state} is a list of events 

   348   \end{itemize}

   349 

   350   \pause

   351 

   352   \begin{center}

   353   \includegraphics[scale=0.4]{EventAbstract.png}

   354   \end{center}

   355 

   356   \end{frame}}

   357   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   358 

   359 *}

   360 

   361 text_raw {*

   362   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   363   \mode<presentation>{

   364   \begin{frame}[c]

   365   \frametitle{Events}

   386   \frametitle{Precedences}

   409   \frametitle{Scheduling States}

   387   \large

   410   \Large

   388 

   411   

   389   \begin{center}

   412   \begin{itemize}

   390   \begin{tabular}{l}

   413   \item A \alert{state} is a list of event\bigskip

   391   @{thm preced_def[where thread="th"]} 

   414   \begin{center}

   392   \end{tabular}

   415   \begin{tikzpicture}

   393   \end{center}

   416   \draw [->, line width=1.5mm] (-4,0) -- (4, 0);

   394 

   417   \draw [line width=0.8mm] (-4, 0.3) -- (-4, -0.3);

   395   

   418   \draw [line width=0.8mm] (1, 0.3) -- (1, -0.3);

   396 

   419   \node at (1,-0.7) {\large s};

   397   \end{frame}}

   420   \node at (-4,-0.7) {\large 0};

   398   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   421   \node at (3.2,-0.7) {\large time};

   399 *}

   422   \end{tikzpicture}

   400 

   423   \end{center}\pause

   401 

   424 

   402 text_raw {*

   425   \item Scheduling according to \alert{precedences}:

   403   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   426   \begin{center}

   404   \mode<presentation>{

   427   \begin{tabular}{@ {}l@ {}}

   405   \begin{frame}[c]

   428   \large @{thm preced_def[where thread="th"]} 

   406   \frametitle{RAGs}

   429   \end{tabular}

   430   \end{center}

   431   \end{itemize}

   432 

   433   \end{frame}}

   434   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   435 *}

   436 

   437 

   438 text_raw {*

   439   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   440   \mode<presentation>{

   441   \begin{frame}[c]

   442   \frametitle{Waiting Queues}

   443   \large

   444 

   445   \begin{itemize}

   446   \item A \alert{waiting queue} function returns a list of threads

   447   associated with every resource

   448   \item The head of the list is the thread holding the resource.

   449   \medskip

   450 

   451   \begin{center}\normalsize

   452   \begin{tabular}{@ {}l}

   453   @{thm cs_holding_def[where thread="th"]}\\

   454   @{thm cs_waiting_def[where thread="th"]}

   455   \end{tabular}

   456   \end{center}

   457   \end{itemize}

   458 

   459   \end{frame}}

   460   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   461 *}

   462 

   463 

   464 text_raw {*

   465   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   466   \mode<presentation>{

   467   \begin{frame}[c]

   468   \frametitle{Resource Allocation Graphs}

   411   %%\draw[step=2mm] (-3,2) grid (1,-1);

   473   

   412 

   418   \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};

   479   \node (E1) at (6, 0.3) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};

   421   \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);

   482   \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds}  (B);

   422   \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);

   483   \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waits}  (B);

   423   \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);

   484   \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waits}  (B);

   424   \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);

   485   \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holds}  (E);

   425   \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);

   486   \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds}  (E1);

   426   \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);

   487   \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waits}  (E);

   435   \end{center}\pause

   504   \end{center}

   436 

   505 

   437   

   506   

   438 

   507 

   439   \end{frame}}

   508   \end{frame}}

   440   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   509   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   441 

   510 *}

   442 *}

   511 

   443 

   512 

   444 text_raw {*

   513 text_raw {*

   445   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   514   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   446   \mode<presentation>{

   515   \mode<presentation>{

   447   \begin{frame}[c]

   516   \begin{frame}[c]

   448   \frametitle{Good Next Events}

   517   \frametitle{The Scheduler}

   518   \large

   519 

   520   \begin{itemize}

   521   \item \underline{Start}: all priorities/precedences are 0, all resources are unlocked

   522   \item \underline{Create th p}: set precedence of th

   523   \item \underline{Exit th}: reset precedence to 0

   524   \item \underline{Set th p}: reset precedence of th

   525   \item \underline{Lock th cs}: add th to the end of the waiting queue of cs

   526   \item \underline{Unlock th cs}:\\ delete th from the waiting queue of cs\\

   527   \hspace{1cm}\alert{and who to give the resource next?}

   528   \end{itemize}

   529   

   530 

   531   \end{frame}}

   532   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   533 *}

   534 

   535 text_raw {*

   536   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   537   \mode<presentation>{

   538   \begin{frame}[c]

   539   \frametitle{The Scheduler (2)}

   469   \frametitle{Good Next Events}

   630   \frametitle{Valid Next Events (2)}

   470   %%\large

   631   \large

   476   \end{center}

   637   \end{center}\bigskip\pause

   477 

   638 

   478   

   639   \begin{itemize}

   479 

   640   \item Done with the specification. \ldots

   480   \end{frame}}

   641   \end{itemize}

   481   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   642 

   482 *}

   643   \end{frame}}

   644   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   645 *}

   646 

   647 text_raw {*

   648   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   649   \mode<presentation>{

   650   \begin{frame}[c]

   651   \frametitle{Correctness Criterion}

   652   \large

   653   

   654 

   655   \begin{center}

   656   \begin{tikzpicture}

   657   \draw [->, line width=1.5mm] (-4,0) -- (4, 0);

   658   \draw [line width=0.8mm] (-4, 0.3) -- (-4, -0.3);

   659   \draw [line width=0.8mm] (1, 0.3) -- (1, -0.3);

   660   \draw [line width=0.8mm] (0, 0.3) -- (0, -0.3);

   661   \node at (1,-0.7) {\large s'};

   662   \node at (0,-0.7) {\large s};

   663   \node at (1,-1.5) {\small(th')};

   664   \node at (0,-1.5) {\small(th)};

   665   \node at (-4,-0.7) {\large 0};

   666   \node at (3.2,-0.7) {\large time};

   667   \end{tikzpicture}

   668   \end{center}

   669 

   670   \normalsize

   671   \begin{itemize}

   672   \item {\bf If} th is alive in s and has the highest precedence

   673   \item plus some further assumption (like th not reset, exited, no higher precedences)

   674   \item and th is {\bf not} running in s', \\ {\bf then} the running

   675   thread th' (in s') is a thread that was alive in {\bf s} and has in s' the same 

   676   precedence as th in s.

   677   \end{itemize}

   678 

   679   \end{frame}}

   680   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   681 *}

   682 

   683 

   533   

   694 

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

   695   

   535 

   696   \begin{itemize}

   536   When @{text "e"} = \alert{Create th prio}, \alert{Exit th} 

   697   \item Create/Exit events:

   537   

   698   \begin{itemize}

   538   \begin{itemize}

   699   \item we do not have to recalculate the RAG

   539   \item @{text "RAG s' = RAG s"}

   700   \item we do not have to recalculate the other precedences

   540   \item No precedence needs to be recomputed

   701   \end{itemize}\bigskip

   541   \end{itemize}

   702   \item Set event:

   703   \begin{itemize}

   704   \item we do not have to recalculate the RAG

   705   \item also the other precedences do not have to be recalculated

   706   (since this is the currently running thread, it cannot affect

   707   other threads)

   708   \end{itemize}

   709   \item Unlock event (2 cases: a thread to take over, no thread to take over)

   710   \begin{itemize}

   711   \item case 1: RAG need to be modified, but appart from th and th' no

   712   other precedence needs to be recalculated

   713   \item case 2: RAG needs to be prunned, no precedence needs to be recalculated

   714   \end{itemize}

   715   \end{itemize}

   716 

   552 

   756   

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

   757   \begin{itemize} 

   554   

   758   \item in PINTOS (Stanford), written in C for educational purposes\bigskip

   555 

   759   \begin{center}

   556   When @{text "e"} = \alert{Set th prio}

   760   \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}

   557   

   761   \hline

   558   \begin{itemize}

   762   {\bf Event} & {\bf PINTOS function} \\

   559   \item @{text "RAG s' = RAG s"}

   763   \hline

   560   \item No precedence needs to be recomputed

   764   @{text Create} & @{text "thread_create"}\\

   561   \end{itemize}

   765   @{text Exit}   & @{text "thread_exit"}\\

   562 

   766   @{text Set}    & @{text "thread_set_priority"}\\

   563   \end{frame}}

   767   @{text Lock}      & @{text "lock_acquire"}\\

   564   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   768   @{text Unlock}      & @{text "lock_release"}\\ 

   565 *}

   769   \hline

   566 

   770   \end{tabular}

   567 text_raw {*

   771   \end{center}\pause\bigskip

   568   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   772 

   569   \mode<presentation>{

   773   \item \alert{We did not verify our C-code!}\pause

   570   \begin{frame}[t]

   774   \item We were much faster: we gave an unlocked resource to

   571   \frametitle{Implementation}

   775   the thread with the highest precedence

   572 

   776   \end{itemize}

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

   777   \end{frame}}

   574 

   778   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   575   When @{text "e"} = \alert{Unlock th cs} where there is a thread to take over

   779 *}

   576   

   780 

   577   \begin{itemize}

   781 text_raw {*

   578   \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"}

   782   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   579   \item we have to recalculate the precedence of the direct descendants

   783   \mode<presentation>{

   784   \begin{frame}[c]

   785   \frametitle{What Next?}

   786   \large

   787 

   788   \begin{itemize} 

   789   \item Did we make any impact? No!\medskip\pause

   790   

   791   \item real-time scheduling on multiprocessors seems to be a very

   792   underdeveloped area. 

   793   \item implementations exist: RT-Linux\bigskip

   794 

   795   \item The inductive approach can deal with distributed

   796   algorithms\\ \normalsize(a clock syncronisation algorithm developed by NASA)

   797   \end{itemize}

   798   \end{frame}}

   799   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   800 *}

   801 

   802 text_raw {*

   803   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   804   \mode<presentation>{

   805   \begin{frame}[c]

   806   \frametitle{Theorem Provers}

   807   \large

   808 

   809   \begin{itemize} 

   810   \item We found a mistake in a refereed paper by Harper \& Pfenning

   811   \item I also found a mistake in my PhD thesis\bigskip

   812   

   813   \item scratching on the surface of an completely ``alien'' subject 

   814   to us --- we were able to make progress

   815   \item a string algorithm about suffix sorting (appeared at ICALP 2005)\smallskip\\

   816   \small no implementation exists, claim: ``we are the best'';

   817   we found an error the {\bf old-fashioned way}; now we need to verify our fix :(

   818   \end{itemize}

   819   \end{frame}}

   820   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   821 *}

   822 

   823 text_raw {*

   824   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   825   \mode<presentation>{

   826   \begin{frame}[c]

   827   \frametitle{State of the Art}

   828   \large

   829 

   830   theorem provers are bad with:

   831 

   832   \begin{itemize} 

   833   \item real number arithmetic (Big-O stuff)

   834   \item C-programs

   581 

   836  

   582   \pause

   837   what others(we) are working on:

   583 

   838 

   584   When @{text "e"} =  \alert{Unlock th cs} where no thread takes over

   839   \begin{itemize} 

   585   

   840   \item write your programs inside your theorem prover, verify it,

   586   \begin{itemize}

   841   compile it to efficient machine code (compilation is verified)

   587   \item @{text "RAG s' = RAG s - {(C cs, T th)}"}

   842   \end{itemize}

   588   \item no recalculation of precedences

   843  

   589   \end{itemize}

   844 

   590 

   845  \end{frame}}

   591 

   846   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   592   \end{frame}}

   847 *}

   593   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   848 

   594 *}

   849 

   595 

   850 text_raw {*

   596 text_raw {*

   851   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   597   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   852   \mode<presentation>{

   598   \mode<presentation>{

   853   \begin{frame}[c]

   599   \begin{frame}[t]

   854   \frametitle{Questions?}

   600   \frametitle{Implementation}

   601 

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

   603 

   604   When @{text "e"} = \alert{Lock th cs} where cs is not locked

   605   

   606   \begin{itemize}

   607   \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"}

   608   \item no recalculation of precedences

   609   \end{itemize}\bigskip

   610 

   611   \pause

   612 

   613   When @{text "e"} = \alert{Lock th cs} where cs is locked

   614   

   615   \begin{itemize}

   616   \item @{text "RAG s' = RAG s - {(T th, C cs)}"}

   617   \item we have to recalculate the precedence of the descendants

   618   \end{itemize}

   619 

   620 

   621   \end{frame}}

   622   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   623 *}

   624 

   625 

   626 text_raw {*

   627   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   628   \mode<presentation>{

   629   \begin{frame}[c]

   630   \frametitle{Conclusion}

   633   \item Aims fulfilled \medskip \pause

   857   \item Thank you for the invitation and for listening!

   634   \item Alternative way \pause

   635        \begin{itemize} 

   636            \item using Isabelle/HOL in OS code development \medskip

   637            \item through the Inductive Approach

   638        \end{itemize} \pause

   639   \item Future research \pause

   640        \begin{itemize}

   641            \item scheduler in RT-Linux\medskip

   642            \item multiprocessor case\medskip

   643            \item other ``nails'' ? (networks, \ldots) \medskip \pause

   644            \item Refinement to real code and relation between implementations

   645         \end{itemize}

   646   \end{itemize}

   647   \end{frame}}

   648   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   649 *}

   650 

   651 text_raw {*

   652   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   653   \mode<presentation>{

   654   \begin{frame}[c]

   655   \frametitle{Questions?}

   656   

   657   \begin{itemize} \large

   658   \item Thank you for listening!