Sciweavers

Share
JCST
2010

Certification of Thread Context Switching

8 years 5 months ago
Certification of Thread Context Switching
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 the context switching in a single logical framework, and the other certifies and the context switching at different abstraction levels. The former requires heavyweight extensions in the logical framework to support first-class code pointers and recursive specifications. Moreover, the specification for context switching is very complex. The later 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 ion 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 the context switching hold p...
Yu Guo, Xinyu Jiang, Yiyun Chen
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Where JCST
Authors Yu Guo, Xinyu Jiang, Yiyun Chen
Comments (0)
books