--- a/prio/Paper/Paper.thy Mon Feb 06 12:08:35 2012 +0000
+++ b/prio/Paper/Paper.thy Tue Feb 07 00:50:23 2012 +0000
@@ -6,29 +6,37 @@
open Printer;
show_question_marks_default := false;
*}
+
+notation (latex output)
+ Cons ("_::_" [78,77] 73) and
+ vt ("valid'_state") and
+ runing ("running") and
+ birthtime ("inception") and
+ If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+ DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
(*>*)
section {* Introduction *}
text {*
- Many real-time systems need to support processes with priorities and
+ Many real-time systems need to support threads involving priorities and
locking of resources. Locking of resources ensures mutual exclusion
when accessing shared data or devices that cannot be
- preempted. Priorities allow scheduling of processes that need to
+ preempted. Priorities allow scheduling of threads that need to
finish their work within deadlines. Unfortunately, both features
can interact in subtle ways leading to a problem, called
- \emph{Priority Inversion}. Suppose three processes having priorities
- $H$(igh), $M$(edium) and $L$(ow). We would expect that the process
- $H$ blocks any other process with lower priority and itself cannot
- be blocked by any process with lower priority. Alas, in a naive
+ \emph{Priority Inversion}. Suppose three threads having priorities
+ $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
+ $H$ blocks any other thread with lower priority and itself cannot
+ be blocked by any thread with lower priority. Alas, in a naive
implementation of resource looking and priorities this property can
be violated. Even worse, $H$ can be delayed indefinitely by
- processes with lower priorities. For this let $L$ be in the
+ threads with lower priorities. For this let $L$ be in the
possession of a lock for a resource that also $H$ needs. $H$ must
therefore wait for $L$ to exit the critical section and release this
lock. The problem is that $L$ might in turn be blocked by any
- process with priority $M$, and so $H$ sits there potentially waiting
- indefinitely. Since $H$ is blocked by processes with lower
+ thread with priority $M$, and so $H$ sits there potentially waiting
+ indefinitely. Since $H$ is blocked by threads with lower
priorities, the problem is called Priority Inversion. It was first
described in \cite{Lampson80} in the context of the
Mesa programming language designed for concurrent programming.
@@ -36,41 +44,43 @@
If the problem of Priority Inversion is ignored, real-time systems
can become unpredictable and resulting bugs can be hard to diagnose.
The classic example where this happened is the software that
- controlled the Mars Pathfinder mission in 1997
- \cite{Reeves98}. Once the spacecraft landed, the software
- shut down at irregular intervals leading to loss of project time as
- normal operation of the craft could only resume the next day (the
- mission and data already collected were fortunately not lost, because
- of a clever system design). The reason for the shutdowns was that
- the scheduling software fell victim of Priority Inversion: a low
- priority task locking a resource prevented a high priority process
- from running in time leading to a system reset. Once the problem was found,
- it was rectified by enabling the \emph{Priority Inheritance Protocol}
- (PIP) \cite{Sha90}\footnote{Sha et al.~call it the
- \emph{Basic Priority Inheritance Protocol} \cite{Sha90}.} in the scheduling software.
+ controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
+ Once the spacecraft landed, the software shut down at irregular
+ intervals leading to loss of project time as normal operation of the
+ craft could only resume the next day (the mission and data already
+ collected were fortunately not lost, because of a clever system
+ design). The reason for the shutdowns was that the scheduling
+ software fell victim of Priority Inversion: a low priority thread
+ locking a resource prevented a high priority thread from running in
+ time leading to a system reset. Once the problem was found, it was
+ rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
+ \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
+ Inheritance Protocol} \cite{Sha90} and others sometimes call it
+ also \emph{Priority Boosting}.} in the scheduling software.
- The idea behind PIP is to let the process $L$ temporarily
- inherit the high priority from $H$ until $L$ leaves the critical
- section by unlocking the resource. This solves the problem of $H$
- having to wait indefinitely, because $L$ cannot be
- blocked by processes having priority $M$. While a few other
- solutions exist for the Priority Inversion problem, PIP is one that is widely deployed
- and implemented. This includes VxWorks (a proprietary real-time OS
- used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner,
- Honda's ASIMO robot, etc.), but also the POSIX 1003.1c Standard
- realised for example in libraries for FreeBSD, Solaris and Linux.
+ The idea behind PIP is to let the thread $L$ temporarily inherit
+ the high priority from $H$ until $L$ leaves the critical section by
+ unlocking the resource. This solves the problem of $H$ having to
+ wait indefinitely, because $L$ cannot be blocked by threads having
+ priority $M$. While a few other solutions exist for the Priority
+ Inversion problem, PIP is one that is widely deployed and
+ implemented. This includes VxWorks (a proprietary real-time OS used
+ in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
+ 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 process
+ One advantage of PIP is that increasing the priority of a thread
can be dynamically calculated 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 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). Though, most criticism against PIP centres
- around unreliable implementations and PIP being too complicated and
- too inefficient. For example, Yodaiken writes in \cite{Yodaiken02}:
+ analysis of the program in order to prevent Priority
+ Inversion. 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).
+ Though, most criticism against PIP centres around unreliable
+ implementations and PIP being too complicated and too inefficient.
+ For example, Yodaiken writes in \cite{Yodaiken02}:
\begin{quote}
\it{}``Priority inheritance is neither efficient nor reliable. Implementations
@@ -82,7 +92,7 @@
sections to be preempted. While this might have been a reasonable
solution in 2002, in our modern multiprocessor world, this seems out
of date. The reason is that this precludes other high-priority
- processes from running even when they do not make any use of the locked
+ threads from running even when they do not make any use of the locked
resource.
However, there is clearly a need for investigating correct
@@ -106,50 +116,138 @@
again at PIP from a more abstract level (but still concrete enough
to inform an implementation) and makes PIP an ideal candidate for a
formal verification. One reason, of course, is that the original
- presentation of PIP \cite{Sha90}, despite being informally
+ presentation of PIP~\cite{Sha90}, despite being informally
``proved'' correct, is actually \emph{flawed}.
Yodaiken \cite{Yodaiken02} points to a subtlety that had been
overlooked in the informal proof by Sha et al. They specify in
- \cite{Sha90} that after the process (whose priority has been raised)
+ \cite{Sha90} that after the thread (whose priority has been raised)
completes its critical section and releases the lock, it ``returns
to its original priority level.'' This leads them to believe that an
- implementation of PIP is ``rather straightforward'' \cite{Sha90}.
- Unfortunately, as Yodaiken pointed out, this behaviour is too
- simplistic. Consider the case where the low priority process $L$
- locks \emph{two} resources, and two high-priority processes $H$ and
+ implementation of PIP is ``rather straightforward''~\cite{Sha90}.
+ Unfortunately, as Yodaiken points out, this behaviour is too
+ simplistic. Consider the case where the low priority thread $L$
+ locks \emph{two} resources, and two high-priority threads $H$ and
$H'$ each wait for one of them. If $L$ then releases one resource
so that $H$, say, can proceed, then we still have Priority Inversion
with $H'$ (which waits for the other resource). The correct
behaviour for $L$ is to revert to the highest remaining priority of
- processes that it blocks. The advantage of a formalisation in a
- theorem prover for the correctness of a high-level specification of
- PIP is that such issues clearly show up and cannot be overlooked as
- in informal reasoning (since we have to analyse all possible program
- behaviours, i.e.~\emph{traces}, that could possibly happen).
+ the threads that it blocks. The advantage of formalising the
+ 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).
There have been earlier formal investigations into PIP, but ...\cite{Faria08}
+
+ vt (valid trace) was introduced earlier, cite
+
+ distributed PIP
*}
section {* Formal Model of the Priority Inheritance Protocol *}
text {*
- Our formal model of PIP is based on Paulson's inductive approach to protocol
- verification \cite{Paulson98}, where the state of the system is modelled as a list of events
- that happened so far. \emph{Events} fall into four categories defined as the datatype
+ We follow the original work by Sha et al.~\cite{Sha90} by modelling
+ first a classical single CPU system where only one \emph{thread} is
+ active at any given moment. We shall discuss later how to lift this
+ restriction. Our model of PIP is based on Paulson's inductive
+ approach to protocol verification \cite{Paulson98}, where the
+ \emph{state} of a system is given by a list of events that
+ happened so far. \emph{Events} fall into four categories defined as
+ the datatype
\begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
- \isacommand{datatype} event & @{text "="} & @{term "Create thread priority"}\\
- & @{text "|"} & @{term "Exit thread"}\\
- & @{text "|"} & @{term "P thread cs"} & {\rm Request of a resource} @{text "cs"} {\rm by} @{text "thread"}\\
- & @{text "|"} & @{term "V thread cs"} & {\rm Release of a resource} @{text "cs"} {\rm by} @{text "thread"}
- \end{tabular}
+ \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
+ \isacommand{datatype} event
+ & @{text "="} & @{term "Create thread priority"}\\
+ & @{text "|"} & @{term "Exit thread"} \\
+ & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the proprity for} @{text thread}\\
+ & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
+ & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ whereby threads, priorities and (critical) resources are represented
+ as natural numbers. As in Paulson's work, we need to define
+ functions that allow one to make some observations about states.
+ One is the ``live'' threads we have seen so far in a state:
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(1)}\\
+ @{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(2)[where thread="th"]}\\
+ @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(3)[where thread="th"]}\\
+ @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
+ \end{tabular}}
\end{isabelle}
\noindent
- whereby threads, priorities and resources are represented as natural numbers.
- A \emph{state} is a list of events.
+ Another is that given a thread @{text "th"}, what is the original priority was at
+ its inception.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
+ @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ In this definition we set @{text 0} as the default priority for
+ threads that have not (yet) been created. The last function we need
+ calculates the ``time'', or index, at which a process was created.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
+ @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
+ \end{tabular}}
+ \end{isabelle}
+
+ \begin{center}
+ threads, original-priority, birth time, precedence.
+ \end{center}
+
+
+
+ resources
+
+ step relation:
+
+ \begin{center}
+ \begin{tabular}{c}
+ @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
+ @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\
+
+ @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
+ @{thm[mode=Rule] thread_V[where thread=th]}\\
+ \end{tabular}
+ \end{center}
+
+ valid state:
+
+ \begin{center}
+ \begin{tabular}{c}
+ @{thm[mode=Axiom] vt_nil[where cs=step]}\hspace{1cm}
+ @{thm[mode=Rule] vt_cons[where cs=step]}
+ \end{tabular}
+ \end{center}
+
To define events, the identifiers of {\em threads},
{\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
@@ -159,25 +257,28 @@
text {*
\bigskip
- The priority inversion phenomenon was first published in \cite{Lampson80}.
- The two protocols widely used to eliminate priority inversion, namely
- PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed
- in \cite{Sha90}. PCE is less convenient to use because it requires
- static analysis of programs. Therefore, PI is more commonly used in
- practice\cite{locke-july02}. However, as pointed out in the literature,
- the analysis of priority inheritance protocol is quite subtle\cite{yodaiken-july02}.
- A formal analysis will certainly be helpful for us to understand and correctly
- implement PI. All existing formal analysis of PI
- \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the model checking
- technology. Because of the state explosion problem, model check
- is much like an exhaustive testing of finite models with limited size.
- The results obtained can not be safely generalized to models with arbitrarily
- large size. Worse still, since model checking is fully automatic, it give little
- insight on why the formal model is correct. It is therefore
- definitely desirable to analyze PI using theorem proving, which gives
- more general results as well as deeper insight. And this is the purpose
- of this paper which gives a formal analysis of PI in the interactive
- theorem prover Isabelle using Higher Order Logic (HOL). The formalization
+ The priority inversion phenomenon was first published in
+ \cite{Lampson80}. The two protocols widely used to eliminate
+ priority inversion, namely PI (Priority Inheritance) and PCE
+ (Priority Ceiling Emulation), were proposed in \cite{Sha90}. PCE is
+ less convenient to use because it requires static analysis of
+ programs. Therefore, PI is more commonly used in
+ practice\cite{locke-july02}. However, as pointed out in the
+ literature, the analysis of priority inheritance protocol is quite
+ subtle\cite{yodaiken-july02}. A formal analysis will certainly be
+ helpful for us to understand and correctly implement PI. All
+ existing formal analysis of PI
+ \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the
+ model checking technology. Because of the state explosion problem,
+ model check is much like an exhaustive testing of finite models with
+ limited size. The results obtained can not be safely generalized to
+ models with arbitrarily large size. Worse still, since model
+ checking is fully automatic, it give little insight on why the
+ formal model is correct. It is therefore definitely desirable to
+ analyze PI using theorem proving, which gives more general results
+ as well as deeper insight. And this is the purpose of this paper
+ which gives a formal analysis of PI in the interactive theorem
+ prover Isabelle using Higher Order Logic (HOL). The formalization
focuses on on two issues:
\begin{enumerate}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Paper/document/mathpartir.sty Tue Feb 07 00:50:23 2012 +0000
@@ -0,0 +1,446 @@
+% Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
+%
+% Author : Didier Remy
+% Version : 1.2.0
+% Bug Reports : to author
+% Web Site : http://pauillac.inria.fr/~remy/latex/
+%
+% Mathpartir is free software; you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either version 2, or (at your option)
+% any later version.
+%
+% Mathpartir is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details
+% (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+ [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+%% \newdimen \mpr@tmpdim
+%% Dimens are a precious ressource. Uses seems to be local.
+\let \mpr@tmpdim \@tempdima
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+ \edef \MathparNormalpar
+ {\noexpand \lineskiplimit \the\lineskiplimit
+ \noexpand \lineskip \the\lineskip}%
+ }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+ {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+ \let \and \mpr@andcr
+ \let \par \mpr@andcr
+ \let \\\mpr@cr
+ \let \eqno \mpr@eqno
+ \let \hva \mpr@hva
+ }
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+ {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+ \noindent $\displaystyle\fi
+ \MathparBindings}
+ {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+\newenvironment{mathparpagebreakable}[1][]
+ {\begingroup
+ \par
+ \mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \mpr@prebindings \mpr@paroptions #1%
+ \vskip \abovedisplayskip \vskip -\lineskip%
+ \ifmmode \else $\displaystyle\fi
+ \MathparBindings
+ }
+ {\unskip
+ \ifmmode $\fi \par\endgroup
+ \vskip \belowdisplayskip
+ \noindent
+ \ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
+ \vbox \bgroup \tabskip 0em \let \\ \cr
+ \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+ \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+ \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+ \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+ \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
+ \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+ \mpr@flatten \mpr@all \mpr@to \mpr@one
+ \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+ \mpr@all \mpr@stripend
+ \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+ \ifx 1\mpr@isempty
+ \repeat
+}
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+ \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+%% Part III -- Type inference rules
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+ \setbox \mpr@hlist
+ \hbox {\strut
+ \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+ \unhbox \mpr@hlist}%
+ \setbox \mpr@vlist
+ \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+ \else \unvbox \mpr@vlist \box \mpr@hlist
+ \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+% \setbox \mpr@hlist
+% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+% \setbox \mpr@vlist
+% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+% \else \unvbox \mpr@vlist \box \mpr@hlist
+% \fi}%
+% }
+
+\def \mpr@item #1{$\displaystyle #1$}
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+ \bgroup
+ \ifx #1T\@premissetrue
+ \else \ifx #1B\@premissefalse
+ \else
+ \PackageError{mathpartir}
+ {Premisse orientation should either be T or B}
+ {Fatal error in Package}%
+ \fi \fi
+ \def \@test {#2}\ifx \@test \mpr@blank\else
+ \setbox \mpr@hlist \hbox {}%
+ \setbox \mpr@vlist \vbox {}%
+ \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+ \let \@hvlist \empty \let \@rev \empty
+ \mpr@tmpdim 0em
+ \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+ \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+ \def \\##1{%
+ \def \@test {##1}\ifx \@test \empty
+ \mpr@htovlist
+ \mpr@tmpdim 0em %%% last bug fix not extensively checked
+ \else
+ \setbox0 \hbox{\mpr@item {##1}}\relax
+ \advance \mpr@tmpdim by \wd0
+ %\mpr@tmpdim 1.02\mpr@tmpdim
+ \ifnum \mpr@tmpdim < \hsize
+ \ifnum \wd\mpr@hlist > 0
+ \if@premisse
+ \setbox \mpr@hlist
+ \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+ \else
+ \setbox \mpr@hlist
+ \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
+ \fi
+ \else
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \else
+ \ifnum \wd \mpr@hlist > 0
+ \mpr@htovlist
+ \mpr@tmpdim \wd0
+ \fi
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \advance \mpr@tmpdim by \mpr@sep
+ \fi
+ }%
+ \@rev
+ \mpr@htovlist
+ \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+ \fi
+ \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+ \let\@@over\over % fallback if amsmath is not loaded
+ \let\@@overwithdelims\overwithdelims
+ \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+ \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+ }{}
+
+%% The default
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\mpr@over #2}$}}
+\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\@@atop #2}$}}
+
+\let \mpr@fraction \mpr@@fraction
+
+%% A generic solution to arrow
+
+\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
+ \def \mpr@tail{#1}%
+ \def \mpr@body{#2}%
+ \def \mpr@head{#3}%
+ \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
+ \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
+ \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
+ \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
+ \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
+ \setbox0=\hbox {$\box1 \@@atop \box2$}%
+ \dimen0=\wd0\box0
+ \box0 \hskip -\dimen0\relax
+ \hbox to \dimen0 {$%
+ \mathrel{\mpr@tail}\joinrel
+ \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
+ $}}}
+
+%% Old stuff should be removed in next version
+\def \mpr@@nothing #1#2
+ {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
+\def \mpr@@reduce #1#2{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+ {\bgroup
+ \ifnum \linewidth<\hsize \hsize \linewidth\fi
+ \mpr@rulelineskip
+ \let \and \qquad
+ \let \hva \mpr@hva
+ \let \@rulename \mpr@empty
+ \let \@rule@options \mpr@empty
+ \let \mpr@over \@@over
+ \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+ {\everymath={\displaystyle}%
+ \def \@test {#2}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+ \else
+ \def \@test {#3}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+ \else
+ \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+ \fi \fi
+ \def \@test {#1}\ifx \@test\empty \box0
+ \else \vbox
+%%% Suggestion de Francois pour les etiquettes longues
+%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+ {\hbox {\RefTirName {#1}}\box0}\fi
+ \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \\
+% Each \\ produces a break, attempting horizontal breaks if possible,
+% and vertical breaks if needed.
+%
+% An empty element obtained by \\\\ produces a vertical break in all cases.
+%
+% The former rule is aligned on the fraction bar.
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+%
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%
+% width set the width of the rule to val
+% narrower set the width of the rule to val\hsize
+% before execute val at the beginning/left
+% lab put a label [Val] on top of the rule
+% lskip add negative skip on the right
+% left put a left label [Val]
+% Left put a left label [Val], ignoring its width
+% right put a right label [Val]
+% Right put a right label [Val], ignoring its width
+% leftskip skip negative space on the left-hand side
+% rightskip skip negative space on the right-hand side
+% vdots lift the rule by val and fill vertical space with dots
+% after execute val at the end/right
+%
+% Note that most options must come in this order to avoid strange
+% typesetting (in particular leftskip must preceed left and Left and
+% rightskip must follow Right or right; vdots must come last
+% or be only followed by rightskip.
+%
+
+%% Keys that make sence in all kinds of rules
+\def \mprset #1{\setkeys{mprset}{#1}}
+\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
+\define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
+\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mprset}{sep}{\def\mpr@sep{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+ {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+ {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+ \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+ \setbox \mpr@right \hbox{}%
+ $\setkeys{mpr}{#1}%
+ \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+ \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+ \box \mpr@right \mpr@vdots$}
+ \setbox1 \hbox {\strut}
+ \@tempdima \dp0 \advance \@tempdima by -\dp1
+ \raise \@tempdima \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode
+ \let \@do \mpr@inferstar@
+ \else
+ \let \@do \mpr@err@skipargs
+ \PackageError {mathpartir}
+ {\string\inferrule* can only be used in math mode}{}%
+ \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \TirNameStyle #1{\small \textsc{#1}}
+\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
+\let \TirName \tir@name
+\let \DefTirName \TirName
+\let \RefTirName \TirName
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
--- a/prio/Paper/document/root.tex Mon Feb 06 12:08:35 2012 +0000
+++ b/prio/Paper/document/root.tex Tue Feb 07 00:50:23 2012 +0000
@@ -3,6 +3,7 @@
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
+\usepackage{mathpartir}
%\usepackage{tikz}
%\usepackage{pgf}
%\usetikzlibrary{arrows,automata,decorations,fit,calc}
@@ -44,9 +45,9 @@
\maketitle
\begin{abstract}
-In real-time systems with support for resource locking and for
-processes with priorities, one faces the problem of Priority
-IBnversion. This problem can make the behaviour of processes
+In real-time systems with threads, resource locking and
+priority sched\-uling, one faces the problem of Priority
+Inversion. This problem can make the behaviour of threads
unpredictable and the resulting bugs can be hard to find. The
Priority Inheritance Protocol is one solution implemented in many
systems for solving this problem, but the correctness of this solution
@@ -62,7 +63,7 @@
Paulson's inductive approach to verifying protocols.\medskip
{\bf Keywords:} Priority Inheritance Protocol, formal connectness proof,
-real-time systems
+real-time systems, Isabelle/HOL
\end{abstract}
\input{session}