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