Validation of RCU

This repository contains code and tests that aim to verify some key properties of the Linux kernel's Read-Copy-Update (RCU) mechanism.

You can find some more information about our attempt to verify the grace period guarantee of Hierarchical RCU (Tree RCU) in this draft (latest revision: 2016/11/30), or this paper (presented at SPIN 2017).

Author: Michalis Kokologiannakis.

• License
• Requirements
• Directories
• Contact

License

The code at this repository is distributed under the GPL, version 2 or (at your option) later. Please see the LICENSE file for details.

Requirements

In order to run the tests in this repository you need the stateless model checking tool Nidhugg.

More information about this tool can be found at this paper.

Directories

• The valtiny directory aims at validating the Tiny RCU flavour.
• The valtree directory aims at validating the Tree RCU flavour.

Contact

Feel free to contact me at: mixaskok at gmail dot com.