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...

• Type: Journal
• Year: 2010
• Where: JCST
• Authors: Yu Guo, Xinyu Jiang, Yiyun Chen
• Keywords: JCST 2010, Specifications, Thread Contexts, Threads