Priority Inheritance Protocol Proved Correct

TY - JOUR

T1 - Priority Inheritance Protocol Proved Correct

AU - Zhang, Xingyuan

AU - Urban, Christian

AU - Wu, Chunhan

PY - 2020/1/1

Y1 - 2020/1/1

N2 - In real-time systems with threads, resource locking and priority scheduling, one faces the problem of Priority Inversion. This problem can make the behaviour of threads unpredictable and the resulting bugs can be hard to find. The Priority Inheritance Protocol is one solution implemented in many systems for solving this problem, but the correctness of this solution has never been formally verified in a theorem prover. As already pointed out in the literature, the original informal investigation of the Property Inheritance Protocol presents a correctness “proof” for an incorrect algorithm. In this paper we fix the problem of this proof by making all notions precise and implementing a variant of a solution proposed earlier. We also generalise the scheduling problem to the practically relevant case where crit- ical sections can overlap. Our formalisation in Isabelle/HOL is based on Paulson’s inductive approach to protocol verification. The formalisation not only uncovers facts overlooked in the literature, but also helps with an efficient implementation of this protocol. Earlier imple- mentations were criticised as too inefficient. Our implementation builds on top of the small PINTOS operating system used for teaching.

AB - In real-time systems with threads, resource locking and priority scheduling, one faces the problem of Priority Inversion. This problem can make the behaviour of threads unpredictable and the resulting bugs can be hard to find. The Priority Inheritance Protocol is one solution implemented in many systems for solving this problem, but the correctness of this solution has never been formally verified in a theorem prover. As already pointed out in the literature, the original informal investigation of the Property Inheritance Protocol presents a correctness “proof” for an incorrect algorithm. In this paper we fix the problem of this proof by making all notions precise and implementing a variant of a solution proposed earlier. We also generalise the scheduling problem to the practically relevant case where crit- ical sections can overlap. Our formalisation in Isabelle/HOL is based on Paulson’s inductive approach to protocol verification. The formalisation not only uncovers facts overlooked in the literature, but also helps with an efficient implementation of this protocol. Earlier imple- mentations were criticised as too inefficient. Our implementation builds on top of the small PINTOS operating system used for teaching.

KW - Formal correctness proof

KW - Isabelle/HOL

KW - Priority Inheritance Protocol

KW - Real-time systems

UR - http://www.scopus.com/inward/record.url?scp=85061374877&partnerID=8YFLogxK

U2 - 10.1007/s10817-019-09511-5

DO - 10.1007/s10817-019-09511-5

M3 - Article

SN - 0168-7433

VL - 64

SP - 73

EP - 95

JO - JOURNAL OF AUTOMATED REASONING

JF - JOURNAL OF AUTOMATED REASONING

IS - 1

ER -