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
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 <[email protected]>");
--
2.33.1
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
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 <[email protected]>
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/[email protected]
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 <[email protected]>
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/[email protected]
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
>
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
> >