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