Advertisement

Static Analysis for Detecting High-Level Races in RTOS Kernels

  • Abhishek Singh
  • Rekha PaiEmail author
  • Deepak D’Souza
  • Meenakshi D’Souza
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

We propose a static analysis based approach for detecting high-level races in RTOS kernels popularly used in safety-critical embedded software. High-Level races are indicators of atomicity violations and can lead to erroneous software behaviour with serious consequences. Hitherto techniques for detecting high-level races have relied on model-checking approaches, which are inefficient and apriori unsound. In contrast we propose a technique based on static analysis that is both efficient and sound. The technique is based on the notion of disjoint blocks recently introduced in Chopra et al. [5]. We evaluate our technique on three popular RTOS kernels and show that it is effective in detecting races, many of them harmful, with a high rate of precision.

Keywords

Static analysis RTOS kernel Interrupt-driven programs High-level data races 

References

  1. 1.
    Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: static race detection for Java. ACM Trans. Program. Lang. Syst. (TOPLAS) 28(2), 207–255 (2006)CrossRefGoogle Scholar
  2. 2.
    Alur, R., McMillan, K.L., Peled, D.A.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1–2), 167–188 (2000)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Artho, C., Havelund, K., Biere, A.: High-level data races. J. Softw. Test. Verif. Reliab. 13, 207–227 (2003)CrossRefGoogle Scholar
  4. 4.
    Barry, R.: The FreeRTOS kernel, v10.0.0 (2017). https://freertos.org
  5. 5.
    Chopra, N., Pai, R., D’Souza, D.: Data races and static analysis for interrupt-driven kernels. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 697–723. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-17184-1_25CrossRefGoogle Scholar
  6. 6.
    Dias, R.J., Pessanha, V., Lourenço, J.M.: Precise detection of atomicity violations. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 8–23. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39611-3_8CrossRefGoogle Scholar
  7. 7.
    Elmas, T., Qadeer, S., Tasiran, S.: Precise race detection and efficient model checking using locksets. Technical Report MSR-TR-2005-118. Microsoft Research (2005)Google Scholar
  8. 8.
    Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. SIGOPS Oper. Syst. Rev. 37(5), 237–252 (2003)CrossRefGoogle Scholar
  9. 9.
    Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In Proceedings ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 338–349 (2003)Google Scholar
  10. 10.
    Havelund, K., Lowry, M.R., Penix, J.: Formal analysis of a space-craft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749–765 (2001)CrossRefGoogle Scholar
  11. 11.
    Havelund, K., Skakkebæk, J.U.: Applying model checking in Java verification. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 216–231. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48234-2_17CrossRefGoogle Scholar
  12. 12.
    Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Proceedings of ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 1–13 (2004)Google Scholar
  13. 13.
    Texas Instruments: TI-RTOS: A Real-Time Operating System for Microcontrollers. http://www.ti.com/tool/ti-rtos, 2017
  14. 14.
    Mukherjee, S., Kumar, A., D’Souza, D.: Detecting all high-level dataraces in an RTOS kernel. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 405–423. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52234-0_22CrossRefGoogle Scholar
  15. 15.
    Necula, G.: CIL - infrastructure for C Program Analysis and Transformation (v. 1.3.7) (2002). http://people.eecs.berkeley.edu/~necula/cil/
  16. 16.
    Regehr, J., Cooprider, N.: Interrupt verification via thread verification. Electr. Notes Theor. Comput. Sci. 174(9), 139–150 (2007)CrossRefGoogle Scholar
  17. 17.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)CrossRefGoogle Scholar
  18. 18.
    Schwarz, M.D., Seidl, H., Vojdani, V., Apinis, K.: Precise analysis of value-dependent synchronization in priority scheduled programs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 21–38. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54013-4_2CrossRefGoogle Scholar
  19. 19.
    Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., Müller-Olm, M.: Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In Proceedings of ACM SIGPLAN-SIGACT Principles of Programming Languages (POPL), pp. 93–104 (2011)Google Scholar
  20. 20.
    Sterling, N.: WARLOCK - a static data race analysis tool. In: Proceedings of Usenix Winter Technical Conference, pp. 97–106 (1993)Google Scholar
  21. 21.
    Sung, C., Kusano, M., Wang, C.: Modular verification of interrupt-driven software. In: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, pp. 206–216 (2017)Google Scholar
  22. 22.
    von Praun, C., Gross, T.R.: Static detection of atomicity violations in object-oriented programs. J. Object Technol. 3(6), 103–122 (2004)CrossRefGoogle Scholar
  23. 23.
    Voung, J.W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Proceedings of ESEC/SIGSOFT Foundations of Software Engineering (FSE), pp. 205–214 (2007)Google Scholar
  24. 24.
    Wang, Y., Wang, L., Yu, T., Zhao, J., Li, X.: Automatic detection and validation of race conditions in interrupt-driven embedded software. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2017, pp. 113–124. ACM (2017)Google Scholar
  25. 25.
    Zeng, R., Sun, Z., Liu, S., He, X.: McPatom: a predictive analysis tool for atomicity violation using model checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 191–207. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31759-0_14CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Abhishek Singh
    • 2
  • Rekha Pai
    • 1
    Email author
  • Deepak D’Souza
    • 1
  • Meenakshi D’Souza
    • 2
  1. 1.Indian Institute of ScienceBangaloreIndia
  2. 2.International Institute of Information Technology, BangaloreBangaloreIndia

Personalised recommendations