%\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}.+
−
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.+
−
Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol.+
−
}+
−
\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  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:+
−