Skip to content
Systematic Testing of the Read-Copy-Update (RCU) mechanism
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

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.


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


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.


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


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

You can’t perform that action at this time.