lkml.org 
[lkml]   [2021]   [Oct]   [19]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
From
Subject[PATCH 0/2] rbtree: Test against a verified oracle
Date
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-19 11:16    [W:0.063 / U:0.272 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site