Commit Graph

4 Commits

Author SHA1 Message Date
Gabriele Monaco
e4a1e415eb Documentation/rv: Adapt documentation after da_monitor refactoring
Previous changes refactored the da_monitor header file to avoid using
macros. This implies a few changes in how to import and use da_monitor
helpers:

 DECLARE_DA_MON_<TYPE>(name, type) is substituted by
 #define RV_MON_TYPE RV_MON_<TYPE>

 da_handle_event_<name>() is substituted by
 da_handle_event()

Update the documentation to reflect the changes.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20251126104241.291258-4-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-01-12 07:43:50 +01:00
Gopi Krishna Menon
70d476b63a Documentation/rv: Fix minor typo in monitor_synthesis page
Specifically, fix spelling of "practice"

Signed-off-by: Gopi Krishna Menon <krishnagopi487@gmail.com>
Signed-off-by: Jonathan Corbet <corbet@lwn.net>
Link: https://lore.kernel.org/r/20250810111249.93181-1-krishnagopi487@gmail.com
2025-08-12 12:41:20 -06:00
Nam Cao
e93648e862 Documentation/rv: Add documentation for linear temporal logic monitors
Add documents describing linear temporal logic runtime verification
monitors and how to generate them using rvgen.

Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/be13719e66fd8da147d7c69d5365aa23c52b743f.1751634289.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24 10:42:47 -04:00
Nam Cao
f40a7c0602 Documentation/rv: Prepare monitor synthesis document for LTL inclusion
Monitor synthesis from deterministic automaton and linear temporal logic
have a lot in common. Therefore a single document should describe both.

Change da_monitor_synthesis.rst to monitor_synthesis.rst. LTL monitor
synthesis will be added to this file by a follow-up commit.

This makes the diff far easier to read. If renaming and adding LTL info is
done in a single commit, git wouldn't recognize it as a rename, but a file
removal and a file addition.

While at it, correct the old dot2k commands to the new rvgen commands.

Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/d91c6e4600287f4732d68a014219e576a75ce6dc.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24 10:42:46 -04:00