Formal specifications and proofs of inheritance protocols for real-time scheduling

Publisher Website
Google Scholar
Abstract
Priority is one means of representing scheduling information in a concurrent real-time programming language. Unfortunately, a static priority scheme can give rise to inversion when combined with synchronisation primitives. In this paper the use of semaphores for protecting access to critical regions is investigated. The formal notation Z is used for this treatment. It is shown that the normal semantics for semaphores can lead to a high priority process being delayed indefinitely. The inclusion of inheritance into the semaphore model improves the situation, but delays can still be significant. To overcome this lack of responsiveness, Lui Sha et al. [1] have developed a ceiling protocol that both removes the possibility of deadlock and limits (to one) the number of times a high priority process can be blocked. This paper contains a formal specification of a complete and a simplified version of the ceiling protocol, together with proofs of their important properties. The simplified version is suitable only for soft real-time systems and was generated while working from an incomplete natural language description given by Sha. The results of the proofs give considerable insight into the ceiling protocols and clarify many areas of their operation.

This publication has 1 reference indexed in Scilit: