Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

12-02-2019 | Issue 1/2020 Open Access

Journal of Automated Reasoning 1/2020

Priority Inheritance Protocol Proved Correct

Journal:
Journal of Automated Reasoning > Issue 1/2020
Authors:
Xingyuan Zhang, Christian Urban, Chunhan Wu
Important notes
This paper is a revised, corrected and expanded version of [31]. In Sect. 4 we improve our previous result by proving a finite bound for Priority Inversion. Moreover, we are giving in this paper more details about our proof and describe some of our (unverified) C-code for implementing the Priority Inversion Protocol, as well as surveying the existing literature in more depth. Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

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 critical 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 implementations were criticised as too inefficient. Our implementation builds on top of the small PINTOS operating system used for teaching.

Our product recommendations

Premium-Abo der Gesellschaft für Informatik

Sie erhalten uneingeschränkten Vollzugriff auf alle acht Fachgebiete von Springer Professional und damit auf über 45.000 Fachbücher und ca. 300 Fachzeitschriften.

Literature
About this article

Other articles of this Issue 1/2020

Journal of Automated Reasoning 1/2020 Go to the issue

Premium Partner

    Image Credits