Abstract
We present a simple yet scalable framework for formal reasoning and machine-assisted proof of interrupt-driven concurrency in operating-system code, and use it to prove the principal scheduling property of the embedded, real-time eChronos OS: that the running task is always the highest-priority runnable task. The key differentiator of this verification is that the OS code itself runs with interrupts on, even within the scheduler, to minimise latency. Our reasoning includes context switching, interleaving with interrupt handlers and nested interrupts; and it is formalised in Isabelle/HOL, building on the Owicki-Gries method for fine-grained concurrency. We add support for explicit concurrency control and the composition of multiple independently-proven invariants. Finally, we discuss how scalability issues are addressed with proof engineering techniques, in order to handle thousands of proof obligations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Broadly speaking, this was the “Hoare/Dijkstra/Gries School” of Formal Methods.
- 2.
The eChronos OS [3] comes in many variants, varying in the hardware they run on, the scheduling policy they enforce and the synchronisation primitives they offer. In this paper we simply refer to the eChronos OS for the specific variant that we are targeting, called Kochab, which supports the features that create interesting reasoning challenges (preemption, nested-interrupts, etc.).
- 3.
We specifically target an ARM Cortex-M4 platform, simply referred to as ARM here.
- 4.
The model is written in a simple formalised imperative language with parallel composition and await statements, which has the following syntax:
The SCHEME constructor models a parametric number of parallel programs, as seen in [20]. Here this is the number of handlers plus the number of application tasks.
- 5.
For presentation purposes, we omit ghost variables added to the program for verification purposes. The notation \(x :\in S\) stands for non-deterministically updating x to be any element of S.
- 6.
Disabling the scheduler is one of the functions that the eChronos OS does not export, to keep control of latency, as mentioned in Sect. 1.
References
eChronos model and proofs. https://github.com/echronos/echronos-proofs
FreeRTOS. http://www.freertos.org/
The eChronos OS. http://echronos.systems
Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: Workshop on Models for Formal Analysis of Real Systems (MARS) (2015)
Chandrasekaran, P., Kumar, K.B.S., Minz, R.L., D’Souza, D., Meshram, L.: A multi-core version of FreeRTOS verified for datarace and deadlock freedom. In: MEMOCODE, pp. 62–71. IEEE (2014)
Cheng, S., Woodcock, J., D’Souza, D.: Using formal reasoning on a model of tasks for FreeRTOS. Formal Aspects Comput. 27(1), 167–192 (2015)
Divakaran, S., D’Souza, D., Kushwah, A., Sampath, P., Sridhar, N., Woodcock, J.: Refinement-based verification of the FreeRTOS scheduler in VCC. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) Formal Methods and Software Engineering. LNCS, vol. 9047, pp. 170–186. Springer, Heidelberg (2015)
Feijen, W.H.J., van Gasteren, A.J.M.: On a Method of Multiprogramming. Monographs in Computer Science. Springer, New York (1999)
Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reasoning 42(2–4), 301–347 (2009)
Ferreira, J.F., Gherghina, C., He, G., Qin, S., Chin, W.N.: Automated verification of the FreeRTOS scheduler in HIP/SLEEK. Int. J. Softw. Tools Technol. Transf. 16(4), 381–397 (2014)
Gammie, P., Hosking, T.A., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Blackburn, S. (ed.) PLDI 2015: The 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation, p. 11. ACM, New York (2015)
Gotsman, A., Yang, H.: Modular verification of preemptive OS kernels. J. Funct. Program. 23(4), 452–514 (2013)
Guo, Y., Zhang, H.: Verifying preemptive kernel code with preemption control support. In: 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, 1–3 September 2014, pp. 26–33. IEEE (2014)
Huang, Y., Zhao, Y., Zhu, L., Li, Q., Zhu, H., Shi, J.: Modeling and verifying the code-level OSEK/VDX operating system with CSP. In: Theoretical Aspects of Software Engineering (TASE), pp. 142–149. IEEE (2011)
Klein, G.: Proof engineering considered essential. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 16–21. Springer, Heidelberg (2014)
Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. Trans. Comput. Syst. 32(1), 2:1–2:70 (2014)
Matthews, D.C., Wenzel, M.: Efficient parallel programming in Poly/ML and Isabelle/ML. In: Petersen, L., Pontelli, E. (eds.) POPL 2010 WS Declarative Aspects of Multicore Programming, pp. 53–62. ACM, New York (2010)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319–340 (1976)
Prensa Nieto, L.: Verification of parallel programs with the Owicki-Gries and rely-guarantee methods in Isabelle/HOL. Ph.D. thesis, T.U. München (2002)
Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: 2010 PLDI, pp. 99–110. ACM (2010)
Acknowledgements
The authors would like to thanks Gerwin Klein and Stefan Götz for their feedback on drafts of this paper. NICTA is funded by the Australian Government through the Department of Communications and by the Australian Research Council through the ICT Centre-of-Excellence Program.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Andronick, J., Lewis, C., Matichuk, D., Morgan, C., Rizkallah, C. (2016). Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-43144-4_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-43143-7
Online ISBN: 978-3-319-43144-4
eBook Packages: Computer ScienceComputer Science (R0)