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...
Main Authors: | , , , |
---|---|
Format: | Conference item |
Published: |
IEEE
2018
|