\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}

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

\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 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. 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; our implementation

is 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: