Martin D Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich and Markus Müller-Olm. Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. POPL'11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pages 93–104, Austin, Texas, USA, 2011. ACM.
We consider programs for embedded real-time systems which use priority-driven preemptive scheduling with task priorities adjusted dynamically according to the immediate ceiling priority protocol. 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.
Download: PDF Reference: Bibtex Electronic Copy: DOI