%\documentclass{article}
\documentclass{llncs}
%\textwidth 130mm
%\textheight 200mm
%\renewenvironment{abstract}{\section*{Abstract}\small}{}
\pagestyle{headings}
\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{endnotes}
\usetikzlibrary{patterns}
\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 paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
Compared with that paper we give an actual implementation of our formalised scheduling 
algorithm in C and the operating system PINTOS. Our implementation follows closely all results
we proved about optimisations of the Priority Inheritance Protocol. We are giving in this paper
more details about the proof and also surveying 
the existing literature in more depth.}
\renewcommand{\thefootnote}{\arabic{footnote}}

\title{Priority Inheritance Protocol Proved Correct}
\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}
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 scheduling problem 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 helps
with implementing efficiently 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 used
for teaching.\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: