Idea: Linux Kernel tests on RCU

[zemanlx]

Linux Kernel tests on RCU

Requested by Daniel Kroening.

Including these tests to CBMC testing to test cbmc and/or linux-rcu.
To be able to to test linux-rcu somebody need to maintain awk script (strip
all things that cbmc is not able to process) in the kernel source so for now
it is feasible to use these tests as another regression tests for cbmc.

Preparation for running tests

git clone git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git

git checkout srcu.2017.01.14a

cd tools/testing/selftests/rcutorture/formal/srcu-cbmc

cbmc binary have to be in PATH or defined in tests/test_script.sh as

CBMC_BIN=/home/zeman/git/cbmc/src/cbmc/cbmc

Test run and expected results

make

awk genarate include/linux/srcu.h and srcu.c.

If we do not need to create those files (we are not following changes in kernel)
we do not need whole kernel just files from current folder
linux-rcu/tools/testing/selftests/rcutorture/formal/srcu-cbmc

Tests are in tests/store_buffering/

• those that have *.pass in file name should have
  VERIFICATION SUCCESSFUL in the last line of *.pass.out file.
• those that have *.fail in file name should have
  VERIFICATION FAILED in the last line of *.fail.out file.

[tautschnig]

While Paul was right in dragging together that awk script, really "strip all things that cbmc is not able to process" should not exist, because the C front end should be able to process all such code.

[tautschnig]

Also note licensing issues, for linux-rcu/the kernel are GPL, which is needs extra care over CBMC's BSD-style licensing.

[TGWDB]

Closing this as old and not touched for a long time. If there is desire to reopen and do something here, see #5916 for some inspiration.

[martin-cs]

Paul McKenney @paulmckrcu does this:

http://www.rdrop.com/users/paulmck/RCU/Validation.2017.01.16a.LCA.pdf

I guess the question is whether there is a gain in having this CI'd in CBMC?

[paulmckrcu]

On Thu, May 20, 2021 at 04:23:25AM -0700, Martin wrote: Paul McKenney @paulmckrcu does this: http://www.rdrop.com/users/paulmck/RCU/Validation.2017.01.16a.LCA.pdf I guess the question is whether there is a gain in having this CI'd in CBMC?

If you are talking about the CBMC verification of SRCU, if you would like to add this, please make sure to use the kernel at the time that it was originally introduced, which I believe is v4.11. The problem we have with this is that the SRCU implementation changes too quickly to reasonably keep the extraction scripts operating correctly. The extraction scripts end up needing to be very tightly coupled to the implementation due to the need to remove code and data that are not absolutely necessary to the verification. In addition, there were some workarounds for CBMC issues involving array accesses back in the day, which for all I know might be fixed by now. Plus the move from the old SRCU implementation to the new Tree SRCU implementation was a bit of a killer, though the central algorithm being verified is conceptually unchanged. But thank you for your interest in this! Thanx, Paul