Messages in this thread | | | Date | Fri, 22 Oct 2021 02:32:06 -0700 | From | Michel Lespinasse <> | Subject | Re: [PATCH 0/2] rbtree: Test against a verified oracle |
| |
Hi Mete,
I have two questions regarding the approach:
- Has it been considered to compare the tools/lib/rbtree.c library against the oracle, instead of the lib/rbtree.c one, so that the test can run fully in userspace ? The two versions closely follow each other, is there a worry that results would vary between them ?
- lib/rbtree_test.c has code that validates the rbtree invariants (i.e. that all leaf paths have the same black_path_count, etc); is that significantly weaker than comparing the rbtree shape against the oracle ? My worry here is that, if one were to update the rbtree code in ways that preserve the design invariants, but result in a different tree shape, they would now have to reflect those changes into the oracle, which may be difficult if they are not too familiar with haskel ?
(if validating rbtree invariants makes sense, it might still be useful to extend the lib/rbtree_test.c test case generator to cover more than random test cases, as you have done in your proposal...)
Thanks,
On Tue, Oct 19, 2021 at 11:13:47AM +0200, Mete Polat wrote: > 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 >
| |