Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) client-ip=23.128.96.18;
From:   Mete Polat <metepolat2000@gmail.com>
To:     Lukas Bulwahn <lukas.bulwahn@gmail.com>,
        Shuah Khan <shuah@kernel.org>,
        Michel Lespinasse <michel@lespinasse.org>
Cc:     Andrii Nakryiko <andrii@kernel.org>,
        Alexei Starovoitov <ast@kernel.org>,
        "David S. Miller" <davem@davemloft.net>,
        Paolo Bonzini <pbonzini@redhat.com>,
        Daniel Borkmann <daniel@iogearbox.net>,
        "Paul E. McKenney" <paulmck@kernel.org>,
        linux-kernel@vger.kernel.org, Mete Polat <metepolat2000@gmail.com>
Subject: [PATCH 0/2] rbtree: Test against a verified oracle
Date:   Tue, 19 Oct 2021 11:13:47 +0200
Message-Id: <20211019091349.39788-1-metepolat2000@gmail.com>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
Precedence: bulk

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