Re: [RFC PATCH 1/4] rv/tlob: Add tlob model DOT file

[Gabriele Monaco <gmonaco@redhat.com>]

On Mon, 2026-04-13 at 03:27 +0800, wen.yang@linux.dev wrote:
> From: Wen Yang <wen.yang@linux.dev>
> 
> Add the Graphviz DOT specification for the tlob (task latency over
> budget) deterministic automaton.
> 
> The model has three states: unmonitored, on_cpu, and off_cpu.
> trace_start transitions from unmonitored to on_cpu; switch_out and
> switch_in cycle between on_cpu and off_cpu; trace_stop and
> budget_expired return to unmonitored from either active state.
> unmonitored is the sole accepting state.
> 
> switch_in, switch_out, and sched_wakeup self-loop in unmonitored;
> sched_wakeup self-loops in on_cpu; switch_out and sched_wakeup
> self-loop in off_cpu.
> 
> Signed-off-by: Wen Yang <wen.yang@linux.dev>
> ---

Interesting monitor! Thanks.
I'm going to go through it more in details later, but let me share some initial
comments.

>  MAINTAINERS                        |  3 +++
>  tools/verification/models/tlob.dot | 25 +++++++++++++++++++++++++
>  2 files changed, 28 insertions(+)
>  create mode 100644 tools/verification/models/tlob.dot
> 
> diff --git a/MAINTAINERS b/MAINTAINERS
> index 9fbb619c6..c2c56236c 100644
> --- a/MAINTAINERS
> +++ b/MAINTAINERS
> @@ -23242,7 +23242,10 @@ S:	Maintained
>  F:	Documentation/trace/rv/
>  F:	include/linux/rv.h
>  F:	include/rv/
> +F:	include/uapi/linux/rv.h
>  F:	kernel/trace/rv/
> +F:	samples/rv/
> +F:	tools/testing/selftests/rv/
>  F:	tools/testing/selftests/verification/
>  F:	tools/verification/

This change doesn't belong here, the patch itself is not adding those file, you
should probably move it later.

>  
> diff --git a/tools/verification/models/tlob.dot
> b/tools/verification/models/tlob.dot
> new file mode 100644
> index 000000000..df34a14b8
> --- /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_unmonitored"};
> +	{node [shape = ellipse] "unmonitored"};
> +	{node [shape = plaintext] "unmonitored"};
> +	{node [shape = plaintext] "on_cpu"};
> +	{node [shape = plaintext] "off_cpu"};
> +	"__init_unmonitored" -> "unmonitored";
> +	"unmonitored" [label = "unmonitored", color = green3];
> +	"unmonitored" -> "on_cpu" [ label = "trace_start" ];
> +	"unmonitored" -> "unmonitored" [ label =
> "switch_in\nswitch_out\nsched_wakeup" ];
> +	"on_cpu" [label = "on_cpu"];
> +	"on_cpu" -> "off_cpu" [ label = "switch_out" ];
> +	"on_cpu" -> "unmonitored" [ label = "trace_stop\nbudget_expired" ];
> +	"on_cpu" -> "on_cpu" [ label = "sched_wakeup" ];
> +	"off_cpu" [label = "off_cpu"];
> +	"off_cpu" -> "on_cpu" [ label = "switch_in" ];
> +	"off_cpu" -> "unmonitored" [ label = "trace_stop\nbudget_expired" ];
> +	"off_cpu" -> "off_cpu" [ label = "switch_out\nsched_wakeup" ];
> +	{ rank = min ;
> +		"__init_unmonitored";
> +		"unmonitored";
> +	}
> +}