All of lore.kernel.org
 help / color / mirror / Atom feed
* [PATCH 0/2] rbtree: Test against a verified oracle
@ 2021-10-19  9:13 Mete Polat
  2021-10-19  9:13 ` [PATCH 1/2] rbtree: Expose a test tree to userspace Mete Polat
                   ` (2 more replies)
  0 siblings, 3 replies; 9+ messages in thread
From: Mete Polat @ 2021-10-19  9:13 UTC (permalink / raw)
  To: Lukas Bulwahn, Shuah Khan, Michel Lespinasse
  Cc: Andrii Nakryiko, Alexei Starovoitov, David S. Miller,
	Paolo Bonzini, Daniel Borkmann, Paul E. McKenney, linux-kernel,
	Mete Polat

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


^ permalink raw reply	[flat|nested] 9+ messages in thread
* [PATCH 1/2] rbtree: Expose a test tree to userspace
  2021-10-19  9:13 [PATCH 0/2] rbtree: Test against a verified oracle Mete Polat
@ 2021-10-19  9:13 ` Mete Polat
  2021-10-20  6:46     ` kernel test robot
  2021-10-22  5:45     ` kernel test robot
  2021-10-19  9:13 ` [PATCH 2/2] rbtree: add verified oracle with testing harness Mete Polat
  2021-10-22  9:32 ` [PATCH 0/2] rbtree: Test against a verified oracle Michel Lespinasse
  2 siblings, 2 replies; 9+ messages in thread
From: Mete Polat @ 2021-10-19  9:13 UTC (permalink / raw)
  To: Lukas Bulwahn, Shuah Khan, Michel Lespinasse
  Cc: Andrii Nakryiko, Alexei Starovoitov, David S. Miller,
	Paolo Bonzini, Daniel Borkmann, Paul E. McKenney, linux-kernel,
	Mete Polat

Expose rbtree manipulation functions on debugfs. These can be used for
testing the core rbtree implementation from userspace against a verified
oracle (a mathematically proven correct Red-Black tree):

<debugfs>/rbt_if/cmd
  write:
    0 = Reset rbtree (remove all nodes).
    1 = Insert key (see other file) into rbtree.
    2 = Delete key (see other file) from rbtree.
read:
  Print tree.

<debugfs>/rbt_if/key
  Read or write the key used for cmds
---
 lib/Kconfig.debug           |  19 +++++
 lib/Makefile                |   1 +
 lib/test_rbtree_interface.c | 161 ++++++++++++++++++++++++++++++++++++
 3 files changed, 181 insertions(+)
 create mode 100644 lib/test_rbtree_interface.c

diff --git a/lib/Kconfig.debug b/lib/Kconfig.debug
index 3266fef7cb53..675c1a9fab67 100644
--- a/lib/Kconfig.debug
+++ b/lib/Kconfig.debug
@@ -2623,6 +2623,25 @@ config TEST_CLOCKSOURCE_WATCHDOG
 
 	  If unsure, say N.
 
+config TEST_RBTREE_INTERFACE
+	tristate "Expose an Red-Black tree instance to userspace for testing"
+	depends on DEBUG_FS
+	help
+	  Exposes rbtree maniplation functions on debugfs. These can be used for
+	  testing the core rbtree implementation from userspace against a
+	  verified oracle (a mathematically proven correct Red-Black tree):
+	  <debugfs>/rbt_if/cmd
+		write:
+		0 = Reset rbtree (remove all nodes).
+		1 = Insert key (see other file) into rbtree.
+		2 = Delete key (see other file) from rbtree.
+		read:
+		Print tree.
+	  <debugfs>/rbt_if/key
+		Read or write the key used for cmds
+
+	  If unsure, say N.
+
 endif # RUNTIME_TESTING_MENU
 
 config ARCH_USE_MEMTEST
diff --git a/lib/Makefile b/lib/Makefile
index b0cb89451cd3..8e563b959c60 100644
--- a/lib/Makefile
+++ b/lib/Makefile
@@ -100,6 +100,7 @@ obj-$(CONFIG_TEST_MEMINIT) += test_meminit.o
 obj-$(CONFIG_TEST_LOCKUP) += test_lockup.o
 obj-$(CONFIG_TEST_HMM) += test_hmm.o
 obj-$(CONFIG_TEST_FREE_PAGES) += test_free_pages.o
+obj-$(CONFIG_TEST_RBTREE_INTERFACE) += test_rbtree_interface.o
 
 #
 # CFLAGS for compiling floating point code inside the kernel. x86/Makefile turns
diff --git a/lib/test_rbtree_interface.c b/lib/test_rbtree_interface.c
new file mode 100644
index 000000000000..627c41c78a7a
--- /dev/null
+++ b/lib/test_rbtree_interface.c
@@ -0,0 +1,161 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+#define pr_fmt(fmt) "%s:%s: " fmt, KBUILD_MODNAME, __func__
+
+#include <linux/debugfs.h>
+#include <linux/init.h>
+#include <linux/module.h>
+#include <linux/rbtree_augmented.h>
+#include <linux/seq_file.h>
+#include <linux/slab.h>
+#include <linux/types.h>
+
+enum Cmd { RESET, INSERT, DELETE };
+
+static struct dentry *rbt_if_root;
+static struct rb_root rbt = RB_ROOT;
+static u64 input_key;
+
+struct data {
+	struct rb_node node;
+	u64 key;
+};
+
+#define data_from_node(from) (rb_entry(from, struct data, node))
+
+#define print(...) seq_printf(m, __VA_ARGS__)
+#define print_parent print(" (%llu,%s) ", \
+		data_from_node(parent)->key, rb_is_red(parent) ? "Red" : "Black")
+
+static int cmd_show(struct seq_file *m, void *p)
+{
+	struct rb_node *node = rbt.rb_node, *parent = NULL;
+	bool left = false;
+	while(true) {
+		if (!node) {
+			print("Leaf");
+
+			if (!parent)
+				break;
+
+			if (left) {
+				print_parent;
+				node = parent->rb_right;
+				left = false;
+			} else {
+				while (rb_parent(parent) && parent->rb_right == node) {
+					print(")");
+					node = parent;
+					parent = rb_parent(node);
+				}
+
+				if (parent->rb_right == node)
+					break;
+
+				print_parent;
+				node = parent->rb_right;
+				left = false;
+			}
+		} else {
+			if (parent)
+				print("(");
+
+			print("Node ");
+			parent = node;
+			node = node->rb_left;
+			left = true;
+		}
+
+	}
+	print("\n");
+	return 0;
+}
+
+static int key_cmp(const void *_a, const struct rb_node *_b)
+{
+	u64 a = *(typeof(a) *) _a;
+	u64 b = data_from_node(_b)->key;
+	if (a < b)
+		return -1;
+	if (a > b)
+		return 1;
+	else
+		return 0;
+}
+
+static int node_cmp(struct rb_node *a, const struct rb_node *b)
+{
+	return key_cmp(&data_from_node(a)->key, b);
+}
+
+ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
+{
+	int cmd;
+	struct data *data, *_n;
+	struct rb_node *node;
+	int ret = kstrtoint_from_user(ubuf, len, 10, &cmd);
+	if (ret)
+		return ret;
+
+	switch (cmd) {
+	case RESET:
+		rbtree_postorder_for_each_entry_safe(data, _n, &rbt, node)
+			kfree(data);
+		rbt = RB_ROOT;
+		break;
+	case INSERT:
+		data = kzalloc(sizeof(*data), GFP_KERNEL);
+		data->key = input_key;
+		rb_find_add(&data->node, &rbt, node_cmp);
+		break;
+	case DELETE:
+		node = rb_find(&input_key, &rbt, key_cmp);
+		if (!node)
+			break;
+		rb_erase(node, &rbt);
+		kfree(data_from_node(node));
+		break;
+	default:
+		return -EINVAL;
+	}
+	return len;
+}
+
+static int cmd_open(struct inode *inode, struct file *file)
+{
+	return single_open(file, cmd_show, inode->i_private);
+}
+
+static const struct file_operations cmd_fops = {
+	.owner		= THIS_MODULE,
+	.open		= cmd_open,
+	.read		= seq_read,
+	.write		= cmd_exec,
+	.llseek		= seq_lseek,
+	.release	= single_release,
+};
+
+int __init rbt_if_init(void)
+{
+	rbt_if_root = debugfs_create_dir("rbt_if", NULL);
+	if (IS_ERR(rbt_if_root))
+		return PTR_ERR(rbt_if_root);
+
+	debugfs_create_file("cmd", 0644, rbt_if_root, NULL, &cmd_fops);
+	debugfs_create_u64("key", 0644, rbt_if_root, &input_key);
+	return 0;
+}
+
+void __exit rbt_if_exit(void)
+{
+	struct data *_n, *pos;
+	debugfs_remove_recursive(rbt_if_root);
+	rbtree_postorder_for_each_entry_safe(pos, _n, &rbt, node)
+		kfree(pos);
+
+}
+
+module_init(rbt_if_init);
+module_exit(rbt_if_exit);
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Mete Polat <metepolat2000@gmail.com>");
-- 
2.33.1


^ permalink raw reply related	[flat|nested] 9+ messages in thread
* [PATCH 2/2] rbtree: add verified oracle with testing harness
  2021-10-19  9:13 [PATCH 0/2] rbtree: Test against a verified oracle Mete Polat
  2021-10-19  9:13 ` [PATCH 1/2] rbtree: Expose a test tree to userspace Mete Polat
@ 2021-10-19  9:13 ` Mete Polat
  2021-10-22  9:32 ` [PATCH 0/2] rbtree: Test against a verified oracle Michel Lespinasse
  2 siblings, 0 replies; 9+ messages in thread
From: Mete Polat @ 2021-10-19  9:13 UTC (permalink / raw)
  To: Lukas Bulwahn, Shuah Khan, Michel Lespinasse
  Cc: Andrii Nakryiko, Alexei Starovoitov, David S. Miller,
	Paolo Bonzini, Daniel Borkmann, Paul E. McKenney, linux-kernel,
	Mete Polat

The folder rbtree_oracle hosts a Haskell project that consists of:
- the verified Haskell RBT implementation (RBT/Verified.hs)
- a Haskell interface to communicate to the kernel module that exposes
  some rbtree operations (RBT/Kernel.hs)
- two different test strategies (Strategy.hs) which propose test cases
  that are then applied on the oracle (the verified implementation
  RBT/Verified.hs) and on the kernel rbt using the kernel module
  interface.
- a entry point for the executable (Main.hs) which also compares the
  kernel and verified rbtree after executing a test case
- an Isabelle (the proof assistant in which the verified RBT was
  formalized and proved) export file to export the proved RBT
  implementation to Haskell (RBT/Verified.hs; requires Isabelle to
  export).
- files to build the Haskell project with cabal (a build system for
  Haskell)

The whole test suite is in the functional programming language Haskell
because the verified RBT (the oracle) is also written in a functional
language (Isabelle/HOL).

Use 'cabal run rbtTestHarness -- <OPTIONS>' to build and run the test
harness with the specified options. This requires the GHC Haskell
compiler and the Haskell cabal build system.

$ cabal run --verbose=0 rbtTestHarness -- --help
Testing harness for comparing the Linux Red-Black trees against a
verified oracle. The harness immediately stops when a kernel RBT
violates an RBT invariant and prints an error message.

Usage: rbtTestHarness [-v] COMMAND

Available options:
  -v                       Print all executed operations and the
                           resulting trees.
  -h,--help                Show this help text

Available commands:
  random                   Randomly call insert and delete operations on
                           the kernel and oracle without resetting their
			   trees. Will lead to large trees.
  exhaustive               Try (almost) all combinations up to a limit.

$ cabal run --verbose=0 rbtTestHarness -- random --help
Usage: rbtTestHarness random -n ARG [-s <seed>]
  Randomly call insert and delete operations on the kernel and oracle
  without resetting their trees. Will lead to large trees.

Available options:
  -s <seed>                Seed for the pseudo-random-number generator
                           (default: 42)
  -h,--help                Show this help text

$ cabal run --verbose=0 rbtTestHarness -- exhaustive --help
Usage: rbtTestHarness exhaustive -n ARG
  Try (almost) all combinations up to a limit.

Available options:
  -h,--help                Show this help text
---
 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 ++
 8 files changed, 576 insertions(+)
 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

diff --git a/tools/testing/rbtree_oracle/.gitignore b/tools/testing/rbtree_oracle/.gitignore
new file mode 100644
index 000000000000..cfe7d10d198f
--- /dev/null
+++ b/tools/testing/rbtree_oracle/.gitignore
@@ -0,0 +1 @@
+dist-*
diff --git a/tools/testing/rbtree_oracle/Main.hs b/tools/testing/rbtree_oracle/Main.hs
new file mode 100644
index 000000000000..13a83c1b3ce3
--- /dev/null
+++ b/tools/testing/rbtree_oracle/Main.hs
@@ -0,0 +1,128 @@
+{- SPDX-License-Identifier: GPL-2.0-or-later -}
+{- Copyright (C) 2021 Mete Polat -}
+
+module Main where
+
+import Control.Monad
+import Control.Monad.Reader
+import Data.Monoid
+import Data.Word
+import Options.Applicative
+import RBT.Kernel (IRBT, Cmd(..))
+import RBT.Verified
+import Strategy
+import qualified RBT.Kernel as Kernel
+import qualified RBT.Verified as RBT (empty, equal_tree)
+import qualified RBT.Verified as Verified (insert, delete)
+
+data Options = Options {
+  verbose :: Bool,
+  strategy :: Strategy }
+
+type OptionsT m a = ReaderT Options m a
+
+data RandomOptions = RandomOptions {
+  n :: Word64,
+  seed :: Int }
+
+data ExhaustiveOptions = ExhaustiveOptions { n :: Word64 }
+
+data Strategy = Random RandomOptions | Exhaustive ExhaustiveOptions
+
+restartHeader = "------Restart------\n"
+
+
+main :: IO ()
+main = do
+  options@Options{..} <- execParser options
+
+  let rss = case strategy of
+        Random (RandomOptions n seed) -> Strategy.random n seed
+        Exhaustive (ExhaustiveOptions n) -> Strategy.exhaustive n
+
+  unless (null rss) $ do
+    hdl <- Kernel.init
+
+    forM_ rss $ \rs -> do
+      Kernel.reset hdl
+      when verbose $ putStrLn restartHeader
+      runReaderT (checkResults rs RBT.empty hdl) options
+
+    Kernel.cleanup hdl
+
+
+invariantCompare :: IRBT -> IRBT -> Either [String] ()
+invariantCompare vTree kTree = unless (rbt kTree && inorder kTree == inorder vTree) $
+  Left $ map fst $ filter (not . snd) [
+      ("color"     ,  invc kTree) ,
+      ("height"    ,  invh kTree) ,
+      ("root_black",  rootBlack kTree) ,
+      ("inorder"   ,  inorder vTree == inorder kTree) ]
+
+
+printTrees :: Input -> IRBT -> IRBT -> IRBT -> [String] -> IO ()
+printTrees (cmd,key) vTree kTree kTreePrev invs = do
+  putStrLn $ unwords $ if null invs
+  then [show cmd, show key]
+  else ["After", show cmd, show key, "following invariants failed:"] ++ invs
+  putStrLn $ "Kernel tree before:  " ++ show kTreePrev
+  putStrLn $ "Kernel tree after:   " ++ show kTree
+  putStrLn $ "Verified tree after: " ++ show vTree
+  putStrLn ""
+
+
+checkResults :: [Result] -> IRBT -> Kernel.Handle -> OptionsT IO ()
+checkResults [] _ _  = liftIO $ return ()
+checkResults (Result{..}:rs) kTreePrev hdl = do
+  kTree <- liftIO $ kTreeIO hdl
+  case invariantCompare vTree kTree of
+    Left invs -> liftIO $
+      printTrees input vTree kTree kTreePrev invs
+    Right _ -> do
+      v <- asks verbose
+      when v $ liftIO $ printTrees input vTree kTree kTreePrev []
+      checkResults rs kTree hdl
+
+
+{- HLINT ignore options "Monoid law, left identity" -}
+options :: ParserInfo Options
+options = info (opts <**> helper) desc where
+  desc = fullDesc <> header "Testing harness for comparing the \
+    \Linux Red-Black trees against a verified oracle. The harness immediately stops\
+    \ when a kernel RBT violates an RBT invariant and prints an error message."
+  opts = Options
+    <$> switch (short 'v' <> help "Print all executed operations and the resulting trees.")
+    <*> strategies
+
+  randomDesc = progDesc "Randomly call insert and delete operations \
+    \on the kernel and oracle without resetting their trees. Will lead to \
+    \large trees."
+
+  exhaustiveDesc = progDesc "Try (almost) all combinations up to a limit."
+
+  strategies :: Parser Strategy
+  strategies = hsubparser $ mempty
+    <> command "random" (info randomOpts randomDesc)
+    <> command "exhaustive" (info exhaustiveOpts exhaustiveDesc)
+
+  naturalParser :: (Integral i, Read i) => ReadM i
+  naturalParser = eitherReader $ \s ->
+    if 0 <= read s
+    then Right $ read s
+    else Left "Not a positive value"
+
+  numberParser :: (Integral i, Read i) => Parser i
+  numberParser = option naturalParser (short 'n')
+
+  randomOpts :: Parser Strategy
+  randomOpts = fmap Random $ RandomOptions
+    <$> numberParser
+    <*> option auto (mempty
+          <> short 's'
+          <> metavar "<seed>"
+          <> showDefault
+          <> value 42
+          <> help "Seed for the pseudo-random-number generator" )
+
+  exhaustiveOpts :: Parser Strategy
+  exhaustiveOpts = Exhaustive <$> ExhaustiveOptions <$> numberParser
diff --git a/tools/testing/rbtree_oracle/RBT/Kernel.hs b/tools/testing/rbtree_oracle/RBT/Kernel.hs
new file mode 100644
index 000000000000..d1dae30502fc
--- /dev/null
+++ b/tools/testing/rbtree_oracle/RBT/Kernel.hs
@@ -0,0 +1,64 @@
+{- SPDX-License-Identifier: GPL-2.0-or-later -}
+{- Copyright (C) 2021 Mete Polat -}
+
+module RBT.Kernel(Cmd(..), IRBT, RBT.Kernel.Handle, RBT.Kernel.init, cleanup, reset, insert, delete) where
+
+import Control.Exception
+import Control.Monad.Extra
+import Data.Word
+import GHC.IO.Handle
+import RBT.Verified (Tree, Color)
+import System.IO
+import qualified RBT.Verified as RBT
+
+type IRBT = Tree (Word64, Color)
+
+keyFile = "/sys/kernel/debug/rbt_if/key"
+cmdFile = "/sys/kernel/debug/rbt_if/cmd"
+
+data Cmd = Reset | Insert | Delete deriving (Enum, Bounded)
+
+printCmd hdl = hPrint hdl . fromEnum
+
+instance Show Cmd where
+  show Reset = "resetting"
+  show Insert = "inserting"
+  show Delete = "deleting"
+
+data Handle = Handle {
+  keyHdl :: GHC.IO.Handle.Handle,
+  cmdHdl :: GHC.IO.Handle.Handle }
+
+init :: IO RBT.Kernel.Handle
+init = do
+  keyHdl <- openFile keyFile WriteMode
+  cmdHdl <- openFile cmdFile ReadWriteMode
+  let hdl = Handle{..}
+  hSetBuffering keyHdl LineBuffering
+  hSetBuffering cmdHdl LineBuffering
+  reset hdl
+  return hdl
+
+cleanup :: RBT.Kernel.Handle -> IO ()
+cleanup hdl = do
+  reset hdl
+  hClose $ keyHdl hdl
+  hClose $ cmdHdl hdl
+
+exec :: Cmd -> Maybe Word64 -> RBT.Kernel.Handle -> IO IRBT
+exec cmd x Handle{..} = do
+  whenJust x $ hPrint keyHdl
+  printCmd cmdHdl cmd
+  hSeek cmdHdl AbsoluteSeek 0
+  read <$> hGetLine cmdHdl
+
+reset :: RBT.Kernel.Handle -> IO IRBT
+reset hdl = do
+  tree <- exec Reset Nothing hdl
+  assert (RBT.equal_tree RBT.empty tree) $ return tree
+
+insert :: RBT.Kernel.Handle -> Word64 -> IO IRBT
+insert hdl x = exec Insert (Just x) hdl
+
+delete :: RBT.Kernel.Handle -> Word64 -> IO IRBT
+delete hdl x = exec Delete (Just x) hdl
diff --git a/tools/testing/rbtree_oracle/RBT/Verified.hs b/tools/testing/rbtree_oracle/RBT/Verified.hs
new file mode 100644
index 000000000000..74be4722cab6
--- /dev/null
+++ b/tools/testing/rbtree_oracle/RBT/Verified.hs
@@ -0,0 +1,253 @@
+{- SPDX-License-Identifier: BSD-3-Clause -}
+{- Copyright (c) 1986-2021,
+   University of Cambridge,
+   Technische Universitaet Muenchen,
+   and contributors.
+
+   All rights reserved.
+-}
+
+{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}
+
+module
+  RBT.Verified(Color, Nat, Tree, equal_tree, invc, invh, empty, inorder, delete,
+                insert, rootBlack, rbt)
+  where {
+
+import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
+  (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
+  error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
+  zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
+  String, Bool(True, False), Maybe(Nothing, Just));
+import qualified Prelude;
+
+data Color = Red | Black deriving (Prelude.Read, Prelude.Show);
+
+equal_color :: Color -> Color -> Bool;
+equal_color Red Black = False;
+equal_color Black Red = False;
+equal_color Black Black = True;
+equal_color Red Red = True;
+
+instance Eq Color where {
+  a == b = equal_color a b;
+};
+
+newtype Nat = Nat Integer deriving (Prelude.Read, Prelude.Show);
+
+data Num = One | Bit0 Num | Bit1 Num deriving (Prelude.Read, Prelude.Show);
+
+data Tree a = Leaf | Node (Tree a) a (Tree a)
+  deriving (Prelude.Read, Prelude.Show);
+
+data Cmp_val = LT | EQ | GT deriving (Prelude.Read, Prelude.Show);
+
+cmp :: forall a. (Eq a, Prelude.Ord a) => a -> a -> Cmp_val;
+cmp x y = (if x < y then LT else (if x == y then EQ else GT));
+
+paint :: forall a. Color -> Tree (a, Color) -> Tree (a, Color);
+paint c Leaf = Leaf;
+paint c (Node l (a, uu) r) = Node l (a, c) r;
+
+baliR :: forall a. Tree (a, Color) -> a -> Tree (a, Color) -> Tree (a, Color);
+baliR t1 a (Node t2 (b, Red) (Node t3 (c, Red) t4)) =
+  Node (Node t1 (a, Black) t2) (b, Red) (Node t3 (c, Black) t4);
+baliR t1 a (Node (Node t2 (b, Red) t3) (c, Red) Leaf) =
+  Node (Node t1 (a, Black) t2) (b, Red) (Node t3 (c, Black) Leaf);
+baliR t1 a (Node (Node t2 (b, Red) t3) (c, Red) (Node v (vc, Black) vb)) =
+  Node (Node t1 (a, Black) t2) (b, Red)
+    (Node t3 (c, Black) (Node v (vc, Black) vb));
+baliR t1 a Leaf = Node t1 (a, Black) Leaf;
+baliR t1 a (Node v (vc, Black) vb) = Node t1 (a, Black) (Node v (vc, Black) vb);
+baliR t1 a (Node Leaf va Leaf) = Node t1 (a, Black) (Node Leaf va Leaf);
+baliR t1 a (Node (Node vb (ve, Black) vd) va Leaf) =
+  Node t1 (a, Black) (Node (Node vb (ve, Black) vd) va Leaf);
+baliR t1 a (Node Leaf va (Node vc (vf, Black) ve)) =
+  Node t1 (a, Black) (Node Leaf va (Node vc (vf, Black) ve));
+baliR t1 a (Node (Node vb (vh, Black) vg) va (Node vc (vf, Black) ve)) =
+  Node t1 (a, Black)
+    (Node (Node vb (vh, Black) vg) va (Node vc (vf, Black) ve));
+
+baldL :: forall a. Tree (a, Color) -> a -> Tree (a, Color) -> Tree (a, Color);
+baldL (Node t1 (a, Red) t2) b t3 = Node (Node t1 (a, Black) t2) (b, Red) t3;
+baldL Leaf a (Node t2 (b, Black) t3) = baliR Leaf a (Node t2 (b, Red) t3);
+baldL (Node v (vc, Black) vb) a (Node t2 (b, Black) t3) =
+  baliR (Node v (vc, Black) vb) a (Node t2 (b, Red) t3);
+baldL Leaf a (Node (Node t2 (b, Black) t3) (c, Red) t4) =
+  Node (Node Leaf (a, Black) t2) (b, Red) (baliR t3 c (paint Red t4));
+baldL (Node v (vc, Black) vb) a (Node (Node t2 (b, Black) t3) (c, Red) t4) =
+  Node (Node (Node v (vc, Black) vb) (a, Black) t2) (b, Red)
+    (baliR t3 c (paint Red t4));
+baldL Leaf a Leaf = Node Leaf (a, Red) Leaf;
+baldL Leaf a (Node Leaf (vc, Red) vb) =
+  Node Leaf (a, Red) (Node Leaf (vc, Red) vb);
+baldL Leaf a (Node (Node va (vf, Red) ve) (vc, Red) vb) =
+  Node Leaf (a, Red) (Node (Node va (vf, Red) ve) (vc, Red) vb);
+baldL (Node v (vc, Black) vb) a Leaf =
+  Node (Node v (vc, Black) vb) (a, Red) Leaf;
+baldL (Node v (vc, Black) vb) a (Node Leaf (vf, Red) ve) =
+  Node (Node v (vc, Black) vb) (a, Red) (Node Leaf (vf, Red) ve);
+baldL (Node v (vc, Black) vb) a (Node (Node vd (vi, Red) vh) (vf, Red) ve) =
+  Node (Node v (vc, Black) vb) (a, Red)
+    (Node (Node vd (vi, Red) vh) (vf, Red) ve);
+
+join :: forall a. Tree (a, Color) -> Tree (a, Color) -> Tree (a, Color);
+join Leaf t = t;
+join (Node v va vb) Leaf = Node v va vb;
+join (Node t1 (a, Red) t2) (Node t3 (c, Red) t4) =
+  (case join t2 t3 of {
+    Leaf -> Node t1 (a, Red) (Node Leaf (c, Red) t4);
+    Node u2 (b, Red) u3 ->
+      Node (Node t1 (a, Red) u2) (b, Red) (Node u3 (c, Red) t4);
+    Node u2 (b, Black) u3 ->
+      Node t1 (a, Red) (Node (Node u2 (b, Black) u3) (c, Red) t4);
+  });
+join (Node t1 (a, Black) t2) (Node t3 (c, Black) t4) =
+  (case join t2 t3 of {
+    Leaf -> baldL t1 a (Node Leaf (c, Black) t4);
+    Node u2 (b, Red) u3 ->
+      Node (Node t1 (a, Black) u2) (b, Red) (Node u3 (c, Black) t4);
+    Node u2 (b, Black) u3 ->
+      baldL t1 a (Node (Node u2 (b, Black) u3) (c, Black) t4);
+  });
+join (Node v (vc, Black) vb) (Node t2 (a, Red) t3) =
+  Node (join (Node v (vc, Black) vb) t2) (a, Red) t3;
+join (Node t1 (a, Red) t2) (Node v (vc, Black) vb) =
+  Node t1 (a, Red) (join t2 (Node v (vc, Black) vb));
+
+baliL :: forall a. Tree (a, Color) -> a -> Tree (a, Color) -> Tree (a, Color);
+baliL (Node (Node t1 (a, Red) t2) (b, Red) t3) c t4 =
+  Node (Node t1 (a, Black) t2) (b, Red) (Node t3 (c, Black) t4);
+baliL (Node Leaf (a, Red) (Node t2 (b, Red) t3)) c t4 =
+  Node (Node Leaf (a, Black) t2) (b, Red) (Node t3 (c, Black) t4);
+baliL (Node (Node v (vc, Black) vb) (a, Red) (Node t2 (b, Red) t3)) c t4 =
+  Node (Node (Node v (vc, Black) vb) (a, Black) t2) (b, Red)
+    (Node t3 (c, Black) t4);
+baliL Leaf a t2 = Node Leaf (a, Black) t2;
+baliL (Node Leaf (v, Black) vb) a t2 =
+  Node (Node Leaf (v, Black) vb) (a, Black) t2;
+baliL (Node Leaf va Leaf) a t2 = Node (Node Leaf va Leaf) (a, Black) t2;
+baliL (Node Leaf va (Node v (ve, Black) vd)) a t2 =
+  Node (Node Leaf va (Node v (ve, Black) vd)) (a, Black) t2;
+baliL (Node (Node vc (vf, Black) ve) (v, Black) vb) a t2 =
+  Node (Node (Node vc (vf, Black) ve) (v, Black) vb) (a, Black) t2;
+baliL (Node (Node vc (vf, Black) ve) va Leaf) a t2 =
+  Node (Node (Node vc (vf, Black) ve) va Leaf) (a, Black) t2;
+baliL (Node (Node vc (vf, Black) ve) va (Node v (vh, Black) vg)) a t2 =
+  Node (Node (Node vc (vf, Black) ve) va (Node v (vh, Black) vg)) (a, Black) t2;
+baliL (Node v (vc, Black) vb) a t2 = Node (Node v (vc, Black) vb) (a, Black) t2;
+
+baldR :: forall a. Tree (a, Color) -> a -> Tree (a, Color) -> Tree (a, Color);
+baldR t1 a (Node t2 (b, Red) t3) = Node t1 (a, Red) (Node t2 (b, Black) t3);
+baldR (Node t1 (a, Black) t2) b Leaf = baliL (Node t1 (a, Red) t2) b Leaf;
+baldR (Node t1 (a, Black) t2) b (Node v (vc, Black) vb) =
+  baliL (Node t1 (a, Red) t2) b (Node v (vc, Black) vb);
+baldR (Node t1 (a, Red) (Node t2 (b, Black) t3)) c Leaf =
+  Node (baliL (paint Red t1) a t2) (b, Red) (Node t3 (c, Black) Leaf);
+baldR (Node t1 (a, Red) (Node t2 (b, Black) t3)) c (Node v (vc, Black) vb) =
+  Node (baliL (paint Red t1) a t2) (b, Red)
+    (Node t3 (c, Black) (Node v (vc, Black) vb));
+baldR Leaf a Leaf = Node Leaf (a, Red) Leaf;
+baldR (Node v (vc, Red) Leaf) a Leaf =
+  Node (Node v (vc, Red) Leaf) (a, Red) Leaf;
+baldR (Node v (vc, Red) (Node va (vf, Red) ve)) a Leaf =
+  Node (Node v (vc, Red) (Node va (vf, Red) ve)) (a, Red) Leaf;
+baldR Leaf a (Node v (vc, Black) vb) =
+  Node Leaf (a, Red) (Node v (vc, Black) vb);
+baldR (Node va (vf, Red) Leaf) a (Node v (vc, Black) vb) =
+  Node (Node va (vf, Red) Leaf) (a, Red) (Node v (vc, Black) vb);
+baldR (Node va (vf, Red) (Node vd (vi, Red) vh)) a (Node v (vc, Black) vb) =
+  Node (Node va (vf, Red) (Node vd (vi, Red) vh)) (a, Red)
+    (Node v (vc, Black) vb);
+
+equal_tree :: forall a. (Eq a) => Tree a -> Tree a -> Bool;
+equal_tree Leaf (Node x21 x22 x23) = False;
+equal_tree (Node x21 x22 x23) Leaf = False;
+equal_tree (Node x21 x22 x23) (Node y21 y22 y23) =
+  equal_tree x21 y21 && x22 == y22 && equal_tree x23 y23;
+equal_tree Leaf Leaf = True;
+
+color :: forall a. Tree (a, Color) -> Color;
+color Leaf = Black;
+color (Node uu (uv, c) uw) = c;
+
+del ::
+  forall a. (Eq a, Prelude.Ord a) => a -> Tree (a, Color) -> Tree (a, Color);
+del x Leaf = Leaf;
+del x (Node l (a, uu) r) =
+  (case cmp x a of {
+    LT -> (if not (equal_tree l Leaf) && equal_color (color l) Black
+            then baldL (del x l) a r else Node (del x l) (a, Red) r);
+    EQ -> join l r;
+    GT -> (if not (equal_tree r Leaf) && equal_color (color r) Black
+            then baldR l a (del x r) else Node l (a, Red) (del x r));
+  });
+
+ins ::
+  forall a. (Eq a, Prelude.Ord a) => a -> Tree (a, Color) -> Tree (a, Color);
+ins x Leaf = Node Leaf (x, Red) Leaf;
+ins x (Node l (a, Black) r) = (case cmp x a of {
+                                LT -> baliL (ins x l) a r;
+                                EQ -> Node l (a, Black) r;
+                                GT -> baliR l a (ins x r);
+                              });
+ins x (Node l (a, Red) r) = (case cmp x a of {
+                              LT -> Node (ins x l) (a, Red) r;
+                              EQ -> Node l (a, Red) r;
+                              GT -> Node l (a, Red) (ins x r);
+                            });
+
+invc :: forall a. Tree (a, Color) -> Bool;
+invc Leaf = True;
+invc (Node l (a, c) r) =
+  (if equal_color c Red
+    then equal_color (color l) Black && equal_color (color r) Black
+    else True) &&
+    invc l && invc r;
+
+integer_of_nat :: Nat -> Integer;
+integer_of_nat (Nat x) = x;
+
+equal_nat :: Nat -> Nat -> Bool;
+equal_nat m n = integer_of_nat m == integer_of_nat n;
+
+zero_nat :: Nat;
+zero_nat = Nat (0 :: Integer);
+
+plus_nat :: Nat -> Nat -> Nat;
+plus_nat m n = Nat (integer_of_nat m + integer_of_nat n);
+
+one_nat :: Nat;
+one_nat = Nat (1 :: Integer);
+
+bheight :: forall a. Tree (a, Color) -> Nat;
+bheight Leaf = zero_nat;
+bheight (Node l (x, c) r) =
+  (if equal_color c Black then plus_nat (bheight l) one_nat else bheight l);
+
+invh :: forall a. Tree (a, Color) -> Bool;
+invh Leaf = True;
+invh (Node l (x, c) r) = equal_nat (bheight l) (bheight r) && invh l && invh r;
+
+empty :: forall a. Tree (a, Color);
+empty = Leaf;
+
+inorder :: forall a b. Tree (a, b) -> [a];
+inorder Leaf = [];
+inorder (Node l (a, uu) r) = inorder l ++ a : inorder r;
+
+delete ::
+  forall a. (Eq a, Prelude.Ord a) => a -> Tree (a, Color) -> Tree (a, Color);
+delete x t = paint Black (del x t);
+
+insert ::
+  forall a. (Eq a, Prelude.Ord a) => a -> Tree (a, Color) -> Tree (a, Color);
+insert x t = paint Black (ins x t);
+
+rootBlack :: forall a. Tree (a, Color) -> Bool;
+rootBlack t = equal_color (color t) Black;
+
+rbt :: forall a. Tree (a, Color) -> Bool;
+rbt t = invc t && invh t && rootBlack t;
+
+}
diff --git a/tools/testing/rbtree_oracle/RBT_export.thy b/tools/testing/rbtree_oracle/RBT_export.thy
new file mode 100644
index 000000000000..4d4f916ce0e3
--- /dev/null
+++ b/tools/testing/rbtree_oracle/RBT_export.thy
@@ -0,0 +1,41 @@
+(* SPDX-License-Identifier: GPL-2.0-or-later *)
+(* Copyright (C) 2021 Mete Polat *)
+
+theory RBT_export
+imports
+  "HOL-Data_Structures.RBT_Set"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Code_Target_Numeral"
+begin
+
+(*
+Map all the different orderings to Haskell's linorder class.
+This is fine because the RBT interface only uses linorder.
+*)
+
+code_printing
+  type_class ord \<rightharpoonup> (Haskell) "Prelude.Ord"
+| constant Orderings.less \<rightharpoonup> (Haskell) infixl 4 "<"
+| constant Orderings.less_eq \<rightharpoonup> (Haskell) infixl 4 "<="
+| type_class order \<rightharpoonup> (Haskell) "Prelude.Ord"
+| type_class preorder \<rightharpoonup> (Haskell) "Prelude.Ord"
+| type_class linorder \<rightharpoonup> (Haskell) "Prelude.Ord"
+
+definition rootBlack :: "'a rbt \<Rightarrow> bool" where
+"rootBlack t \<equiv> color t = Black"
+
+definition rbt :: "'a rbt \<Rightarrow> bool" where
+"rbt t \<equiv> invc t \<and> invh t \<and> rootBlack t"
+
+lemma "RBT_Set.rbt t \<equiv> rbt t"
+  by (simp add: RBT_Set.rbt_def rbt_def rootBlack_def)
+
+export_code
+  rootBlack rbt
+  RBT_Set.invc RBT_Set.invh
+  RBT_Set.empty RBT_Set.insert RBT_Set.delete
+  Tree2.inorder
+  equal_tree_inst.equal_tree
+in Haskell module_name RBT.Verified (string_classes)
+
+end
diff --git a/tools/testing/rbtree_oracle/Setup.hs b/tools/testing/rbtree_oracle/Setup.hs
new file mode 100644
index 000000000000..9a994af677b0
--- /dev/null
+++ b/tools/testing/rbtree_oracle/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/tools/testing/rbtree_oracle/Strategy.hs b/tools/testing/rbtree_oracle/Strategy.hs
new file mode 100644
index 000000000000..e929ef8e4172
--- /dev/null
+++ b/tools/testing/rbtree_oracle/Strategy.hs
@@ -0,0 +1,72 @@
+{- SPDX-License-Identifier: GPL-2.0-or-later -}
+{- Copyright (C) 2021 Mete Polat -}
+
+module Strategy (Result(..), Input, TestCase, random, exhaustive) where
+
+
+import Control.Applicative
+import Control.Monad
+import Data.Bifunctor
+import Data.List
+import Data.Word
+import RBT.Kernel (IRBT, Cmd(..))
+import RBT.Verified (Tree, Color)
+import System.Random (uniform, mkStdGen)
+import System.Random.Stateful (Uniform, uniformM, uniformRM)
+import qualified RBT.Kernel as Kernel
+import qualified RBT.Verified as RBT (empty)
+import qualified RBT.Verified as Verified (insert, delete)
+
+type Input = (Cmd,Word64)
+type TestCase a = [a]
+
+data Result = Result {
+  input :: Input,
+  vTree :: IRBT,
+  kTreeIO :: Kernel.Handle -> IO IRBT }
+
+instance Uniform Cmd where
+  uniformM g = toEnum <$> uniformRM (succ minCmd, maxCmd) g
+    where
+      minCmd = fromEnum (minBound :: Cmd)
+      maxCmd = fromEnum (maxBound :: Cmd)
+
+cmdMap :: Cmd -> (Word64 -> IRBT -> IRBT, Kernel.Handle -> Word64 -> IO IRBT)
+cmdMap Insert = (Verified.insert, Kernel.insert)
+cmdMap Delete = (Verified.delete, Kernel.delete)
+cmdMap Reset = undefined
+
+vCmd :: IRBT -> Input -> IRBT
+vCmd t (c,x) = (fst $ cmdMap c) x t
+
+kCmd :: Input -> Kernel.Handle -> IO IRBT
+kCmd (c,x) hdl = (snd $ cmdMap c) hdl x
+
+buildInput :: [Word64] -> [Word64] -> [Cmd] -> TestCase Input
+buildInput _ _ [] = []
+buildInput (i:is) ds (Insert : cs) = (Insert, i) : buildInput is ds cs
+buildInput is (d:ds) (Delete : cs) = (Delete, d) : buildInput is ds cs
+buildInput _ _ _ = undefined
+
+buildResults :: [TestCase Input] -> [TestCase Result]
+buildResults testCases = do
+  inputs <- testCases
+  let vTrees = tail $ scanl vCmd RBT.empty inputs
+  let kTrees = map kCmd inputs
+  return $ zipWith3 Result inputs vTrees kTrees
+
+random :: Word64 -> Int -> [TestCase Result]
+random runs seed = do
+  let rndCmds = randoms seed
+  let rndXs = randoms seed
+  let inputs = genericTake runs (buildInput rndXs rndXs rndCmds)
+  buildResults [inputs]
+  where
+    randoms :: Uniform a => Int -> [a]
+    randoms = unfoldr (Just . uniform) . mkStdGen
+
+exhaustive :: Word64 -> [TestCase Result]
+exhaustive n = do
+  let distributions = [genericReplicate i Insert ++ genericReplicate (n-i) Delete | i <- [n,n-1..]]
+  let inputRuns = concatMap (permutations . buildInput [1..n] [1..n]) distributions
+  buildResults inputRuns
diff --git a/tools/testing/rbtree_oracle/rbtTestHarness.cabal b/tools/testing/rbtree_oracle/rbtTestHarness.cabal
new file mode 100644
index 000000000000..f2e403d1dd8f
--- /dev/null
+++ b/tools/testing/rbtree_oracle/rbtTestHarness.cabal
@@ -0,0 +1,15 @@
+cabal-version:       2.4
+name:                rbtTestHarness
+version:             1.0.0.0
+
+executable rbtTestHarness
+  main-is:             Main.hs
+  other-modules:       Strategy RBT.Kernel RBT.Verified
+  build-depends:       base ^>=4.15,
+                       random,
+                       optparse-applicative,
+                       extra,
+                       mtl
+  default-language:    Haskell2010
+  default-extensions:  RecordWildCards, DuplicateRecordFields
+  license:             GPL-2.0
-- 
2.33.1


^ permalink raw reply related	[flat|nested] 9+ messages in thread
* Re: [PATCH 1/2] rbtree: Expose a test tree to userspace
  2021-10-19  9:13 ` [PATCH 1/2] rbtree: Expose a test tree to userspace Mete Polat
@ 2021-10-20  6:46     ` kernel test robot
  2021-10-22  5:45     ` kernel test robot
  1 sibling, 0 replies; 9+ messages in thread
From: kernel test robot @ 2021-10-20  6:46 UTC (permalink / raw)
  To: Mete Polat, Lukas Bulwahn, Shuah Khan, Michel Lespinasse
  Cc: llvm, kbuild-all, Andrii Nakryiko, Alexei Starovoitov,
	Paolo Bonzini, Daniel Borkmann, Paul E. McKenney, linux-kernel,
	Mete Polat

[-- Attachment #1: Type: text/plain, Size: 4811 bytes --]

Hi Mete,

Thank you for the patch! Perhaps something to improve:

[auto build test WARNING on linus/master]
[also build test WARNING on v5.15-rc6 next-20211019]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch]

url:    https://github.com/0day-ci/linux/commits/Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
base:   https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git 519d81956ee277b4419c723adfb154603c2565ba
config: hexagon-randconfig-r033-20211019 (attached as .config)
compiler: clang version 14.0.0 (https://github.com/llvm/llvm-project b37efed957ed0a0193d80020aefd55cb587dfc1f)
reproduce (this is a W=1 build):
        wget https://raw.githubusercontent.com/intel/lkp-tests/master/sbin/make.cross -O ~/bin/make.cross
        chmod +x ~/bin/make.cross
        # https://github.com/0day-ci/linux/commit/d73723d42ad47ca335de00e899a9e94b03d8b57d
        git remote add linux-review https://github.com/0day-ci/linux
        git fetch --no-tags linux-review Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
        git checkout d73723d42ad47ca335de00e899a9e94b03d8b57d
        # save the attached .config to linux build tree
        COMPILER_INSTALL_PATH=$HOME/0day COMPILER=clang make.cross W=1 ARCH=hexagon 

If you fix the issue, kindly add following tag as appropriate
Reported-by: kernel test robot <lkp@intel.com>

All warnings (new ones prefixed by >>):

>> lib/test_rbtree_interface.c:91:9: warning: no previous prototype for function 'cmd_exec' [-Wmissing-prototypes]
   ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
           ^
   lib/test_rbtree_interface.c:91:1: note: declare 'static' if the function is not intended to be used outside of this translation unit
   ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
   ^
   static 
>> lib/test_rbtree_interface.c:138:12: warning: no previous prototype for function 'rbt_if_init' [-Wmissing-prototypes]
   int __init rbt_if_init(void)
              ^
   lib/test_rbtree_interface.c:138:1: note: declare 'static' if the function is not intended to be used outside of this translation unit
   int __init rbt_if_init(void)
   ^
   static 
>> lib/test_rbtree_interface.c:149:13: warning: no previous prototype for function 'rbt_if_exit' [-Wmissing-prototypes]
   void __exit rbt_if_exit(void)
               ^
   lib/test_rbtree_interface.c:149:1: note: declare 'static' if the function is not intended to be used outside of this translation unit
   void __exit rbt_if_exit(void)
   ^
   static 
   3 warnings generated.


vim +/cmd_exec +91 lib/test_rbtree_interface.c

    90	
  > 91	ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
    92	{
    93		int cmd;
    94		struct data *data, *_n;
    95		struct rb_node *node;
    96		int ret = kstrtoint_from_user(ubuf, len, 10, &cmd);
    97		if (ret)
    98			return ret;
    99	
   100		switch (cmd) {
   101		case RESET:
   102			rbtree_postorder_for_each_entry_safe(data, _n, &rbt, node)
   103				kfree(data);
   104			rbt = RB_ROOT;
   105			break;
   106		case INSERT:
   107			data = kzalloc(sizeof(*data), GFP_KERNEL);
   108			data->key = input_key;
   109			rb_find_add(&data->node, &rbt, node_cmp);
   110			break;
   111		case DELETE:
   112			node = rb_find(&input_key, &rbt, key_cmp);
   113			if (!node)
   114				break;
   115			rb_erase(node, &rbt);
   116			kfree(data_from_node(node));
   117			break;
   118		default:
   119			return -EINVAL;
   120		}
   121		return len;
   122	}
   123	
   124	static int cmd_open(struct inode *inode, struct file *file)
   125	{
   126		return single_open(file, cmd_show, inode->i_private);
   127	}
   128	
   129	static const struct file_operations cmd_fops = {
   130		.owner		= THIS_MODULE,
   131		.open		= cmd_open,
   132		.read		= seq_read,
   133		.write		= cmd_exec,
   134		.llseek		= seq_lseek,
   135		.release	= single_release,
   136	};
   137	
 > 138	int __init rbt_if_init(void)
   139	{
   140		rbt_if_root = debugfs_create_dir("rbt_if", NULL);
   141		if (IS_ERR(rbt_if_root))
   142			return PTR_ERR(rbt_if_root);
   143	
   144		debugfs_create_file("cmd", 0644, rbt_if_root, NULL, &cmd_fops);
   145		debugfs_create_u64("key", 0644, rbt_if_root, &input_key);
   146		return 0;
   147	}
   148	
 > 149	void __exit rbt_if_exit(void)
   150	{
   151		struct data *_n, *pos;
   152		debugfs_remove_recursive(rbt_if_root);
   153		rbtree_postorder_for_each_entry_safe(pos, _n, &rbt, node)
   154			kfree(pos);
   155	

---
0-DAY CI Kernel Test Service, Intel Corporation
https://lists.01.org/hyperkitty/list/kbuild-all@lists.01.org

[-- Attachment #2: .config.gz --]
[-- Type: application/gzip, Size: 31462 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread
* Re: [PATCH 1/2] rbtree: Expose a test tree to userspace
@ 2021-10-20  6:46     ` kernel test robot
  0 siblings, 0 replies; 9+ messages in thread
From: kernel test robot @ 2021-10-20  6:46 UTC (permalink / raw)
  To: kbuild-all

[-- Attachment #1: Type: text/plain, Size: 4938 bytes --]

Hi Mete,

Thank you for the patch! Perhaps something to improve:

[auto build test WARNING on linus/master]
[also build test WARNING on v5.15-rc6 next-20211019]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch]

url:    https://github.com/0day-ci/linux/commits/Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
base:   https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git 519d81956ee277b4419c723adfb154603c2565ba
config: hexagon-randconfig-r033-20211019 (attached as .config)
compiler: clang version 14.0.0 (https://github.com/llvm/llvm-project b37efed957ed0a0193d80020aefd55cb587dfc1f)
reproduce (this is a W=1 build):
        wget https://raw.githubusercontent.com/intel/lkp-tests/master/sbin/make.cross -O ~/bin/make.cross
        chmod +x ~/bin/make.cross
        # https://github.com/0day-ci/linux/commit/d73723d42ad47ca335de00e899a9e94b03d8b57d
        git remote add linux-review https://github.com/0day-ci/linux
        git fetch --no-tags linux-review Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
        git checkout d73723d42ad47ca335de00e899a9e94b03d8b57d
        # save the attached .config to linux build tree
        COMPILER_INSTALL_PATH=$HOME/0day COMPILER=clang make.cross W=1 ARCH=hexagon 

If you fix the issue, kindly add following tag as appropriate
Reported-by: kernel test robot <lkp@intel.com>

All warnings (new ones prefixed by >>):

>> lib/test_rbtree_interface.c:91:9: warning: no previous prototype for function 'cmd_exec' [-Wmissing-prototypes]
   ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
           ^
   lib/test_rbtree_interface.c:91:1: note: declare 'static' if the function is not intended to be used outside of this translation unit
   ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
   ^
   static 
>> lib/test_rbtree_interface.c:138:12: warning: no previous prototype for function 'rbt_if_init' [-Wmissing-prototypes]
   int __init rbt_if_init(void)
              ^
   lib/test_rbtree_interface.c:138:1: note: declare 'static' if the function is not intended to be used outside of this translation unit
   int __init rbt_if_init(void)
   ^
   static 
>> lib/test_rbtree_interface.c:149:13: warning: no previous prototype for function 'rbt_if_exit' [-Wmissing-prototypes]
   void __exit rbt_if_exit(void)
               ^
   lib/test_rbtree_interface.c:149:1: note: declare 'static' if the function is not intended to be used outside of this translation unit
   void __exit rbt_if_exit(void)
   ^
   static 
   3 warnings generated.


vim +/cmd_exec +91 lib/test_rbtree_interface.c

    90	
  > 91	ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
    92	{
    93		int cmd;
    94		struct data *data, *_n;
    95		struct rb_node *node;
    96		int ret = kstrtoint_from_user(ubuf, len, 10, &cmd);
    97		if (ret)
    98			return ret;
    99	
   100		switch (cmd) {
   101		case RESET:
   102			rbtree_postorder_for_each_entry_safe(data, _n, &rbt, node)
   103				kfree(data);
   104			rbt = RB_ROOT;
   105			break;
   106		case INSERT:
   107			data = kzalloc(sizeof(*data), GFP_KERNEL);
   108			data->key = input_key;
   109			rb_find_add(&data->node, &rbt, node_cmp);
   110			break;
   111		case DELETE:
   112			node = rb_find(&input_key, &rbt, key_cmp);
   113			if (!node)
   114				break;
   115			rb_erase(node, &rbt);
   116			kfree(data_from_node(node));
   117			break;
   118		default:
   119			return -EINVAL;
   120		}
   121		return len;
   122	}
   123	
   124	static int cmd_open(struct inode *inode, struct file *file)
   125	{
   126		return single_open(file, cmd_show, inode->i_private);
   127	}
   128	
   129	static const struct file_operations cmd_fops = {
   130		.owner		= THIS_MODULE,
   131		.open		= cmd_open,
   132		.read		= seq_read,
   133		.write		= cmd_exec,
   134		.llseek		= seq_lseek,
   135		.release	= single_release,
   136	};
   137	
 > 138	int __init rbt_if_init(void)
   139	{
   140		rbt_if_root = debugfs_create_dir("rbt_if", NULL);
   141		if (IS_ERR(rbt_if_root))
   142			return PTR_ERR(rbt_if_root);
   143	
   144		debugfs_create_file("cmd", 0644, rbt_if_root, NULL, &cmd_fops);
   145		debugfs_create_u64("key", 0644, rbt_if_root, &input_key);
   146		return 0;
   147	}
   148	
 > 149	void __exit rbt_if_exit(void)
   150	{
   151		struct data *_n, *pos;
   152		debugfs_remove_recursive(rbt_if_root);
   153		rbtree_postorder_for_each_entry_safe(pos, _n, &rbt, node)
   154			kfree(pos);
   155	

---
0-DAY CI Kernel Test Service, Intel Corporation
https://lists.01.org/hyperkitty/list/kbuild-all(a)lists.01.org

[-- Attachment #2: config.gz --]
[-- Type: application/gzip, Size: 31462 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread
* Re: [PATCH 1/2] rbtree: Expose a test tree to userspace
  2021-10-19  9:13 ` [PATCH 1/2] rbtree: Expose a test tree to userspace Mete Polat
@ 2021-10-22  5:45     ` kernel test robot
  2021-10-22  5:45     ` kernel test robot
  1 sibling, 0 replies; 9+ messages in thread
From: kernel test robot @ 2021-10-22  5:45 UTC (permalink / raw)
  To: Mete Polat, Lukas Bulwahn, Shuah Khan, Michel Lespinasse
  Cc: kbuild-all, Andrii Nakryiko, Alexei Starovoitov, Paolo Bonzini,
	Daniel Borkmann, Paul E. McKenney, linux-kernel, Mete Polat

[-- Attachment #1: Type: text/plain, Size: 4148 bytes --]

Hi Mete,

Thank you for the patch! Perhaps something to improve:

[auto build test WARNING on linus/master]
[also build test WARNING on v5.15-rc6 next-20211021]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch]

url:    https://github.com/0day-ci/linux/commits/Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
base:   https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git 519d81956ee277b4419c723adfb154603c2565ba
config: nds32-randconfig-r032-20211019 (attached as .config)
compiler: nds32le-linux-gcc (GCC) 11.2.0
reproduce (this is a W=1 build):
        wget https://raw.githubusercontent.com/intel/lkp-tests/master/sbin/make.cross -O ~/bin/make.cross
        chmod +x ~/bin/make.cross
        # https://github.com/0day-ci/linux/commit/d73723d42ad47ca335de00e899a9e94b03d8b57d
        git remote add linux-review https://github.com/0day-ci/linux
        git fetch --no-tags linux-review Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
        git checkout d73723d42ad47ca335de00e899a9e94b03d8b57d
        # save the attached .config to linux build tree
        COMPILER_INSTALL_PATH=$HOME/0day COMPILER=gcc-11.2.0 make.cross ARCH=nds32 

If you fix the issue, kindly add following tag as appropriate
Reported-by: kernel test robot <lkp@intel.com>

All warnings (new ones prefixed by >>):

>> lib/test_rbtree_interface.c:91:9: warning: no previous prototype for 'cmd_exec' [-Wmissing-prototypes]
      91 | ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
         |         ^~~~~~~~
>> lib/test_rbtree_interface.c:138:12: warning: no previous prototype for 'rbt_if_init' [-Wmissing-prototypes]
     138 | int __init rbt_if_init(void)
         |            ^~~~~~~~~~~
>> lib/test_rbtree_interface.c:149:13: warning: no previous prototype for 'rbt_if_exit' [-Wmissing-prototypes]
     149 | void __exit rbt_if_exit(void)
         |             ^~~~~~~~~~~


vim +/cmd_exec +91 lib/test_rbtree_interface.c

    90	
  > 91	ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
    92	{
    93		int cmd;
    94		struct data *data, *_n;
    95		struct rb_node *node;
    96		int ret = kstrtoint_from_user(ubuf, len, 10, &cmd);
    97		if (ret)
    98			return ret;
    99	
   100		switch (cmd) {
   101		case RESET:
   102			rbtree_postorder_for_each_entry_safe(data, _n, &rbt, node)
   103				kfree(data);
   104			rbt = RB_ROOT;
   105			break;
   106		case INSERT:
   107			data = kzalloc(sizeof(*data), GFP_KERNEL);
   108			data->key = input_key;
   109			rb_find_add(&data->node, &rbt, node_cmp);
   110			break;
   111		case DELETE:
   112			node = rb_find(&input_key, &rbt, key_cmp);
   113			if (!node)
   114				break;
   115			rb_erase(node, &rbt);
   116			kfree(data_from_node(node));
   117			break;
   118		default:
   119			return -EINVAL;
   120		}
   121		return len;
   122	}
   123	
   124	static int cmd_open(struct inode *inode, struct file *file)
   125	{
   126		return single_open(file, cmd_show, inode->i_private);
   127	}
   128	
   129	static const struct file_operations cmd_fops = {
   130		.owner		= THIS_MODULE,
   131		.open		= cmd_open,
   132		.read		= seq_read,
   133		.write		= cmd_exec,
   134		.llseek		= seq_lseek,
   135		.release	= single_release,
   136	};
   137	
 > 138	int __init rbt_if_init(void)
   139	{
   140		rbt_if_root = debugfs_create_dir("rbt_if", NULL);
   141		if (IS_ERR(rbt_if_root))
   142			return PTR_ERR(rbt_if_root);
   143	
   144		debugfs_create_file("cmd", 0644, rbt_if_root, NULL, &cmd_fops);
   145		debugfs_create_u64("key", 0644, rbt_if_root, &input_key);
   146		return 0;
   147	}
   148	
 > 149	void __exit rbt_if_exit(void)
   150	{
   151		struct data *_n, *pos;
   152		debugfs_remove_recursive(rbt_if_root);
   153		rbtree_postorder_for_each_entry_safe(pos, _n, &rbt, node)
   154			kfree(pos);
   155	

---
0-DAY CI Kernel Test Service, Intel Corporation
https://lists.01.org/hyperkitty/list/kbuild-all@lists.01.org

[-- Attachment #2: .config.gz --]
[-- Type: application/gzip, Size: 25009 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread
* Re: [PATCH 1/2] rbtree: Expose a test tree to userspace
@ 2021-10-22  5:45     ` kernel test robot
  0 siblings, 0 replies; 9+ messages in thread
From: kernel test robot @ 2021-10-22  5:45 UTC (permalink / raw)
  To: kbuild-all

[-- Attachment #1: Type: text/plain, Size: 4262 bytes --]

Hi Mete,

Thank you for the patch! Perhaps something to improve:

[auto build test WARNING on linus/master]
[also build test WARNING on v5.15-rc6 next-20211021]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch]

url:    https://github.com/0day-ci/linux/commits/Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
base:   https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git 519d81956ee277b4419c723adfb154603c2565ba
config: nds32-randconfig-r032-20211019 (attached as .config)
compiler: nds32le-linux-gcc (GCC) 11.2.0
reproduce (this is a W=1 build):
        wget https://raw.githubusercontent.com/intel/lkp-tests/master/sbin/make.cross -O ~/bin/make.cross
        chmod +x ~/bin/make.cross
        # https://github.com/0day-ci/linux/commit/d73723d42ad47ca335de00e899a9e94b03d8b57d
        git remote add linux-review https://github.com/0day-ci/linux
        git fetch --no-tags linux-review Mete-Polat/rbtree-Test-against-a-verified-oracle/20211019-171711
        git checkout d73723d42ad47ca335de00e899a9e94b03d8b57d
        # save the attached .config to linux build tree
        COMPILER_INSTALL_PATH=$HOME/0day COMPILER=gcc-11.2.0 make.cross ARCH=nds32 

If you fix the issue, kindly add following tag as appropriate
Reported-by: kernel test robot <lkp@intel.com>

All warnings (new ones prefixed by >>):

>> lib/test_rbtree_interface.c:91:9: warning: no previous prototype for 'cmd_exec' [-Wmissing-prototypes]
      91 | ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
         |         ^~~~~~~~
>> lib/test_rbtree_interface.c:138:12: warning: no previous prototype for 'rbt_if_init' [-Wmissing-prototypes]
     138 | int __init rbt_if_init(void)
         |            ^~~~~~~~~~~
>> lib/test_rbtree_interface.c:149:13: warning: no previous prototype for 'rbt_if_exit' [-Wmissing-prototypes]
     149 | void __exit rbt_if_exit(void)
         |             ^~~~~~~~~~~


vim +/cmd_exec +91 lib/test_rbtree_interface.c

    90	
  > 91	ssize_t cmd_exec(struct file *file, const char __user *ubuf, size_t len, loff_t *offp)
    92	{
    93		int cmd;
    94		struct data *data, *_n;
    95		struct rb_node *node;
    96		int ret = kstrtoint_from_user(ubuf, len, 10, &cmd);
    97		if (ret)
    98			return ret;
    99	
   100		switch (cmd) {
   101		case RESET:
   102			rbtree_postorder_for_each_entry_safe(data, _n, &rbt, node)
   103				kfree(data);
   104			rbt = RB_ROOT;
   105			break;
   106		case INSERT:
   107			data = kzalloc(sizeof(*data), GFP_KERNEL);
   108			data->key = input_key;
   109			rb_find_add(&data->node, &rbt, node_cmp);
   110			break;
   111		case DELETE:
   112			node = rb_find(&input_key, &rbt, key_cmp);
   113			if (!node)
   114				break;
   115			rb_erase(node, &rbt);
   116			kfree(data_from_node(node));
   117			break;
   118		default:
   119			return -EINVAL;
   120		}
   121		return len;
   122	}
   123	
   124	static int cmd_open(struct inode *inode, struct file *file)
   125	{
   126		return single_open(file, cmd_show, inode->i_private);
   127	}
   128	
   129	static const struct file_operations cmd_fops = {
   130		.owner		= THIS_MODULE,
   131		.open		= cmd_open,
   132		.read		= seq_read,
   133		.write		= cmd_exec,
   134		.llseek		= seq_lseek,
   135		.release	= single_release,
   136	};
   137	
 > 138	int __init rbt_if_init(void)
   139	{
   140		rbt_if_root = debugfs_create_dir("rbt_if", NULL);
   141		if (IS_ERR(rbt_if_root))
   142			return PTR_ERR(rbt_if_root);
   143	
   144		debugfs_create_file("cmd", 0644, rbt_if_root, NULL, &cmd_fops);
   145		debugfs_create_u64("key", 0644, rbt_if_root, &input_key);
   146		return 0;
   147	}
   148	
 > 149	void __exit rbt_if_exit(void)
   150	{
   151		struct data *_n, *pos;
   152		debugfs_remove_recursive(rbt_if_root);
   153		rbtree_postorder_for_each_entry_safe(pos, _n, &rbt, node)
   154			kfree(pos);
   155	

---
0-DAY CI Kernel Test Service, Intel Corporation
https://lists.01.org/hyperkitty/list/kbuild-all(a)lists.01.org

[-- Attachment #2: config.gz --]
[-- Type: application/gzip, Size: 25009 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread
* Re: [PATCH 0/2] rbtree: Test against a verified oracle
  2021-10-19  9:13 [PATCH 0/2] rbtree: Test against a verified oracle Mete Polat
  2021-10-19  9:13 ` [PATCH 1/2] rbtree: Expose a test tree to userspace Mete Polat
  2021-10-19  9:13 ` [PATCH 2/2] rbtree: add verified oracle with testing harness Mete Polat
@ 2021-10-22  9:32 ` Michel Lespinasse
  2021-10-28 14:44   ` Mete Polat
  2 siblings, 1 reply; 9+ messages in thread
From: Michel Lespinasse @ 2021-10-22  9:32 UTC (permalink / raw)
  To: Mete Polat
  Cc: Lukas Bulwahn, Shuah Khan, Michel Lespinasse, Andrii Nakryiko,
	Alexei Starovoitov, David S. Miller, Paolo Bonzini,
	Daniel Borkmann, Paul E. McKenney, linux-kernel

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
> 

^ permalink raw reply	[flat|nested] 9+ messages in thread
* Re: [PATCH 0/2] rbtree: Test against a verified oracle
  2021-10-22  9:32 ` [PATCH 0/2] rbtree: Test against a verified oracle Michel Lespinasse
@ 2021-10-28 14:44   ` Mete Polat
  0 siblings, 0 replies; 9+ messages in thread
From: Mete Polat @ 2021-10-28 14:44 UTC (permalink / raw)
  To: Michel Lespinasse
  Cc: Lukas Bulwahn, Shuah Khan, Andrii Nakryiko, Alexei Starovoitov,
	David S. Miller, Paolo Bonzini, Daniel Borkmann,
	Paul E. McKenney, linux-kernel

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

^ permalink raw reply	[flat|nested] 9+ messages in thread
end of thread, other threads:[~2021-10-28 14:44 UTC | newest]

Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-10-19  9:13 [PATCH 0/2] rbtree: Test against a verified oracle Mete Polat
2021-10-19  9:13 ` [PATCH 1/2] rbtree: Expose a test tree to userspace Mete Polat
2021-10-20  6:46   ` kernel test robot
2021-10-20  6:46     ` kernel test robot
2021-10-22  5:45   ` kernel test robot
2021-10-22  5:45     ` kernel test robot
2021-10-19  9:13 ` [PATCH 2/2] rbtree: add verified oracle with testing harness Mete Polat
2021-10-22  9:32 ` [PATCH 0/2] rbtree: Test against a verified oracle Michel Lespinasse
2021-10-28 14:44   ` Mete Polat

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.