\documentclass{article}
\textwidth 130mm
\textheight 200mm
\renewenvironment{abstract}{\section*{Abstract}\small}{}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathpartir}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
\usepackage{stmaryrd}
\usepackage{url}
\usepackage{color}
\usepackage{courier}
\usepackage{listings}
\lstset{language=C,
        numbers=left,
        basicstyle=\small\ttfamily,
        numberstyle=\footnotesize, frame=tb}

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

%%%\titlerunning{Proving the Priority Inheritance Protocol Correct}
\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}

\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}
\renewcommand{\thefootnote}{$\star$}
\footnotetext[1]{This is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.}
\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}
\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. We also generalise the original informal proof to the
practically relevant case where critical sections can
overlap. Our formalisation in Isabelle/HOL not just
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; our implementation
builds on top of the small PINTOS operating system.\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: