Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel

Lihao Liang, Paul E. McKenney, Daniel Kroening +1

Read-Copy Update (RCU) is a scalable, high-performance Linux-kernel synchronization mechanism that runs low-overhead readers concurrently with updaters. Production-quality RCU impl…