README

Formal verification of Sleepable Read-copy-update using CBMC.

This project has been moved into the Linux kernel source tree. See
https://github.com/torvalds/linux/tree/master/tools/testing/selftests/rcutorture/formal/srcu-cbmc
and https://lkml.org/lkml/2017/1/24/736

To run the tests, use the following commands.
autoreconf --install # (If you got the code from git and not a tarball)
./configure --with-linux=<Path to linux kernel source>
make
make check -j<Number of threads>

The version of SRCU in the linux source tree you pass to configure will be used
for verification. Currently only include/linux/srcu.h and kernel/rcu/srcu.c will
be used.

You may want to pass CFLAGS to configure to enable compiler warnings. I
recommend using
CFLAGS="-Wall -Wextra -Wno-unused-parameter -Wno-unused-variable -O2"

The following environment variables specific to this code may be passed to
make check.
CBMC: The command to run CBMC. Default: cbmc
CBMC_FLAGS: Additional flags to pass to CBMC.
NR_CPUS: Number of cpus to run tests with. Default varies depending on the test.
SYNC_SRCU_MODE: Choose implementation of synchronize_srcu. Defaults to "simple".
                kernel: Version included in the linux kernel source.
                simple: Use try_check_zero directly.

Generic options for make check are listed in
https://www.gnu.org/software/automake/manual/html_node/Parallel-Test-Harness.html