51 \begin{document} |
51 \begin{document} |
52 \renewcommand{\thefootnote}{$\star$} |
52 \renewcommand{\thefootnote}{$\star$} |
53 \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 |
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 |
55 algorithm in C and the operating system PINTOS. Our implementation follows closely all results |
56 we proved about optimisations of the Priority Inheritance Protocol.} |
56 we proved about optimisations of the Priority Inheritance Protocol. We are giving in this paper |
|
57 more details about the proof and also surveying |
|
58 the existing literature in more depth.} |
57 \renewcommand{\thefootnote}{\arabic{footnote}} |
59 \renewcommand{\thefootnote}{\arabic{footnote}} |
58 |
60 |
59 \title{Priority Inheritance Protocol Proved Correct} |
61 \title{Priority Inheritance Protocol Proved Correct} |
60 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
62 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
61 \institute{PLA University of Science and Technology, China \and |
63 \institute{PLA University of Science and Technology, China \and |
62 King's College London, United Kingdom} |
64 King's College London, United Kingdom} |
63 \maketitle |
65 \maketitle |
64 |
66 |
65 \begin{abstract} |
67 \begin{abstract} |
66 In real-time systems with threads, resource locking and |
68 In real-time systems with threads, resource locking and priority |
67 priority sched\-uling, one faces the problem of Priority |
69 sched\-uling, one faces the problem of Priority Inversion. This |
68 Inversion. This problem can make the behaviour of threads |
70 problem can make the behaviour of threads unpredictable and the |
69 unpredictable and the resulting bugs can be hard to find. The |
71 resulting bugs can be hard to find. The Priority Inheritance Protocol |
70 Priority Inheritance Protocol is one solution implemented in many |
72 is one solution implemented in many systems for solving this problem, |
71 systems for solving this problem, but the correctness of this solution |
73 but the correctness of this solution has never been formally verified |
72 has never been formally verified in a theorem prover. As already |
74 in a theorem prover. As already pointed out in the literature, the |
73 pointed out in the literature, the original informal investigation of |
75 original informal investigation of the Property Inheritance Protocol |
74 the Property Inheritance Protocol presents a correctness ``proof'' for |
76 presents a correctness ``proof'' for an \emph{incorrect} algorithm. In |
75 an \emph{incorrect} algorithm. In this paper we fix the problem of |
77 this paper we fix the problem of this proof by making all notions |
76 this proof by making all notions precise and implementing a variant of |
78 precise and implementing a variant of a solution proposed earlier. We |
77 a solution proposed earlier. We also generalise the original informal proof to the |
79 also generalise the scheduling problem to the practically relevant case where |
78 practically relevant case where critical sections can |
80 critical sections can overlap. Our formalisation in Isabelle/HOL not |
79 overlap. Our formalisation in Isabelle/HOL not just |
81 just uncovers facts not mentioned in the literature, but also helps |
80 uncovers facts not mentioned in the literature, but also helps with |
82 with implementing efficiently this protocol. Earlier correct |
81 implementing efficiently this protocol. Earlier correct implementations |
83 implementations were criticised as too inefficient. Our formalisation |
82 were criticised as too inefficient. Our formalisation is based on |
84 is based on Paulson's inductive approach to verifying protocols; our |
83 Paulson's inductive approach to verifying protocols; our implementation |
85 implementation builds on top of the small PINTOS operating system used |
84 builds on top of the small PINTOS operating system used for teaching.\medskip |
86 for teaching.\medskip |
85 |
87 |
86 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
88 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
87 %real-time systems, Isabelle/HOL |
89 real-time systems, Isabelle/HOL |
88 \end{abstract} |
90 \end{abstract} |
89 |
91 |
90 \input{session} |
92 \input{session} |
91 |
93 |
92 %\bibliographystyle{plain} |
94 %\bibliographystyle{plain} |