summaryrefslogtreecommitdiff
path: root/tools/verification
AgeCommit message (Collapse)AuthorFilesLines
2023-04-25rv: Fix addition on an uninitialized variable 'run'Colin Ian King1-1/+1
The variable run is not initialized however it is being accumulated by the return value from the call to ikm_run_monitor. Fix this by initializing run to zero at the start of the function. Link: https://lkml.kernel.org/r/20230424094730.105313-1-colin.i.king@gmail.com Fixes: 4bc4b131d44c ("rv: Add rv tool") Signed-off-by: Colin Ian King <colin.i.king@gmail.com> Acked-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2023-01-31tools/rv: Remove unneeded semicolonzhang songyi1-1/+1
The semicolon after the "}" is unneeded. Link: https://lore.kernel.org/linux-trace-devel/202212191431057948891@zte.com.cn Signed-off-by: zhang songyi <zhang.songyi@zte.com.cn> Acked-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-12-21Merge tag 'trace-v6.2-1' of ↵Linus Torvalds1-1/+1
git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace Pull tracing fix from Steven Rostedt: "I missed this minor hardening of the kernel in the first pull. - Make monitor structures read only" * tag 'trace-v6.2-1' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: rv/monitors: Move monitor structure in rodata
2022-12-20rv/monitors: Move monitor structure in rodataAlessandro Carminati1-1/+1
It makes sense to move the important monitor structure into rodata to prevent accidental structure modification. Link: https://lkml.kernel.org/r/20221122173648.4732-1-acarmina@redhat.com Signed-off-by: Alessandro Carminati <acarmina@redhat.com> Acked-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-12-09Documentation/rv: Add verification/rv man pagesDaniel Bristot de Oliveira1-2/+24
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>
2022-12-09tools/rv: Add in-kernel monitor interfaceDaniel Bristot de Oliveira3-0/+704
Add the ability to control and trace in-kernel monitors. This is a generic interface, it will check for existing monitors and enable standard setup, like enabling reactors. For example: # rv list wip wakeup in preemptive per-cpu testing monitor. [OFF] wwnr wakeup while not running per-task testing model. [OFF] # rv mon wwnr --help rv version 6.1.0-rc4: help usage: rv mon wwnr [-h] [-q] [-r reactor] [-s] [-v] -h/--help: print this menu and the reactor list -r/--reactor 'reactor': enables the 'reactor' -s/--self: when tracing (-t), also trace rv command -t/--trace: trace monitor's event -v/--verbose: print debug messages available reactors: nop printk panic # rv mon wwnr --trace <TASK>-PID [CPU] TYPE ID STATE x EVENT -> NEXT_STATE FINAL | | | | | | | | | rv-3613 [001] event 3613 running x switch_out -> not_running Y sshd-1248 [005] event 1248 running x switch_out -> not_running Y <idle>-0 [005] event 71 not_running x wakeup -> not_running Y <idle>-0 [005] event 71 not_running x switch_in -> running N kcompactd0-71 [005] event 71 running x switch_out -> not_running Y <idle>-0 [000] event 860 not_running x wakeup -> not_running Y <idle>-0 [000] event 860 not_running x switch_in -> running N systemd-oomd-860 [000] event 860 running x switch_out -> not_running Y <idle>-0 [000] event 860 not_running x wakeup -> not_running Y <idle>-0 [000] event 860 not_running x switch_in -> running N systemd-oomd-860 [000] event 860 running x switch_out -> not_running Y <idle>-0 [005] event 71 not_running x wakeup -> not_running Y <idle>-0 [005] event 71 not_running x switch_in -> running N kcompactd0-71 [005] event 71 running x switch_out -> not_running Y <idle>-0 [000] event 860 not_running x wakeup -> not_running Y <idle>-0 [000] event 860 not_running x switch_in -> running N systemd-oomd-860 [000] event 860 running x switch_out -> not_running Y <idle>-0 [001] event 3613 not_running x wakeup -> not_running Y Link: https://lkml.kernel.org/r/1e57547e3acadda6e23949b2672c89e76ec2ec42.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>
2022-12-09rv: Add rv toolDaniel Bristot de Oliveira8-0/+558
This is the (user-space) runtime verification tool, named rv. This tool aims to be the interface for in-kernel rv monitors, as well as the home for monitors in user-space (online asynchronous), and in *eBPF. The tool receives a command as the first argument, the current commands are: list - list all available monitors mon - run a given monitor Each monitor is an independent piece of software inside the tool and can have their own arguments. There is no monitor implemented in this patch, it only adds the basic structure of the tool, based on rtla. # rv --help rv version 6.1.0-rc4: help usage: rv command [-h] [command_options] -h/--help: print this menu command: run one of the following command: list: list all available monitors mon: run a monitor [command options]: each command has its own set of options run rv command -h for further information *dot2bpf is the next patch set, depends on this, doing cleanups. Link: https://lkml.kernel.org/r/fb51184f3b95aea0d7bfdc33ec09f4153aee84fa.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>
2022-10-20rv/dot2c: Make automaton definition staticDaniel Bristot de Oliveira1-1/+1
Monitor's automata definition is only used locally, so make dot2c generate a static definition. Link: https://lore.kernel.org/all/202208210332.gtHXje45-lkp@intel.com Link: https://lore.kernel.org/all/202208210358.6HH3OrVs-lkp@intel.com Link: https://lkml.kernel.org/r/ffbb92010f643307766c9307fd42f416e5b85fa0.1661266564.git.bristot@kernel.org Cc: Steven Rostedt <rostedt@goodmis.org> Fixes: e3c9fc78f096 ("tools/rv: Add dot2c") Reported-by: kernel test robot <lkp@intel.com> Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-09-26rv/monitor: Add __init/__exit annotations to module init/exit funcsXiu Jianfeng3-6/+6
Add missing __init/__exit annotations to module init/exit funcs. Link: https://lkml.kernel.org/r/20220922103208.162869-1-xiujianfeng@huawei.com Fixes: 24bce201d798 ("tools/rv: Add dot2k") Fixes: 8812d21219b9 ("rv/monitor: Add the wip monitor skeleton created by dot2k") Fixes: ccc319dcb450 ("rv/monitor: Add the wwnr monitor") Signed-off-by: Xiu Jianfeng <xiujianfeng@huawei.com> Acked-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-09-26rv/dot2K: add 'static' qualifier for local variableZeng Heng3-6/+6
Following Daniel's suggestion, fix similar warning in template files, which would prevent new monitors from such warning. Link: https://lkml.kernel.org/r/20220824034357.2014202-3-zengheng4@huawei.com Cc: <mingo@redhat.com> Fixes: 24bce201d798 ("tools/rv: Add dot2k") Suggested-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Zeng Heng <zengheng4@huawei.com> Acked-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-07-30rv/monitor: Add the wwnr monitorDaniel Bristot de Oliveira1-0/+16
Per task wakeup while not running (wwnr) monitor. This model is broken, the reason is that a task can be running in the processor without being set as RUNNABLE. Think about a task about to sleep: 1: set_current_state(TASK_UNINTERRUPTIBLE); 2: schedule(); And then imagine an IRQ happening in between the lines one and two, waking the task up. BOOM, the wakeup will happen while the task is running. Q: Why do we need this model, so? A: To test the reactors. Link: https://lkml.kernel.org/r/473c0fc39967250fdebcff8b620311c11dccad30.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <wim@linux-watchdog.org> Cc: Guenter Roeck <linux@roeck-us.net> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Ingo Molnar <mingo@redhat.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will@kernel.org> Cc: Catalin Marinas <catalin.marinas@arm.com> Cc: Marco Elver <elver@google.com> Cc: Dmitry Vyukov <dvyukov@google.com> Cc: "Paul E. McKenney" <paulmck@kernel.org> Cc: Shuah Khan <skhan@linuxfoundation.org> Cc: Gabriele Paoloni <gpaoloni@redhat.com> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: Tao Zhou <tao.zhou@linux.dev> Cc: Randy Dunlap <rdunlap@infradead.org> Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-07-30rv/monitor: Add the wip monitorDaniel Bristot de Oliveira1-0/+16
The wakeup in preemptive (wip) monitor verifies if the wakeup events always take place with preemption disabled: | | v #==================# H preemptive H <+ #==================# | | | | preempt_disable | preempt_enable v | sched_waking +------------------+ | +--------------- | | | | | non_preemptive | | +--------------> | | -+ +------------------+ The wakeup event always takes place with preemption disabled because of the scheduler synchronization. However, because the preempt_count and its trace event are not atomic with regard to interrupts, some inconsistencies might happen. The documentation illustrates one of these cases. Link: https://lkml.kernel.org/r/c98ca678df81115fddc04921b3c79720c836b18f.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <wim@linux-watchdog.org> Cc: Guenter Roeck <linux@roeck-us.net> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Ingo Molnar <mingo@redhat.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will@kernel.org> Cc: Catalin Marinas <catalin.marinas@arm.com> Cc: Marco Elver <elver@google.com> Cc: Dmitry Vyukov <dvyukov@google.com> Cc: "Paul E. McKenney" <paulmck@kernel.org> Cc: Shuah Khan <skhan@linuxfoundation.org> Cc: Gabriele Paoloni <gpaoloni@redhat.com> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: Tao Zhou <tao.zhou@linux.dev> Cc: Randy Dunlap <rdunlap@infradead.org> Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-07-30Documentation/rv: Add deterministic automata monitor synthesis documentationDaniel Bristot de Oliveira2-0/+6
Add the da_monitor_synthesis.rst introduces some concepts behind the Deterministic Automata (DA) monitor synthesis and interface. Link: https://lkml.kernel.org/r/7873bdb7b2e5d2bc0b2eb6ca0b324af9a0ba27a0.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <wim@linux-watchdog.org> Cc: Guenter Roeck <linux@roeck-us.net> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Ingo Molnar <mingo@redhat.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will@kernel.org> Cc: Catalin Marinas <catalin.marinas@arm.com> Cc: Marco Elver <elver@google.com> Cc: Dmitry Vyukov <dvyukov@google.com> Cc: "Paul E. McKenney" <paulmck@kernel.org> Cc: Shuah Khan <skhan@linuxfoundation.org> Cc: Gabriele Paoloni <gpaoloni@redhat.com> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: Tao Zhou <tao.zhou@linux.dev> Cc: Randy Dunlap <rdunlap@infradead.org> Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-07-30tools/rv: Add dot2kDaniel Bristot de Oliveira6-0/+496
transform .dot file into kernel rv monitor usage: dot2k [-h] -d DOT_FILE -t MONITOR_TYPE [-n MODEL_NAME] [-D DESCRIPTION] optional arguments: -h, --help show this help message and exit -d DOT_FILE, --dot DOT_FILE -t MONITOR_TYPE, --monitor_type MONITOR_TYPE -n MODEL_NAME, --model_name MODEL_NAME -D DESCRIPTION, --description DESCRIPTION Link: https://lkml.kernel.org/r/083b3ae61e5a62c1e2e5d08009baa91f82181618.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <wim@linux-watchdog.org> Cc: Guenter Roeck <linux@roeck-us.net> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Ingo Molnar <mingo@redhat.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will@kernel.org> Cc: Catalin Marinas <catalin.marinas@arm.com> Cc: Marco Elver <elver@google.com> Cc: Dmitry Vyukov <dvyukov@google.com> Cc: "Paul E. McKenney" <paulmck@kernel.org> Cc: Shuah Khan <skhan@linuxfoundation.org> Cc: Gabriele Paoloni <gpaoloni@redhat.com> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: Tao Zhou <tao.zhou@linux.dev> Cc: Randy Dunlap <rdunlap@infradead.org> Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-07-30Documentation/rv: Add deterministic automaton documentationDaniel Bristot de Oliveira3-0/+9
Add documentation about deterministic automaton and its possible representations (formal, graphic, .dot and C). Link: https://lkml.kernel.org/r/387edaed87630bd5eb37c4275045dfd229700aa6.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <wim@linux-watchdog.org> Cc: Guenter Roeck <linux@roeck-us.net> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Ingo Molnar <mingo@redhat.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will@kernel.org> Cc: Catalin Marinas <catalin.marinas@arm.com> Cc: Marco Elver <elver@google.com> Cc: Dmitry Vyukov <dvyukov@google.com> Cc: "Paul E. McKenney" <paulmck@kernel.org> Cc: Shuah Khan <skhan@linuxfoundation.org> Cc: Gabriele Paoloni <gpaoloni@redhat.com> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: Tao Zhou <tao.zhou@linux.dev> Cc: Randy Dunlap <rdunlap@infradead.org> Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2022-07-30tools/rv: Add dot2cDaniel Bristot de Oliveira4-0/+466
dot2c is a tool that transforms an automata in the graphiviz .dot file into an C representation of the automata. usage: dot2c [-h] dot_file dot2c: converts a .dot file into a C structure positional arguments: dot_file The dot file to be converted optional arguments: -h, --help show this help message and exit Link: https://lkml.kernel.org/r/b26204ba9509c80bcda31b76cdea31ddb188cd24.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <wim@linux-watchdog.org> Cc: Guenter Roeck <linux@roeck-us.net> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Ingo Molnar <mingo@redhat.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will@kernel.org> Cc: Catalin Marinas <catalin.marinas@arm.com> Cc: Marco Elver <elver@google.com> Cc: Dmitry Vyukov <dvyukov@google.com> Cc: "Paul E. McKenney" <paulmck@kernel.org> Cc: Shuah Khan <skhan@linuxfoundation.org> Cc: Gabriele Paoloni <gpaoloni@redhat.com> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: Tao Zhou <tao.zhou@linux.dev> Cc: Randy Dunlap <rdunlap@infradead.org> Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 00:32:58 +0000