xref: /linux/tools/verification/rv/README.txt (revision 7ae9fb1b7ecbb5d85d07857943f677fd1a559b18)
1*4bc4b131SDaniel Bristot de OliveiraRV: Runtime Verification
2*4bc4b131SDaniel Bristot de Oliveira
3*4bc4b131SDaniel Bristot de OliveiraRuntime Verification (RV) is a lightweight (yet rigorous) method that
4*4bc4b131SDaniel Bristot de Oliveiracomplements classical exhaustive verification techniques (such as model
5*4bc4b131SDaniel Bristot de Oliveirachecking and theorem proving) with a more practical approach for
6*4bc4b131SDaniel Bristot de Oliveiracomplex systems.
7*4bc4b131SDaniel Bristot de Oliveira
8*4bc4b131SDaniel Bristot de OliveiraThe rv tool is the interface for a collection of monitors that aim
9*4bc4b131SDaniel Bristot de Oliveiraanalysing the logical and timing behavior of Linux.
10*4bc4b131SDaniel Bristot de Oliveira
11*4bc4b131SDaniel Bristot de OliveiraInstalling RV
12*4bc4b131SDaniel Bristot de Oliveira
13*4bc4b131SDaniel Bristot de OliveiraRV depends on the following libraries and tools:
14*4bc4b131SDaniel Bristot de Oliveira
15*4bc4b131SDaniel Bristot de Oliveira - libtracefs
16*4bc4b131SDaniel Bristot de Oliveira - libtraceevent
17*4bc4b131SDaniel Bristot de Oliveira
18*4bc4b131SDaniel Bristot de OliveiraIt also depends on python3-docutils to compile man pages.
19*4bc4b131SDaniel Bristot de Oliveira
20*4bc4b131SDaniel Bristot de OliveiraFor development, we suggest the following steps for compiling rtla:
21*4bc4b131SDaniel Bristot de Oliveira
22*4bc4b131SDaniel Bristot de Oliveira  $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git
23*4bc4b131SDaniel Bristot de Oliveira  $ cd libtraceevent/
24*4bc4b131SDaniel Bristot de Oliveira  $ make
25*4bc4b131SDaniel Bristot de Oliveira  $ sudo make install
26*4bc4b131SDaniel Bristot de Oliveira  $ cd ..
27*4bc4b131SDaniel Bristot de Oliveira  $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git
28*4bc4b131SDaniel Bristot de Oliveira  $ cd libtracefs/
29*4bc4b131SDaniel Bristot de Oliveira  $ make
30*4bc4b131SDaniel Bristot de Oliveira  $ sudo make install
31*4bc4b131SDaniel Bristot de Oliveira  $ cd ..
32*4bc4b131SDaniel Bristot de Oliveira  $ cd $rv_src
33*4bc4b131SDaniel Bristot de Oliveira  $ make
34*4bc4b131SDaniel Bristot de Oliveira  $ sudo make install
35*4bc4b131SDaniel Bristot de Oliveira
36*4bc4b131SDaniel Bristot de OliveiraFor further information, please see rv manpage and the kernel documentation:
37*4bc4b131SDaniel Bristot de Oliveira  Runtime Verification:
38*4bc4b131SDaniel Bristot de Oliveira    Documentation/trace/rv/runtime-verification.rst
39