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>
This commit is contained in:
Daniel Bristot de Oliveira
Steven Rostedt (Google)
parent
6d60f89691
commit
afc70ccb96
|
|
@ -11,6 +11,7 @@ more additions are needed here:
|
|||
:maxdepth: 1
|
||||
|
||||
rtla/index
|
||||
rv/index
|
||||
|
||||
.. only:: subproject and html
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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).
|
||||
|
|
@ -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.
|
||||
|
|
@ -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`
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue