Document Open Access Logo

Static Race Detection for RTOS Applications

Authors Rishi Tulsyan, Rekha Pai, Deepak D'Souza

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.57.pdf
  • Filesize: 0.63 MB
  • 20 pages

Document Identifiers

Author Details

Rishi Tulsyan
  • Indian Institute of Science Bangalore, India
Rekha Pai
  • Indian Institute of Science Bangalore, India
Deepak D'Souza
  • Indian Institute of Science Bangalore, India

Acknowledgements

The second author want to thank University Grants Commission (UGC) India for the Dr. DS Kothari Post Doctoral Fellowship EN/17-18/0039.

Cite AsGet BibTex

Rishi Tulsyan, Rekha Pai, and Deepak D'Souza. Static Race Detection for RTOS Applications. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 57:1-57:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.57

Abstract

We present a static analysis technique for detecting data races in Real-Time Operating System (RTOS) applications. These applications are often employed in safety-critical tasks and the presence of races may lead to erroneous behaviour with serious consequences. Analyzing these applications is challenging due to the variety of non-standard synchronization mechanisms they use. We propose a technique based on the notion of an "occurs-in-between" relation between statements. This notion enables us to capture the interplay of various synchronization mechanisms. We use a pre-analysis and a small set of not-occurs-in-between patterns to detect whether two statements may race with each other. Our experimental evaluation shows that the technique is efficient and effective in identifying races with high precision.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Static analysis
  • concurrency
  • data-race detection
  • RTOS

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. ArduPilot: Open source drone software. versatile, trusted, open. https://ardupilot.org/, 2020.
  2. Martin Abadi, Cormac Flanagan, and Stephen N Freund. Types for safe locking: Static race detection for Java. ACM Transactions on Programming Languages and Systems (TOPLAS), 28(2):207-255, 2006. Google Scholar
  3. Rajeev Alur, Ken McMillan, and Doron Peled. Model-checking of correctness conditions for concurrent objects. Information and Computation, 160(1):167-188, 2000. Google Scholar
  4. Cyrille Artho, Klaus Havelund, and Armin Biere. High-level data races. Software Testing, Verification and Reliability, 13(4):207-227, 2003. Google Scholar
  5. Richard Barry. The FreeRTOS kernel, v10.0.0. https://freertos.org, 2017.
  6. Takashi C. The NxtOSEK project. https://sourceforge.net/projects/lejos-osek/, 2014.
  7. Rui Chen, Xiangying Guo, Yonghao Duan, Bin Gu, and Mengfei Yang. Static data race detection for interrupt-driven embedded software. In Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C ’11, page 47–52, USA, 2011. IEEE Computer Society. Google Scholar
  8. Nikita Chopra, Rekha Pai, and Deepak D'Souza. Data races and static analysis for interrupt-driven kernels. In Proceedings of the 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, volume 11423 of Lecture Notes in Computer Science, pages 697-723, Prague, Czech Republic, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-17184-1_25.
  9. Ricardo J. Dias, Vasco Pessanha, and João Lourenço. Precise detection of atomicity violations. In Proceedings of the 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers, volume 7857 of Lecture Notes in Computer Science, pages 8-23, Haifa, Israel, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-39611-3_8.
  10. Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. Precise race detection and efficient model checking using locksets. Technical Report MSR-TR-2005-118, Microsoft Research, 2005. Google Scholar
  11. Dawson Engler and Ken Ashcraft. Racerx: Effective, static detection of race conditions and deadlocks. SIGOPS Operating Systems Review, 37(5):237–252, October 2003. Google Scholar
  12. Cormac Flanagan and Stephen N. Freund. Type-based race detection for java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2000, pages 219-232, Vancouver, Britith Columbia, Canada, 2000. ACM. URL: https://doi.org/10.1145/349299.349328.
  13. Cormac Flanagan and Stephen N. Freund. Detecting race conditions in large programs. In Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE, 2001, pages 90-96, Snowbird, Utah, USA, 2001. ACM. URL: https://doi.org/10.1145/379605.379687.
  14. Klaus Havelund, Michael R. Lowry, and John Penix. Formal analysis of a space-craft controller using SPIN. IEEE Transactions on Software Engineering, 27(8):749-765, 2001. Google Scholar
  15. Klaus Havelund and Jens U. Skakkebæk. Applying model checking in java verification. In Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, page 216–231, Berlin, Heidelberg, 1999. Springer-Verlag. URL: https://doi.org/10.1007/3-540-48234-2_17.
  16. Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Race checking by context inference. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI ’04, pages 1-13, New York, NY, USA, 2004. Association for Computing Machinery. Google Scholar
  17. Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, and Michael Tautschnig. Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems, 17(2):36:1-36:26, December 2017. Google Scholar
  18. Antoine Miné, Laurent Mauborgne, Xavier Rival, Jerome Feret, Patrick Cousot, Daniel Kästner, Stephan Wilhelm, and Christian Ferdinand. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée. In Proceedings of the 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France, 2016. Google Scholar
  19. Suvam Mukherjee, Arun Kumar, and Deepak D'Souza. Detecting all high-level dataraces in an RTOS kernel. In Proceedings of the 18th International Conference on VMCAI 2017, volume 10145 of Lecture Notes in Computer Science, pages 405-423, Paris, France, 2017. Springer. URL: https://doi.org/10.1007/978-3-319-52234-0_22.
  20. George Necula. CIL - infrastructure for C Program Analysis and Transformation (v. 1.3.7). http://people.eecs.berkeley.edu/~necula/cil/, 2002.
  21. John Regehr and Nathan Cooprider. Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science, 174(9):139-150, 2007. Google Scholar
  22. Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, and Kalmer Apinis. Precise analysis of value-dependent synchronization in priority scheduled programs. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014, volume 8318 of Lecture Notes in Computer Science, pages 21-38, San Diego, CA, USA, 2014. Springer. URL: https://doi.org/10.1007/978-3-642-54013-4_2.
  23. 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. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pages 93-104, Austin, TX, USA, 2011. ACM. URL: https://doi.org/10.1145/1926385.1926398.
  24. Abhishek Singh, Rekha Pai, Deepak D'Souza, and Meenakshi D'Souza. Static analysis for detecting high-level races in RTOS kernels. In Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, FM 2019, volume 11800 of Lecture Notes in Computer Science, pages 337-353, Porto, Portugal, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-30942-8_21.
  25. Nicholas Sterling. WARLOCK - A static data race analysis tool. In Proc. Usenix Winter Technical Conference, pages 97-106, 1993. Google Scholar
  26. Chungha Sung, Markus Kusano, and Chao Wang. Modular verification of interrupt-driven software. In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, pages 206-216, Urbana, IL, USA, 2017. IEEE Computer Society. URL: https://doi.org/10.1109/ASE.2017.8115634.
  27. Christoph von Praun and Thomas R. Gross. Static detection of atomicity violations in object-oriented programs. Journal of Object Technology, 3(6):103-122, 2004. Google Scholar
  28. Jan Wen Voung, Ranjit Jhala, and Sorin Lerner. RELAY: static race detection on millions of lines of code. In Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, pages 205-214, Dubrovnik, Croatia, 2007. ACM. URL: https://doi.org/10.1145/1287624.1287654.
  29. Yu Wang, Linzhang Wang, Tingting Yu, Jianhua Zhao, and Xuandong Li. 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, 2017, pages 113-124, Santa Barbara, CA, USA, 2017. ACM. URL: https://doi.org/10.1145/3092703.3092724.
  30. Reng Zeng, Zhuo Sun, Su Liu, and Xudong He. Mcpatom: A predictive analysis tool for atomicity violation using model checking. In Proceedings of the 19th International Workshop on Model Checking Software SPIN 2012, volume 7385 of Lecture Notes in Computer Science, pages 191-207, Oxford, UK, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-31759-0_14.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact