summaryrefslogtreecommitdiff
path: root/Documentation/tools
diff options
context:
space:
mode:
authorDaniel Bristot de Oliveira <bristot@kernel.org>2022-11-11 18:53:07 +0300
committerSteven Rostedt (Google) <rostedt@goodmis.org>2022-12-10 02:06:24 +0300
commitafc70ccb962861e068e04c6089827493f5160a0a (patch)
tree22e7f85e80cd0a399beb0826303da395251edb4a /Documentation/tools
parent6d60f89691fc979e55b88508f4cfa8f6b4c56eac (diff)
downloadlinux-afc70ccb962861e068e04c6089827493f5160a0a.tar.xz
Documentation/rv: Add verification/rv man pages
Add man pages for the rv command line, using the same scheme we used in rtla. Link: https://lkml.kernel.org/r/e841d7cfbdfc3ebdaf7cbd40278571940145d829.1668180100.git.bristot@kernel.org Cc: Jonathan Corbet <corbet@lwn.net> Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
Diffstat (limited to 'Documentation/tools')
-rw-r--r--Documentation/tools/index.rst1
-rw-r--r--Documentation/tools/rv/Makefile52
-rw-r--r--Documentation/tools/rv/common_appendix.rst16
-rw-r--r--Documentation/tools/rv/common_ikm.rst21
-rw-r--r--Documentation/tools/rv/index.rst24
-rw-r--r--Documentation/tools/rv/rv-list.rst43
-rw-r--r--Documentation/tools/rv/rv-mon-wip.rst44
-rw-r--r--Documentation/tools/rv/rv-mon-wwnr.rst43
-rw-r--r--Documentation/tools/rv/rv-mon.rst55
-rw-r--r--Documentation/tools/rv/rv.rst63
10 files changed, 362 insertions, 0 deletions
diff --git a/Documentation/tools/index.rst b/Documentation/tools/index.rst
index 0bb1e61bdcc0..80488e290e10 100644
--- a/Documentation/tools/index.rst
+++ b/Documentation/tools/index.rst
@@ -11,6 +11,7 @@ more additions are needed here:
:maxdepth: 1
rtla/index
+ rv/index
.. only:: subproject and html
diff --git a/Documentation/tools/rv/Makefile b/Documentation/tools/rv/Makefile
new file mode 100644
index 000000000000..ec8713c1b35f
--- /dev/null
+++ b/Documentation/tools/rv/Makefile
@@ -0,0 +1,52 @@
+# SPDX-License-Identifier: GPL-2.0-only
+
+INSTALL ?= install
+RM ?= rm -f
+RMDIR ?= rmdir --ignore-fail-on-non-empty
+
+PREFIX ?= /usr/share
+MANDIR ?= $(PREFIX)/man
+MAN1DIR = $(MANDIR)/man1
+
+MAN1_RST = $(wildcard rv*.rst)
+
+_DOC_MAN1 = $(patsubst %.rst,%.1,$(MAN1_RST))
+DOC_MAN1 = $(addprefix $(OUTPUT),$(_DOC_MAN1))
+
+RST2MAN_DEP := $(shell command -v rst2man 2>/dev/null)
+RST2MAN_OPTS += --verbose
+
+TEST_RST2MAN = $(shell sh -c "rst2man --version > /dev/null 2>&1 || echo n")
+
+$(OUTPUT)%.1: %.rst
+ifndef RST2MAN_DEP
+ $(info ********************************************)
+ $(info ** NOTICE: rst2man not found)
+ $(info **)
+ $(info ** Consider installing the latest rst2man from your)
+ $(info ** distribution, e.g., 'dnf install python3-docutils' on Fedora,)
+ $(info ** or from source:)
+ $(info **)
+ $(info ** https://docutils.sourceforge.io/docs/dev/repository.html )
+ $(info **)
+ $(info ********************************************)
+ $(error NOTICE: rst2man required to generate man pages)
+endif
+ rst2man $(RST2MAN_OPTS) $< > $@
+
+man1: $(DOC_MAN1)
+man: man1
+
+clean:
+ $(RM) $(DOC_MAN1)
+
+install: man
+ $(INSTALL) -d -m 755 $(DESTDIR)$(MAN1DIR)
+ $(INSTALL) -m 644 $(DOC_MAN1) $(DESTDIR)$(MAN1DIR)
+
+uninstall:
+ $(RM) $(addprefix $(DESTDIR)$(MAN1DIR)/,$(_DOC_MAN1))
+ $(RMDIR) $(DESTDIR)$(MAN1DIR)
+
+.PHONY: man man1 clean install uninstall
+.DEFAULT_GOAL := man
diff --git a/Documentation/tools/rv/common_appendix.rst b/Documentation/tools/rv/common_appendix.rst
new file mode 100644
index 000000000000..f4239192bee8
--- /dev/null
+++ b/Documentation/tools/rv/common_appendix.rst
@@ -0,0 +1,16 @@
+REPORTING BUGS
+==============
+
+Report bugs to <linux-kernel@vger.kernel.org>
+and <linux-trace-devel@vger.kernel.org>
+
+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).
diff --git a/Documentation/tools/rv/common_ikm.rst b/Documentation/tools/rv/common_ikm.rst
new file mode 100644
index 000000000000..e50a5f8a7142
--- /dev/null
+++ b/Documentation/tools/rv/common_ikm.rst
@@ -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.
diff --git a/Documentation/tools/rv/index.rst b/Documentation/tools/rv/index.rst
new file mode 100644
index 000000000000..8fd16d91d639
--- /dev/null
+++ b/Documentation/tools/rv/index.rst
@@ -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`
diff --git a/Documentation/tools/rv/rv-list.rst b/Documentation/tools/rv/rv-list.rst
new file mode 100644
index 000000000000..51e4608f9e99
--- /dev/null
+++ b/Documentation/tools/rv/rv-list.rst
@@ -0,0 +1,43 @@
+.. 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 <bristot@kernel.org>
+
+.. include:: common_appendix.rst
diff --git a/Documentation/tools/rv/rv-mon-wip.rst b/Documentation/tools/rv/rv-mon-wip.rst
new file mode 100644
index 000000000000..2d42104d63d1
--- /dev/null
+++ b/Documentation/tools/rv/rv-mon-wip.rst
@@ -0,0 +1,44 @@
+.. 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
+checks 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 <bristot@kernel.org>
+
+.. include:: common_appendix.rst
diff --git a/Documentation/tools/rv/rv-mon-wwnr.rst b/Documentation/tools/rv/rv-mon-wwnr.rst
new file mode 100644
index 000000000000..a18f3fd54af4
--- /dev/null
+++ b/Documentation/tools/rv/rv-mon-wwnr.rst
@@ -0,0 +1,43 @@
+.. 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 <bristot@kernel.org>
+
+.. include:: common_appendix.rst
diff --git a/Documentation/tools/rv/rv-mon.rst b/Documentation/tools/rv/rv-mon.rst
new file mode 100644
index 000000000000..af0f329a7c9c
--- /dev/null
+++ b/Documentation/tools/rv/rv-mon.rst
@@ -0,0 +1,55 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+=======
+rv-list
+=======
+-----------------------
+List available monitors
+-----------------------
+
+:Manual section: 1
+
+SYNOPSIS
+========
+
+**rv mon** [*-h*] **monitor_name** [*-h*] [*MONITOR OPTIONS*]
+
+DESCRIPTION
+===========
+
+The **rv mon** command runs the monitor named *monitor_name*. Each monitor
+has its own set of options. The **rv list** command shows all available
+monitors.
+
+OPTIONS
+=======
+
+**-h**, **--help**
+
+ Print help menu.
+
+AVAILABLE MONITORS
+==================
+
+The **rv** tool provides the interface for a set of monitors. Use the
+**rv list** command to list all available monitors.
+
+Each monitor has its own set of options. See man **rv-mon**-*monitor_name*
+for details about each specific monitor. Also, running **rv mon**
+**monitor_name** **-h** display the help menu with the available
+options.
+
+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 <bristot@kernel.org>
+
+.. include:: common_appendix.rst
diff --git a/Documentation/tools/rv/rv.rst b/Documentation/tools/rv/rv.rst
new file mode 100644
index 000000000000..cee93dc21a76
--- /dev/null
+++ b/Documentation/tools/rv/rv.rst
@@ -0,0 +1,63 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+==
+rv
+==
+--------------------
+Runtime Verification
+--------------------
+
+:Manual section: 1
+
+SYNOPSIS
+========
+
+**rv** *COMMAND* [*OPTIONS*]
+
+DESCRIPTION
+===========
+
+Runtime Verification (**RV**) is a lightweight (yet rigorous) method
+for formal verification with a practical approach for complex systems.
+Instead of relying on a fine-grained model of a system (e.g., a
+re-implementation a instruction level), RV works by analyzing the trace
+of the system's actual execution, comparing it against a formal
+specification of the system behavior.
+
+The **rv** tool provides the interface for a collection of runtime
+verification (rv) monitors.
+
+COMMANDS
+========
+
+**list**
+
+ List all available monitors.
+
+**mon**
+
+ Run monitor.
+
+OPTIONS
+=======
+
+**-h**, **--help**
+
+ Display the help text.
+
+For other options, see the man page for the corresponding command.
+
+SEE ALSO
+========
+
+**rv-list**\(1), **rv-mon**\(1)
+
+Linux kernel *RV* documentation:
+<https://www.kernel.org/doc/html/latest/trace/rv/index.html>
+
+AUTHOR
+======
+
+Daniel Bristot de Oliveira <bristot@kernel.org>
+
+.. include:: common_appendix.rst