Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol

ABSTRACT

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.

References

1. C. Artho, K. Havelund, and A. Biere. Using block-local atomicity to detect stale-value concurrency errors. In ATVA'04, vol. 3299 of LNCS, pp. 150--164. Springer, 2004.
2. M. F. Atig, A. Bouajjani, and T. Touili. Analyzing asynchronous programs with preemption. In FSTTCS'08, vol. 2 of LIPIcs, pp. 37--48. Schloss Dagstuhl, 2008.
3. Autosar consortium. Autosar Architecture Specification, Release 4.0, 2009. URL http://www.autosar.org/.
4. T. P. Baker. Stack-based scheduling of realtime processes. Real-Time Systems, 3(1):67--99, 1991.
5. A. Bouajjani, M. Müller-Olm, and T. Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In CONCUR'05, vol. 3653 of LNCS, pp. 473--487. Springer, 2005.
6. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In PLILP'92, pp. 269--295. Springer, 1992.
7. B. Dutertre. Formal analysis of the priority ceiling protocol. In RTSS'00, pp. 151--160. IEEE Press, 2000.
8. J. Esparza and A. Podelski. Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In POPL'00, pp. 1--11. ACM Press, 2000.
9. C. Fecht and H. Seidl. A Faster Solver for General Systems of Equations. Sci. Comput. Programming, 35(2):137--161, 1999.
10. C. Flanagan, S. N. Freund, S. Qadeer, and S. A. Seshia. Modular verification of multithreaded programs. Theoretical Comput. Sci., 338 (1--3):153--183, 2005.
11. C. Flanagan, S. N. Freund, M. Lifshin, and S. Qadeer. Types for atomicity: Static checking and inference for java. ACM Trans. Prog. Lang. Syst., 30(4):1--53, 2008.
12. M. S. Hecht. Flow Analysis of Computer Programs. Elsevier, 1977.
13. T. Henties, J. J. Hunt, D. Locke, K. Nilsen,M. Schoeberl, and J. Vitek. Java for safety-critical applications. In SafeCert'09, ENTCS. Elsevier, 2010.
14. V. Kahlon and A. Gupta. On the analysis of interacting pushdown systems. In POPL'07, pp. 303--314. ACM Press, 2007.
15. V. Kahlon, F. Ivančić, and A. Gupta. Reasoning about threads communicating via locks. In CAV'05, vol. 3576 of LNCS, pp. 505--518. Springer, 2005.
16. V. Kahlon, Y. Yang, S. Sankaranarayanan, and A. Gupta. Fast and accurate static data-race detection for concurrent programs. In CAV'07, vol. 4590 of LNCS, pp. 226--239. Springer, 2007.
17. N. Kidd, P. Lammich, T. Touili, and T. Reps. A decision procedure for detecting atomicity violations for communicating processes with locks. In SPIN'09, vol. 5578 of LNCS, pp. 125--142. Springer, 2009.
18. N. Kidd, S. Jagannathan, and J. Vitek. One stack to run them all reducing concurrent analysis to sequential analysis under priority scheduling. In SPIN'10, vol. 6349 of LNCS, pp. 245--261. Springer, 2010.
19. P. Lammich and M. Müller-Olm. Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In SAS'08, vol. 5079 of LNCS, pp. 205--220. Springer, 2008.
20. P. Lammich, M. Müller-Olm, and A. Wenner. Predecessor sets of dynamic pushdown networks with Tree-Regular constraints. In CAV'09, vol. 5643 of LNCS, pp. 525--539. Springer, 2009.
21. M. Müller-Olm and H. Seidl. Precise interprocedural analysis through linear algebra. In POPL'04, pp. 330--341. ACM Press, 2004.
22. OSEK/VDX Group. OSEK/VDX Operating System Specification, Version 2.2.3, 2005. URL http://www.osek-vdx.org.
23. M. Pilling, A. Burns, and K. Raymond. Formal specifications and proofs of inheritance protocols for real-time scheduling. Softw. Eng. J., 5(5):263--279, 1990.
24. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Prog. Lang. Syst., 22(2):416--430, 2000.
25. J. Regehr and N. Cooprider. Interrupt verification via thread verification. ENTCS, 174(9):139--150, 2007.
26. J. Regehr, A. Reid, and K. Webb. Eliminating stack overflow by abstract interpretation. ACM Trans. Embedded Comput. Syst., 4(4): 751--778, 2005.
27. L. Sha, R. Rajkumar, and J. P. Lehoczky. Priority inheritance protocols: an approach to real-time synchronization. IEEE Trans. Comput., 39(9):1175--1185, Sept. 1990.
28. M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. Program Flow Analysis: Theory and Applications, pp. 189--234, 1981.
29. Takashi Chikamasa et al. OSEK platform for LEGO MINDSTORMS 2010. URL http://lejos-osek.sourceforge.net/.
30. M. Vaziri, F. Tip, and J. Dolby. Associating synchronization constraints with data in an object-oriented language. In POPL'06, pp. 334--345. ACM Press, 2006.
31. V. Vojdani and V. Vene. Goblint: Path-sensitive data race analysis. Annales Univ. Sci. Budapest., Sect. Comp., 30:141--155, 2009.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program analysis

      • Program verification

    • Program semantics