Priority Inheritance Protocol Proved Correct
- Submitting institution
-
King's College London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 138795838
- Type
- D - Journal article
- DOI
-
10.1007/s10817-019-09511-5
- Title of journal
- JOURNAL OF AUTOMATED REASONING
- Article number
- -
- First page
- 73
- Volume
- 64
- Issue
- 1
- ISSN
- 0168-7433
- Open access status
- Compliant
- Month of publication
- February
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper studies the priority inheritance algorithm - a central algorithm for scheduling processes in many operating systems. A generalised version of this algorithm is given, which works in more instances than the original proposal in the seminal 1990 paper by Sha, Rajkumar and Lehoczky. The generalised version is fully formalised and rigorously proven to be correct, not only extending Sha et al. algorithm, but also correcting their proof. Completeness and correctness of Sha et al. algorithm have been long overlooked, with errors repeated in many textbooks on real-time operating systems, including the famous book by Silberschatz et al.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -