Verified Process-Context Switch for C-Programmed Kernels

  • Artem Starostin
  • Alexandra Tsyban
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


A context switch — an act of saving and restoring the state of a CPU such that multiple processes can share a single CPU resource — is an essential feature of multitasking operating systems. Commonly computationally intensive and necessarily accessing hardware registers, context-switch procedures are implemented as inline assembly portions in C-programmed operating-system kernels. Feasible verification of operating systems is usually attempted in some kind of C semantics. However, seamless verification of kernels requires reasoning about context-switch routines in semantics of assembly language. At the end of the day, both semantics meet together in an overall correctness theorem of operating system. The task of formal integration of correctness results achieved on different semantical layers is challenging but inevitable for systems verification.

The paper describes a formal approach to pervasive reasoning about interleaved computations of user processes and a C-programmed kernel. The interleaving is achieved by context-switch procedures implemented in inline assembly. We report on the correctness proof of the context-switch procedures and elaborate on our experience in formal integration of this result into the correctness proof of CVM, a verified framework for microkernel programmers.


Virtual Machine Physical Machine User Process Context Switch Physical Memory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 109–123. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning 5(4), 411–428 (1989)Google Scholar
  3. 3.
    Beyer, S.: Putting It All Together: Formal Verification of the VAMP. PhD thesis, Saarland University, Computer Science Dept. (2005)Google Scholar
  4. 4.
    Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.: Putting it all together: Formal verification of the VAMP. Intl Journal on Software Tools for Technology Transfer 8(4–5), 411–430 (2006)CrossRefGoogle Scholar
  5. 5.
    Dalinger, I., Hillebrand, M., Paul, W.: On the verification of memory management mechanisms. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 301–316. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Daum, M., Dörenbächer, J., Wolff, B., Schmidt, M.: A verification approach for system-level concurrent programs. In: 2nd IFIP Working Conference on Verified Software: Theories, Tools, and Experiments. LNCS. Springer, Heidelberg (2008)Google Scholar
  7. 7.
    Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 170–182. ACM, New York (2008)CrossRefGoogle Scholar
  8. 8.
    Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the correctness of operating system kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 1–16. Springer, Heidelberg (2005)Google Scholar
  9. 9.
    Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.M.: Towards trustworthy computing systems: Taking microkernels to the next level. Operating Systems Review 41(4), 3–11 (2007)CrossRefGoogle Scholar
  10. 10.
    Hoare, T., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: A manifesto (2007),
  11. 11.
    Hunt, G.C., Larus, J.R.: Singularity: Rethinking the software stack. Operating Systems Review 41(2), 37–49 (2007)CrossRefGoogle Scholar
  12. 12.
    der Rieden, T.I., Knapp, S.: An approach to the pervasive formal specification and verification of an automotive system. In: 10th Intl Workshop on Formal Methods for Industrial Critical Systems, pp. 115–124. IEEE, Los Alamitos (2005)CrossRefGoogle Scholar
  13. 13.
    der Rieden, T.I., Tsyban, A.: CVM — a verified framework for microkernel programmers. In: 3rd Intl Workshop on Systems Software Verification. ENTCS, vol. 217, pp. 151–168. Elsevier Science B.V, Amsterdam (2008)Google Scholar
  14. 14.
    Leinenbach, D.: Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University, Computer Science Dept (2008)Google Scholar
  15. 15.
    Leinenbach, D., Petrova, E.: Pervasive compiler verification – from verified programs to verified systems. In: 3rd Intl Workshop on Systems Software Verification. ENTCS, vol. 217, pp. 23–40. Elsevier Science B. V, Amsterdam (2008)Google Scholar
  16. 16.
    Moore, S.J.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 161–172. Springer, Heidelberg (2003)Google Scholar
  17. 17.
    Müller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000)zbMATHGoogle Scholar
  18. 18.
    Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: Machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 189–206. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  19. 19.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  20. 20.
    Starostin, A., Tsyban, A.: Correct microkernel primitives. In: 3rd Intl Workshop on Systems Software Verification. ENTCS, vol. 217, pp. 169–185. Elsevier Science B. V, Amsterdam (2008)Google Scholar
  21. 21.
    The Verisoft Consortium. The Verisoft Project (2003),

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Artem Starostin
    • 1
  • Alexandra Tsyban
    • 1
  1. 1.Computer Science Dept.Saarland UniversityGermany

Personalised recommendations