Thank you for your contribution! Sashiko AI review found 1 potential issue(s) to consider:
- [Medium] The implemented DOT model contradicts explicit claims made in the commit message regarding states, transitions, and invariants.
--
--- Patch [3]: [PATCH v6 3/9] rv: Add tlob model DOT file ---
commit 8a3ea61817d2834335f8a9230c5ffaf2a08353b7
Author: Wen Yang [off-list ref]
rv: Add tlob model DOT file
This commit adds the Graphviz DOT specification of the tlob hybrid
automaton to the kernel's verification models.
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]
Does this description accurately reflect the implemented model?
The text mentions three states, five transitions, and an invariant active
in all states. However, the included DOT file defines a fourth "stopped"
state, two additional transitions ("stop" and "start"), and omits the
invariant from the "stopped" state:
tools/verification/models/tlob.dot:
"running" [label = "running\nclk_elapsed < BUDGET_NS()", color = green3];
"waiting" [label = "waiting\nclk_elapsed < BUDGET_NS()"];
"sleeping" [label = "sleeping\nclk_elapsed < BUDGET_NS()"];
"stopped" [label = "stopped"];
"running" -> "sleeping" [ label = "sleep" ];
"running" -> "waiting" [ label = "preempt" ];
"waiting" -> "running" [ label = "switch_in" ];
"sleeping" -> "waiting" [ label = "wakeup" ];
"running" -> "stopped" [ label = "stop" ];
"stopped" -> "running" [ label = "start;reset(clk_elapsed)" ];
Could the commit message be updated to match the actual automaton
implemented in the code?
--
Sashiko AI review · https://sashiko.dev/#/patchset/cover.1787243842.git.wen.yang@linux.dev?part=3