47 %\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}} |
48 %\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}} |
48 |
49 |
49 |
50 |
50 \begin{document} |
51 \begin{document} |
51 \renewcommand{\thefootnote}{$\star$} |
52 \renewcommand{\thefootnote}{$\star$} |
52 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.} |
53 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}. |
|
54 Compared with that paper we give an actual implementation of our formalised scheduling |
|
55 algorithm in C and the operating system PINTOS. Our implementation follows closely all results |
|
56 we proved about optimisations.} |
53 \renewcommand{\thefootnote}{\arabic{footnote}} |
57 \renewcommand{\thefootnote}{\arabic{footnote}} |
54 |
58 |
55 \title{Priority Inheritance Protocol Proved Correct} |
59 \title{Priority Inheritance Protocol Proved Correct} |
56 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
60 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
57 \institute{PLA University of Science and Technology, China \and |
61 \institute{PLA University of Science and Technology, China \and |
71 an \emph{incorrect} algorithm. In this paper we fix the problem of |
75 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 |
76 this proof by making all notions precise and implementing a variant of |
73 a solution proposed earlier. We also generalise the original informal proof to the |
77 a solution proposed earlier. We also generalise the original informal proof to the |
74 practically relevant case where critical sections can |
78 practically relevant case where critical sections can |
75 overlap. Our formalisation in Isabelle/HOL not just |
79 overlap. Our formalisation in Isabelle/HOL not just |
76 uncovers facts not mentioned in the literature, but also shows how to |
80 uncovers facts not mentioned in the literature, but also helps with |
77 efficiently implement this protocol. Earlier correct implementations |
81 implementing efficiently this protocol. Earlier correct implementations |
78 were criticised as too inefficient. Our formalisation is based on |
82 were criticised as too inefficient. Our formalisation is based on |
79 Paulson's inductive approach to verifying protocols; our implementation |
83 Paulson's inductive approach to verifying protocols; our implementation |
80 builds on top of the small PINTOS operating system.\medskip |
84 builds on top of the small PINTOS operating system used for teaching.\medskip |
81 |
85 |
82 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
86 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
83 %real-time systems, Isabelle/HOL |
87 %real-time systems, Isabelle/HOL |
84 \end{abstract} |
88 \end{abstract} |
85 |
89 |