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 |
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 |
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. We are giving in this paper |
57 we proved about optimisations of the Priority Inheritance Protocol. |
58 more details about the proof and also surveying |
58 In Section 4 we improve our previous result by proving a finite bound for Priority Inversion. |
|
59 Moreover, we are giving in this paper |
|
60 more details about our proof and also surveying |
59 the existing literature in more depth.} |
61 the existing literature in more depth.} |
60 \renewcommand{\thefootnote}{\arabic{footnote}} |
62 \renewcommand{\thefootnote}{\arabic{footnote}} |
61 |
63 |
62 \title{Priority Inheritance Protocol Proved Correct} |
64 \title{Priority Inheritance Protocol Proved Correct$^\star$} |
63 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
65 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
64 \institute{PLA University of Science and Technology, China \and |
66 \institute{PLA University of Science and Technology, China \and |
65 King's College London, United Kingdom} |
67 King's College London, United Kingdom} |
66 \maketitle |
68 \maketitle |
67 |
69 |