From: Daniel Bristot de Oliveira <bristot@kernel.org>
To: Steven Rostedt <rostedt@goodmis.org>, linux-trace-devel@vger.kernel.org
Cc: Daniel Bristot de Oliveira <bristot@kernel.org>,
Jonathan Corbet <corbet@lwn.net>,
linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org
Subject: [PATCH 3/3] Documentation/rv: Add verification/rv man pages
Date: Wed, 26 Oct 2022 12:44:41 +0200 [thread overview]
Message-ID: <320de46ad632099cdbaa24dc6fc690781017ff6f.1666776642.git.bristot@kernel.org> (raw)
In-Reply-To: <cover.1666776642.git.bristot@kernel.org>
Add man pages for the rv command line, using the same scheme we used
in rtla.
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Steven Rostedt <rostedt@goodmis.org>
Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org>
---
Documentation/tools/index.rst | 1 +
Documentation/tools/rv/Makefile | 52 ++++++++++++++++++++
Documentation/tools/rv/common_appendix.rst | 13 +++++
Documentation/tools/rv/common_ikm.rst | 21 ++++++++
Documentation/tools/rv/index.rst | 24 +++++++++
Documentation/tools/rv/rv-list.rst | 39 +++++++++++++++
Documentation/tools/rv/rv-mon-wip.rst | 40 +++++++++++++++
Documentation/tools/rv/rv-mon-wwnr.rst | 39 +++++++++++++++
Documentation/tools/rv/rv-mon.rst | 51 +++++++++++++++++++
Documentation/tools/rv/rv.rst | 57 ++++++++++++++++++++++
tools/verification/rv/Makefile | 26 +++++++++-
11 files changed, 361 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
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..f8ffd271d886
--- /dev/null
+++ b/Documentation/tools/rv/common_appendix.rst
@@ -0,0 +1,13 @@
+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..0f206e985c27
--- /dev/null
+++ b/Documentation/tools/rv/common_ikm.rst
@@ -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.
diff --git a/Documentation/tools/rv/index.rst b/Documentation/tools/rv/index.rst
new file mode 100644
index 000000000000..50f40a3ee256
--- /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..727bd3fbcce9
--- /dev/null
+++ b/Documentation/tools/rv/rv-list.rst
@@ -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 <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..27a026f80cb7
--- /dev/null
+++ b/Documentation/tools/rv/rv-mon-wip.rst
@@ -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 <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..18807528c04c
--- /dev/null
+++ b/Documentation/tools/rv/rv-mon-wwnr.rst
@@ -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 <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..9e6e5db2de57
--- /dev/null
+++ b/Documentation/tools/rv/rv-mon.rst
@@ -0,0 +1,51 @@
+.. 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..16c1a3b8e1f7
--- /dev/null
+++ b/Documentation/tools/rv/rv.rst
@@ -0,0 +1,57 @@
+.. 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
diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile
index 1de111ac2641..3d0f3888a58c 100644
--- a/tools/verification/rv/Makefile
+++ b/tools/verification/rv/Makefile
@@ -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
--
2.37.3
prev parent reply other threads:[~2022-10-26 10:45 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-10-26 10:44 [PATCH 0/3] verification/rv: Add rv tool Daniel Bristot de Oliveira
2022-10-26 10:44 ` [PATCH 1/3] rv: " Daniel Bristot de Oliveira
2022-10-26 10:44 ` [PATCH 2/3] tools/rv: Add in-kernel monitor interface Daniel Bristot de Oliveira
2022-10-26 12:31 ` Daniel Bristot de Oliveira
2022-10-26 10:44 ` Daniel Bristot de Oliveira [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=320de46ad632099cdbaa24dc6fc690781017ff6f.1666776642.git.bristot@kernel.org \
--to=bristot@kernel.org \
--cc=corbet@lwn.net \
--cc=linux-doc@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=linux-trace-devel@vger.kernel.org \
--cc=rostedt@goodmis.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.