%\documentclass{article}

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

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 describe some of our (unverified) C-code for implementing the

Priority Inversion

Protocol, as well as surveying 

the existing literature in more depth.

\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  protocol verification.  The formalisation not

  only uncovers facts overlooked in the literature, but also helps

  with an efficient implementation of this protocol. Earlier

  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: