verification/rv: Add rv tool
Subsystems (2)
v2 cover verification/rv: Add rv tool
This is the (user-space) runtime verification tool named rv.
This tool aims to be the interface for in-kernel rv monitors, as well as the home for user-space controlled monitors.
The tool receives a command as the first argument, the current commands are:
list - list all available monitors
mon - run a given monitor
Each monitor is an independent piece of software inside the tool and can have their own arguments.
Changes from v1:
- typos and format
- fixed __ikm_read_enable() value check in ikm_read_enable()
- adjust patch 2 log
- improved function comments (mainly those /**).
Daniel Bristot de Oliveira (3):
rv: Add rv tool
tools/rv: Add in-kernel monitor interface
Documentation/rv: Add verification/rv man pages
Documentation/tools/index.rst | 1 + Documentation/tools/rv/Makefile | 52 ++ Documentation/tools/rv/common_appendix.rst | 16 + Documentation/tools/rv/common_ikm.rst | 21 + Documentation/tools/rv/index.rst | 24 + Documentation/tools/rv/rv-list.rst | 43 ++ Documentation/tools/rv/rv-mon-wip.rst | 44 ++ Documentation/tools/rv/rv-mon-wwnr.rst | 43 ++ Documentation/tools/rv/rv-mon.rst | 55 ++ Documentation/tools/rv/rv.rst | 63 ++ tools/verification/rv/Makefile | 141 +++++ tools/verification/rv/README.txt | 38 ++ tools/verification/rv/include/in_kernel.h | 3 + tools/verification/rv/include/rv.h | 12 + tools/verification/rv/include/trace.h | 16 + tools/verification/rv/include/utils.h | 8 + tools/verification/rv/src/in_kernel.c | 698 +++++++++++++++++++++ tools/verification/rv/src/rv.c | 188 ++++++ tools/verification/rv/src/trace.c | 133 ++++ tools/verification/rv/src/utils.c | 47 ++ 20 files changed, 1646 insertions(+) create mode 100644 Documentation/tools/rv/Makefile create mode 100644 Documentation/tools/rv/common_appendix.rst create mode 100644 Documentation/tools/rv/common_ikm.rst create mode 100644 Documentation/tools/rv/index.rst create mode 100644 Documentation/tools/rv/rv-list.rst create mode 100644 Documentation/tools/rv/rv-mon-wip.rst create mode 100644 Documentation/tools/rv/rv-mon-wwnr.rst create mode 100644 Documentation/tools/rv/rv-mon.rst create mode 100644 Documentation/tools/rv/rv.rst create mode 100644 tools/verification/rv/Makefile create mode 100644 tools/verification/rv/README.txt create mode 100644 tools/verification/rv/include/in_kernel.h create mode 100644 tools/verification/rv/include/rv.h create mode 100644 tools/verification/rv/include/trace.h create mode 100644 tools/verification/rv/include/utils.h create mode 100644 tools/verification/rv/src/in_kernel.c create mode 100644 tools/verification/rv/src/rv.c create mode 100644 tools/verification/rv/src/trace.c create mode 100644 tools/verification/rv/src/utils.c
Signature · 1 line
2.37.3
PATCH v2 1/3 Add rv tool
This is the (user-space) runtime verification tool, named rv.
This tool aims to be the interface for in-kernel rv monitors, as well as the home for monitors in user-space (online asynchronous), and in *eBPF.
The tool receives a command as the first argument, the current commands are:
list - list all available monitors
mon - run a given monitor
Each monitor is an independent piece of software inside the tool and can have their own arguments.
There is no monitor implemented in this patch, it only adds the basic structure of the tool, based on rtla.
# rv --help
rv version 6.1.0-rc4: help usage: rv command [-h] [command_options]
-h/--help: print this menu
command: run one of the following command:
list: list all available monitors
mon: run a monitor
[command options]: each command has its own set of options
run rv command -h for further information
*dot2bpf is the next patch set, depends on this, doing cleanups.
Cc Jonathan Corbet <[email protected]>
Cc Steven Rostedt <[email protected]>
Signed-off-by Daniel Bristot de Oliveira <[email protected]>
--- tools/verification/rv/Makefile | 119 +++++++++++++++++ tools/verification/rv/README.txt | 38 ++++++ tools/verification/rv/include/rv.h | 12 ++ tools/verification/rv/include/trace.h | 16 +++ tools/verification/rv/include/utils.h | 8 ++ tools/verification/rv/src/rv.c | 185 ++++++++++++++++++++++++++ tools/verification/rv/src/trace.c | 133 ++++++++++++++++++ tools/verification/rv/src/utils.c | 47 +++++++ 8 files changed, 558 insertions(+) create mode 100644 tools/verification/rv/Makefile create mode 100644 tools/verification/rv/README.txt create mode 100644 tools/verification/rv/include/rv.h create mode 100644 tools/verification/rv/include/trace.h create mode 100644 tools/verification/rv/include/utils.h create mode 100644 tools/verification/rv/src/rv.c create mode 100644 tools/verification/rv/src/trace.c create mode 100644 tools/verification/rv/src/utils.c
tools/verification/rv/Makefile new file +119 -0
@@ -0,0 +1,119 @@ +NAME := rv +# Follow the kernel version +VERSION := $(shell cat VERSION 2> /dev/null || make -sC ../../.. kernelversion | grep -v make) + +# From libtracefs: +# Makefiles suck: This macro sets a default value of $(2) for the +# variable named by $(1), unless the variable has been set by +# environment or command line. This is necessary for CC and AR +# because make sets default values, so the simpler ?= approach +# won't work as expected. +define allow-override + $(if $(or $(findstring environment,$(origin $(1))),\ + $(findstring command line,$(origin $(1)))),,\ + $(eval $(1) = $(2))) +endef + +# Allow setting CC and AR, or setting CROSS_COMPILE as a prefix. +$(call allow-override,CC,$(CROSS_COMPILE)gcc) +$(call allow-override,AR,$(CROSS_COMPILE)ar) +$(call allow-override,STRIP,$(CROSS_COMPILE)strip) +$(call allow-override,PKG_CONFIG,pkg-config) +$(call allow-override,LD_SO_CONF_PATH,/etc/ld.so.conf.d/) +$(call allow-override,LDCONFIG,ldconfig) + +INSTALL = install +MKDIR = mkdir +FOPTS := -flto=auto -ffat-lto-objects -fexceptions -fstack-protector-strong \ + -fasynchronous-unwind-tables -fstack-clash-protection +WOPTS := -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -Wno-maybe-uninitialized + +TRACEFS_HEADERS := $$($(PKG_CONFIG) --cflags libtracefs) + +CFLAGS := -O -g -DVERSION=\"$(VERSION)\" $(FOPTS) $(MOPTS) $(WOPTS) $(TRACEFS_HEADERS) $(EXTRA_CFLAGS) -I include +LDFLAGS := -ggdb $(EXTRA_LDFLAGS) +LIBS := $$($(PKG_CONFIG) --libs libtracefs) + +SRC := $(wildcard src/*.c) +HDR := $(wildcard src/*.h) +OBJ := $(SRC:.c=.o) +DIRS := src +FILES := Makefile README.txt +CEXT := bz2 +TARBALL := $(NAME)-$(VERSION).tar.$(CEXT) +TAROPTS := -cvjf $(TARBALL) +BINDIR := /usr/bin +DATADIR := /usr/share +MANDIR := $(DATADIR)/man +LICDIR := $(DATADIR)/licenses +SRCTREE := $(or $(BUILD_SRC),$(CURDIR)) + +LIBTRACEEVENT_MIN_VERSION = 1.5 +LIBTRACEFS_MIN_VERSION = 1.3 + +.PHONY: all warnings show_warnings +all: warnings rv + +TEST_LIBTRACEEVENT = $(shell sh -c "$(PKG_CONFIG) --atleast-version $(LIBTRACEEVENT_MIN_VERSION) libtraceevent > /dev/null 2>&1 || echo n") +ifeq ("$(TEST_LIBTRACEEVENT)", "n") +WARNINGS = show_warnings +MISSING_LIBS += echo "** libtraceevent version $(LIBTRACEEVENT_MIN_VERSION) or higher"; +MISSING_PACKAGES += "libtraceevent-devel" +MISSING_SOURCE += echo "** https://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git/ "; +endif + +TEST_LIBTRACEFS = $(shell sh -c "$(PKG_CONFIG) --atleast-version $(LIBTRACEFS_MIN_VERSION) libtracefs > /dev/null 2>&1 || echo n") +ifeq ("$(TEST_LIBTRACEFS)", "n") +WARNINGS = show_warnings +MISSING_LIBS += echo "** libtracefs version $(LIBTRACEFS_MIN_VERSION) or higher"; +MISSING_PACKAGES += "libtracefs-devel" +MISSING_SOURCE += echo "** https://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git/ "; +endif + +define show_dependencies + @echo "********************************************"; \ + echo "** NOTICE: Failed build dependencies"; \ + echo "**"; \ + echo "** Required Libraries:"; \ + $(MISSING_LIBS) \ + echo "**"; \ + echo "** Consider installing the latest libtracefs from your"; \ + echo "** distribution, e.g., 'dnf install $(MISSING_PACKAGES)' on Fedora,"; \ + echo "** or from source:"; \ + echo "**"; \ + $(MISSING_SOURCE) \ + echo "**"; \ + echo "********************************************" +endef + +show_warnings: + $(call show_dependencies); + +ifneq ("$(WARNINGS)", "") +ERROR_OUT = $(error Please add the necessary dependencies) + +warnings: $(WARNINGS) + $(ERROR_OUT) +endif + +rv: $(OBJ) + $(CC) -o rv $(LDFLAGS) $(OBJ) $(LIBS) + +.PHONY: install +install: + $(MKDIR) -p $(DESTDIR)$(BINDIR) + $(INSTALL) rv -m 755 $(DESTDIR)$(BINDIR) + $(STRIP) $(DESTDIR)$(BINDIR)/rv + +.PHONY: clean tarball +clean: + @test ! -f rv || rm rv + @test ! -f $(TARBALL) || rm -f $(TARBALL) + @rm -rf *~ $(OBJ) *.tar.$(CEXT) + +tarball: clean + rm -rf $(NAME)-$(VERSION) && mkdir $(NAME)-$(VERSION) + echo $(VERSION) > $(NAME)-$(VERSION)/VERSION + cp -r $(DIRS) $(FILES) $(NAME)-$(VERSION) + tar $(TAROPTS) --exclude='*~' $(NAME)-$(VERSION) + rm -rf $(NAME)-$(VERSION)
tools/verification/rv/README.txt new file +38 -0
@@ -0,0 +1,38 @@ +RV: Runtime Verification + +Runtime Verification (RV) is a lightweight (yet rigorous) method that +complements classical exhaustive verification techniques (such as model +checking and theorem proving) with a more practical approach for +complex systems. + +The rv tool is the interface for a collection of monitors that aim +analysing the logical and timing behavior of Linux. + +Installing RV + +RV depends on the following libraries and tools: + + - libtracefs + - libtraceevent + +It also depends on python3-docutils to compile man pages. + +For development, we suggest the following steps for compiling rtla: + + $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git + $ cd libtraceevent/ + $ make + $ sudo make install + $ cd .. + $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git + $ cd libtracefs/ + $ make + $ sudo make install + $ cd .. + $ cd $rv_src + $ make + $ sudo make install + +For further information, please see rv manpage and the kernel documentation: + Runtime Verification: + Documentation/trace/rv/runtime-verification.rst
tools/verification/rv/include/rv.h new file +12 -0
@@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-2.0 + +#define MAX_DESCRIPTION 1024 +#define MAX_DA_NAME_LEN 24 + +struct monitor { +char name[MAX_DA_NAME_LEN ]; +char desc[MAX_DESCRIPTION ]; +int enabled; +}; + +int should_stop (void );
tools/verification/rv/include/trace.h new file +16 -0
@@ -0,0 +1,16 @@ +// SPDX-License-Identifier: GPL-2.0 + +#include <tracefs.h> + +struct trace_instance { +struct tracefs_instance *inst; +struct tep_handle *tep; +struct trace_seq *seq; +}; + +int trace_instance_init (struct trace_instance *trace,char *name); +int trace_instance_start (struct trace_instance *trace); +void trace_instance_destroy (struct trace_instance *trace); + +int collect_registered_events (struct tep_event *event,struct tep_record *record, +int cpu,void *context);
tools/verification/rv/include/utils.h new file +8 -0
@@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-2.0 + +#define MAX_PATH 1024 + +void debug_msg (const char *fmt, ...); +void err_msg (const char *fmt, ...); + +extern int config_debug;
tools/verification/rv/src/rv.c new file +185 -0
185 lines not on this page · raw message
tools/verification/rv/src/trace.c new file +133 -0
133 lines not on this page · raw message
tools/verification/rv/src/utils.c new file +47 -0
47 lines not on this page · raw message
Signature · 1 line
2.37.3
PATCH v2 2/3 tools/rv: Add in-kernel monitor interface
In reply to Daniel Bristot de OliveiraAdd the ability to control and trace in-kernel monitors. This is a generic interface, it will check for existing monitors and enable standard setup, like enabling reactors.
For example:
# rv list wip wakeup in preemptive per-cpu testing monitor. [OFF] wwnr wakeup while not running per-task testing model. [OFF]
# rv mon wwnr --help rv version 6.1.0-rc4: help
usage: rv mon wwnr [-h] [-q] [-r reactor] [-s] [-v]
-h/--help: print this menu and the reactor list -r/--reactor 'reactor': enables the 'reactor' -s/--self: when tracing (-t), also trace rv command -t/--trace: trace monitor's event -v/--verbose: print debug messages
available reactors: nop printk panic
# rv mon wwnr --trace
<TASK>-PID [CPU] TYPE ID STATE x EVENT -> NEXT_STATE FINAL
| | | | | | | | |
rv-3613 [001] event 3613 running x switch_out -> not_running Y
sshd-1248 [005] event 1248 running x switch_out -> not_running Y
<idle>-0 [005] event 71 not_running x wakeup -> not_running Y
<idle>-0 [005] event 71 not_running x switch_in -> running N
kcompactd0-71 [005] event 71 running x switch_out -> not_running Y
<idle>-0 [000] event 860 not_running x wakeup -> not_running Y
<idle>-0 [000] event 860 not_running x switch_in -> running N
systemd-oomd-860 [000] event 860 running x switch_out -> not_running Y
<idle>-0 [000] event 860 not_running x wakeup -> not_running Y
<idle>-0 [000] event 860 not_running x switch_in -> running N
systemd-oomd-860 [000] event 860 running x switch_out -> not_running Y
<idle>-0 [005] event 71 not_running x wakeup -> not_running Y
<idle>-0 [005] event 71 not_running x switch_in -> running N
kcompactd0-71 [005] event 71 running x switch_out -> not_running Y
<idle>-0 [000] event 860 not_running x wakeup -> not_running Y
<idle>-0 [000] event 860 not_running x switch_in -> running N
systemd-oomd-860 [000] event 860 running x switch_out -> not_running Y
<idle>-0 [001] event 3613 not_running x wakeup -> not_running YCc Jonathan Corbet <[email protected]>
Cc Steven Rostedt <[email protected]>
Signed-off-by Daniel Bristot de Oliveira <[email protected]>
--- tools/verification/rv/include/in_kernel.h | 3 + tools/verification/rv/src/in_kernel.c | 698 ++++++++++++++++++++++ tools/verification/rv/src/rv.c | 3 + 3 files changed, 704 insertions(+) create mode 100644 tools/verification/rv/include/in_kernel.h create mode 100644 tools/verification/rv/src/in_kernel.c
tools/verification/rv/include/in_kernel.h new file +3 -0
@@ -0,0 +1,3 @@ +// SPDX-License-Identifier: GPL-2.0 +int ikm_list_monitors (void ); +int ikm_run_monitor (char *monitor,int argc,char **argv);
tools/verification/rv/src/in_kernel.c new file +698 -0
698 lines not on this page · raw message
tools/verification/rv/src/rv.c +3 -0
@@ -12,6 +12,7 @@#include <trace.h> #include <utils.h> +#include <in_kernel.h> static int stop_session;
@@ -63,6 +64,7 @@ static void rv_list(int argc, char **argv)exit (1 ); } +ikm_list_monitors ();exit (0 ); }
@@ -109,6 +111,7 @@ static void rv_mon(int argc, char **argv)* Call all possible monitor implementations, looking * for the [monitor]. */ + run +=ikm_run_monitor (monitor_name, argc-1 , &argv[1 ]);if (!run)err_msg ("rv: monitor %s does not exist\n" , monitor_name);
Signature · 1 line
2.37.3
PATCH v2 3/3 Documentation/rv: Add verification/rv man pages
In reply to Daniel Bristot de OliveiraAdd man pages for the rv command line, using the same scheme we used in rtla.
Cc Jonathan Corbet <[email protected]>
Cc Steven Rostedt <[email protected]>
Signed-off-by Daniel Bristot de Oliveira <[email protected]>
--- Documentation/tools/index.rst | 1 + Documentation/tools/rv/Makefile | 52 ++++++++++++++++++ Documentation/tools/rv/common_appendix.rst | 16 ++++++ Documentation/tools/rv/common_ikm.rst | 21 ++++++++ Documentation/tools/rv/index.rst | 24 +++++++++ Documentation/tools/rv/rv-list.rst | 43 +++++++++++++++ Documentation/tools/rv/rv-mon-wip.rst | 44 +++++++++++++++ Documentation/tools/rv/rv-mon-wwnr.rst | 43 +++++++++++++++ Documentation/tools/rv/rv-mon.rst | 55 +++++++++++++++++++ Documentation/tools/rv/rv.rst | 63 ++++++++++++++++++++++ tools/verification/rv/Makefile | 26 ++++++++- 11 files changed, 386 insertions(+), 2 deletions(-) create mode 100644 Documentation/tools/rv/Makefile create mode 100644 Documentation/tools/rv/common_appendix.rst create mode 100644 Documentation/tools/rv/common_ikm.rst create mode 100644 Documentation/tools/rv/index.rst create mode 100644 Documentation/tools/rv/rv-list.rst create mode 100644 Documentation/tools/rv/rv-mon-wip.rst create mode 100644 Documentation/tools/rv/rv-mon-wwnr.rst create mode 100644 Documentation/tools/rv/rv-mon.rst create mode 100644 Documentation/tools/rv/rv.rst
Documentation/tools/index.rst +1 -0
@@ -11,6 +11,7 @@ more additions are needed here: :maxdepth: 1 rtla/index + rv/index .. only:: subproject and html
Documentation/tools/rv/Makefile new file +52 -0
52 lines not on this page · raw message
Documentation/tools/rv/common_appendix.rst new file +16 -0
@@ -0,0 +1,16 @@ +REPORTING BUGS +============== + +Report bugs to <[email protected]> +and <[email protected]> + +LICENSE +======= + +**rv** is Free Software licensed under the GNU GPLv2 + +COPYING +======= + +Copyright \(C) 2022 Red Hat, Inc. Free use of this software is granted under +the terms of the GNU Public License (GPL).
Documentation/tools/rv/common_ikm.rst new file +21 -0
@@ -0,0 +1,21 @@ +**-h**, **--help** + + Print the monitor's options and the available reactors list. + +**-r**, **--reactor** *reactor* + + Enables the *reactor*. See **-h** for a list of available reactors. + +**-s**, **--self** + + When tracing (**-t**), also print the events that happened during the **rv** + command itself. If the **rv** command itself generates too many events, + the tool might get busy processing its own events only. + +**-t**, **--trace** + + Trace monitor's events and error. + +**-v**, **--verbose** + + Print debug messages.
Documentation/tools/rv/index.rst new file +24 -0
@@ -0,0 +1,24 @@ +.. SPDX-License-Identifier: GPL-2.0 + +============================== +Runtime verification (rv) tool +============================== + +**rv** tool provides the interface for a collection of runtime verification +(rv) monitors. + +.. toctree:: + :maxdepth: 1 + + rv + rv-list + rv-mon + rv-mon-wip + rv-mon-wwnr + +.. only:: subproject and html + + Indices + ======= + + * :ref:`genindex`
Documentation/tools/rv/rv-list.rst new file +43 -0
43 lines not on this page · raw message
Documentation/tools/rv/rv-mon-wip.rst new file +44 -0
44 lines not on this page · raw message
Documentation/tools/rv/rv-mon-wwnr.rst new file +43 -0
43 lines not on this page · raw message
Documentation/tools/rv/rv-mon.rst new file +55 -0
55 lines not on this page · raw message
Documentation/tools/rv/rv.rst new file +63 -0
63 lines not on this page · raw message
tools/verification/rv/Makefile +24 -2
@@ -44,10 +44,20 @@ TARBALL := $(NAME)-$(VERSION).tar.$(CEXT) TAROPTS := -cvjf $(TARBALL) BINDIR := /usr/bin DATADIR := /usr/share +DOCDIR := $(DATADIR)/doc MANDIR := $(DATADIR)/man LICDIR := $(DATADIR)/licenses SRCTREE := $(or $(BUILD_SRC),$(CURDIR)) +# If running from the tarball, man pages are stored in the Documentation +# dir. If running from the kernel source, man pages are stored in +# Documentation/tools/rv/. +ifneq ($(wildcard Documentation/.*),) +DOCSRC = Documentation/ +else +DOCSRC = $(SRCTREE)/../../../Documentation/tools/rv/ +endif + LIBTRACEEVENT_MIN_VERSION = 1.5 LIBTRACEFS_MIN_VERSION = 1.3
@@ -100,13 +110,13 @@ rv: $(OBJ) $(CC) -o rv $(LDFLAGS) $(OBJ) $(LIBS) .PHONY: install -install: +install: doc_install $(MKDIR) -p $(DESTDIR)$(BINDIR) $(INSTALL) rv -m 755 $(DESTDIR)$(BINDIR) $(STRIP) $(DESTDIR)$(BINDIR)/rv .PHONY: clean tarball -clean: +clean: doc_clean @test ! -f rv || rm rv @test ! -f $(TARBALL) || rm -f $(TARBALL) @rm -rf *~ $(OBJ) *.tar.$(CEXT)
@@ -115,5 +125,17 @@ tarball: clean rm -rf $(NAME)-$(VERSION) && mkdir $(NAME)-$(VERSION) echo $(VERSION) > $(NAME)-$(VERSION)/VERSION cp -r $(DIRS) $(FILES) $(NAME)-$(VERSION) + mkdir $(NAME)-$(VERSION)/Documentation/ + cp -rp $(SRCTREE)/../../../Documentation/tools/rv/* $(NAME)-$(VERSION)/Documentation/ tar $(TAROPTS) --exclude='*~' $(NAME)-$(VERSION) rm -rf $(NAME)-$(VERSION) + +.PHONY: doc doc_clean doc_install +doc: + $(MAKE) -C $(DOCSRC) + +doc_clean: + $(MAKE) -C $(DOCSRC) clean + +doc_install: + $(MAKE) -C $(DOCSRC) install
Signature · 1 line
2.37.3