ABSTRACT
Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU, where the scheduler and processes interact in complex ways.
We propose the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components. The logic hides the manipulation of control by the scheduler when reasoning about preemptable code and soundly inherits proof rules from concurrent separation logic to verify it thread-modularly. This is achieved by establishing a novel form of refinement between an operational semantics of the real machine and an axiomatic semantics of OS processes, where the latter assumes an abstract machine with each process executing on a separate virtual CPU. The refinement is local in the sense that the logic focuses only on the relevant state of the kernel while verifying the scheduler. We illustrate the power of our logic by verifying an example scheduler, modelled on the one from Linux 2.6.11.
Supplemental Material
- R.-J. Back. On correct refinement of programs. Journal of Computer and System Sciences, 23:49--68, 1981.Google ScholarCross Ref
- D. Bovet and M. Cesati. Understanding the Linux Kernel, 3rd ed. O'Reilly, 2005. Google ScholarDigital Library
- E. Cohen, W. Schulte, and S. Tobies. Local verification of global invariants in concurrent programs. In CAV'10: Conference on Computer-Aided Verification, volume 6174 of LNCS, pages 480--494. Springer, 2010. Google ScholarDigital Library
- T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. In ECOOP'10: European Conference on Object-Oriented Programming, pages 504--528. Springer, 2010. Google ScholarDigital Library
- X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP'07: European Conference on Programming, volume 4421 of LNCS, pages 173--188. Springer, 2007. Google ScholarDigital Library
- X. Feng, Z. Ni, Z. Shao, and Y. Guo. An open framework for foundational proof-carrying code. In TLDI'07: Workshop on Types in Language Design and Implementation, pages 67--78. ACM, 2007. Google ScholarDigital Library
- X. Feng, Z. Shao, Y. Dong, and Y. Guo. Certifying low-level programs with hardware interrupts and preemptive threads. In PLDI'08: Conference on Programming Language Design and Implementation, pages 170--182. ACM, 2008. Google ScholarDigital Library
- X. Feng, Z. Shao, Y. Guo, and Y. Dong. Combining domain-specific and foundational logics to verify complete software systems. In VSTTE'08: Conference on Verified Software: Theories, Tools, Experiments, volume 5295 of LNCS, pages 54--69. Springer, 2008. Google ScholarDigital Library
- X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verification of assembly code with stack-based control abstractions. In PLDI'06: Conference on Programming Language Design and Implementation, pages 401--414. ACM, 2006. Google ScholarDigital Library
- M. Gargano, M. Hillebrand, D. Leinenbach, and W. Paul. On the correctness of operating system kernels. In TPHOLs: Conference on Theorem Proving in Higher Order Logics, volume 3603 of LNCS, pages 1--16. Springer, 2005. Google ScholarDigital Library
- A. Gotsman. Logics and analyses for concurrent heap-manipulating programs. PhD Thesis, University of Cambridge, 2009.Google Scholar
- A. Gotsman, J. Berdine, and B. Cook. Precision and the conjunction rule in concurrent separation logic. In MFPS'11: Conference on Mathematical Foundations of Programming Semantics, 2011. To appear.Google ScholarDigital Library
- A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv. Local reasoning for storable locks and threads. In APLAS'07: Asian Symposium on Programming Languages and Systems, volume 4807 of LNCS, pages 19--37. Springer, 2007. Google ScholarDigital Library
- A. Gotsman and H. Yang. Modular verification of preemptive OS kernels (extended version). Available from www.software.imdea.org/~gotsman. Google ScholarDigital Library
- C. Jones. Splitting atoms safely. Theoretical Computer Science, 375:109--119, 2007. Google ScholarDigital Library
- G. Klein. Operating system verification - an overview. Sādhanā, 34:26--69, 2009.Google ScholarCross Ref
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In SOSP'09: Symposium on Operating Systems Principles, pages 207--220. ACM, 2009. Google ScholarDigital Library
- R. Love. Linux Kernel Development, 3rd ed. Addison Wesley, 2010. Google ScholarDigital Library
- T. Maeda and A. Yonezawa. Writing an OS kernel in a strictly and statically typed language. In Formal to Practical Security, volume 5458 of LNCS, pages 181--197. Springer, 2009. Google ScholarDigital Library
- P. W. O'Hearn. Resources, concurrency and local reasoning. Theoretical Computer Science, 375:271--307, 2007. Google ScholarDigital Library
- J. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS'02: Symposium on Logic in Computer Science, pages 55--74. IEEE, 2002. Google ScholarDigital Library
- A. Turon and M. Wand. A separation logic for refining concurrent objects. In POPL'11: Symposium on Principles of Programming Languages, pages 247--258. ACM, 2011. Google ScholarDigital Library
- V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR'07: Conference on Concurrency Theory, volume 4703 of LNCS, pages 256--271. Springer, 2007. Google ScholarDigital Library
- J. Yang and C. Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In PLDI'10: Conference on Programming Language Design and Implementation, pages 99--110. ACM, 2010. Google ScholarDigital Library
Index Terms
- Modular verification of preemptive OS kernels
Recommendations
Modular verification of preemptive OS kernels
ICFP '11Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this ...
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 ...
Preemptive scheduling with simple linear deterioration on a single machine
In this paper we study the problem of scheduling n deteriorating jobs with release dates on a single machine. The processing time of a job is assumed to be the product of its deteriorating rate and its starting time. Precedence relations may be imposed ...
Comments