39 |
39 |
40 \title{A Formalisation of Priority Inheritance Protocol \\ |
40 \title{A Formalisation of Priority Inheritance Protocol \\ |
41 for Correct and Efficient Implementation} |
41 for Correct and Efficient Implementation} |
42 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}} |
42 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}} |
43 \institute{PLA University of Science and Technology, China \and |
43 \institute{PLA University of Science and Technology, China \and |
44 King's College London, U.K.} |
44 King's College London, United Kingdom} |
45 \maketitle |
45 \maketitle |
46 |
46 |
47 %\mbox{}\\[-10mm] |
|
48 \begin{abstract} |
47 \begin{abstract} |
49 Despite the wide use of Priority Inheritance Protocol in real time operating |
48 In realtime systems with support for resource locking and |
50 system, it's correctness has never been formally proved and mechanically checked. |
49 processes involving priorities, one faces the problem of |
51 All existing verification are based on model checking technology. Full automatic |
50 priority inversion. This problem can make the behaviour of processes unpredictable |
52 verification gives little help to understand why the protocol is correct. |
51 and the resulting bugs can be hard to find. The Priority Inheritance |
53 And results such obtained only apply to models of limited size. |
52 Protocol is one solution implemented in many systems for |
54 This paper presents a formal verification based on theorem proving. |
53 solving the priority inversion problem, but the correctness of this solution has never |
55 Machine checked formal proof does help to get deeper understanding. We found |
54 been formally verified in a theorem prover. The original description |
56 the fact which is not mentioned in the literature, that the choice of next |
55 of the Property Inheritance Protocol presents a ``correctness proof'' |
57 thread to take over when an critical resource is release does not affect the correctness |
56 done with pencil-and-paper for an \emph{incorrect} algorithm. This has |
58 of the protocol. The paper also shows how formal proof can help to construct |
57 already been pointed out in the literature. In this paper we fix the |
59 correct and efficient implementation. |
58 problem of the original proof by making all notions precise and implement a |
|
59 variant of a solution proposed earlier. Our formalisation in |
|
60 Isabelle/HOL uncovered facts not mentioned in the literature, but also |
|
61 shows how to efficiently implement this protocol. Earlier correct |
|
62 implementations were criticised as too inefficient. Our formalisation |
|
63 is based on Paulson's inductive approach to verifying |
|
64 protocols.\medskip |
|
65 |
|
66 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, |
|
67 realtime systems |
60 \end{abstract} |
68 \end{abstract} |
61 |
|
62 |
69 |
63 \input{session} |
70 \input{session} |
64 |
71 |
65 %%\mbox{}\\[-10mm] |
|
66 \bibliographystyle{plain} |
72 \bibliographystyle{plain} |
67 \bibliography{root} |
73 \bibliography{root} |
68 |
74 |
69 \end{document} |
75 \end{document} |
70 |
76 |