Messages in this thread | | | From | Mete Polat <> | Subject | [PATCH 0/2] rbtree: Test against a verified oracle | Date | Tue, 19 Oct 2021 11:13:47 +0200 |
| |
Hi,
This patch series provides a pipeline for testing the kernel Red-Black tree implementation against a verified oracle and is based on the work which we presented on the LPC [1]. A verified oracle is an equivalent algorithm that is proven to be mathematically correct. The testing pipeline consists of a kernel module that exposes the core rbtree functions to userspace using debugfs, and a testing harness that implements two strategies to generate test cases which are then applied on the kernel rbtree and the verified rbtree (the oracle). After executing an operation on both versions, the harness checks if the kernel rbtree is valid by partially comparing it to the verified oracle.
See the second patch for a description of how to use the harness.
Some notes:
The verified rbtree was verified in the proof assistant Isabelle [2] and is written in a functional programming language. That's why I also wrote the testing harness in the functional programming Haskell.
I decided to not try to integrate this work into kselftests because (1) Haskell (obviously) has another build system (2) The tests can run several minutes and would just slow down the execution of all kselftests
There already is a decent rbtree testing module in the kernel. This work tries to address the issue of functional correctness using a more formal method and can be seen as an baseline for future (more complex) testing against verified oracles.
Regards,
Mete
[1] https://linuxplumbersconf.org/event/11/contributions/1036/ [2] https://isabelle.in.tum.de/
Mete Polat (2): rbtree: Expose a test tree to userspace rbtree: add verified oracle with testing harness
lib/Kconfig.debug | 19 ++ lib/Makefile | 1 + lib/test_rbtree_interface.c | 161 +++++++++++ tools/testing/rbtree_oracle/.gitignore | 1 + tools/testing/rbtree_oracle/Main.hs | 128 +++++++++ tools/testing/rbtree_oracle/RBT/Kernel.hs | 64 +++++ tools/testing/rbtree_oracle/RBT/Verified.hs | 253 ++++++++++++++++++ tools/testing/rbtree_oracle/RBT_export.thy | 41 +++ tools/testing/rbtree_oracle/Setup.hs | 2 + tools/testing/rbtree_oracle/Strategy.hs | 72 +++++ .../rbtree_oracle/rbtTestHarness.cabal | 15 ++ 11 files changed, 757 insertions(+) create mode 100644 lib/test_rbtree_interface.c create mode 100644 tools/testing/rbtree_oracle/.gitignore create mode 100644 tools/testing/rbtree_oracle/Main.hs create mode 100644 tools/testing/rbtree_oracle/RBT/Kernel.hs create mode 100644 tools/testing/rbtree_oracle/RBT/Verified.hs create mode 100644 tools/testing/rbtree_oracle/RBT_export.thy create mode 100644 tools/testing/rbtree_oracle/Setup.hs create mode 100644 tools/testing/rbtree_oracle/Strategy.hs create mode 100644 tools/testing/rbtree_oracle/rbtTestHarness.cabal
-- 2.33.1
| |