50 |
50 |
51 |
51 |
52 \begin{document} |
52 \begin{document} |
53 \renewcommand{\thefootnote}{$\star$} |
53 \renewcommand{\thefootnote}{$\star$} |
54 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}. |
54 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}. |
55 Compared with that paper we give an actual implementation of our formalised scheduling |
|
56 algorithm in C and the operating system PINTOS. Our implementation follows closely all results |
|
57 we proved about optimisations of the Priority Inheritance Protocol. |
|
58 In Section 4 we improve our previous result by proving a finite bound for Priority Inversion. |
55 In Section 4 we improve our previous result by proving a finite bound for Priority Inversion. |
59 Moreover, we are giving in this paper |
56 Moreover, we are giving in this paper |
60 more details about our proof and also surveying |
57 more details about our proof and describe some of our (unverified) C-code for implementing the |
61 the existing literature in more depth.} |
58 Priority Inversion |
|
59 Protocol, as well as surveying |
|
60 the existing literature in more depth. |
|
61 Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol. |
|
62 } |
62 \renewcommand{\thefootnote}{\arabic{footnote}} |
63 \renewcommand{\thefootnote}{\arabic{footnote}} |
63 |
64 |
64 \title{Priority Inheritance Protocol Proved Correct$^\star$} |
65 \title{Priority Inheritance Protocol Proved Correct$^\star$} |
65 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
66 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
66 \institute{PLA University of Science and Technology, China \and |
67 \institute{PLA University of Science and Technology, China \and |
82 solution proposed earlier. We also generalise the scheduling problem |
83 solution proposed earlier. We also generalise the scheduling problem |
83 to the practically relevant case where critical sections can |
84 to the practically relevant case where critical sections can |
84 overlap. Our formalisation in Isabelle/HOL is based on Paulson's |
85 overlap. Our formalisation in Isabelle/HOL is based on Paulson's |
85 inductive approach to verifying protocols. The formalisation not |
86 inductive approach to verifying protocols. The formalisation not |
86 only uncovers facts overlooked in the literature, but also helps |
87 only uncovers facts overlooked in the literature, but also helps |
87 with an efficient implementation of this protocol. Earlier correct |
88 with an efficient implementation of this protocol. Earlier |
88 implementations were criticised as too inefficient. Our |
89 implementations were criticised as too inefficient. Our |
89 implementation builds on top of the small PINTOS operating system |
90 implementation builds on top of the small PINTOS operating system |
90 used for teaching.\medskip |
91 used for teaching.\medskip |
91 |
92 |
92 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
93 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |