Paper/document/root.tex
changeset 2 a04084de4946
equal deleted inserted replaced
1:c4783e4ef43f 2:a04084de4946
       
     1 \documentclass[runningheads]{llncs}
       
     2 \usepackage{isabelle}
       
     3 \usepackage{isabellesym}
       
     4 \usepackage{amsmath}
       
     5 \usepackage{amssymb}
       
     6 \usepackage{mathpartir}
       
     7 \usepackage{tikz}
       
     8 \usepackage{pgf}
       
     9 %\usetikzlibrary{arrows,automata,decorations,fit,calc}
       
    10 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
       
    11 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
       
    12 %\usetikzlibrary{matrix}
       
    13 \usepackage{pdfsetup}
       
    14 \usepackage{ot1patch}
       
    15 \usepackage{times}
       
    16 %%\usepackage{proof}
       
    17 %%\usepackage{mathabx}
       
    18 \usepackage{stmaryrd}
       
    19 \usepackage{url}
       
    20 \usepackage{color}
       
    21 \titlerunning{Proving the Priority Inheritance Protocol Correct}
       
    22 
       
    23 
       
    24 \urlstyle{rm}
       
    25 \isabellestyle{it}
       
    26 \renewcommand{\isastyleminor}{\it}%
       
    27 \renewcommand{\isastyle}{\normalsize\it}%
       
    28 
       
    29 
       
    30 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
       
    31 \renewcommand{\isasymequiv}{$\dn$}
       
    32 \renewcommand{\isasymemptyset}{$\varnothing$}
       
    33 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
       
    34 \renewcommand{\isasymiota}{}
       
    35 
       
    36 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
       
    37 \definecolor{mygrey}{rgb}{.80,.80,.80}
       
    38 
       
    39 \begin{document}
       
    40 
       
    41 \title{Priority Inheritance Protocol Proved Correct}
       
    42 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
       
    43 \institute{PLA University of Science and Technology, China \and 
       
    44            King's College London, United Kingdom}
       
    45 \maketitle
       
    46 
       
    47 \begin{abstract}
       
    48 In real-time systems with threads, resource locking and 
       
    49 priority sched\-uling, one faces the problem of Priority
       
    50 Inversion. This problem can make the behaviour of threads
       
    51 unpredictable and the resulting bugs can be hard to find.  The
       
    52 Priority Inheritance Protocol is one solution implemented in many
       
    53 systems for solving this problem, but the correctness of this solution
       
    54 has never been formally verified in a theorem prover. As already
       
    55 pointed out in the literature, the original informal investigation of
       
    56 the Property Inheritance Protocol presents a correctness ``proof'' for
       
    57 an \emph{incorrect} algorithm. In this paper we fix the problem of
       
    58 this proof by making all notions precise and implementing a variant of
       
    59 a solution proposed earlier. Our formalisation in Isabelle/HOL
       
    60 uncovers facts not mentioned in the literature, but also shows how to
       
    61 efficiently implement this protocol. Earlier correct implementations
       
    62 were criticised as too inefficient. Our formalisation is based on
       
    63 Paulson's inductive approach to verifying protocols.\medskip
       
    64 
       
    65 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
       
    66 real-time systems, Isabelle/HOL
       
    67 \end{abstract}
       
    68 
       
    69 \input{session}
       
    70 
       
    71 %\bibliographystyle{plain}
       
    72 %\bibliography{root}
       
    73 
       
    74 \end{document}
       
    75 
       
    76 %%% Local Variables:
       
    77 %%% mode: latex
       
    78 %%% TeX-master: t
       
    79 %%% End: