Xinyu Feng
Zhong Shao
ABSTRACT
Hardware interrupts are widely used in the world's critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system programming. Unfortunately, interrupts are also extremely hard to reason about: they dramatically alter the program control flow and complicate the invariants in low-level concurrent code (e.g., implementation of synchronization primitives). Existing formal verification techniques---including Hoare logic, typed assembly language, concurrent separation logic, and the assume-guarantee method---have consistently ignored the issues of interrupts; this severely limits the applicability and power of today's program verification systems.
In this paper we present a novel Hoare-logic-like framework for certifying low-level system programs involving both hardware interrupts and preemptive threads. We show that enabling and disabling interrupts can be formalized precisely using simple ownership-transfer semantics, and the same technique also extends to the concurrent setting. By carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we are able to---for the first time---successfully certify a preemptive thread implementation and a large number of common synchronization primitives. Our work provides a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified operating system kernels and hypervisors.
- William R. Bevier. Kit: A study in operating system verification. IEEE Trans. Softw. Eng., 15 (11): 1382--1396, 1989. Google Scholar
Digital Library
- Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In Proc. 32nd ACM Symp. on Principles of Prog. Lang., pages 259--270, January 2005. Google ScholarDigital Library
- Per Brinch Hansen. The programming language concurrent pascal. IEEE Trans. Software Eng., 1 (2): 199--207, 1975.Google ScholarDigital Library
- Stephen Brookes. A semantics for concurrent separation logic. In Proc. 15th Int'l Conf. on Concurrency Theory (CONCUR'04), volume 3170 of LNCS, pages 16--34. Springer, September 2004.Google ScholarCross Ref
- Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.1, 2006.Google Scholar
- Rober DeLine and Manual Fähndrich. Enforcing high-level protocols in low-level software. In Proc. 2001 ACM Conf. on Prog. Lang. Design and Impl., pages 59--69. ACM Press, June 2001. Google ScholarDigital Library
- Xinyu Feng and Zhong Shao. Modular verification of concurrent assembly code with dynamic thread creation and termination. In Proc. 2005 ACM Int'l Conf. on Functional Prog., pages 254--267, September 2005. Google ScholarDigital Library
- Xinyu Feng and Zhong Shao. Local reasoning and information hiding in SCAP. Technical Report YALEU/DCS/TR-1398, Dept. of Computer Science, Yale University, New Haven, CT, February 2008. http://flint.cs.yale.edu/publications/SCAPFrame.html.Google Scholar
- Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni. Modular verification of assembly code with stack-based control abstractions. In Proc. 2006 ACM Conf. on Prog. Lang. Design and Impl., pages 401--414. ACM Press, June 2006. Google ScholarDigital Library
- Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In Proc. 16th European Symp. on Prog. (ESOP'07), volume 4421 of LNCS, pages 173--188. Springer, March 2007a. Google ScholarDigital Library
- Feng, Ni, Shao, and Guo}feng07:ocapXinyu Feng, Zhaozhong Ni, Zhong Shao, and Yu Guo. An open framework for foundational proof-carrying code. In Proc. 2007 ACM Workshop on Types in Lang. Design and Impl., pages 67--78, January 2007b. Google ScholarDigital Library
- Xinyu Feng, Zhong Shao, Yuan Dong, and Yu Guo. Certifying low-level programs with hardware interrupts and preemptive threads. Technical Report YALEU/DCS/TR-1396 and Coq Implementations, Dept. of Computer Science, Yale University, New Haven, CT, November 2007c. http://flint.cs.yale.edu/publications/aim.html.Google Scholar
- Mauro Gargano, Mark A. Hillebrand, Dirk Leinenbach, and Wolfgang J. Paul. On the correctness of operating system kernels. In Proc. 18th Int'l Conf. on Theorem Proving in Higher Order Logics, volume 3603 of LNCS, pages 1--16, August 2005. Google ScholarDigital Library
- Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. In Proc. 5th ASIAN Symp. on Prog. Lang. and Sys. (APLAS'07), pages 19--37, 2007. Google ScholarDigital Library
- C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 26 (1): 53--56, October 1969. Google ScholarDigital Library
- C. A. R. Hoare. Monitors: An operating system structuring concept. Communications of the ACM, 17 (10): 549--557, October 1974. Google ScholarDigital Library
- C. A. R. Hoare. Towards a theory of parallel programming. In Operating Systems Techniques, pages 61--71. Academic Press, 1972.Google Scholar
- Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. In Proc. 17th European Symp. on Prog. (ESOP'08), page to appear, 2008. Google ScholarDigital Library
- Galen C. Hunt and James R. Larus. Singularity design motivation. Technical Report MSR-TR-2004-105, Microsoft Corporation, December 2004.Google Scholar
- Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Proc. 28th ACM Symp. on Principles of Prog. Lang., pages 14--26. ACM Press, January 2001. Google ScholarDigital Library
- Butler W. Lampson and David D. Redell. Experience with processes and monitors in Mesa. Commun. ACM, 23 (2): 105--117, 1980. Google ScholarDigital Library
- Andrew McCreight, Zhong Shao, Chunxiao Lin, and Long Li. A general framework for certifying garbage collectors and their mutators. In Proc. 2007 ACM Conf. on Prog. Lang. Design and Impl., pages 468--479. ACM Press, June 2007. Google ScholarDigital Library
- Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Prog. Lang., pages 85--97. ACM Press, January 1998. Google ScholarDigital Library
- Zhaozhong Ni, Dachuan Yu, and Zhong Shao. Using XCAP to certify realistic systems code: Machine context management. In Proc. 20th Int'l Conf. on Theorem Proving in Higher Order Logics, volume 4421 of LNCS, pages 189--206. Springer, September 2007. Google ScholarDigital Library
- Peter W. O'Hearn. Resources, concurrency and local reasoning. In Proc. 15th Int'l Conf. on Concurrency Theory (CONCUR'04), volume 3170 of LNCS, pages 49--67. Springer, September 2004.Google Scholar
- Peter W. O'Hearn, Hongseok Yang, and John C. Reynolds. Separation and information hiding. In Proc. 31th ACM Symp. on Principles of Prog. Lang., pages 268--280. ACM Press, January 2004. Google ScholarDigital Library
- Jens Palsberg and Di Ma. A typed interrupt calculus. In Proc. 7th Int'l Symp. on Formal Tech. in Real-Time and Fault-Tolerant Sys. (FTRTFT'02), volume 2469 of LNCS, pages 291--310, September 2002. Google ScholarDigital Library
- Wolfgang Paul, Manfred Broy, and Thomas In der Rieden. The Verisoft XT project. URL: http://www.verisoft.de, 2007.Google Scholar
- John Regehr and Nathan Cooprider. Interrupt verification via thread verification. Electron. Notes Theor. Comput. Sci., 174 (9), 2007. Google ScholarDigital Library
- John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. 17th Annual IEEE Symp. on Logic in Comp. Sci. (LICS'02), pages 55--74. IEEE Computer Society, July 2002. Google ScholarDigital Library
- Kohei Suenaga and Naoki Kobayashi. Type based analysis of deadlock for a concurrent calculus with interrupts. In Proc. 16th European Symp. on Prog. (ESOP'07), volume 4421 of LNCS, pages 490--504, March 2007. Google ScholarDigital Library
- Harvey Tuch, Gerwin Klein, and Gernot Heiser. OS verification -- now! In Proc. 10th Workshop on Hot Topics in Operating Systems, June 2005. Google ScholarDigital Library
- Viktor Vafeiadis and Matthew Parkinson. A marriage of rely/guarantee and separation logic. In Proc. 18th Int'l Conf. on Concurrency Theory (CONCUR'07), volume 4703 of LNCS, pages 256--271, September 2007. Google ScholarDigital Library
Index Terms
- Certifying low-level programs with hardware interrupts and preemptive threads
Recommendations
Certifying low-level programs with hardware interrupts and preemptive threads
PLDI '08Hardware interrupts are widely used in the world's critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system ...
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads
Hardware interrupts are widely used in the world's critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system ...
Mechanized verification of preemptive OS kernels (invited talk)
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and ProofsWe propose a practical verification framework for preemptive OS kernels. The framework models the correctness of API implementations in OS kernels as contextual refinement of their abstract specifications. It provides a specification language for ...
Comments