| Age | Commit message (Collapse) | Author |
|---|
|
Monitors generated with dot2k have their registration function (the one
called during monitor initialisation) return always 0, even if the
registration failed on RV side.
This can hide potential errors.
Return the value returned by the RV register function.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Tomas Glozar <tglozar@redhat.com>
Cc: Juri Lelli <jlelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: John Kacur <jkacur@redhat.com>
Link: https://lore.kernel.org/20250723161240.194860-6-gmonaco@redhat.com
Reviewed-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
|
|
The current behaviour of rvgen when running with the -a option is to
append the necessary lines at the end of the configuration for Kconfig,
Makefile and tracepoints.
This is not always the desired behaviour in case of nested monitors:
while tracepoints are not affected by nesting and the Makefile's only
requirement is that the parent monitor is built before its children, in
the Kconfig it is better to have children defined right after their
parent, otherwise the result has wrong indentation:
[*] foo_parent monitor
[*] foo_child1 monitor
[*] foo_child2 monitor
[*] bar_parent monitor
[*] bar_child1 monitor
[*] bar_child2 monitor
[*] foo_child3 monitor
[*] foo_child4 monitor
Adapt rvgen to look for a different marker for nested monitors in the
Kconfig file and append the line right after the last sibling, instead
of the last monitor.
Also add the marker when creating a new parent monitor.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Tomas Glozar <tglozar@redhat.com>
Cc: Juri Lelli <jlelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: John Kacur <jkacur@redhat.com>
Link: https://lore.kernel.org/20250723161240.194860-5-gmonaco@redhat.com
Reviewed-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
|
|
The dot2c.py script generates all states in a single line. This breaks the
100 column limit when the state machines are non-trivial.
Change dot2c.py to generate the states in separate lines in case the
generated line is going to be too long.
Also adapt existing monitors with line length over the limit.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Tomas Glozar <tglozar@redhat.com>
Cc: Juri Lelli <jlelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: John Kacur <jkacur@redhat.com>
Link: https://lore.kernel.org/20250723161240.194860-4-gmonaco@redhat.com
Suggested-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
|
|
ltl2k generates all variable definition in both ltl_start() and
ltl_possible_next_states(). However, these two functions may not use all
the variables, causing "unused variable" compiler warning.
Change the script to only generate used variables.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/636b2b2d99a9bd46a9f77a078d44ebd7ffc7508c.1752850449.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
|
|
If a variable appears multiple times in the specification, ltl2k generates
multiple variable definitions. This fails the build.
Make sure each variable is only defined once.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/107dcf0d0aa8482d5fbe0314c3138f61cd284e91.1752850449.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
|
|
The 'next' operator is a unary operator. It is defined as: "next time, the
operand must be true".
Support this operator. For RV monitors, "next time" means the next
invocation of ltl_validate().
Cc: John Ogness <john.ogness@linutronix.de>
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/9c32cec04dd18d2e956fddd84b0e0a2503daa75a.1752239482.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Tested-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
|
|
Add support for generating RV monitors from linear temporal logic, similar
to the generation of deterministic automaton monitors.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/f3c63b363ff9c5af3302ba2b5d92a26a98700eaf.1751634289.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
|
|
Both container generation and DA monitor generation is implemented in the
class dot2k. That requires some ugly "if is_container ... else ...". If
linear temporal logic support is added at the current state, the "if else"
chain is longer and uglier.
Furthermore, container generation is irrevelant to .dot files. It is
therefore illogical to be implemented in class "dot2k".
Clean it up, restructure the dot2k class into the following class
hierarchy:
(RVGenerator)
/\
/ \
/ \
/ \
/ \
(Container) (Monitor)
/\
/ \
/ \
/ \
(dot2k) [ltl2k] <- intended
This allows a simple and clean integration of LTL.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/692137a581ba6bee7a64d37fb7173ae137c47bbd.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>
|
|
To simply the scripts and to allow easy integration of new monitor types,
restructure the template files as followed:
1. Move the template files to be in the same directory as the rvgen
package. Furthermore, the installation will now only install the
templates to the package directory, not /usr/share/. This simplify
templates reading, as the scripts do not need to find the templates at
multiple places.
2. Move dot2k_templates/* to:
- templates/dot2k/
- templates/container/
This allows sharing templates reading code between DA monitor generation
and container generation (and any future generation type).
For template files which can be shared between different generation
types, support putting them in templates/
This restructure aligns with the recommendation from:
https://python-packaging.readthedocs.io/en/latest/non-code-files.html
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/462d90273f96804d3ba850474877d5f727031258.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>
|
|
The dot2k tool has some code that can be reused for linear temporal logic
monitor. Prepare its frontend for LTL inclusion:
1. Rename to be generic: rvgen
2. Replace the parameter --dot with 2 parameters:
--class: to specific the monitor class, can be 'da' or 'ltl'
--spec: the monitor specification file, .dot file for DA, and .ltl
file for LTL
The old command:
python3 dot2/dot2k monitor -d wip.dot -t per_cpu
is equivalent to the new commands:
python3 rvgen monitor -c da -s wip.dot -t per_cpu
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.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>
|
