1 (*<*)

     2 theory Slides4

     3 imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 (*

    11 ML {*

    12   open Printer;

    13   show_question_marks_default := false;

    14   *}

    15 *)

    16 

    17 notation (latex output)

    18   Cons ("_::_" [78,77] 73) and

    19   vt ("valid'_state") and

    20   runing ("running") and

    21   birthtime ("last'_set") and

    22   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and

    23   Prc ("'(_, _')") and

    24   holding ("holds") and

    25   waiting ("waits") and

    26   Th ("T") and

    27   Cs ("C") and

    28   P ("Lock") and

    29   V ("Unlock") and

    30   readys ("ready") and

    31   depend ("RAG") and 

    32   preced ("prec") and

    33   cpreced ("cprec") and

    34   dependents ("dependants") and

    35   cp ("cprec") and

    36   holdents ("resources") and

    37   original_priority ("priority") and

    38   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

    39 

    40 (*>*)

    41 

    42 

    43 

    44 text_raw {*

    45   \renewcommand{\slidecaption}{NASA, 20 June 2013}

    46   \newcommand{\bl}[1]{#1}                        

    47   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    48   \mode<presentation>{

    49   \begin{frame}

    50   \frametitle{%

    51   \begin{tabular}{@ {}c@ {}}

    52   \\[-3mm]

    53   \LARGE Formalisations and the\\[-1mm] 

    54   \LARGE Isabelle Theorem Prover\\[-3mm] 

    55   \end{tabular}}

    56   

    57   \begin{center}

    58    Christian Urban\\[1mm]

    59   \small King's College London

    60   \end{center}\bigskip

    61  

    62   \begin{center}

    63   many thanks to Mahyar Malekpour and Cesar Munoz for the invitation and 

    64   hospitality

    65   \end{center}

    66   \end{frame}}

    67   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    68 *}

    69 

    70 text_raw {*

    71   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    72   \mode<presentation>{

    73   \begin{frame}<2->[c]

    74   \frametitle{Isabelle Theorem Prover}

    75 

    76   \begin{center}

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

    78   \end{center}  

    79 

    80   \only<2>{

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

    82   \begin{tikzpicture}

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

    84   {\normalsize\color{darkgray}

    85   \begin{minipage}{9cm}\raggedright

    86   \ldots to make sure large proofs are correct

    87   \end{minipage}};

    88   \end{tikzpicture}

    89   \end{textblock}}

    90 

    91 

    92   \end{frame}}

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

    94 

    95 *}

    96 

    97 text_raw {*

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

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

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

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

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

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

   104   \mode<presentation>{

   105   \begin{frame}[c]

   106   \frametitle{}

   107 

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

   109   \\[6mm]

   110   \begin{tabular}{c}

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

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

   113   {\footnotesize (CMU)}

   114   \end{tabular}

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

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

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

   118   {\footnotesize (CMU)}

   119   \end{tabular} &

   120 

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

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

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

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

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

   126     \&[-10mm] 

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

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

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

   130   };

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

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

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

   134   \end{tikzpicture}

   135   \end{tabular}\\

   136 

   137   \pause

   138   \\[0mm]

   139   

   140   \multicolumn{2}{c}{

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

   142   \raggedright

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

   144   \end{tabular}

   145   

   146   \begin{tabular}{c}

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

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

   149   {\footnotesize (Princeton)}

   150   \end{tabular}}

   151   \end{tabular} 

   152 

   153   \end{frame}}

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

   155 

   156 *}

   157 

   158 text_raw {*

   159   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   160   \mode<presentation>{

   161   \begin{frame}<4-> 

   162   \frametitle{\LARGE\begin{tabular}{c}An Example for a Small TCB\end{tabular}}

   163   \mbox{}\\[-14mm]\mbox{}

   164 

   165   \begin{columns}

   166   \begin{column}{0.2\textwidth}

   167   \begin{tabular}{@ {} c@ {}}

   168   \includegraphics[scale=0.3]{appel.jpg}\\[-2mm] 

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

   170   {\footnotesize (Princeton)}

   171   \end{tabular}

   172   \end{column}

   173   

   174   \begin{column}{0.8\textwidth}

   175   \begin{textblock}{10}(4.5,3.95)

   176   \begin{block}{Proof-Carrying Code:}

   177   \begin{center}

   178   \begin{tikzpicture}

   179   \draw[help lines,cream] (0,0.2) grid (8,4);

   180   

   181   \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);

   182   \node[anchor=base] at (6.5,2.8) 

   183      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user can run untrusted code\end{tabular}};

   184 

   185   \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);

   186   \node[anchor=base] at (1.5,2.3) 

   187      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  code developer/ web server/ Apple 

   188   Store\end{tabular}};

   189   

   190   \onslide<4->{

   191   \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);

   192   \node[anchor=base,white] at (6.5,1.1) 

   193      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

   194 

   195   \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};

   196   \onslide<3->{

   197   \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};

   198   \node at (3.8,1.9) {\small certificate};

   199   }

   200 

   201   \onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}

   202   % Code Developer

   203   % User (runs untrusted code)

   204   % transmits a proof that the code is safe

   205   % 

   206   \end{tikzpicture}

   207   \end{center}

   208   \end{block}

   209   \end{textblock}

   210   \end{column}

   211   \end{columns}

   212   

   213   \small\mbox{}\\[3.2cm]

   214   \begin{itemize}

   215   \item<4-> TCB of the checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 

   216   803 loc in C including 2 library functions)\\[-3mm]

   217   \item<4-> 167 loc in C implement a type-checker

   218   \end{itemize}

   219 

   220   \end{frame}}

   221   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   222 

   223 *}

   224 

   225 

   226 

   227 

   228 text_raw {*

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

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

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

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

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

   234   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   235   \mode<presentation>{

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

   237   \frametitle{} 

   238   

   239   \begin{columns}

   240   

   241   \begin{column}{0.8\textwidth}

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

   243 

   244   \begin{tikzpicture}

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

   246   { \&[-10mm] 

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

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

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

   250     

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

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

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

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

   255      

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

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

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

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

   260 

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

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

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

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

   265   };

   266 

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

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

   269   

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

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

   272 

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

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

   275   

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

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

   278 

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

   280   \end{tikzpicture}

   281 

   282   \end{textblock}

   283   \end{column}

   284   \end{columns}

   285 

   286 

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

   288   \onslide<4->{

   289   \begin{tikzpicture}

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

   291   \end{tikzpicture}}

   292   \end{textblock}

   293 

   294   \end{frame}}

   295   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   296 *}

   297 

   298 text_raw {*

   299   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   300   \mode<presentation>{

   301   \begin{frame}[c]

   302   \frametitle{Other Formalisations}

   303   

   304 

   305   \begin{itemize} 

   306   \item I also found a (fixable) mistake in my PhD thesis\bigskip

   307   

   308   \item Nominal Isabelle: found out that the variable convention 

   309   can be used to prove false (a surprising result in PL-research)\bigskip

   310 

   311   \item Computability and Logic Book (5th ed.)\\ by Boolos, Burgess and Jeffrey ---

   312   two definitions about halting computations in UTMs are inconsistent

   313   \end{itemize}

   314   \end{frame}}

   315   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   316 *}

   317 

   318 text_raw {*

   319   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   320   \mode<presentation>{

   321   \begin{frame}[c]

   322   \frametitle{Scheduling in RTOS}

   323 

   324   \begin{itemize}

   325   \item RTOS: priorities and resource locking

   326 

   327   \item Purpose:\\

   328   guarantee tasks to be completed in time\medskip\pause

   329 

   330   \item \alert{this already results into a surprisingly non-trivial algorithmic problem}

   331   \end{itemize}

   332 

   333   \end{frame}}

   334   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   335 

   336 *}

   337 

   338 

   339 text_raw {*

   340   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   341   \mode<presentation>{

   342   \begin{frame}[c]

   343   \frametitle{The Problem}

   344   \Large

   345 

   346   \begin{center}

   347   \begin{tabular}{l}

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

   349   \onslide<2->{\alert{M}edium-priority process}\\[4mm]

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

   351   \end{tabular}

   352   \end{center}

   353 

   354   \onslide<3->{

   355   \begin{itemize}

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

   357   \mbox{}\hfill with lower priority

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

   359   \end{itemize}}

   360 

   361   \end{frame}}

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

   363 

   364 *}

   365 

   366 

   367 text_raw {*

   368   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   369   \mode<presentation>{

   370   \begin{frame}[c]

   371   \frametitle{Mars Pathfinder Mission 1997}

   372   \large

   373 

   374   \begin{center}

   375   \includegraphics[scale=0.15]{marspath1.png}

   376   \includegraphics[scale=0.16]{marspath3.png}

   377   \includegraphics[scale=0.3]{marsrover.png}

   378   \end{center}

   379   

   380   \begin{itemize}

   381   \item the lander reset frequently on Mars

   382   \item the problem: priority inversion

   383   \end{itemize}

   384 

   385   \end{frame}}

   386   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   387 *}

   388 

   389 text_raw {*

   390   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   391   \mode<presentation>{

   392   \begin{frame}[c]

   393   \frametitle{The Solution}

   394   \Large

   395 

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

   397 

   398   \begin{center}

   399   \begin{tabular}{l}

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

   401   \textcolor{gray}{Medium-priority process}\\[4mm]

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

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

   404   \end{tabular}

   405   \end{center}

   406 

   407   \end{frame}}

   408   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   409 *}

   410 

   411 

   412 

   413 

   414 text_raw {*

   415   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   416   \mode<presentation>{

   417   \begin{frame}[c]

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

   419   \Large

   420 

   421   \begin{itemize}

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

   423   correctness:\\[5mm]

   424   \end{itemize}

   425 

   426   \normalsize

   427   \begin{quote}

   428   \ldots{}after the thread (whose priority has been raised) completes its 

   429   critical section and releases the lock, it ``returns to its original 

   430   priority level''.

   431   \end{quote}\bigskip

   432 

   433   \small

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

   435   \end{frame}}

   436   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   437 *}

   438 

   439 text_raw {*

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

   441   \mode<presentation>{

   442   \begin{frame}[c]

   443   \frametitle{}

   444   \Large

   445 

   446   \begin{center}

   447   \begin{tabular}{l}

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

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

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

   451   \end{tabular}

   452   \end{center}

   453 

   454   \onslide<2->{

   455   \begin{itemize}

   456   \item Solution: return to the highest

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

   458   \end{itemize}}

   459 

   460   \end{frame}}

   461   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   462 *}

   463 

   464 text_raw {*

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

   466   \mode<presentation>{

   467   \begin{frame}[c]

   468   \frametitle{Specification}

   469   \Large

   470   

   471    \begin{itemize}\Large

   472   \item Use Inductive Method with events of the form:

   473    \end{itemize}

   474 

   475   \begin{center}

   476   \begin{tabular}{l}

   477   Create \textcolor{gray}{thread priority}\\

   478   Exit \textcolor{gray}{thread}\\

   479   Set \textcolor{gray}{thread priority}\\

   480   Lock \textcolor{gray}{thread cs}\\

   481   Unlock \textcolor{gray}{thread cs}\\

   482   \end{tabular}

   483   \end{center}\medskip

   484 

   485   \end{frame}}

   486   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   487 *}

   488 

   489 text_raw {*

   490   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   491   \mode<presentation>{

   492   \begin{frame}[c]

   493   \frametitle{Scheduling States}

   494   \Large

   495   

   496   \begin{itemize}

   497   \item A \alert{state s} is a list of events\bigskip

   498   \begin{center}

   499   \begin{tikzpicture}

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

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

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

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

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

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

   506   \end{tikzpicture}

   507   \end{center}\pause

   508 

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

   510   \begin{center}

   511   \begin{tabular}{@ {}l@ {}}

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

   513   \end{tabular}

   514   \end{center}

   515   \end{itemize}

   516 

   517   \end{frame}}

   518   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   519 *}

   520 

   521 

   522 text_raw {*

   523   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   524   \mode<presentation>{

   525   \begin{frame}[c]

   526   \frametitle{Waiting Queues}

   527   \large

   528 

   529   \begin{itemize}

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

   531   associated with every resource

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

   533   \medskip

   534 

   535   \begin{center}\normalsize

   536   \begin{tabular}{@ {}l}

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

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

   539   \end{tabular}

   540   \end{center}

   541   \end{itemize}

   542 

   543   \end{frame}}

   544   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   545 *}

   546 

   547 

   548 text_raw {*

   549   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   550   \mode<presentation>{

   551   \begin{frame}[c]

   552   \frametitle{Resource Allocation Graphs}

   553 

   554 \begin{center}

   555   \newcommand{\fnt}{\fontsize{7}{8}\selectfont}

   556   \begin{tikzpicture}[scale=1]

   557   

   558   \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};

   559   \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};

   560   \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};

   561   \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};

   562   \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};

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

   564   \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};

   565 

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

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

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

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

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

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

   572   \end{tikzpicture}

   573   \end{center}\bigskip

   574 

   575   \begin{center}

   576   \begin{minipage}{0.8\linewidth}

   577   \raggedleft

   578   @{thm cs_depend_def}

   579   \end{minipage}\medskip\\

   580   \begin{minipage}{1\linewidth}

   581   @{thm cs_dependents_def}

   582   \end{minipage}\medskip\\\pause

   583   \begin{minipage}{1\linewidth}

   584   \alert{cprec wq s th} $\dn$\\

   585   \mbox{}\hspace{1cm}Max(\{prec th s\} $\cup$\\ 

   586   \mbox{}\hspace{1cm}\phantom{Max(}\{prec th' s $\mid$ th' $\in$ dependants wq th\})

   587   \end{minipage}

   588   \end{center}

   589 

   590   

   591 

   592   \end{frame}}

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

   594 *}

   595 

   596 

   597 text_raw {*

   598   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   599   \mode<presentation>{

   600   \begin{frame}[c]

   601   \frametitle{The Scheduler}

   602   \large

   603 

   604   \begin{itemize}

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

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

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

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

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

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

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

   612   \end{itemize}

   613   

   614 

   615   \end{frame}}

   616   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   617 *}

   618 

   619 text_raw {*

   620   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   621   \mode<presentation>{

   622   \begin{frame}[c]

   623   \frametitle{The Scheduler (2)}

   624   %%\large

   625 

   626   \begin{itemize}

   627   \item \large threads ready to run\normalsize

   628 

   629   \begin{center}

   630   \begin{tabular}{@ {}l}

   631   @{thm (lhs) readys_def} $\dn$\\

   632   \;@{thm (rhs) readys_def}

   633   \end{tabular}

   634   \end{center}\bigskip

   635 

   636   \item \large the thread that is running in a state:\\[-10mm]\normalsize

   637   \begin{center}

   638   \begin{tabular}{@ {}l@ {}}

   639   @{thm (lhs) runing_def} $\dn$\\

   640   \;@{thm (rhs) runing_def}

   641   \end{tabular}

   642   \end{center}

   643 

   644   \end{itemize}

   645 

   646   \end{frame}}

   647   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   648 *}

   649 

   650 text_raw {*

   651   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   652   \mode<presentation>{

   653   \begin{frame}[c]

   654   \frametitle{Inductive Method}

   655   %%\large

   656 

   657   \begin{center}

   658 \begin{tikzpicture}[scale=1.6]

   659 %%\draw[step=2mm] (-4,-1) grid (4,1.4);

   660 \draw (0,0.2) node {\begin{tabular}{l} valid\\[-1mm] scheduler\\[-1mm] states\\ \end{tabular}};

   661 \draw (3,0) node {\begin{tabular}{l} set of invalid\\[-1mm] scheduler states \\[-1mm](e.g., deadlocks)\\ \end{tabular}};

   662 \draw[<-, line width=0.5mm] (1.0,0) -- (1.8,0);

   663 \draw[<-, line width=0.5mm] (-0.2,-0.55) -- (-0.4,-1.3);

   664 \draw (-0.0,-1.5) node {\begin{tabular}{l} inductively defined set \end{tabular}};

   665 

   666 \draw[line width=0.5mm, rounded corners=6.3pt] 

   667   (-0.9,-0.05) -- (-0.8,0.6) -- (-0.3,0.95) -- (0,1) -- (0.5,0.8) -- (0.65,0.5) -- (0.7,0) -- (0.4,-0.5) -- (0,-0.6) -- (-0.5,-0.45) -- cycle;

   668 

   669 \draw[line width=0.5mm, rounded corners=15pt] 

   670  (-1.2,0) -- (-0.9,0.95) -- (0,1.2) -- (1.0,1.0) -- (1.7,0) -- (0.95,-1.0) -- (0,-1.2) -- (-0.9,-0.9) -- cycle;

   671 

   672 \end{tikzpicture}

   673 \end{center}

   674 

   675   \begin{itemize}

   676   \item We have to exclude situations where there is a deadlock,

   677   a thread exited before created, \ldots

   678   

   679   \end{itemize}

   680 

   681   \end{frame}}

   682   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   683 *}

   684 

   685 text_raw {*

   686   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   687   \mode<presentation>{

   688   \begin{frame}[c]

   689   \frametitle{Valid Next Events}

   690   \large

   691 

   692   \begin{itemize}

   693   \item In a state s, the following events can occur:

   694   \end{itemize}

   695 

   696   \begin{center}

   697   @{thm[mode=Rule] thread_create[where thread=th]}\bigskip

   698 

   699   @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip

   700 

   701   @{thm[mode=Rule] thread_set[where thread=th]}

   702   \end{center}

   703 

   704   

   705 

   706   \end{frame}}

   707   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   708 *}

   709 

   710 text_raw {*

   711   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   712   \mode<presentation>{

   713   \begin{frame}[c]

   714   \frametitle{Valid Next Events (2)}

   715   \large

   716 

   717   \begin{center}

   718   @{thm[mode=Rule] thread_P[where thread=th]}\bigskip

   719   

   720   @{thm[mode=Rule] thread_V[where thread=th]}\bigskip

   721   \end{center}\bigskip\pause

   722 

   723   \begin{itemize}

   724   \item Done with the specification. \ldots

   725   \end{itemize}

   726 

   727   \end{frame}}

   728   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   729 *}

   730 

   731 text_raw {*

   732   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   733   \mode<presentation>{

   734   \begin{frame}[c]

   735   \frametitle{Correctness Criterion}

   736   \large

   737   

   738 

   739   \begin{center}

   740   \begin{tikzpicture}

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

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

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

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

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

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

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

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

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

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

   751   \end{tikzpicture}

   752   \end{center}

   753 

   754   \normalsize

   755   \begin{itemize}

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

   757   \item plus some further assumption (like th not reset, not exited, no higher precedences in s - s')

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

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

   760   precedence as th in s.

   761   \end{itemize}

   762 

   763   \end{frame}}

   764   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   765 *}

   766 

   767 

   768 (*<*)

   769 context extend_highest_gen

   770 begin

   771 (*>*)

   772 

   773 text_raw {*

   774   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   775   \mode<presentation>{

   776   \begin{frame}[t]

   777   \frametitle{Implementation}

   778 

   779   

   780   \begin{itemize}

   781   \item Create/Exit events:

   782   \begin{itemize}

   783   \item we do not have to recalculate the RAG

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

   785   \end{itemize}\bigskip

   786   \item Set event:

   787   \begin{itemize}

   788   \item we do not have to recalculate the RAG

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

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

   791   other threads)

   792   \end{itemize}

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

   794   \begin{itemize}

   795   \item case 1: RAG needs to be modified, but apart from th and th' no

   796   other precedence needs to be recalculated

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

   798   \end{itemize}

   799   \end{itemize}

   800 

   801 

   802   \end{frame}}

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

   804 *}

   805 

   806 text_raw {*

   807   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   808   \mode<presentation>{

   809   \begin{frame}[t]

   810   \frametitle{Implementation (2)}

   811 

   812   

   813   \begin{itemize}

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

   815   \begin{itemize}

   816   \item case 1: RAG needs to be modified, but apart from th and th' no

   817   other precedence needs to be recalculated

   818   \item case 2: RAG needs to be pruned, no precedence needs to be recalculated

   819   \end{itemize}\bigskip

   820   \item Lock event (2 cases: cs is locked, not locked)

   821   \begin{itemize}

   822   \item case 1: a waiting edge needs to be added to the RAG, precedences of 

   823   all dependants need to recalculated (where there is a change)  

   824   \item case 2: a holding edge needs to be added to the RAG, no

   825   precedences need to be recalculated

   826   \end{itemize}

   827   \end{itemize}

   828 

   829 

   830   \end{frame}}

   831   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   832 *}

   833 

   834 

   835 text_raw {*

   836   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   837   \mode<presentation>{

   838   \begin{frame}[c]

   839   \frametitle{Implementation}

   840   

   841   \begin{itemize} 

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

   843   \begin{center}

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

   845   \hline

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

   847   \hline

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

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

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

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

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

   853   \hline

   854   \end{tabular}

   855   \end{center}\pause\bigskip

   856 

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

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

   859   the thread with the highest precedence

   860   \end{itemize}

   861   \end{frame}}

   862   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   863 *}

   864 

   865 text_raw {*

   866   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   867   \mode<presentation>{

   868   \begin{frame}[c]

   869   \frametitle{A Step Back\ldots}

   870   \large

   871 

   872   \begin{itemize} 

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

   874   

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

   876   underdeveloped area 

   877   \item implementations exist, e.g.~RT-Linux

   878   \end{itemize}

   879   \end{frame}}

   880   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   881 *}

   882 

   883 text_raw {*

   884   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   885   \mode<presentation>{

   886   \begin{frame}[c]

   887   \frametitle{Theorem Provers}

   888 

   889   \begin{itemize} 

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

   891   \item I also found a mistake in my PhD thesis

   892   \item also a popular textbook book on Computability contained an

   893   error\bigskip

   894   

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

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

   897 

   898   \end{itemize}

   899   \end{frame}}

   900   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   901 *}

   902 

   903 text_raw {*

   904   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   905   \mode<presentation>{

   906   \begin{frame}[c]

   907   \frametitle{Inductive Method / Protocols}

   908 

   909   \begin{itemize} 

   910   \item the inductive method was developed/used by Larry Paulson

   911   for verifying security protocols\bigskip\bigskip

   912   \item we used it for a different `kind' of protocols (scheduling)

   913   \item but this was restricted to only single-processors, no timing information

   914 

   915 

   916   \end{itemize}

   917   \end{frame}}

   918   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   919 *}

   920 

   921 text_raw {*

   922   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   923   \mode<presentation>{

   924   \begin{frame}[c]

   925   \frametitle{Clock Synchronisation}

   926 

   927   \begin{itemize} 

   928   \item Mahyar Malekpour introduced a distributed clock-synchronisation

   929   algorithm\\ (perfect example for us)\bigskip\bigskip

   930 

   931   \item connected units exchange messages according to a protocol

   932   and reach a stable, synchronised state

   933   \item messages have to reach the receiver within a time-window\pause

   934 

   935   \item \alert{verification still ongoing}

   936   \end{itemize}

   937   \end{frame}}

   938   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   939 *}

   940 

   941 

   942 text_raw {*

   943   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   944   \mode<presentation>{

   945   \begin{frame}[c]

   946   \frametitle{Questions?}

   947   

   948   \begin{itemize} \large

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

   950   \end{itemize}

   951   

   952   \begin{center}

   953   \begin{tabular}{c}

   954   \includegraphics[scale=0.13]{isabelle.png}\\[-2mm]

   955   \small\url{http://isabelle.in.tum.de}

   956   \end{tabular}

   957   \end{center}  

   958   \end{frame}}

   959   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   960 *}

   961 

   962 

   963 (*<*)

   964 end

   965 end

   966 (*>*)