Common real-time operating systems rely on priority-based, preemptive scheduling. Resource sharing in such systems potentially leads to priority inversion: processes of high priority can be prevented from entering a critical section and be delayed by processes of lower priority. Since uncontrolled priority inversion can cause high priority processes to miss their deadlines, a real-time operating system must use resource-sharing mechanisms that limit the effects of priority inversion. The priority ceiling protocol is one such mechanism. It ensures mutual exclusion and absence of deadlocks, and minimizes the length of priority inversion periods. This paper presents a formal specification and analysis of the protocol using PVS and the rigorous proof of associated schedulability results.

• prio-ceiling.ps
• prio-ceiling.txt