sen-material: slides/slides09.tex@54a1fbe96b14 (annotated)

75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass[dvipsnames,14pt,t]{beamer}
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	2	\usepackage{../slides}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	3	\usepackage{../graphics}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	4	\usepackage{../langs}
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	% beamer stuff
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	7	\renewcommand{\slidecaption}{APP 09, King's College London}
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\newcommand{\bl}[1]{\textcolor{blue}{#1}}
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	\begin{document}
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	13	\begin{frame}[t]
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\frametitle{%
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\begin{tabular}{@ {}c@ {}}
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\\
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\LARGE Access Control and \\[-3mm]
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	18	\LARGE Privacy Policies (9)\\[-6mm]
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\end{tabular}}\bigskip\bigskip\bigskip
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	21	\normalsize
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	\begin{center}
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	\begin{tabular}{ll}
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	Email: & christian.urban at kcl.ac.uk\\
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	25	Office: & S1.27 (1st floor Strand Building)\\
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	Slides: & KEATS (also homework is there)\\
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	\end{tabular}
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\end{center}
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	30	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	31	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	32
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	33	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	34	\begin{frame}[c]
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	36	\begin{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	37	\includegraphics[scale=0.6]{../pics/bridge-limits.png}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	38	\end{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	39
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	40	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	41	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	42
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	43	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	44	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	45	\frametitle{Old-Fashioned Eng.~vs.~CS}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	46
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	47	\begin{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	48	\begin{tabular}{@{}cc@{}}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	49	\begin{tabular}{@{}p{5.2cm}}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	50	\includegraphics[scale=0.058]{../pics/towerbridge.jpg}\\
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	51	{\bf bridges}: \\
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	52	\raggedright\small
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	53	engineers can ``look'' at a bridge and have a pretty good
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	54	intuition about whether it will hold up or not\\
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	55	(redundancy; predictive theory)
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	56	\end{tabular} &
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	57	\begin{tabular}{p{5cm}}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	58	\includegraphics[scale=0.265]{../pics/code.jpg}\\
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	59	\raggedright
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	60	{\bf code}: \\
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	61	\raggedright\small
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	62	programmers have very little intuition about their code;
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	63	often it is too expensive to have redundancy;
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	64	not ``continuous''
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	65	\end{tabular}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	66	\end{tabular}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	67	\end{center}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	68
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	69	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	70	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	71
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	72
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	73	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	74	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	75	\frametitle{Dijkstra on Testing}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	76
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	77	\begin{bubble}[10cm]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	78	``Program testing can be a very effective way to show the
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	79	presence of bugs, but it is hopelessly inadequate for showing
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	80	their absence.''
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	81	\end{bubble}\bigskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	82
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	83	unfortunately attackers exploit bugs (Satan's computer vs
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	84	Murphy's)
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	85
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	86	\vfill
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	87	\small
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	88	Dijkstra: shortest path algorithm,
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	89	dining philosophers problem,
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	90	semaphores
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	91	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	92	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	93
ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	94	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	95	\begin{frame}[c]
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	96	\frametitle{\Large Proving Programs to be Correct}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	97
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	98	\begin{bubble}[10cm]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	99	\small
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	100	{\bf Theorem:} There are infinitely many prime
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	101	numbers.\medskip\\
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	102
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	103	{\bf Proof} \ldots\\
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	104	\end{bubble}\bigskip
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	105
ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	106
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	107	similarly\bigskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	108
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	109	\begin{bubble}[10cm]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	110	\small
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	111	{\bf Theorem:} The program is doing what
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	112	it is supposed to be doing.\medskip
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	113
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	114	{\bf Long, long proof} \ldots\\
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	115	\end{bubble}\bigskip\medskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	116
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	117	\small This can be a gigantic proof. The only hope is to have
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	118	help from the computer. `Program' is here to be understood to be
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	119	quite general (protocol, OS,\ldots).
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	120
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	121	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	122	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	123
ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	124	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	125	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	126	\frametitle{\Large{}Mars Pathfinder Mission 1997}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	127
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	128	\begin{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	129	\includegraphics[scale=0.15]{../pics/marspath1.png}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	130	\includegraphics[scale=0.16]{../pics/marspath3.png}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	131	\includegraphics[scale=0.3]{../pics/marsrover.png}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	132	\end{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	133
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	134	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	135	\item despite NASA's famous testing procedures, the lander crashed frequently on Mars
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	136	\item a scheduling algorithm was not used in the OS
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	137	\end{itemize}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	138
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	139	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	140	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	141
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	142	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	143	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	144
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	145
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	146	\begin{textblock}{11}(1,3)
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	147	\begin{tabular}{@{\hspace{-10mm}}l}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	148	\begin{tikzpicture}[scale=1.1]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	149	\node at (-2.5,-1.5) {\textcolor{white}{a}};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	150	\node at (8,4) {\textcolor{white}{a}};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	151
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	152
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	153
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	154	\only<1>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	155	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	156	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	157	\only<2>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	158	\draw[fill, blue!50] (1,0) rectangle (2,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	159	\draw[fill, blue!50] (3,0) rectangle (5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	160	\draw[fill, blue!100] (2,3) rectangle (3,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	161	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	162	\only<3>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	163	\draw[fill, blue!50] (1,0) rectangle (2,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	164	\draw[fill, blue!50] (3,0) rectangle (4.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	165	\draw[fill, blue!50] (5.5,0) rectangle (6,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	166	\draw[fill, blue!100] (2,3) rectangle (3,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	167	\draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	168	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	169	\only<4>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	170	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	171	\draw[fill, blue!50] (1,0) rectangle (2,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	172	\draw[blue!50, very thick] (2,0) rectangle (4,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	173	\draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	174	\draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	175	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	176	\only<5>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	177	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	178	\draw[fill, blue!50] (1,0) rectangle (4,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	179	\draw[blue!100, fill] (4,3) rectangle (5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	180	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	181	\only<6>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	182	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	183	\draw[fill, blue!50] (1,0) rectangle (2,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	184	\draw[blue!50, very thick] (2,0) rectangle (4,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	185	\draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	186	\draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	187	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	188	\only<7>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	189	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	190	\draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	191	\draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	192	\draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	193	\draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	194	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	195	\only<8>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	196	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	197	\draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	198	\draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	199	\draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	200	\draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	201	\draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	202	\draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	203	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	204	\only<9>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	205	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	206	\draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	207	\draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	208	\draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	209	\draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	210	\draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	211	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	212	\only<10>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	213	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	214	\draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	215	\draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	216	\draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	217	\draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	218	\draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	219	\draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	220	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	221	\only<11>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	222	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	223	\draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	224	\draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	225	\draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	226	\draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	227	\draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	228	\draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	229	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	230	\only<12>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	231	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	232	\draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	233	\draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	234	\draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	235	\draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	236	\draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	237	\draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	238	\draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	239	\node [anchor=base] at (6.3, 1.8) {\Large\ldots};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	240	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	241	\only<13>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	242	\node at (2.5,0.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	243	\draw[fill, blue!50] (1,0) rectangle (2,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	244	\draw[blue!50, very thick] (2,0) rectangle (4,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	245	\draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	246	\draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	247	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	248	\only<14>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	249	\node at (2.5,3.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	250	\draw[fill, blue!50] (1,0) rectangle (2,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	251	\draw[blue!50, fill] (2,3) rectangle (4,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	252	\draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	253	\draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	254	\draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	255	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	256	\only<15>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	257	\node at (2.5,3.9) {\small locked a resource};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	258	\draw[fill, blue!50] (1,0) rectangle (2,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	259	\draw[blue!50, fill] (2,3) rectangle (4,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	260	\draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	261	\draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	262	\draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	263	}
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	264
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	265
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	266	\draw[very thick,->](0,0) -- (8,0);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	267	\node [anchor=base] at (8, -0.3) {\scriptsize time};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	268	\node [anchor=base] at (0, -0.3) {\scriptsize 0};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	269	\node [anchor=base] at (-1.2, 0.2) {\small low priority};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	270	\only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	271	\only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	272
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	273	\end{tikzpicture}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	274	\end{tabular}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	275	\end{textblock}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	276
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	277	\begin{textblock}{0}(2.5,13)%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	278	\small
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	279	\onslide<3->{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	280	\begin{bubble}[8cm]%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	281	Scheduling: You want to avoid that a high
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	282	priority process is staved indefinitely.
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	283	\end{bubble}}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	284	\end{textblock}
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	285
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	286	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	287	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	288
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	289	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	290	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	291	\frametitle{\Large Priority Inheritance Scheduling}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	292
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	293	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	294	\item Let a low priority process $L$ temporarily inherit
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	295	the high priority of $H$ until $L$ leaves the critical
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	296	section unlocking the resource.\bigskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	297	\item Once the resource is unlocked $L$ returns to its original
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	298	priority level.
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	299	\end{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	300
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	301	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	302	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	303
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	304	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	305	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	306
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	307
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	308	\begin{textblock}{11}(1,3)
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	309	\begin{tabular}{@{\hspace{-10mm}}l}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	310	\begin{tikzpicture}[scale=1.1]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	311	\node at (-2.5,-1.5) {\textcolor{white}{a}};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	312	\node at (8,4) {\textcolor{white}{a}};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	313
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	314
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	315
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	316	\only<1>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	317	\draw[fill, blue!50] (1,0) rectangle (6,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	318	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	319	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	320	\node at (3.5,0.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	321	\node at (5.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	322	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	323	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	324	\draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	325	\draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	326	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	327	\only<2>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	328	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	329	\draw[very thick, blue!50] (3,0) rectangle (6,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	330	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	331	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	332	\node at (3.5,0.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	333	\node at (5.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	334	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	335	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	336	\draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	337	\draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	338	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	339	\only<3>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	340	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	341	\draw[very thick, blue!50] (3,0) rectangle (6,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	342	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	343	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	344	\node at (3.5,0.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	345	\node at (5.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	346	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	347	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	348	\draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	349	\draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	350	\draw[very thick,blue!100] (3,3) rectangle (4,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	351	\node at (3.5,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	352	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	353	\only<4>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	354	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	355	\draw[very thick, blue!50] (3,0) rectangle (6,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	356	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	357	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	358	\node at (3.5,0.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	359	\node at (5.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	360	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	361	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	362	\draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	363	\draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	364	\draw[very thick,blue!100] (3,3) rectangle (4,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	365	\node at (3.5,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	366	\draw[very thick,blue!100] (4,3) rectangle (5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	367	\node at (4.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	368	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	369	\only<5>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	370	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	371	\draw[very thick, blue!50] (3,3) rectangle (6,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	372	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	373	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	374	\node at (3.5,3.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	375	\node at (5.7,3.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	376	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	377	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	378	\draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	379	\draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	380	\draw[very thick,blue!100] (6,3) rectangle (7,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	381	\node at (6.5,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	382	\draw[very thick,blue!100] (7,3) rectangle (8,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	383	\node at (7.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	384	\draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	385	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	386	\only<6>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	387	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	388	\draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	389	\draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	390	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	391	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	392	\node at (3.5,3.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	393	\node at (5.7,3.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	394	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	395	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	396	\draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	397	\draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	398	\draw[very thick,blue!100] (6,3) rectangle (7,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	399	\node at (6.5,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	400	\draw[very thick,blue!100] (7,3) rectangle (8,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	401	\node at (7.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	402	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	403	\only<7>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	404	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	405	\draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	406	\draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	407	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	408	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	409	\node at (3.5,3.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	410	\node at (5.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	411	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	412	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	413	\draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	414	\draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	415	\draw[very thick,blue!100] (6,3) rectangle (7,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	416	\node at (6.5,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	417	\draw[very thick,blue!100] (7,3) rectangle (8,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	418	\node at (7.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	419	\draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	420	\draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	421	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	422	\only<8>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	423	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	424	\draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	425	\draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	426	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	427	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	428	\node at (3.5,3.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	429	\node at (6.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	430	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	431	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	432	\draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	433	\draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	434	\draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	435	\node at (4,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	436	\draw[very thick,blue!100] (7,3) rectangle (8,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	437	\node at (7.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	438	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	439	\only<9>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	440	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	441	\draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	442	\draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	443	\draw[very thick, blue!50] (5,0) rectangle (7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	444	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	445	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	446	\node at (3.5,3.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	447	\node at (6.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	448	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	449	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	450	\draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	451	\draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	452	\draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	453	\node at (4,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	454	\draw[very thick,blue!100] (7,3) rectangle (8,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	455	\node at (7.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	456	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	457	\only<10>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	458	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	459	\draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	460	\draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	461	\draw[very thick, blue!50] (5,0) rectangle (7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	462	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	463	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	464	\node at (3.5,3.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	465	\node at (6.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	466	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	467	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	468	\draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	469	\draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	470	\draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	471	\node at (4,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	472	\draw[very thick,blue!100] (7,3) rectangle (8,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	473	\node at (7.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	474	\draw[red, fill] (5,1.5) rectangle (6,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	475	\draw[red, fill] (6.05,1.5) rectangle (7,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	476	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	477	\only<11>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	478	\draw[fill, blue!50] (1,0) rectangle (3,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	479	\draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	480	\draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	481	\draw[very thick, blue!50] (5,0) rectangle (7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	482	\node at (1.5,0.9) {\small $A_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	483	\node at (2.0,0.9) {\small $B_L$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	484	\node at (3.5,3.9) {\small $A_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	485	\node at (6.7,0.9) {\small $B_R$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	486	\draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	487	\draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	488	\draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	489	\draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	490	\draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	491	\node at (4,3.3) {\small $A$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	492	\draw[very thick,blue!100] (7,3) rectangle (8,3.6);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	493	\node at (7.5,3.3) {\small $B$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	494	\draw[red, fill] (5,1.5) rectangle (6,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	495	\draw[red, fill] (6.05,1.5) rectangle (7,2.1);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	496	\draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	497	\draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	498	}
76 dde58256fc35 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 75 diff changeset	499
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	500	\draw[very thick,->](0,0) -- (8,0);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	501	\node [anchor=base] at (8, -0.3) {\scriptsize time};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	502	\node [anchor=base] at (0, -0.3) {\scriptsize 0};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	503	\node [anchor=base] at (-1.2, 0.2) {\small low priority};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	504	\only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	505	\only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	506
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	507	\end{tikzpicture}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	508	\end{tabular}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	509	\end{textblock}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	510
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	511	\begin{textblock}{0}(2.5,13)%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	512	\small
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	513	\onslide<11>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	514	\begin{bubble}[8cm]%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	515	Scheduling: You want to avoid that a high
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	516	priority process is staved indefinitely.
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	517	\end{bubble}}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	518	\end{textblock}
79 2eaca58f9bcc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 78 diff changeset	519
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	520
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	521	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	522	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	523
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	524	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	525	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	526	\frametitle{\Large Priority Inheritance Scheduling}
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	527
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	528	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	529	\item Let a low priority process $L$ temporarily inherit
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	530	the high priority of $H$ until $L$ leaves the critical
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	531	section unlocking the resource.\bigskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	532	\item Once the resource is unlocked $L$ returns to its original
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	533	priority level. \alert{\bf BOGUS}\pause\bigskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	534	\item \ldots $L$ needs to switch to the highest
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	535	\alert{remaining} priority of the threads that it blocks.
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	536	\end{itemize}\bigskip
76 dde58256fc35 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 75 diff changeset	537
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	538	\small this error is already known since around 1999
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	539
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	540	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	541	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
76 dde58256fc35 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 75 diff changeset	542
dde58256fc35 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 75 diff changeset	543	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	544	\begin{frame}[c]
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	545
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	546	\begin{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	547	\includegraphics[scale=0.25]{../pics/p3.jpg}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	548	\end{center}
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	549
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	550	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	551	\item by Rajkumar, 1991
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	552	\item \it ``it resumes the priority it had at the point of entry into the critical
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	553	section''
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	554	\end{itemize}
148 083c07f8668a added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	555
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	556	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	557	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	558
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	559
161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	560	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	561	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	562
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	563	\begin{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	564	\includegraphics[scale=0.25]{../pics/p2.jpg}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	565	\end{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	566
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	567	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	568	\item by Jane Liu, 2000
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	569	\item {\it ``The job $J_l$ executes at its inherited
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	570	priority until it releases $R$; at that time, the
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	571	priority of $J_l$ returns to its priority
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	572	at the time when it acquires the resource $R$.''}\medskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	573	\item \small gives pseudo code and totally bogus data structures
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	574	\item \small interesting part ``{\it left as an exercise}''
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	575	\end{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	576
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	577	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	578	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	579
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	580	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	581	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	582
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	583	\begin{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	584	\includegraphics[scale=0.15]{../pics/p1.pdf}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	585	\end{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	586
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	587	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	588	\item by Laplante and Ovaska, 2011 (\$113.76)
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	589	\item \it ``when $[$the task$]$ exits the critical section that
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	590	caused the block, it reverts to the priority it had
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	591	when it entered that section''
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	592	\end{itemize}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	593
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	594	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	595	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	596
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	597	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	598	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	599	\frametitle{Priority Scheduling}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	600
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	601	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	602	\item a scheduling algorithm that is widely used in real-time operating systems
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	603	\item has been ``proved'' correct by hand in a paper in 1983
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	604	\item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	605
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	606	\item we corrected the algorithm and then {\bf really} proved that it is correct
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	607	\item we implemented this algorithm in a small OS called PINTOS (used for teaching at Stanford)
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	608	\item our implementation was much more efficient than their reference implementation
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	609	\end{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	610
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	611	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	612	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	613
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	614
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	615	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	616	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	617	\frametitle{Design of AC-Policies}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	618
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	619	\Large
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	620	\begin{quote}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	621	''what you specify is what you get but not necessarily what you want\ldots''
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	622	\end{quote}\bigskip\bigskip\bigskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	623
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	624	\normalsize main work by Chunhan Wu (PhD-student)
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	625
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	626	\end{frame}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	627	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	628
ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	629	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	630	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	631	\frametitle{Testing Policies}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	632
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	633	\begin{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	634	\begin{tikzpicture}[scale=1]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	635	%\draw[black!10,step=2mm] (-5,-3) grid (5,4);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	636	%\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	637	\draw[white,thick,step=10mm] (-5,-3) grid (5,4);
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	638
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	639	\draw [black!20, line width=1mm] (0,0) circle (1cm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	640	\draw [line width=1mm] (0,0) circle (3cm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	641	\node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	642
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	643	\draw [red, line width=2mm, <-] (-2.1,2.1) -- (-3.5,3.2);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	644	\node at (-3.5,3.6) {your system};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	645	\node at (-4.8,0) {\Large policy $+$};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	646
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	647
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	648	\only<2>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	649	\draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	650	\draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	651	\node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	652
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	653	\only<3>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	654	\draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	655	\node[white] at (2,1) {\small tainted};}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	656
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	657	\only<4>{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	658	\begin{scope}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	659	\draw [clip] (0,0) circle (2.955cm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	660	\draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	661	\node[white] at (2,1) {\small tainted};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	662	\end{scope}}
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	663
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	664	\only<5->{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	665	\begin{scope}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	666	\draw [clip] (0,0) circle (2.955cm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	667	\draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	668	\node[white] at (2,1) {\small tainted};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	669	\end{scope}}
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	670
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	671	\only<6->{
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	672	\draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	673	\draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm);
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	674	\node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	675	}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	676
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	677	\end{tikzpicture}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	678	\end{center}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	679
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	680	\end{frame}
83 161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	681	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	682
161ec08d70f8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	683	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	684	\begin{frame}[c]
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	685	\frametitle{A Sound and Complete Test}
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	686
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	687	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	688	\item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	689
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	690	\item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	691	\smallskip
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	692	\begin{itemize}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	693	\item suppose a tainted file has type \emph{bin} and
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	694	\item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	695	\item then we would conclude that this tainted file can spread\medskip\pause
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	696	\item but if there is no process with role \bl{$r$} and it will never been
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	697	created, then the file actually does not spread
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	698	\end{itemize}\bigskip\pause
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	699
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	700	\item \alert{our solution:} take a middle ground and record precisely the information
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	701	of the initial state, but be less precise about every newly created object.
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	702	\end{itemize}
77 56dbc339ec87 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 76 diff changeset	703
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	704	\end{frame}}
54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	705	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	706
ab38ed748930 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	707	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
149 66623e169581 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	708	\begin{frame}[c]
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	709	\frametitle{Random Number Generators}
87 e0908dc30b7c added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 86 diff changeset	710
331 54a1fbe96b14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	711	\end{frame}
87 e0908dc30b7c added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 86 diff changeset	712	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
76 dde58256fc35 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 75 diff changeset	713	\end{document}
75 df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	714
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	715	%%% Local Variables:
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	716	%%% mode: latex
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	717	%%% TeX-master: t
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	718	%%% End:
df7cf3d07bd8 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	719

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 25 Nov 2014 02:04:48 +0000
changeset 331	54a1fbe96b14
parent 151	f8dc3dbdaa5c
child 332	8eab185fb187
permissions	-rw-r--r--