Re: [PATCH 0/2] rbtree: Test against a verified oracle

[Mete Polat]

Hi, Michel,

On Fri, Oct 22, 2021 at 02:32:06AM -0700, Michel Lespinasse wrote:
> 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 ?

No I have not considered that, mainly because I wanted to explore what
steps are necessary to test real in-kernel functionality against a
verified oracle and present an example testing pipeline here.

> 
> - 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 ?

The Haskell code also just checks if the kernel rbtrees satisfy the
invariants. While I originally also implemented the option to compare
the shape of the trees, I removed it again because there does not exist
a formal proof for the kernel rbtree delete algorithm yet and the
Haskell variant indeed differs from the kernel one. Currently the
verified oracle is then just used to check if the inorder of kernel and
verified trees equal but one could also check if the shapes equal when
just inserting nodes.

In general, one advantage of comparing shapes instead of checking
invariants is that the former one is faster for bigger inputs. However,
(in my opinion) checking invariants as lib/rbtree_test is doing is at
least as strong as comparing shapes from the correctness point of view.

> 
>   (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...)

This could be a good compromise. An exhaustive (but scoped) test case
generator like in the Haskell code would be a nice extension.

Regards,

Mete
> 
> 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
> >