--- a/Journal/Paper.thy Thu Jun 20 23:28:26 2013 -0400
+++ b/Journal/Paper.thy Tue Feb 25 20:01:47 2014 +0000
@@ -3,19 +3,9 @@
imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
begin
-(*
-find_unused_assms CpsG
-find_unused_assms ExtGG
-find_unused_assms Moment
-find_unused_assms Precedence_ord
-find_unused_assms PrioG
-find_unused_assms PrioGDef
-*)
-ML {*
- open Printer;
- show_question_marks_default := false;
- *}
+declare [[show_question_marks = false]]
+
notation (latex output)
Cons ("_::_" [78,77] 73) and
@@ -38,9 +28,7 @@
original_priority ("priority") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
-(*abbreviation
- "detached s th \<equiv> cntP s th = cntV s th"
-*)
+
(*>*)
section {* Introduction *}
@@ -96,12 +84,15 @@
ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
example in libraries for FreeBSD, Solaris and Linux.
- One advantage of PIP is that increasing the priority of a thread
- can be performed dynamically by the scheduler. This is in contrast
- to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
- solution to the Priority Inversion problem, which requires static
- analysis of the program in order to prevent Priority
- Inversion. However, there has also been strong criticism against
+ Two advantages of PIP are that increasing the priority of a thread
+ can be performed dynamically by the scheduler and is deterministic.
+ This is in contrast to \emph{Priority Ceiling}
+ \cite{Sha90}, another solution to the Priority Inversion problem,
+ which requires static analysis of the program in order to prevent
+ Priority Inversion, and also to the Windows NT scheduler, which avoids
+ this problem by randomly boosting the priority of ready (low priority) threads
+ (e.g.~\cite{WINDOWSNT}).
+ However, there has also been strong criticism against
PIP. For instance, PIP cannot prevent deadlocks when lock
dependencies are circular, and also blocking times can be
substantial (more than just the duration of a critical section).
@@ -160,7 +151,10 @@
correctness of a high-level specification of PIP in a theorem prover
is that such issues clearly show up and cannot be overlooked as in
informal reasoning (since we have to analyse all possible behaviours
- of threads, i.e.~\emph{traces}, that could possibly happen).\medskip
+ of threads, i.e.~\emph{traces}, that could possibly happen).\footnote{While
+ \cite{Sha90} is the only formal publication we have
+ found that describes the incorrect behaviour, not all, but many
+ informal descriptions of PIP overlook the case...}\medskip
\noindent
{\bf Contributions:} There have been earlier formal investigations
@@ -335,26 +329,26 @@
\noindent
If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:
- \begin{figure}[h]
+ \begin{figure}[ph]
\begin{center}
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}
\begin{tikzpicture}[scale=1]
%%\draw[step=2mm] (-3,2) grid (1,-1);
- \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
- \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
- \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
- \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
- \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
- \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
- \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+ \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>0"}};
+ \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>1"}};
+ \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>1"}};
+ \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>2"}};
+ \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>2"}};
+ \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>3"}};
+ \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>3"}};
- \node (X) at (0,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>4"}};
- \node (Y) at (2,-2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>4"}};
- \node (Z) at (2,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>5"}};
- \node (U1) at (4,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>5"}};
- \node (U2) at (4,-2.9) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>6"}};
- \node (R) at (6,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>6"}};
+ \node (X) at (0,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>4"}};
+ \node (Y) at (2,-2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>4"}};
+ \node (Z) at (2,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>5"}};
+ \node (U1) at (4,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>5"}};
+ \node (U2) at (4,-2.9) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>6"}};
+ \node (R) at (6,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>6"}};
\draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B);
\draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
@@ -397,10 +391,10 @@
This definition needs to account for all threads that wait for a thread to
release a resource. This means we need to include threads that transitively
wait for a resource being released (in the picture above this means the dependants
- of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"},
- but also @{text "th\<^isub>3"},
- which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
- in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies
+ of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"},
+ but also @{text "th\<^sub>3"},
+ which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
+ in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies
in a RAG, then clearly
we have a deadlock. Therefore when a thread requests a resource,
we must ensure that the resulting RAG is not circular. In practice, the
@@ -638,7 +632,7 @@
\noindent
Note, however, that apart from the circularity condition, we do not make any
- assumption on how different resources can locked and released relative to each
+ assumption on how different resources can be locked and released relative to each
other. In our model it is possible that critical sections overlap. This is in
contrast to Sha et al \cite{Sha90} who require that critical sections are
properly nested.
@@ -803,9 +797,9 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
- @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
- @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+ @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\
+ @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\
+ @{thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]}
\end{tabular}
\end{isabelle}
@@ -904,7 +898,7 @@
%\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
% @ {thm [display] chain_building[rule_format]}
%\item The ready thread chased to is unique (@{text "dchain_unique"}):
- % @ {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+ % @ {thm [display] dchain_unique[of _ _ "th\<^sub>1" "th\<^sub>2"]}
%\end{enumerate}
%Some deeper results about the system:
@@ -1076,7 +1070,7 @@
\end{isabelle}
\noindent
- This means in an implementation we do not have recalculate the @{text RAG} and also none of the
+ This means in an implementation we do not have to recalculate the @{text RAG} and also none of the
current precedences of the other threads. The current precedence of the created
thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
\smallskip
@@ -1453,7 +1447,7 @@
PIP is a scheduling algorithm for single-processor systems. We are
now living in a multi-processor world. Priority Inversion certainly
- occurs also there, see for example \cite{Brandenburg11, Davis11}.
+ occurs also there, see for example \cite{Brandenburg11,Davis11}.
However, there is very little ``foundational''
work about PIP-algorithms on multi-processor systems. We are not
aware of any correctness proofs, not even informal ones. There is an
--- a/Journal/document/root.bib Thu Jun 20 23:28:26 2013 -0400
+++ b/Journal/document/root.bib Tue Feb 25 20:01:47 2014 +0000
@@ -1,3 +1,14 @@
+@INPROCEEDINGS{WINDOWSNT,
+ author={L.~Budin and L.~Jelenkovic},
+ booktitle={Proc.~of the IEEE International Symposium on
+ Industrial Electronics (ISIE)},
+ title={{T}ime-{C}onstrained {P}rogramming in {W}indows {NT} {E}nvironment},
+ year={1999},
+ volume={1},
+ pages={90--94},
+ }
+
+
@article{seL4,
author = {G.~Klein and
J.~Andronick and
--- a/Journal/document/root.tex Thu Jun 20 23:28:26 2013 -0400
+++ b/Journal/document/root.tex Tue Feb 25 20:01:47 2014 +0000
@@ -1,7 +1,8 @@
-\documentclass{article}
-\textwidth 130mm
-\textheight 200mm
-\renewenvironment{abstract}{\section*{Abstract}\small}{}
+%\documentclass{article}
+\documentclass{llncs}
+%\textwidth 130mm
+%\textheight 200mm
+%\renewenvironment{abstract}{\section*{Abstract}\small}{}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
@@ -37,12 +38,12 @@
\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
\definecolor{mygrey}{rgb}{.80,.80,.80}
-\newtheorem{definition}{Definition}
-\newtheorem{theorem}[definition]{Theorem}
-\newtheorem{lemma}[definition]{Lemma}
-\newtheorem{proof}{Proof}
-\renewcommand{\theproof}{}
-\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}}
+%\newtheorem{definition}{Definition}
+%\newtheorem{theorem}[definition]{Theorem}
+%\newtheorem{lemma}[definition]{Lemma}
+%\newtheorem{proof}{Proof}
+%\renewcommand{\theproof}{}
+%\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}}
\begin{document}
@@ -51,9 +52,9 @@
\renewcommand{\thefootnote}{\arabic{footnote}}
\title{Priority Inheritance Protocol Proved Correct}
-\author{Xingyuan Zhang, Christian Urban and Chunhan Wu}
-%\institute{PLA University of Science and Technology, China \and
-% King's College London, United Kingdom}
+\author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$}
+\institute{PLA University of Science and Technology, China \and
+ King's College London, United Kingdom}
\maketitle
\begin{abstract}
--- a/Paper/Paper.thy Thu Jun 20 23:28:26 2013 -0400
+++ b/Paper/Paper.thy Tue Feb 25 20:01:47 2014 +0000
@@ -336,13 +336,13 @@
\begin{tikzpicture}[scale=1]
%%\draw[step=2mm] (-3,2) grid (1,-1);
- \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
- \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
- \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
- \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
- \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
- \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
- \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+ \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>0"}};
+ \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>1"}};
+ \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>1"}};
+ \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>2"}};
+ \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>2"}};
+ \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>3"}};
+ \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>3"}};
\draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B);
\draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
@@ -366,10 +366,10 @@
This definition needs to account for all threads that wait for a thread to
release a resource. This means we need to include threads that transitively
wait for a resource being released (in the picture above this means the dependants
- of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"},
- but also @{text "th\<^isub>3"},
- which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
- in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies
+ of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"},
+ but also @{text "th\<^sub>3"},
+ which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
+ in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies
in a RAG, then clearly
we have a deadlock. Therefore when a thread requests a resource,
we must ensure that the resulting RAG is not circular. In practice, the
@@ -763,9 +763,9 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
- @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
- @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+ @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\
+ @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\
+ @{thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]}
\end{tabular}
\end{isabelle}
@@ -864,7 +864,7 @@
%\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
% @ {thm [display] chain_building[rule_format]}
%\item The ready thread chased to is unique (@{text "dchain_unique"}):
- % @ {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+ % @ {thm [display] dchain_unique[of _ _ "th\<^sub>1" "th\<^sub>2"]}
%\end{enumerate}
%Some deeper results about the system:
@@ -1335,8 +1335,8 @@
We are grateful for the comments we received from anonymous
referees.
- \bibliographystyle{plain}
- \bibliography{root}
+ %\bibliographystyle{plain}
+ %\bibliography{root}
*}
--- a/ROOT Thu Jun 20 23:28:26 2013 -0400
+++ b/ROOT Tue Feb 25 20:01:47 2014 +0000
@@ -4,7 +4,7 @@
"ExtGG"
session "Slides2" in "Slides" = PIP +
- options [document = pdf, browser_info = false, document_output = "..", document_variants="slides2"]
+ options [document_variants="slides2"]
theories [document = false]
"~~/src/HOL/Library/LaTeXsugar"
theories[document = true]
@@ -19,4 +19,21 @@
theories[document = true, show_question_marks = false]
"Slides3"
files
- "document/build"
\ No newline at end of file
+ "document/build"
+
+session "Slides4" in "Slides" = PIP +
+ options [document = pdf, browser_info = false, document_output = "..",
+document_variants="slides4"]
+ theories [document = false]
+ "~~/src/HOL/Library/LaTeXsugar"
+ theories[document = true, show_question_marks = false]
+ "Slides4"
+ files
+ "document/build"
+
+
+session Journal in "Journal" = PIP +
+ options [document = pdf, document_output = "..", document_variants="journal"]
+ theories
+ "~~/src/HOL/Library/LaTeXsugar"
+ "Paper"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides4.thy Tue Feb 25 20:01:47 2014 +0000
@@ -0,0 +1,966 @@
+(*<*)
+theory Slides4
+imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+(*
+ML {*
+ open Printer;
+ show_question_marks_default := false;
+ *}
+*)
+
+notation (latex output)
+ Cons ("_::_" [78,77] 73) and
+ vt ("valid'_state") and
+ runing ("running") and
+ birthtime ("last'_set") and
+ If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+ Prc ("'(_, _')") and
+ holding ("holds") and
+ waiting ("waits") and
+ Th ("T") and
+ Cs ("C") and
+ P ("Lock") and
+ V ("Unlock") and
+ readys ("ready") and
+ depend ("RAG") and
+ preced ("prec") and
+ cpreced ("cprec") and
+ dependents ("dependants") and
+ cp ("cprec") and
+ holdents ("resources") and
+ original_priority ("priority") and
+ DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
+
+(*>*)
+
+
+
+text_raw {*
+ \renewcommand{\slidecaption}{NASA, 20 June 2013}
+ \newcommand{\bl}[1]{#1}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\[-3mm]
+ \LARGE Formalisations and the\\[-1mm]
+ \LARGE Isabelle Theorem Prover\\[-3mm]
+ \end{tabular}}
+
+ \begin{center}
+ Christian Urban\\[1mm]
+ \small King's College London
+ \end{center}\bigskip
+
+ \begin{center}
+ many thanks to Mahyar Malekpour and Cesar Munoz for the invitation and
+ hospitality
+ \end{center}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<2->[c]
+ \frametitle{Isabelle Theorem Prover}
+
+ \begin{center}
+ \includegraphics[scale=0.23]{isabelle.png}
+ \end{center}
+
+ \only<2>{
+ \begin{textblock}{12}(2,13.6)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\normalsize\color{darkgray}
+ \begin{minipage}{9cm}\raggedright
+ \ldots to make sure large proofs are correct
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ \tikzstyle{node1}=[rectangle, minimum size=8mm, rounded corners=3mm, very thick,
+ draw=black!50, top color=white, bottom color=black!20]
+ \tikzstyle{node2}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
+ draw=red!70, top color=white, bottom color=red!50!black!20]
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+
+ \begin{tabular}{@ {}c@ {\hspace{2mm}}c}
+ \\[6mm]
+ \begin{tabular}{c}
+ \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
+ {\footnotesize Bob Harper}\\[-2.5mm]
+ {\footnotesize (CMU)}
+ \end{tabular}
+ \begin{tabular}{c@ {}}
+ \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
+ {\footnotesize Frank Pfenning}\\[-2.5mm]
+ {\footnotesize (CMU)}
+ \end{tabular} &
+
+ \begin{tabular}{@ {\hspace{-3mm}}p{7cm}}
+ \begin{tikzpicture}[remember picture, scale=0.5]
+ \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+ { \& \& \node (desc) {\makebox[0mm]{\begin{tabular}{l}published in a journal\\
+ \small (ACM ToCL, 31 pages, 2005)\\[3mm]\end{tabular}}};\\
+ \&[-10mm]
+ \node (def1) [node1] {\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+ \node (proof1) [node1] {Proof}; \&
+ \node (alg1) [node1] {\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+ };
+ \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+ \draw[<-,black,line width=0.5mm] (proof1) -- (desc);
+ \end{tikzpicture}
+ \end{tabular}\\
+
+ \pause
+ \\[0mm]
+
+ \multicolumn{2}{c}{
+ \begin{tabular}{p{6cm}}
+ \raggedright
+ \color{black}{relied on their proof in a\\ {\bf security} critical application}
+ \end{tabular}
+
+ \begin{tabular}{c}
+ \includegraphics[scale=0.36]{appel.jpg}\\[-2mm]
+ {\footnotesize Andrew Appel}\\[-2.5mm]
+ {\footnotesize (Princeton)}
+ \end{tabular}}
+ \end{tabular}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<4->
+ \frametitle{\LARGE\begin{tabular}{c}An Example for a Small TCB\end{tabular}}
+ \mbox{}\\[-14mm]\mbox{}
+
+ \begin{columns}
+ \begin{column}{0.2\textwidth}
+ \begin{tabular}{@ {} c@ {}}
+ \includegraphics[scale=0.3]{appel.jpg}\\[-2mm]
+ {\footnotesize Andrew Appel}\\[-2.5mm]
+ {\footnotesize (Princeton)}
+ \end{tabular}
+ \end{column}
+
+ \begin{column}{0.8\textwidth}
+ \begin{textblock}{10}(4.5,3.95)
+ \begin{block}{Proof-Carrying Code:}
+ \begin{center}
+ \begin{tikzpicture}
+ \draw[help lines,cream] (0,0.2) grid (8,4);
+
+ \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
+ \node[anchor=base] at (6.5,2.8)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering user can run untrusted code\end{tabular}};
+
+ \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
+ \node[anchor=base] at (1.5,2.3)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering code developer/ web server/ Apple
+ Store\end{tabular}};
+
+ \onslide<4->{
+ \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
+ \node[anchor=base,white] at (6.5,1.1)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
+
+ \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
+ \onslide<3->{
+ \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};
+ \node at (3.8,1.9) {\small certificate};
+ }
+
+ \onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}
+ % Code Developer
+ % User (runs untrusted code)
+ % transmits a proof that the code is safe
+ %
+ \end{tikzpicture}
+ \end{center}
+ \end{block}
+ \end{textblock}
+ \end{column}
+ \end{columns}
+
+ \small\mbox{}\\[3.2cm]
+ \begin{itemize}
+ \item<4-> TCB of the checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions;
+ 803 loc in C including 2 library functions)\\[-3mm]
+ \item<4-> 167 loc in C implement a type-checker
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+
+
+text_raw {*
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
+ draw=black!50, top color=white, bottom color=black!20]
+ \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
+ draw=red!70, top color=white, bottom color=red!50!black!20]
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<2->[squeeze]
+ \frametitle{}
+
+ \begin{columns}
+
+ \begin{column}{0.8\textwidth}
+ \begin{textblock}{0}(1,2)
+
+ \begin{tikzpicture}
+ \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+ { \&[-10mm]
+ \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+ \node (proof1) [node1] {\large Proof}; \&
+ \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+
+ \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \&
+ \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+ \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+
+ \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+ \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\
+
+ \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+ \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+ };
+
+ \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+
+ \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);}
+ \end{tikzpicture}
+
+ \end{textblock}
+ \end{column}
+ \end{columns}
+
+
+ \begin{textblock}{3}(12,3.6)
+ \onslide<4->{
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Other Formalisations}
+
+
+ \begin{itemize}
+ \item I also found a (fixable) mistake in my PhD thesis\bigskip
+
+ \item Nominal Isabelle: found out that the variable convention
+ can be used to prove false (a surprising result in PL-research)\bigskip
+
+ \item Computability and Logic Book (5th ed.)\\ by Boolos, Burgess and Jeffrey ---
+ two definitions about halting computations in UTMs are inconsistent
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Scheduling in RTOS}
+
+ \begin{itemize}
+ \item RTOS: priorities and resource locking
+
+ \item Purpose:\\
+ guarantee tasks to be completed in time\medskip\pause
+
+ \item \alert{this already results into a surprisingly non-trivial algorithmic problem}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{The Problem}
+ \Large
+
+ \begin{center}
+ \begin{tabular}{l}
+ \alert{H}igh-priority process (waits)\\[4mm]
+ \onslide<2->{\alert{M}edium-priority process}\\[4mm]
+ \alert{L}ow-priority process (has a lock)\\[4mm]
+ \end{tabular}
+ \end{center}
+
+ \onslide<3->{
+ \begin{itemize}
+ \item \alert{priority inversion}\\ \hspace{2cm}@{text "\<equiv>"} H waits for a process\\
+ \mbox{}\hfill with lower priority
+ \item<4> avoid \alert{indefinite} priority inversion
+ \end{itemize}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Mars Pathfinder Mission 1997}
+ \large
+
+ \begin{center}
+ \includegraphics[scale=0.15]{marspath1.png}
+ \includegraphics[scale=0.16]{marspath3.png}
+ \includegraphics[scale=0.3]{marsrover.png}
+ \end{center}
+
+ \begin{itemize}
+ \item the lander reset frequently on Mars
+ \item the problem: priority inversion
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{The Solution}
+ \Large
+
+ \alert{Priority Inheritance Protocol (PIP):}\bigskip
+
+ \begin{center}
+ \begin{tabular}{l}
+ \alert{H}igh-priority process\\[4mm]
+ \textcolor{gray}{Medium-priority process}\\[4mm]
+ \alert{L}ow-priority process\\[15mm]
+ {\normalsize (temporarily raise the priority of \alert{L})}
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{A First Correctness ``Proof''}
+ \Large
+
+ \begin{itemize}
+ \item the paper$^\star$ first describing PIP ``proved'' also its
+ correctness:\\[5mm]
+ \end{itemize}
+
+ \normalsize
+ \begin{quote}
+ \ldots{}after the thread (whose priority has been raised) completes its
+ critical section and releases the lock, it ``returns to its original
+ priority level''.
+ \end{quote}\bigskip
+
+ \small
+ $^\star$ in IEEE Transactions on Computers in 1990 by Sha et al.
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+ \Large
+
+ \begin{center}
+ \begin{tabular}{l}
+ \alert{H}igh-priority process 1 (waits)\\[2mm]
+ \alert{H}igh-priority process 2 (waits)\\[8mm]
+ \alert{L}ow-priority process (has a lock)
+ \end{tabular}
+ \end{center}
+
+ \onslide<2->{
+ \begin{itemize}
+ \item Solution: return to the highest
+ \phantom{Solution:} \alert{remaining} priority\\
+ \end{itemize}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Specification}
+ \Large
+
+ \begin{itemize}\Large
+ \item Use Inductive Method with events of the form:
+ \end{itemize}
+
+ \begin{center}
+ \begin{tabular}{l}
+ Create \textcolor{gray}{thread priority}\\
+ Exit \textcolor{gray}{thread}\\
+ Set \textcolor{gray}{thread priority}\\
+ Lock \textcolor{gray}{thread cs}\\
+ Unlock \textcolor{gray}{thread cs}\\
+ \end{tabular}
+ \end{center}\medskip
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Scheduling States}
+ \Large
+
+ \begin{itemize}
+ \item A \alert{state s} is a list of events\bigskip
+ \begin{center}
+ \begin{tikzpicture}
+ \draw [->, line width=1.5mm] (-4,0) -- (4, 0);
+ \draw [line width=0.8mm] (-4, 0.3) -- (-4, -0.3);
+ \draw [line width=0.8mm] (1, 0.3) -- (1, -0.3);
+ \node at (1,-0.7) {\large s};
+ \node at (-4,-0.7) {\large 0};
+ \node at (3.2,-0.7) {\large time};
+ \end{tikzpicture}
+ \end{center}\pause
+
+ \item Scheduling according to \alert{precedences}:
+ \begin{center}
+ \begin{tabular}{@ {}l@ {}}
+ \large @{thm preced_def[where thread="th"]}
+ \end{tabular}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Waiting Queues}
+ \large
+
+ \begin{itemize}
+ \item A \alert{waiting queue} function returns a list of threads
+ associated with every resource
+ \item The head of the list is the thread holding the resource.
+ \medskip
+
+ \begin{center}\normalsize
+ \begin{tabular}{@ {}l}
+ @{thm cs_holding_def[where thread="th"]}\\
+ @{thm cs_waiting_def[where thread="th"]}
+ \end{tabular}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Resource Allocation Graphs}
+
+\begin{center}
+ \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
+ \begin{tikzpicture}[scale=1]
+
+ \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
+ \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
+ \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
+ \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
+ \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+ \node (E1) at (6, 0.3) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
+ \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+
+ \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds} (B);
+ \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waits} (B);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waits} (B);
+ \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holds} (E);
+ \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds} (E1);
+ \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waits} (E);
+ \end{tikzpicture}
+ \end{center}\bigskip
+
+ \begin{center}
+ \begin{minipage}{0.8\linewidth}
+ \raggedleft
+ @{thm cs_depend_def}
+ \end{minipage}\medskip\\
+ \begin{minipage}{1\linewidth}
+ @{thm cs_dependents_def}
+ \end{minipage}\medskip\\\pause
+ \begin{minipage}{1\linewidth}
+ \alert{cprec wq s th} $\dn$\\
+ \mbox{}\hspace{1cm}Max(\{prec th s\} $\cup$\\
+ \mbox{}\hspace{1cm}\phantom{Max(}\{prec th' s $\mid$ th' $\in$ dependants wq th\})
+ \end{minipage}
+ \end{center}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{The Scheduler}
+ \large
+
+ \begin{itemize}
+ \item \underline{Start}: all priorities/precedences are 0, all resources are unlocked
+ \item \underline{Create th p}: set precedence of th
+ \item \underline{Exit th}: reset precedence to 0
+ \item \underline{Set th p}: reset precedence of th
+ \item \underline{Lock th cs}: add th to the end of the waiting queue of cs
+ \item \underline{Unlock th cs}:\\ delete th from the waiting queue of cs\\
+ \hspace{1cm}\alert{and who to give the resource next?}
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{The Scheduler (2)}
+ %%\large
+
+ \begin{itemize}
+ \item \large threads ready to run\normalsize
+
+ \begin{center}
+ \begin{tabular}{@ {}l}
+ @{thm (lhs) readys_def} $\dn$\\
+ \;@{thm (rhs) readys_def}
+ \end{tabular}
+ \end{center}\bigskip
+
+ \item \large the thread that is running in a state:\\[-10mm]\normalsize
+ \begin{center}
+ \begin{tabular}{@ {}l@ {}}
+ @{thm (lhs) runing_def} $\dn$\\
+ \;@{thm (rhs) runing_def}
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Inductive Method}
+ %%\large
+
+ \begin{center}
+\begin{tikzpicture}[scale=1.6]
+%%\draw[step=2mm] (-4,-1) grid (4,1.4);
+\draw (0,0.2) node {\begin{tabular}{l} valid\\[-1mm] scheduler\\[-1mm] states\\ \end{tabular}};
+\draw (3,0) node {\begin{tabular}{l} set of invalid\\[-1mm] scheduler states \\[-1mm](e.g., deadlocks)\\ \end{tabular}};
+\draw[<-, line width=0.5mm] (1.0,0) -- (1.8,0);
+\draw[<-, line width=0.5mm] (-0.2,-0.55) -- (-0.4,-1.3);
+\draw (-0.0,-1.5) node {\begin{tabular}{l} inductively defined set \end{tabular}};
+
+\draw[line width=0.5mm, rounded corners=6.3pt]
+ (-0.9,-0.05) -- (-0.8,0.6) -- (-0.3,0.95) -- (0,1) -- (0.5,0.8) -- (0.65,0.5) -- (0.7,0) -- (0.4,-0.5) -- (0,-0.6) -- (-0.5,-0.45) -- cycle;
+
+\draw[line width=0.5mm, rounded corners=15pt]
+ (-1.2,0) -- (-0.9,0.95) -- (0,1.2) -- (1.0,1.0) -- (1.7,0) -- (0.95,-1.0) -- (0,-1.2) -- (-0.9,-0.9) -- cycle;
+
+\end{tikzpicture}
+\end{center}
+
+ \begin{itemize}
+ \item We have to exclude situations where there is a deadlock,
+ a thread exited before created, \ldots
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Valid Next Events}
+ \large
+
+ \begin{itemize}
+ \item In a state s, the following events can occur:
+ \end{itemize}
+
+ \begin{center}
+ @{thm[mode=Rule] thread_create[where thread=th]}\bigskip
+
+ @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip
+
+ @{thm[mode=Rule] thread_set[where thread=th]}
+ \end{center}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Valid Next Events (2)}
+ \large
+
+ \begin{center}
+ @{thm[mode=Rule] thread_P[where thread=th]}\bigskip
+
+ @{thm[mode=Rule] thread_V[where thread=th]}\bigskip
+ \end{center}\bigskip\pause
+
+ \begin{itemize}
+ \item Done with the specification. \ldots
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Correctness Criterion}
+ \large
+
+
+ \begin{center}
+ \begin{tikzpicture}
+ \draw [->, line width=1.5mm] (-4,0) -- (4, 0);
+ \draw [line width=0.8mm] (-4, 0.3) -- (-4, -0.3);
+ \draw [line width=0.8mm] (1, 0.3) -- (1, -0.3);
+ \draw [line width=0.8mm] (0, 0.3) -- (0, -0.3);
+ \node at (1,-0.7) {\large s'};
+ \node at (0,-0.7) {\large s};
+ \node at (1,-1.5) {\small(th')};
+ \node at (0,-1.5) {\small(th)};
+ \node at (-4,-0.7) {\large 0};
+ \node at (3.2,-0.7) {\large time};
+ \end{tikzpicture}
+ \end{center}
+
+ \normalsize
+ \begin{itemize}
+ \item {\bf If} th is alive in s and has the highest precedence
+ \item plus some further assumption (like th not reset, not exited, no higher precedences in s - s')
+ \item and th is {\bf not} running in s', \\ {\bf then} the running
+ thread th' (in s') is a thread that was alive in {\bf s} and has in s' the same
+ precedence as th in s.
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Implementation}
+
+
+ \begin{itemize}
+ \item Create/Exit events:
+ \begin{itemize}
+ \item we do not have to recalculate the RAG
+ \item we do not have to recalculate the other precedences
+ \end{itemize}\bigskip
+ \item Set event:
+ \begin{itemize}
+ \item we do not have to recalculate the RAG
+ \item also the other precedences do not have to be recalculated
+ (since this is the currently running thread, it cannot affect
+ other threads)
+ \end{itemize}
+ \item Unlock event (2 cases: a thread to take over, no thread to take over)
+ \begin{itemize}
+ \item case 1: RAG needs to be modified, but apart from th and th' no
+ other precedence needs to be recalculated
+ \item case 2: RAG needs to be prunned, no precedence needs to be recalculated
+ \end{itemize}
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Implementation (2)}
+
+
+ \begin{itemize}
+ \item Unlock event (2 cases: a thread to take over, no thread to take over)
+ \begin{itemize}
+ \item case 1: RAG needs to be modified, but apart from th and th' no
+ other precedence needs to be recalculated
+ \item case 2: RAG needs to be pruned, no precedence needs to be recalculated
+ \end{itemize}\bigskip
+ \item Lock event (2 cases: cs is locked, not locked)
+ \begin{itemize}
+ \item case 1: a waiting edge needs to be added to the RAG, precedences of
+ all dependants need to recalculated (where there is a change)
+ \item case 2: a holding edge needs to be added to the RAG, no
+ precedences need to be recalculated
+ \end{itemize}
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Implementation}
+
+ \begin{itemize}
+ \item in PINTOS (Stanford), written in C for educational purposes\bigskip
+ \begin{center}
+ \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
+ \hline
+ {\bf Event} & {\bf PINTOS function} \\
+ \hline
+ @{text Create} & @{text "thread_create"}\\
+ @{text Exit} & @{text "thread_exit"}\\
+ @{text Set} & @{text "thread_set_priority"}\\
+ @{text Lock} & @{text "lock_acquire"}\\
+ @{text Unlock} & @{text "lock_release"}\\
+ \hline
+ \end{tabular}
+ \end{center}\pause\bigskip
+
+ \item \alert{We did not verify our C-code!}\pause
+ \item We were much faster: we gave an unlocked resource to
+ the thread with the highest precedence
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{A Step Back\ldots}
+ \large
+
+ \begin{itemize}
+ \item Did we make any impact? No!\medskip\pause
+
+ \item real-time scheduling on multiprocessors seems to be a very
+ underdeveloped area
+ \item implementations exist, e.g.~RT-Linux
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Theorem Provers}
+
+ \begin{itemize}
+ \item We found a mistake in a refereed paper by Harper \& Pfenning
+ \item I also found a mistake in my PhD thesis
+ \item also a popular textbook book on Computability contained an
+ error\bigskip
+
+ \item scratching on the surface of an completely ``alien'' subject
+ to us --- we were able to make progress
+
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Inductive Method / Protocols}
+
+ \begin{itemize}
+ \item the inductive method was developed/used by Larry Paulson
+ for verifying security protocols\bigskip\bigskip
+ \item we used it for a different `kind' of protocols (scheduling)
+ \item but this was restricted to only single-processors, no timing information
+
+
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Clock Synchronisation}
+
+ \begin{itemize}
+ \item Mahyar Malekpour introduced a distributed clock-synchronisation
+ algorithm\\ (perfect example for us)\bigskip\bigskip
+
+ \item connected units exchange messages according to a protocol
+ and reach a stable, synchronised state
+ \item messages have to reach the receiver within a time-window\pause
+
+ \item \alert{verification still ongoing}
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Questions?}
+
+ \begin{itemize} \large
+ \item Thank you for the invitation and for listening!
+ \end{itemize}
+
+ \begin{center}
+ \begin{tabular}{c}
+ \includegraphics[scale=0.13]{isabelle.png}\\[-2mm]
+ \small\url{http://isabelle.in.tum.de}
+ \end{tabular}
+ \end{center}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+(*<*)
+end
+end
+(*>*)
\ No newline at end of file
--- a/Slides/document/beamerthemeplaincu.sty Thu Jun 20 23:28:26 2013 -0400
+++ b/Slides/document/beamerthemeplaincu.sty Tue Feb 25 20:01:47 2014 +0000
@@ -11,24 +11,39 @@
\mode<presentation>
+\usepackage{fontspec}
+\usefonttheme{serif}
+\defaultfontfeatures{Ligatures=TeX}
+\setromanfont{Hoefler Text}
+\setmonofont[Scale=MatchLowercase]{Consolas}
+\newfontfamily{\consolas}{Consolas}
+\newcommand{\tttext}[1]{{\consolas{#1}}}
+%%\setttfont{Lucida Console}
+%%\setmainfont[Mapping=tex-text]{Hoefler Text}
+
+%%\renewcommand\ttdefault{lmtt}
+
+
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% comic fonts fonts
-\DeclareFontFamily{T1}{comic}{}%
-\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}%
-\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}%
-\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}%
-\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}%
-\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}%
-\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}%
-\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}%
-\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}%
-\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}%
-\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}%
-\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}%
-\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}%
+%\DeclareFontFamily{T1}{comic}{}%
+%\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}%
+%\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}%
+%\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}%
+%\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}%
+%\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}%
+%\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}%
+%\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}%
+%\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}%
%
-\renewcommand{\rmdefault}{comic}%
-\renewcommand{\sfdefault}{comic}%
+%\renewcommand{\rmdefault}{comic}%
+%\renewcommand{\sfdefault}{comic}%
\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one
%
\DeclareMathVersion{bold}% mathfont needs to be bold
@@ -44,8 +59,10 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Frametitles
+
\setbeamerfont{frametitle}{size={\LARGE}}
-\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}}
+\setbeamerfont{frametitle}{family={\fontspec{Hoefler Text Black}}}
+%\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}
\setbeamercolor{frametitle}{fg=ProcessBlue,bg=white}
\setbeamertemplate{frametitle}{%
--- a/Slides/document/root.tex Thu Jun 20 23:28:26 2013 -0400
+++ b/Slides/document/root.tex Tue Feb 25 20:01:47 2014 +0000
@@ -1,9 +1,9 @@
\documentclass[dvipsnames, 14pt,t]{beamer}
\usepackage{beamerthemeplaincu}
%%\usepackage{ulem}
-\usepackage[T1]{fontenc}
+%\usepackage[T1]{fontenc}
\usepackage{proof}
-\usepackage[latin1]{inputenc}
+%\usepackage[latin1]{inputenc}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{mathpartir}
Binary file journal.pdf has changed