Verification of tree-based hierarchical read-copy update in the Linux kernel

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

Full description

Bibliographic Details
Main Authors: Liang, L, McKenney, PE, Kroening, D, Melham, TF
Format: Conference item
Published: IEEE 2018