From: sashiko-bot@kernel.org
To: wen.yang@linux.dev
Cc: linux-trace-kernel@vger.kernel.org
Subject: Re: [PATCH v6 3/9] rv: Add tlob model DOT file
Date: Thu, 20 Aug 2026 16:53:00 +0000 [thread overview]
Message-ID: <20260820165301.0C64F1F000E9@smtp.kernel.org> (raw)
In-Reply-To: <9e27f8af4520800fd1f19a2b9e9c0a0f2250920a.1787243842.git.wen.yang@linux.dev>
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 <wen.yang@linux.dev>
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
next prev parent reply other threads:[~2026-08-20 16:53 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-08-20 16:45 [PATCH v6 0/9] rv: Add task latency over budget RV monitor wen.yang
2026-08-20 16:45 ` [PATCH v6 1/9] rv: Introduce DA_MON_ALLOCATION_STRATEGY wen.yang
2026-08-20 16:45 ` [PATCH v6 2/9] rv: Add generic uprobe infrastructure for RV monitors wen.yang
2026-08-20 16:59 ` sashiko-bot
2026-08-20 16:45 ` [PATCH v6 3/9] rv: Add tlob model DOT file wen.yang
2026-08-20 16:53 ` sashiko-bot [this message]
2026-08-20 16:45 ` [PATCH v6 4/9] rv: Fix ha_invariant_passed_ns silent bypass of invariant check wen.yang
2026-08-20 16:58 ` sashiko-bot
2026-08-20 16:45 ` [PATCH v6 5/9] rv: Make da_monitor_reset_hook and EVENT_NONE_LBL overridable wen.yang
2026-08-20 16:59 ` sashiko-bot
2026-08-20 16:45 ` [PATCH v6 6/9] rv: Add tlob hybrid automaton monitor wen.yang
2026-08-20 17:03 ` sashiko-bot
2026-08-20 16:45 ` [PATCH v6 7/9] rv: Add KUnit tests for the tlob monitor wen.yang
2026-08-20 16:45 ` [PATCH v6 8/9] selftests/verification: Add tlob selftests wen.yang
2026-08-20 16:56 ` sashiko-bot
2026-08-20 16:45 ` [PATCH v6 9/9] selftests/ftrace: Walk up to find test.d/functions when a subdirectory is passed wen.yang
2026-08-20 16:58 ` sashiko-bot
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20260820165301.0C64F1F000E9@smtp.kernel.org \
--to=sashiko-bot@kernel.org \
--cc=linux-trace-kernel@vger.kernel.org \
--cc=sashiko-reviews@lists.linux.dev \
--cc=wen.yang@linux.dev \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox