diff -r 914288aec495 -r 312497c6d6b9 Journal/document/root.tex --- a/Journal/document/root.tex Wed Aug 02 13:18:14 2017 +0100 +++ b/Journal/document/root.tex Wed Aug 02 14:56:47 2017 +0100 @@ -54,12 +54,14 @@ \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}. Compared with that paper we give an actual implementation of our formalised scheduling algorithm in C and the operating system PINTOS. Our implementation follows closely all results -we proved about optimisations of the Priority Inheritance Protocol. We are giving in this paper -more details about the proof and also surveying +we proved about optimisations of the Priority Inheritance Protocol. +In Section 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 also surveying the existing literature in more depth.} \renewcommand{\thefootnote}{\arabic{footnote}} -\title{Priority Inheritance Protocol Proved Correct} +\title{Priority Inheritance Protocol Proved Correct$^\star$} \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$} \institute{PLA University of Science and Technology, China \and King's College London, United Kingdom}