Abstract
With recent efforts to build foundational certified software systems, two different approaches have been proposed to certify thread context switching. One is to certify both threads and context switching in a single logic system, and the other certifies threads and context switching at different abstraction levels. The former requires heavyweight extensions in the logic system to support first-class code pointers and recursive specifications. Moreover, the specification for context switching is very complex. The latter supports simpler and more natural specifications, but it requires the contexts of threads to be abstracted away completely when threads are certified. As a result, the conventional implementation of context switching used in most systems needs to be revised to make the abstraction work. In this paper, we extend the second approach to certify the conventional implementation, where the clear abstraction for threads is unavailable since both threads and context switching hold pointers of thread contexts. To solve this problem, we allow the program specifications for threads to refer to pointers of thread contexts. Thread contexts are treated as opaque structures, whose contents are unspecified and should never be accessed by the code of threads. Therefore, the advantage of avoiding the direct support of first-class code pointers is still preserved in our method. Besides, our new approach is also more lightweight. Instead of using two different logics to certify threads and context switching, we employ only one program logic with two different specifications for the context switching. One is used to certify the implementation itself, and the more abstract one is used as an interface between threads and context switching at a higher abstraction level. The consistency between the two specifications are enforced by the global program invariant.
Similar content being viewed by others
References
Ni Z, Yu D, Shao Z. Using XCAP to certify realistic systems code: Machine context management. In Proc. the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Kaisers Lautern, Germany, Sept. 10–13, 2007, pp.189–206.
Ni Z. Modular machine code verification [Ph.D. Dissertation]. Yale University, 2007.
Ni Z, Shao Z. Certified assembly programming with embedded code pointers. In Proc. the 33rd ACM Symposium on Principles of Programming Languages, Charleston, USA, Jan. 11-13, 2006, pp.320-333.
Reynolds J C. Separation logic: A logic for shared mutable data structures. In Proc. the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, July 22-25, 2002, pp.55-74.
Feng X, Ni Z, Shao Z, Guo Y. An open framework for foundational proof-carrying code. In Proc. the 3rd ACM Workshop on Types in Language Design and Implementation (TLDI 2007), Nice, France, Jan. 16, 2007, pp.67-78.
Starostin A, Tsyban A. Verified process-context switch for C-programmed kernels. In Proc. the Second International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2008), Toronto, Canada, Oct. 6-9, 2008, pp.240-254.
Feng X, Shao Z, Guo Y, Dong Y. Combining domain-specific and foundational logics to verify complete software systems. In Proc. the Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2008), Toronto, Canada, Oct. 6-9, 2008, pp.54-69.
Guo Y, Jiang X, Chen Y, Lin C. A certified thread library for multithreaded user programs. In Proc. the 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007), Shanghai, China, Jun. 5-8, 2007, pp.127-136.
Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In Proc. 2006 ACM Conf. Prog. Lang. Design and Impl., Ottawa, Canada, Jun. 10-16, 2006, pp.401-414.
O'Hearn P W. Resources, concurrency and local reasoning. In Proc. 15th Int. Conf. Concurrency Theory (CONCUR 2004), London, UK, Aug. 31-Sept. 3, 2004, pp.49-67.
Appel A W, McAllester D. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, Sept. 2001, 23(5): 657-683.
Cai H. Logic-based verification of general machine code [Ph.D. Dissertation]. Tsinghua University, 2008.
Gargano M, Hillebrand M, Leinenbach D, Paul W. On the correctness of operating system kernels. In Proc. the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), Oxford, UK, Aug. 22-25, 2005, pp.1-16.
Tom In der Rieden, Alexandra Tsyban. CVM — A verified framework for microkernel programmers. In Proc. the 3rd International Workshop on Systems Software Verification (SSV 2008), Sydney, Australia, Feb. 25-27, pp.151-168.
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. the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, Oct. 11-14, 2009, pp.207-220.
Feng X, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. In Proc. 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008), Tucson, USA, Jun. 7-13, 2008, pp.170-182.
Author information
Authors and Affiliations
Corresponding author
Additional information
Supported by the National Natural Science Foundation of China under Grant Nos. 90718026 and 60928004, China Postdoctoral Science Foundation under Grant No. 20080430770, and Natural Science Foundation of Jiangsu Province, China under Grant No. BK2008181. Any opinions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies.
Rights and permissions
About this article
Cite this article
Guo, Y., Jiang, XY. & Chen, YY. Certification of Thread Context Switching. J. Comput. Sci. Technol. 25, 827–840 (2010). https://doi.org/10.1007/s11390-010-9368-3
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11390-010-9368-3