Slides/slides01.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sun, 06 Mar 2016 12:48:31 +0000
changeset 116 022503caa187
parent 103 ffe5d850df62
child 157 1fe44fb6d0a4
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
103
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass[dvipsnames,14pt,t, xelatex]{beamer}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
\usepackage{slides}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
\usepackage{graph}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
% beamer stuff 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
\renewcommand{\slidecaption}{SEN 09, King's College London}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
\begin{document}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
\begin{frame}[t]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
\frametitle{%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
  \begin{tabular}{@ {}c@ {}}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
  \\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
  \LARGE Security Engineering (9)\\[-3mm] 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
  \end{tabular}}\bigskip\bigskip\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
  \normalsize
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
  \begin{tabular}{ll}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
  Email:  & christian.urban at kcl.ac.uk\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
  Office: & S1.27 (1st floor Strand Building)\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
  Slides: & KEATS (also homework is there)\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
  \end{tabular}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
  \includegraphics[scale=0.6]{pics/bridge-limits.png}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
  \frametitle{Old-Fashioned Eng.~vs.~CS}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
  \begin{tabular}{@{}cc@{}}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
  \begin{tabular}{@{}p{5.2cm}} 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
  \includegraphics[scale=0.058]{pics/towerbridge.jpg}\\ 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
  {\bf bridges}: \\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
  \raggedright\small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
  engineers can ``look'' at a bridge and have a pretty good
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
  intuition about whether it will hold up or not\\ 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
  (redundancy; predictive theory)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
  \end{tabular} &
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
  \begin{tabular}{p{5cm}} 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
  \includegraphics[scale=0.265]{pics/code.jpg}\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
  \raggedright
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
  {\bf code}: \\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
  \raggedright\small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
  programmers have very little intuition about their code; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
  often it is too expensive to have redundancy;
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
  not ``continuous'' 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
  \end{tabular}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
  \end{tabular}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
\begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
\frametitle{Trusting Computing Base}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
When considering whether a system meets some security
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
objectives, it is important to consider which parts of that
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
system are trusted in order to meet that objective (TCB).
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
\bigskip\pause
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    80
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
The smaller the TCB, the less effort it takes to get
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
some confidence that it is trustworthy, by doing a code 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
review or by performing some (penetration) testing.
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
\footnotesize
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
CPU, compiler, libraries, OS, NP $\not=$ P,
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
random number generator, \ldots
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
  \frametitle{Dijkstra on Testing}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    97
  \begin{bubble}[10cm]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    98
  ``Program testing can be a very effective way to show the
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
  presence of bugs, but it is hopelessly inadequate for showing
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
  their absence.''
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
  \end{bubble}\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   102
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
  unfortunately attackers exploit bugs (Satan's computer vs 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
  Murphy's)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   105
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   106
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   107
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   109
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   110
\begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
\frametitle{\Large Proving Programs to be Correct}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
\begin{bubble}[10cm]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   114
\small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
{\bf Theorem:} There are infinitely many prime 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
numbers.\medskip\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
{\bf Proof} \ldots\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   119
\end{bubble}\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   120
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   122
similarly\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
\begin{bubble}[10cm]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   125
\small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
{\bf Theorem:} The program is doing what 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   127
it is supposed to be doing.\medskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   128
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
{\bf Long, long proof} \ldots\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   130
\end{bubble}\bigskip\medskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
\small This can be a gigantic proof. The only hope is to have
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   133
help from the computer. `Program' is here to be understood to be
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
quite general (protocols, OS, \ldots).
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   135
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   136
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   137
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   138
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   139
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   140
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   141
  \frametitle{\Large{}Mars Pathfinder Mission 1997}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   142
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   143
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
  %\includegraphics[scale=0.15]{../pics/marspath1.png}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   145
  %\includegraphics[scale=0.16]{../pics/marspath3.png}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   146
  %\includegraphics[scale=0.3]{../pics/marsrover.png}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   147
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   149
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   150
  \item despite NASA's famous testing procedures, the lander crashed frequently on Mars
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   151
  \item a scheduling algorithm was not used in the OS
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   152
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   153
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   154
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   155
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   156
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   157
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   158
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   159
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   160
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   161
  \begin{textblock}{11}(1,3)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   162
  \begin{tabular}{@{\hspace{-10mm}}l}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   163
  \begin{tikzpicture}[scale=1.1]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   164
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   165
  \node at (8,4) {\textcolor{white}{a}};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   166
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   167
    
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   168
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   169
  \only<1>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   170
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   171
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   172
  \only<2>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   173
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   174
   \draw[fill, blue!50] (3,0) rectangle (5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   175
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   176
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   177
  \only<3>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   178
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   179
   \draw[fill, blue!50] (3,0) rectangle (4.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   180
   \draw[fill, blue!50] (5.5,0) rectangle (6,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   181
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   182
   \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   183
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   184
  \only<4>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   185
   \node at (2.5,0.9) {\small locked a resource};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   186
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   187
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   188
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   189
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   190
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   191
  \only<5>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   192
   \node at (2.5,0.9) {\small locked a resource};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   193
   \draw[fill, blue!50] (1,0) rectangle (4,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   194
   \draw[blue!100, fill] (4,3) rectangle (5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   195
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   196
  \only<6>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   197
   \node at (2.5,0.9) {\small locked a resource};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   198
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   199
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   200
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   201
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   202
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   203
  \only<7>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   204
   \node at (2.5,0.9) {\small locked a resource};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   205
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   206
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   207
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   208
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   209
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   210
  \only<8>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   211
   \node at (2.5,0.9) {\small locked a resource}; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   212
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   213
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   214
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   215
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   216
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   217
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   218
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   219
  \only<9>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   220
   \node at (2.5,0.9) {\small locked a resource}; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   221
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   223
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   224
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   225
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   226
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   227
  \only<10>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   228
   \node at (2.5,0.9) {\small locked a resource}; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   229
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   230
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   231
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   232
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   233
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   234
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   235
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   236
  \only<11>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   237
   \node at (2.5,0.9) {\small locked a resource};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   238
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   239
   \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   240
   \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   241
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   242
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   243
   \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   244
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   245
  \only<12>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   246
   \node at (2.5,0.9) {\small locked a resource}; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   247
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   248
   \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   249
   \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   250
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   251
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   252
   \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   253
   \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   254
   \node [anchor=base] at (6.3, 1.8) {\Large\ldots};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   255
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   256
  \only<13>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   257
   \node at (2.5,0.9) {\small locked a resource}; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   258
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   259
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   260
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   261
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   262
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   263
  \only<14>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   264
   \node at (2.5,3.9) {\small locked a resource}; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   265
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   266
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   267
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   268
   \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   269
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   270
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   271
  \only<15>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   272
   \node at (2.5,3.9) {\small locked a resource};  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   273
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   274
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   275
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   276
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   277
   \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   278
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   279
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   280
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   281
  \draw[very thick,->](0,0) -- (8,0);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   282
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   283
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   284
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   285
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   286
  \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   287
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   288
  \end{tikzpicture}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   289
  \end{tabular}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   290
  \end{textblock}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   291
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   292
  \begin{textblock}{0}(2.5,13)%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   293
  \small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   294
  \onslide<3->{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   295
  \begin{bubble}[8cm]%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   296
  Scheduling: You want to avoid that a high 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   297
  priority process is starved indefinitely.
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   298
  \end{bubble}}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   299
  \end{textblock}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   300
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   301
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   302
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   303
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   304
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   305
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   306
  \frametitle{\Large Priority Inheritance Scheduling}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   307
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   308
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   309
  \item Let a low priority process $L$ temporarily inherit 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   310
    the high priority of $H$ until $L$ leaves the critical 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   311
    section unlocking the resource.\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   312
  \item Once the resource is unlocked $L$ returns to its original 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   313
    priority level.
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   314
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   315
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   316
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   317
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   318
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   319
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   320
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   321
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   322
  \begin{textblock}{11}(1,3)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   323
  \begin{tabular}{@{\hspace{-10mm}}l}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   324
  \begin{tikzpicture}[scale=1.1]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   325
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   326
  \node at (8,4) {\textcolor{white}{a}};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   327
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   328
  \only<1>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   329
    \draw[fill, blue!50] (1,0) rectangle (6,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   330
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   331
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   332
    \node at (3.5,0.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   333
    \node at (5.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   334
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   335
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   336
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   337
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   338
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   339
  \only<2>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   340
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   341
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   342
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   343
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   344
    \node at (3.5,0.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   345
    \node at (5.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   346
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   347
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   348
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   349
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   350
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   351
  \only<3>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   352
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   353
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   354
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   355
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   356
    \node at (3.5,0.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   357
    \node at (5.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   358
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   359
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   360
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   361
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   362
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   363
    \node at (3.5,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   364
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   365
  \only<4>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   366
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   367
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   368
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   369
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   370
    \node at (3.5,0.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   371
    \node at (5.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   372
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   373
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   374
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   375
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   376
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   377
    \node at (3.5,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   378
    \draw[very thick,blue!100] (4,3) rectangle (5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   379
    \node at (4.5,3.3) {\small $B$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   380
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   381
  \only<5>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   382
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   383
    \draw[very thick, blue!50] (3,3) rectangle (6,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   384
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   385
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   386
    \node at (3.5,3.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   387
    \node at (5.7,3.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   388
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   389
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   390
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   391
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   392
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   393
    \node at (6.5,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   394
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   395
    \node at (7.5,3.3) {\small $B$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   396
    \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   397
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   398
  \only<6>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   399
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   400
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   401
    \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   402
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   403
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   404
    \node at (3.5,3.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   405
    \node at (5.7,3.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   406
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   407
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   408
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   409
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   410
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   411
    \node at (6.5,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   412
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   413
    \node at (7.5,3.3) {\small $B$}; 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   414
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   415
  \only<7>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   416
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   417
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   418
    \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   419
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   420
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   421
    \node at (3.5,3.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   422
    \node at (5.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   423
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   424
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   425
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   426
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   427
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   428
    \node at (6.5,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   429
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   430
    \node at (7.5,3.3) {\small $B$};  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   431
    \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   432
    \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   433
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   434
  \only<8>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   435
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   436
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   437
    \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   438
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   439
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   440
    \node at (3.5,3.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   441
    \node at (6.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   442
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   443
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   444
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   445
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   446
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   447
    \node at (4,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   448
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   449
    \node at (7.5,3.3) {\small $B$};  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   450
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   451
  \only<9>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   452
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   453
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   454
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   455
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   456
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   457
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   458
    \node at (3.5,3.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   459
    \node at (6.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   460
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   461
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   462
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   463
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   464
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   465
    \node at (4,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   466
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   467
    \node at (7.5,3.3) {\small $B$};  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   468
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   469
  \only<10>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   470
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   471
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   472
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   473
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   474
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   475
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   476
    \node at (3.5,3.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   477
    \node at (6.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   478
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   479
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   480
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   481
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   482
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   483
    \node at (4,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   484
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   485
    \node at (7.5,3.3) {\small $B$};  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   486
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   487
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   488
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   489
  \only<11>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   490
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   491
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   492
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   493
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   494
    \node at (1.5,0.9) {\small $A_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   495
    \node at (2.0,0.9) {\small $B_L$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   496
    \node at (3.5,3.9) {\small $A_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   497
    \node at (6.7,0.9) {\small $B_R$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   498
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   499
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   500
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   501
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   502
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   503
    \node at (4,3.3) {\small $A$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   504
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   505
    \node at (7.5,3.3) {\small $B$};  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   506
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   507
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   508
    \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   509
    \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   510
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   511
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   512
  \draw[very thick,->](0,0) -- (8,0);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   513
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   514
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   515
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   516
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   517
  \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   518
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   519
  \end{tikzpicture}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   520
  \end{tabular}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   521
  \end{textblock}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   522
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   523
  \begin{textblock}{0}(2.5,13)%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   524
  \small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   525
  \onslide<11>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   526
  \begin{bubble}[8cm]%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   527
  Scheduling: You want to avoid that a high 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   528
  priority process is staved indefinitely.
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   529
  \end{bubble}}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   530
  \end{textblock}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   531
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   532
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   533
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   534
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   535
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   536
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   537
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   538
  \frametitle{\Large Priority Inheritance Scheduling}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   539
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   540
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   541
  \item Let a low priority process $L$ temporarily inherit 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   542
    the high priority of $H$ until $L$ leaves the critical 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   543
    section unlocking the resource.\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   544
  \item Once the resource is unlocked $L$ returns to its original 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   545
    priority level. \alert{\bf BOGUS}\pause\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   546
  \item \ldots $L$ needs to switch to the highest 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   547
    \alert{remaining} priority of the threads that it blocks.
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   548
  \end{itemize}\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   549
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   550
  \small this error is already known since around 1999
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   551
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   552
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   553
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   554
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   555
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   556
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   557
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   558
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   559
  \includegraphics[scale=0.25]{pics/p3.jpg}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   560
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   561
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   562
   \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   563
  \item by Rajkumar, 1991
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   564
  \item \it ``it resumes the priority it had at the point of entry into the critical 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   565
  section''
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   566
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   567
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   568
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   569
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   570
     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   571
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   572
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   573
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   574
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   575
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   576
  \includegraphics[scale=0.25]{pics/p2.jpg}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   577
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   578
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   579
   \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   580
  \item by Jane Liu, 2000
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   581
  \item {\it ``The job $J_l$ executes at its inherited 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   582
    priority until it releases $R$; at that time, the 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   583
    priority of $J_l$ returns to its priority 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   584
    at the time when it acquires the resource $R$.''}\medskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   585
  \item \small gives pseudo code and totally bogus data structures  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   586
  \item \small interesting part ``{\it left as an exercise}''
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   587
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   588
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   589
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   590
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   591
     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   592
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   593
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   594
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   595
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   596
  \includegraphics[scale=0.15]{pics/p1.pdf}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   597
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   598
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   599
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   600
  \item by Laplante and Ovaska, 2011 (\$113.76)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   601
  \item \it ``when $[$the task$]$ exits the critical section that
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   602
        caused the block, it reverts to the priority it had
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   603
        when it entered that section'' 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   604
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   605
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   606
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   607
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   608
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   609
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   610
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   611
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   612
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   613
  \includegraphics[scale=0.25]{pics/p4.jpg}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   614
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   615
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   616
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   617
  \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   618
  \item \it ``Upon releasing the lock, the 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   619
  $[$low-priority$]$ thread will revert to 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   620
  its original priority.''
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   621
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   622
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   623
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   624
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   625
   
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   626
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   627
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   628
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   629
  \frametitle{Priority Scheduling}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   630
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   631
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   632
  \item a scheduling algorithm that is widely used in real-time operating systems
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   633
  \item has been ``proved'' correct by hand in a paper in 1983
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   634
  \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   635
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   636
  \item we corrected the algorithm and then {\bf really} proved that it is correct	
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   637
  \item we implemented this algorithm in a small OS called PINTOS (used for teaching at Stanford)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   638
  \item our implementation was much more efficient than their reference implementation
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   639
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   640
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   641
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   642
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   643
   
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   644
   
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   645
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   646
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   647
  \frametitle{Design of AC-Policies}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   648
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   649
  Imagine you set up an access policy (root, lpd, users, staff, etc)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   650
  \bigskip\pause
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   651
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   652
  \Large
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   653
  \begin{quote}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   654
  ``what you specify is what you get but not necessarily what you want\ldots''
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   655
  \end{quote}\bigskip\bigskip\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   656
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   657
  \normalsize main work by Chunhan Wu (a PhD-student in Nanjing)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   658
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   659
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   660
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   661
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   662
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   663
  \begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   664
  \frametitle{Testing Policies}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   665
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   666
  \begin{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   667
  \begin{tikzpicture}[scale=1]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   668
  %\draw[black!10,step=2mm] (-5,-3) grid (5,4);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   669
  %\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   670
  \draw[white,thick,step=10mm] (-5,-3) grid (5,4);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   671
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   672
  \draw [black!20, line width=1mm] (0,0) circle (1cm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   673
  \draw [line width=1mm] (0,0) circle (3cm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   674
  \node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   675
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   676
  \draw [red, line width=2mm, <-] (-2.1,2.1) -- (-3.5,3.2);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   677
  \node at (-3.5,3.6) {your system};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   678
  \node at (-4.8,0) {\Large policy $+$};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   679
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   680
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   681
  \only<2>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   682
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   683
  \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   684
  \node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   685
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   686
  \only<3>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   687
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   688
  \node[white] at (2,1) {\small tainted};}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   689
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   690
  \only<4>{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   691
  \begin{scope}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   692
  \draw [clip] (0,0) circle (2.955cm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   693
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   694
  \node[white] at (2,1) {\small tainted};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   695
  \end{scope}}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   696
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   697
  \only<5->{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   698
  \begin{scope}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   699
  \draw [clip] (0,0) circle (2.955cm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   700
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   701
  \node[white] at (2,1) {\small tainted};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   702
  \end{scope}}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   703
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   704
  \only<6->{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   705
  \draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   706
  \draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm);
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   707
  \node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   708
  }
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   709
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   710
  \end{tikzpicture}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   711
  \end{center}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   712
  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   713
  \only<7->{
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   714
  \begin{textblock}{4}(1,12)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   715
  \small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   716
  reduced the problem to a finite problem; gave a proof
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   717
  \end{textblock}} 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   718
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   719
  \end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   720
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   721
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   722
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   723
\begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   724
\frametitle{Fuzzy Testing C-Compilers}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   725
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   726
\begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   727
\item tested GCC, LLVM and others by randomly generating 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   728
C-programs
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   729
\item found more than 300 bugs in GCC and also
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   730
many in LLVM (some of them highest-level critical)\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   731
\item about CompCert:
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   732
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   733
\begin{bubble}[10cm]\small ``The striking thing about our CompCert
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   734
results is that the middle-end bugs we found in all other
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   735
compilers are absent. As of early 2011, the under-development
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   736
version of CompCert is the only compiler we have tested for
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   737
which Csmith cannot find wrong-code errors. This is not for
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   738
lack of trying: we have devoted about six CPU-years to the
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   739
task.'' 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   740
\end{bubble} 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   741
\end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   742
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   743
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   744
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   745
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   746
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   747
\begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   748
\frametitle{Big Proofs in CS (2)}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   749
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   750
\begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   751
\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   752
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   753
  \item used in helicopters and mobile phones
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   754
  \item 200k loc of proof
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   755
  \item 25 - 30 person years
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   756
  \item found 160 bugs in the C code (144 by the proof)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   757
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   758
\end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   759
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   760
\begin{bubble}[10cm]\small
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   761
``Real-world operating-system kernel with an end-to-end proof
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   762
of implementation correctness and security enforcement''
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   763
\end{bubble}\bigskip\pause
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   764
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   765
unhackable kernel (New Scientists, September 2015)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   766
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   767
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   768
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   769
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   770
\begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   771
\frametitle{Big Proofs in CS (3)}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   772
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   773
\begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   774
\item verified TLS implementation\medskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   775
\item verified compilers (CompCert, CakeML)\medskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   776
\item verified distributed systems (Verdi)\medskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   777
\item verified OSes or OS components\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   778
(seL4, CertiKOS, Ironclad Apps, \ldots)\medskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   779
\item verified cryptography
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   780
\end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   781
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   782
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   783
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   784
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   785
\begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   786
\frametitle{How Did This Happen?}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   787
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   788
Lots of ways!
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   789
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   790
\begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   791
\item better programming languages
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   792
  \begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   793
  \item basic safety guarantees built in
  \item powerful mechanisms for abstraction and modularity
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   794
  \end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   795
\item better software development methodology
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   796
\item stable platforms and frameworks
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   797
\item better use of specifications\medskip\\
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   798
  \small If you want to build software that works or is secure, 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   799
    it is helpful to know what you mean by ``works'' and by ``is secure''!
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   800
\end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   801
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   802
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   803
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   804
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   805
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   806
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   807
\begin{frame}[c]
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   808
\frametitle{Goal}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   809
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   810
Remember the Bridges example?
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   811
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   812
\begin{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   813
\item Can we look at our programs and somehow ensure
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   814
they are secure/bug free/correct?\pause\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   815
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   816
\item Very hard: Anything interesting about programs is equivalent
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   817
to halting problem, which is undecidable.\pause\bigskip
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   818
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   819
\item \alert{Solution:} We avoid this ``minor'' obstacle by
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   820
      being as close as possible of deciding the halting
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   821
      problem, without actually deciding the halting problem.
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   822
      \small$\quad\Rightarrow$ yes, no, don't know (static analysis)
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   823
\end{itemize}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   824
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   825
\end{frame}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   826
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   827
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   828
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   829
\end{document}
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   830
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   831
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   832
%%% Local Variables:  
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   833
%%% mode: latex
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   834
%%% TeX-master: t
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   835
%%% End: 
ffe5d850df62 added some slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   836