1 \documentclass{article}

     2 \textwidth 130mm

     3 \textheight 200mm

     4 \renewenvironment{abstract}{\section*{Abstract}\small}{}

     5 \usepackage{isabelle}

     6 \usepackage{isabellesym}

     7 \usepackage{amsmath}

     8 \usepackage{amssymb}

     9 \usepackage{mathpartir}

    10 \usepackage{tikz}

    11 \usepackage{pgf}

    12 %\usetikzlibrary{arrows,automata,decorations,fit,calc}

    13 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}

    14 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf

    15 %\usetikzlibrary{matrix}

    16 \usepackage{pdfsetup}

    17 \usepackage{ot1patch}

    18 \usepackage{times}

    19 %%\usepackage{proof}

    20 %%\usepackage{mathabx}

    21 \usepackage{stmaryrd}

    22 \usepackage{url}

    23 \usepackage{color}

    24 %%%\titlerunning{Proving the Priority Inheritance Protocol Correct}

    25 

    26 

    27 \urlstyle{rm}

    28 \isabellestyle{it}

    29 \renewcommand{\isastyleminor}{\it}%

    30 \renewcommand{\isastyle}{\normalsize\it}%

    31 

    32 

    33 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    34 \renewcommand{\isasymequiv}{$\dn$}

    35 \renewcommand{\isasymemptyset}{$\varnothing$}

    36 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    37 \renewcommand{\isasymiota}{}

    38 

    39 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

    40 \definecolor{mygrey}{rgb}{.80,.80,.80}

    41 

    42 \newtheorem{definition}{Definition}

    43 \newtheorem{theorem}[definition]{Theorem}

    44 \newtheorem{lemma}[definition]{Lemma}

    45 \newtheorem{proof}{Proof}

    46 \renewcommand{\theproof}{}

    47 \newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}}

    48 

    49 

    50 \begin{document}

    51 \renewcommand{\thefootnote}{$\star$}

    52 \footnotetext[1]{This is a revised and expanded version of \cite{ZhangUrbanWu12}.}

    53 \renewcommand{\thefootnote}{\arabic{footnote}}

    54 

    55 \title{Priority Inheritance Protocol Proved Correct}

    56 \author{Xingyuan Zhang, Christian Urban and Chunhan Wu}

    57 %\institute{PLA University of Science and Technology, China \and 

    58 %           King's College London, United Kingdom}

    59 \maketitle

    60 

    61 \begin{abstract}

    62 In real-time systems with threads, resource locking and 

    63 priority sched\-uling, one faces the problem of Priority

    64 Inversion. This problem can make the behaviour of threads

    65 unpredictable and the resulting bugs can be hard to find.  The

    66 Priority Inheritance Protocol is one solution implemented in many

    67 systems for solving this problem, but the correctness of this solution

    68 has never been formally verified in a theorem prover. As already

    69 pointed out in the literature, the original informal investigation of

    70 the Property Inheritance Protocol presents a correctness ``proof'' for

    71 an \emph{incorrect} algorithm. In this paper we fix the problem of

    72 this proof by making all notions precise and implementing a variant of

    73 a solution proposed earlier. Our formalisation in Isabelle/HOL

    74 uncovers facts not mentioned in the literature, but also shows how to

    75 efficiently implement this protocol. Earlier correct implementations

    76 were criticised as too inefficient. Our formalisation is based on

    77 Paulson's inductive approach to verifying protocols; our implementation

    78 is on top of the small PINTOS operating system.\medskip

    79 

    80 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 

    81 %real-time systems, Isabelle/HOL

    82 \end{abstract}

    83 

    84 \input{session}

    85 

    86 %\bibliographystyle{plain}

    87 %\bibliography{root}

    88 

    89 \end{document}

    90 

    91 %%% Local Variables:

    92 %%% mode: latex

    93 %%% TeX-master: t

    94 %%% End: