48 %\renewcommand{\theproof}{} |
47 %\renewcommand{\theproof}{} |
49 %\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}} |
48 %\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}} |
50 |
49 |
51 |
50 |
52 \begin{document} |
51 \begin{document} |
53 \renewcommand{\thefootnote}{$\star$} |
52 |
54 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}. |
53 \title{Priority Inheritance Protocol Proved Correct$^\star$\thanks{$^\star$ This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}. |
55 In Section 4 we improve our previous result by proving a finite bound for Priority Inversion. |
54 In Section 4 we improve our previous result by proving a finite bound for Priority Inversion. |
56 Moreover, we are giving in this paper |
55 Moreover, we are giving in this paper |
57 more details about our proof and describe some of our (unverified) C-code for implementing the |
56 more details about our proof and describe some of our (unverified) C-code for implementing the |
58 Priority Inversion |
57 Priority Inversion |
59 Protocol, as well as surveying |
58 Protocol, as well as surveying |
60 the existing literature in more depth. |
59 the existing literature in more depth. |
61 Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol. |
60 Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol.}} |
62 } |
61 \titlerunning{Priority Inheritance Protocol Proved Correct} |
63 \renewcommand{\thefootnote}{\arabic{footnote}} |
62 \author{Xingyuan Zhang \and Christian Urban \and Chunhan Wu} |
64 |
63 \institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and |
65 \title{Priority Inheritance Protocol Proved Correct$^\star$} |
64 Christian Urban \at King's College London, United Kingdom} |
66 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} |
|
67 \institute{PLA University of Science and Technology, China \and |
|
68 King's College London, United Kingdom} |
|
69 \maketitle |
65 \maketitle |
70 |
66 |
71 \begin{abstract} |
67 \begin{abstract} |
72 In real-time systems with threads, resource locking and priority |
68 In real-time systems with threads, resource locking and priority |
73 sched\-uling, one faces the problem of Priority Inversion. This |
69 sched\-uling, one faces the problem of Priority Inversion. This |
88 with an efficient implementation of this protocol. Earlier |
84 with an efficient implementation of this protocol. Earlier |
89 implementations were criticised as too inefficient. Our |
85 implementations were criticised as too inefficient. Our |
90 implementation builds on top of the small PINTOS operating system |
86 implementation builds on top of the small PINTOS operating system |
91 used for teaching.\medskip |
87 used for teaching.\medskip |
92 |
88 |
|
89 \noindent |
93 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
90 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
94 real-time systems, Isabelle/HOL |
91 real-time systems, Isabelle/HOL |
95 \end{abstract} |
92 \end{abstract} |
96 |
93 |
97 \input{session} |
94 \input{session} |