Journal of Computer Science and Technology
Quick Search in JCST
 Advanced Search 
      Home | PrePrint | SiteMap | Contact Us | FAQ
Indexed by   SCIE, EI ...
Bimonthly    Since 1986
Journal of Computer Science and Technology 2010, Vol. 25 Issue (4) :827-840    DOI: 10.1007/s11390-010-1064-9
Algorithm and Complexity Current Issue | Archive | Adv Search << Previous Articles | Next Articles >>
Certification of Thread Context Switching
Yu Guo(郭 宇), Xin-Yu Jiang(蒋信予), and Yi-Yun Chen(陈意云)
Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China

Related Articles
Download: [PDF 541KB]     Export: BibTeX or EndNote (RIS)  

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.

Articles by authors
Yu Guo
Xin-Yu Jiang
Yi-Yun Chen
Keywordsprogram verification   context switching   proof-carrying code   program safety     
Received 2009-03-27;

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.

Cite this article:   
Yu Guo(郭 宇), Xin-Yu Jiang(蒋信予), and Yi-Yun Chen(陈意云).Certification of Thread Context Switching[J]  Journal of Computer Science and Technology, 2010,V25(4): 827-840
Copyright 2010 by Journal of Computer Science and Technology