Authors

Yu Guo
Xinyu Feng
Zhong Shao
Peizhi Shi

Abstract

Thread management is an essential functionality in OS kernels. However, verification of thread management remains a challenge, due to two conflicting requirements: on the one hand, a thread manager---operating below the thread abstraction layer--should hide its implementation details and be verified independently from the threads being managed; on the other hand, the thread management code in many real-world systems is concurrent, which might be executed by the threads being managed, so it seems inappropriate to abstract threads away in the verification of thread managers. Previous approaches on kernel verification view thread managers as sequential code, thus cannot be applied to thread management in realistic kernels. In this paper, we propose a novel two-layer framework to verify concurrent thread management. We choose a lower abstraction level than the previous approaches, where we abstract away the context switch routine only, and allow the rest of the thread management code to run concurrently in the upper level. We also treat thread management data as abstract resources so that threads in the environment can be specified in assertions and be reasoned about in a proof system similar to concurrent separation logic.

Published

• Proc. 10th Asian Symposium on Programming Languages and Systems (APLAS'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. 7705, pages 315-331. [pdf]