There is an inherent tension in concurrent real-time software between synchronization, needed to preserve data consistency, and prioritized execution, needed to meet hard deadlines.
Retaining execution of high-priority tasks within a predictable time frame, yet allowing lower-priority tasks to complete critical sections, requires sophisticated synchronization primitives which limit the worstcase waiting time of high-priority tasks.
Using common binary semaphores (mutexes) can result in a higher-priority task waiting an indefinite amount of time for a lower-priority task to complete, a situation known as unbounded priority inversion.
But since unbounded priority inversion defeats the possibility of meeting hard deadlines, operating systems for embedded systems provide more sophisticated synchronization primitives than common mutexes.
Typically such primitives are based on priority inheritance: a lower-priority task which blocks a higher-priority task inherits the priority of that higher-priority task for the duration of the critical section which caused the blocking.
This bounds the time a higher-priority task can be blocked. The original ceiling priority protocol ensures that a higher-priority task can only be blocked for the duration of a single critical section.
In this paper, we develop static analyses for programs synchronized via the PCP.We provide methods for uncovering subtle flaws due to the concurrency induced by interrupts.
Specifically, we focus on data races and transactional behavior of procedures. Moreover, we explain how interprocedural value analyses can be enhanced to take priorities and interrupts into account.
We exemplify this with an algorithm for inferring affine equalities. The PCP was engineered to run on uniprocessor systems, which are the de facto standard for embedded real-time systems.
For these programs, we provide static analyses for detecting data races between tasks running at different priorities as well as methods to guarantee transactional execution of procedures. Beyond that, we demonstrate how general techniques for value analyses can be adapted to this setting by developing a precise analysis of affine equalities.
To read this external content in full, download the paper from the author archives at the Westfalische Wilhelms- University