Abstract
Thread management is an essential functionality in OS kernels. However, verification of thread management remains a challenge, due to two conflicting requirements: on the one hand, a thread manager—operating below the thread abstraction layer–should hide its implementation details and be verified independently from the threads being managed; on the other hand, the thread management code in many real-world systems is concurrent, which might be executed by the threads being managed, so it seems inappropriate to abstract threads away in the verification of thread managers. Previous approaches on kernel verification view thread managers as sequential code, thus cannot be applied to thread management in realistic kernels. In this paper, we propose a novel two-layer framework to verify concurrent thread management. We choose a lower abstraction level than the previous approaches, where we abstract away the context switch routine only, and allow the rest of the thread management code to run concurrently in the upper level. We also treat thread management data as abstract resources so that threads in the environment can be specified in assertions and be reasoned about in a proof system similar to concurrent separation logic.
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
Preview
Unable to display preview. Download preview PDF.
References
Engelschall, R.S.: Portable multithreading: the signal stack trick for user-space thread creation. In: Proc. of ATEC 2000, p. 20. USENIX Association, Berkeley (2000)
Engler, D.R., Kaashoek, M.F., O’Toole Jr., J.: Exokernel: an operating system architecture for application-level resource management. In: Proceedings of the 15th ACM Symposium on Operating Systems Principles, SOSP 1995, Copper Mountain Resort, Colorado, pp. 251–266 (December 1995)
Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 54–69. Springer, Heidelberg (2008)
Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: Proc. PLDI 2006, pp. 401–414 (June 2006)
Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the Correctness of Operating System Kernels. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 1–16. Springer, Heidelberg (2005)
Gotsman, A., Yang, H.: Modular verification of preemptive os kernels. In: Proc. ICFP 2011, Tokyo, Japan, pp. 404–417. ACM (2011)
Guo, Y., Feng, X., Shao, Z., Shi, P.: Modular verification of concurrent thread management (technical report and coq proof) (June 2012), http://kyhcs.ustcsz.edu.cn/~guoyu/sched/
Herder, J.N., Bos, H., Gras, B., Homburg, P., Tanenbaum, A.S.: Minix 3: a highly reliable, self-repairing operating system. SIGOPS Oper. Syst. Rev. 40, 80–89 (2006)
Hohmuth, M., Tews, H.: The vfiasco approach for a verified operating system. In: Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems (2005)
In der Rieden, T., Tsyban, A.: CVM – A verified framework for microkernel programmers. In: Proc. SSV 2008. Electronic Notes in Theoretical Computer Science, vol. 217C, pp. 151–168. Elsevier Science B.V. (2008)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proc. SOSP 2009, Big Sky, MT, USA, pp. 207–220. ACM (October 2009)
Love, R.: Linux Kernel Development, 2nd edn. Novell Press (2005)
McKusick, M.K., Neville-Neil, G.V.: The Design and Implementation of the FreeBSD Operating System. Pearson Education (2004)
Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Proc. POPL 2006, pp. 320–333 (January 2006)
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)
O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3), 271–307 (2007)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE Computer Society, Washington, DC (2002)
Starostin, A., Tsyban, A.: Verified Process-Context Switch for C-Programmed Kernels. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 240–254. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guo, Y., Feng, X., Shao, Z., Shi, P. (2012). Modular Verification of Concurrent Thread Management. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-35182-2_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35181-5
Online ISBN: 978-3-642-35182-2
eBook Packages: Computer ScienceComputer Science (R0)