lkml.org 
[lkml]   [2021]   [Oct]   [22]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [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
>

\
 
 \ /
  Last update: 2021-10-22 11:32    [W:0.081 / U:0.224 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site