%\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.
In Section 4 we improve our previous result by proving a finite bound for Priority Inversion.
Moreover, we are giving in this paper
more details about our proof and also surveying 
the existing literature in more depth.}
\renewcommand{\thefootnote}{\arabic{footnote}}

\title{Priority Inheritance Protocol Proved Correct$^\star$}
\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 is based on Paulson's
  inductive approach to verifying protocols.  The formalisation not
  only uncovers facts overlooked in the literature, but also helps
  with an efficient implementation of this protocol. Earlier correct
  implementations were criticised as too inefficient. 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: