verification/rv: Add rv tool

new file mode 100644
index 000000000000..1de111ac2641
@@ -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)

new file mode 100644
index 000000000000..e96be0dfff59
@@ -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

index 0bb1e61bdcc0..80488e290e10 100644
@@ -11,6 +11,7 @@ more additions are needed here:
    :maxdepth: 1
 
    rtla/index
+   rv/index
 
 .. only::  subproject and html
 

52 lines not on this page · raw message

new file mode 100644
index 000000000000..f8ffd271d886
@@ -0,0 +1,13 @@
+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).

new file mode 100644
index 000000000000..0f206e985c27
@@ -0,0 +1,21 @@
+**-h**, **--help**
+
+        Print this menu and the reactor list.
+
+**-r**, **--reactor** *reactor*
+
+        Enables the *reactor*.
+
+**-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.
+
+**-t**, **--trace**
+
+        Trace monitor's events and error.
+
+**-v**, **--verbose**
+
+        Print debug messages.

new file mode 100644
index 000000000000..50f40a3ee256
@@ -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`

new file mode 100644
index 000000000000..727bd3fbcce9
@@ -0,0 +1,39 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+=======
+rv-list
+=======
+-----------------------
+List available monitors
+-----------------------
+
+:Manual section: 1
+
+SYNOPSIS
+========
+**rv list** [*OPTIONS*]
+
+DESCRIPTION
+===========
+
+The **rv list** command prints all available monitors. These
+monitors can be enabled using the **rv mon** command.
+
+OPTIONS
+=======
+
+**-h**, **--help**
+
+        Print help menu.
+
+SEE ALSO
+========
+**rv**\(1), **rv-mon**\(1)
+
+Linux kernel *RV* documentation: <https://www.kernel.org/doc/html/latest/trace/rv/index.html>
+
+AUTHOR
+======
+Written by Daniel Bristot de Oliveira <[email protected]>
+
+.. include:: common_appendix.rst

new file mode 100644
index 000000000000..27a026f80cb7
@@ -0,0 +1,40 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+==========
+rv-mon-wip
+==========
+----------------------------
+Wakeup In Preemptive monitor
+----------------------------
+
+:Manual section: 1
+
+SYNOPSIS
+========
+**rv mon wip** [*OPTIONS*]
+
+DESCRIPTION
+===========
+
+The wakeup in preemptive (**wip**) monitor is a sample per-cpu monitor that
+verifies if the wakeup events always take place with preemption disabled.
+
+See kernel documentation for further information about this monitor:
+<https://docs.kernel.org/trace/rv/monitor_wip.html>
+
+OPTIONS
+=======
+
+.. include:: common_ikm.rst
+
+SEE ALSO
+========
+**rv**\(1), **rv-mon**\(1)
+
+Linux kernel *RV* documentation: <https://www.kernel.org/doc/html/latest/trace/rv/index.html>
+
+AUTHOR
+======
+Written by Daniel Bristot de Oliveira <[email protected]>
+
+.. include:: common_appendix.rst

new file mode 100644
index 000000000000..18807528c04c
@@ -0,0 +1,39 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+===========
+rv-mon-wwnr
+===========
+--------------------------------
+Wakeup While Not Running monitor
+--------------------------------
+
+:Manual section: 1
+
+SYNOPSIS
+========
+**rv mon wip** [*OPTIONS*]
+
+DESCRIPTION
+===========
+
+The wakeup while not running (**wwnr**) is a per-task sample monitor.
+
+See kernel documentation for further information about this monitor:
+<https://docs.kernel.org/trace/rv/monitor_wwnr.html>
+
+OPTIONS
+=======
+
+.. include:: common_ikm.rst
+
+SEE ALSO
+========
+**rv**\(1), **rv-mon**\(1)
+
+Linux kernel *RV* documentation: <https://www.kernel.org/doc/html/latest/trace/rv/index.html>
+
+AUTHOR
+======
+Written by Daniel Bristot de Oliveira <[email protected]>
+
+.. include:: common_appendix.rst

51 lines not on this page · raw message

57 lines not on this page · raw message

index 1de111ac2641..3d0f3888a58c 100644
@@ -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