71 In real-time systems with threads, resource locking and priority

    71   In real-time systems with threads, resource locking and priority

    72 sched\-uling, one faces the problem of Priority Inversion. This

    72   sched\-uling, one faces the problem of Priority Inversion. This

    73 problem can make the behaviour of threads unpredictable and the

    73   problem can make the behaviour of threads unpredictable and the

    74 resulting bugs can be hard to find.  The Priority Inheritance Protocol

    74   resulting bugs can be hard to find.  The Priority Inheritance

    75 is one solution implemented in many systems for solving this problem,

    75   Protocol is one solution implemented in many systems for solving

    76 but the correctness of this solution has never been formally verified

    76   this problem, but the correctness of this solution has never been

    77 in a theorem prover. As already pointed out in the literature, the

    77   formally verified in a theorem prover. As already pointed out in the

    78 original informal investigation of the Property Inheritance Protocol

    78   literature, the original informal investigation of the Property

    79 presents a correctness ``proof'' for an \emph{incorrect} algorithm. In

    79   Inheritance Protocol presents a correctness ``proof'' for an

    80 this paper we fix the problem of this proof by making all notions

    80   \emph{incorrect} algorithm. In this paper we fix the problem of this

    81 precise and implementing a variant of a solution proposed earlier. We

    81   proof by making all notions precise and implementing a variant of a

    82 also generalise the scheduling problem to the practically relevant case where

    82   solution proposed earlier. We also generalise the scheduling problem

    83 critical sections can overlap. Our formalisation in Isabelle/HOL not

    83   to the practically relevant case where critical sections can

    84 just uncovers facts not mentioned in the literature, but also helps

    84   overlap. Our formalisation in Isabelle/HOL is based on Paulson's

    85 with implementing efficiently this protocol. Earlier correct

    85   inductive approach to verifying protocols.  The formalisation not

    86 implementations were criticised as too inefficient. Our formalisation

    86   only uncovers facts overlooked in the literature, but also helps

    87 is based on Paulson's inductive approach to verifying protocols; our

    87   with an efficient implementation of this protocol. Earlier correct

    88 implementation builds on top of the small PINTOS operating system used

    88   implementations were criticised as too inefficient. Our

    89 for teaching.\medskip

    89   implementation builds on top of the small PINTOS operating system

    90   used for teaching.\medskip