Verification of Tree-Based Hierarchical Read-Copy Update in the Linux Kernel
Lihao Liang1, Paul E. McKenney2, Daniel Kroening3 and Tom Melham3
1University of Oxford
2IBM Linux Technology Center
3University of Oxford
ABSTRACT
Read-Copy Update (RCU) is a scalable, high performance Linux-kernel synchronization mechanism that runs low-overhead readers concurrently with updaters. Production quality RCU implementations are decidedly non-trivial and their stringent validation is mandatory. This suggests use of formal verification. Previous formal verification efforts for RCU either focus on simple implementations or use modeling languages. In this paper, we construct a model directly from the source code of Tree RCU in the Linux kernel, and use the CBMC program analyzer to verify its safety and liveness properties. To the best of our knowledge, this is the first verification of a significant part of RCU's source code—an important step towards integration of formal verification into the Linux kernel's regression test suite.
