Re: [PATCH v5 3/9] rv: Add tlob model DOT file
From: sashiko-bot@kernel.org
Date: 2026-08-19 18:25:38
Thank you for your contribution! Sashiko AI review found 2 potential issue(s) to consider: - [High] The 'running' node is defined twice with conflicting shapes, incorrectly designating it as the final state instead of 'stopped'. - [Medium] The commit message significantly contradicts the implemented DOT model's states, transitions, and invariants. --
--- Patch [3]: [PATCH v5 3/9] rv: Add tlob model DOT file ---commit a0f17b48f9f5df47c444bf6d511a4f8c03b0a847 Author: Wen Yang [off-list ref] rv: Add tlob model DOT file Add the Graphviz DOT specification of the tlob hybrid automaton to tools/verification/models/.
The model has three states (running, waiting, sleeping), five transitions (switch_in, preempt, wakeup, sleep), and a single clock invariant clk_elapsed < BUDGET_NS() active in all states.
[Severity: Medium] This isn't a bug, but does this description accurately reflect the implemented model? The DOT file defines four states (running, waiting, sleeping, stopped), six transitions, and the clock invariant is intentionally absent from the "stopped" state.
quoted hunk ↗ jump to hunk
diff --git a/tools/verification/models/tlob.dot b/tools/verification/models/tlob.dot new file mode 100644 index 0000000000000..7f6f09c3d7cf0 --- /dev/null +++ b/tools/verification/models/tlob.dot@@ -0,0 +1,25 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_stopped"}; + {node [shape = ellipse] "running"}; + {node [shape = plaintext] "running"};
[Severity: High]
Is it intentional to define the "running" node twice with conflicting shapes?
Because tools/verification/rvgen/rvgen/automata.py prioritizes the first
definition ("ellipse") over the second ("plaintext") when merging attributes,
this improperly designates "running" as the final accepting state instead of
"stopped".
--
Sashiko AI review · https://sashiko.dev/#/patchset/cover.1787161646.git.wen.yang@linux.dev?part=3