%\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}
\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.}
\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 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 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: