Using XCAP to Certify Realistic Systems Code: Machine Context Management

Formal, modular, and mechanized verification of realistic systems code is desirable but challenging. Verification of machine context management (a basis of multi-tasking) is one representative example. With context operations occurring hundreds to thousands of times per second on every computer, their correctness deserves careful examination. Given the small and stable code bases, it is a common misunderstanding that the context management code is suitable for informal scrutiny and testing. Unfortunately, after being extensively studied and used for decades, it still proves to be a common source of bugs and confusion. Yet its verification remains difficult due to the machine-level detail, irregular patterns of control flows, and rich application scenarios. This paper reports our experience applying XCAP—a recent theoretical verification framework—to certify a realistic x86 implementation of machine context management. XCAP supports expressive and modular logical specificatio...

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: Zhaozhong Ni, Dachuan Yu, Zhong Shao
• Keywords: Artificial Intelligence, Context Management, Context Management Code, Machine Context Management, TPHOL 2007