\documentclass[runningheads]{llncs}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathpartir}
\usepackage{tikz}
\usepackage{pgf}
%\usetikzlibrary{arrows,automata,decorations,fit,calc}
%\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
%\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
%\usetikzlibrary{matrix}
\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
%%\usepackage{proof}
%%\usepackage{mathabx}
\usepackage{stmaryrd}
\usepackage{url}
\usepackage{color}
\titlerunning{Proving the Priority Inheritance Protocol Correct}


\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%


\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymiota}{}

\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
\definecolor{mygrey}{rgb}{.80,.80,.80}

\begin{document}

\title{Priority Inheritance Protocol Proved Correct}
\author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
\institute{PLA University of Science and Technology, China \and 
           King's College London, United Kingdom}
\maketitle

\begin{abstract}
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
has never been formally verified in a theorem prover. As already
pointed out in the literature, the original informal investigation of
the Property Inheritance Protocol presents a correctness ``proof'' for
an \emph{incorrect} algorithm. In this paper we fix the problem of
this proof by making all notions precise and implementing a variant of
a solution proposed earlier. Our formalisation in Isabelle/HOL
uncovers facts not mentioned in the literature, but also shows how to
efficiently implement this protocol. Earlier correct implementations
were criticised as too inefficient. Our formalisation is based on
Paulson's inductive approach to verifying protocols.\medskip

{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
real-time systems, Isabelle/HOL
\end{abstract}

\input{session}

%\bibliographystyle{plain}
%\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: