public inbox for linux-kernel@vger.kernel.org
 help / color / mirror / Atom feed
From: Gabriele Monaco <gmonaco@redhat.com>
To: Nam Cao <namcao@linutronix.de>
Cc: Steven Rostedt <rostedt@goodmis.org>,
	Wander Lairson Costa <wander@redhat.com>,
	linux-trace-kernel@vger.kernel.org,
	 linux-kernel@vger.kernel.org
Subject: Re: [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables
Date: Wed, 06 May 2026 11:15:43 +0200	[thread overview]
Message-ID: <967f1cd8cd6e27aaa65d68194487306bc312caa0.camel@redhat.com> (raw)
In-Reply-To: <a779af6dc89721179e0dbab08623e42aa0191275.1777962130.git.namcao@linutronix.de>

On Tue, 2026-05-05 at 08:59 +0200, Nam Cao wrote:
> Hybrid automata monitors's clock variables have two different
> representations:
> 
>   - The invariant representation, which is the timestamp when the invariant
>     expires
> 
>   - The guard representation, which is the timestamp when the clock is last
>     reset
> 
> This dual representation makes the logic quite difficult to follow (well,
> at least for me). It also complicates the monitors and the generation tool,
> as it requires conversion back and forth between the representation.
> 
> Simplify by using the clock variables for a single purpose: storing the
> time stamp since the clock is last reset.
> 
> This also allows simplifying rvgen, which will be done in a follow-up
> commit.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>

Well, this is roughly what we discussed in [1].
Now, I didn't submit the throttle monitor yet because it depends on unacked
tracepoints.

In short, this works with the assumption that the expires value you pass to
ha_check_invariant() is the same you used to arm the timer.

That's true for constant values only (the deadline) but not for something like
the runtime. I couldn't think of a way to rearrange that model not to require
the runtime left field.


Otherwise.. We could read the remaining time in the timer, but we wouldn't be
able to simulate ns precision when using the timer wheel.

Now if we really wanted to go down that path, we are using a union to allocate
either timer or hrtimer, the latter is larger, so we /could/ add a u64 expire_ns
field to the ha_monitor struct without needing additional memory.

If that doesn't sound too wild to you, I may try and sketch something up to see
if that's viable. Then this patch could go through as is and I would add the
extension together with the submission of throttle.

What do you think?

Thanks,
Gabriele

[1] -
https://lore.kernel.org/lkml/0c61c0bbbdc2002efb638dccda1f0a18c51d29df.camel@redhat.com

> ---
>  include/rv/ha_monitor.h                  | 60 ++++++------------------
>  kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +------
>  kernel/trace/rv/monitors/stall/stall.c   |  2 +-
>  3 files changed, 17 insertions(+), 63 deletions(-)
> 
> diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
> index d59507e8cb30..1ce3fd324d2c 100644
> --- a/include/rv/ha_monitor.h
> +++ b/include/rv/ha_monitor.h
> @@ -253,19 +253,8 @@ static inline void __ha_monitor_timer_callback(struct
> ha_monitor *ha_mon)
>  }
>  
>  /*
> - * The clock variables have 2 different representations in the env_store:
> - * - The guard representation is the timestamp of the last reset
> - * - The invariant representation is the timestamp when the invariant expires
> - * As the representations are incompatible, care must be taken when switching
> - * between them: the invariant representation can only be used when starting
> a
> - * timer when the previous representation was guard (e.g. no other invariant
> - * started since the last reset operation).
> - * Likewise, switching from invariant to guard representation without a reset
> - * can be done only by subtracting the exact value used to start the
> invariant.
> - *
> - * Reading the environment variable (ha_get_clk) also reflects this
> difference
> - * any reads in states that have an invariant return the (possibly negative)
> - * time since expiration, other reads return the time since last reset.
> + * The clock variables store the time epoch - the timestamp when the clock
> was last reset.
> + * They are read by subtracting the time epoch from the current time.
>   */
>  
>  /*
> @@ -279,31 +268,21 @@ static inline void ha_reset_clk_ns(struct ha_monitor
> *ha_mon, enum envs env, u64
>  {
>  	WRITE_ONCE(ha_mon->env_store[env], time_ns);
>  }
> -static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs
> env,
> -				       u64 value, u64 time_ns)
> -{
> -	WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
> -}
> -static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
> -					 enum envs env, u64 time_ns)
> +static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs
> env,
> +					 u64 time_ns, u64 expire_ns)
>  {
> -	return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
> +	return time_ns - READ_ONCE(ha_mon->env_store[env]) <= expire_ns;
>  }
>  /*
>   * ha_invariant_passed_ns - prepare the invariant and return the time since
> reset
>   */
> -static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs
> env,
> -				   u64 expire, u64 time_ns)
> +static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs
> env, u64 time_ns)
>  {
> -	u64 passed = 0;
> -
>  	if (env < 0 || env >= ENV_MAX_STORED)
>  		return 0;
>  	if (ha_monitor_env_invalid(ha_mon, env))
>  		return 0;
> -	passed = ha_get_env(ha_mon, env, time_ns);
> -	ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
> -	return passed;
> +	return ha_get_env(ha_mon, env, time_ns);
>  }
>  
>  /*
> @@ -317,32 +296,21 @@ static inline void ha_reset_clk_jiffy(struct ha_monitor
> *ha_mon, enum envs env)
>  {
>  	WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
>  }
> -static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
> -					  enum envs env, u64 value)
> -{
> -	WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
> -}
> -static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
> -					    enum envs env, u64 time_ns)
> +static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum
> envs env,
> +					    u64 time_ns, u64 expire_jiffy)
>  {
> -	return time_after64(READ_ONCE(ha_mon->env_store[env]),
> get_jiffies_64());
> -
> +	return time_after64(READ_ONCE(ha_mon->env_store[env]) + expire_jiffy,
> get_jiffies_64());
>  }
>  /*
>   * ha_invariant_passed_jiffy - prepare the invariant and return the time
> since reset
>   */
> -static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum
> envs env,
> -				      u64 expire, u64 time_ns)
> +static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum
> envs env, u64 time_ns)
>  {
> -	u64 passed = 0;
> -
>  	if (env < 0 || env >= ENV_MAX_STORED)
>  		return 0;
>  	if (ha_monitor_env_invalid(ha_mon, env))
>  		return 0;
> -	passed = ha_get_env(ha_mon, env, time_ns);
> -	ha_set_invariant_jiffy(ha_mon, env, expire - passed);
> -	return passed;
> +	return ha_get_env(ha_mon, env, time_ns);
>  }
>  
>  /*
> @@ -389,14 +357,14 @@ static inline void ha_setup_timer(struct ha_monitor
> *ha_mon)
>  static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs
> env,
>  					u64 expire, u64 time_ns)
>  {
> -	u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
> +	u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
>  
>  	mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
>  }
>  static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs
> env,
>  				     u64 expire, u64 time_ns)
>  {
> -	u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
> +	u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
>  
>  	ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
>  			     nsecs_to_jiffies(expire - passed + TICK_NSEC -
> 1), time_ns);
> diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c
> b/kernel/trace/rv/monitors/nomiss/nomiss.c
> index 31f90f3638d8..6b3f93866d56 100644
> --- a/kernel/trace/rv/monitors/nomiss/nomiss.c
> +++ b/kernel/trace/rv/monitors/nomiss/nomiss.c
> @@ -57,24 +57,12 @@ static inline bool ha_verify_invariants(struct ha_monitor
> *ha_mon,
>  					enum states next_state, u64 time_ns)
>  {
>  	if (curr_state == ready_nomiss)
> -		return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
> +		return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns,
> DEADLINE_NS(ha_mon));
>  	else if (curr_state == running_nomiss)
> -		return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
> +		return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns,
> DEADLINE_NS(ha_mon));
>  	return true;
>  }
>  
> -static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
> -					enum states curr_state, enum events
> event,
> -					enum states next_state, u64 time_ns)
> -{
> -	if (curr_state == next_state)
> -		return;
> -	if (curr_state == ready_nomiss)
> -		ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon),
> time_ns);
> -	else if (curr_state == running_nomiss)
> -		ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon),
> time_ns);
> -}
> -
>  static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
>  				    enum states curr_state, enum events
> event,
>  				    enum states next_state, u64 time_ns)
> @@ -122,8 +110,6 @@ static bool ha_verify_constraint(struct ha_monitor
> *ha_mon,
>  	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state,
> time_ns))
>  		return false;
>  
> -	ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns);
> -
>  	if (!ha_verify_guards(ha_mon, curr_state, event, next_state,
> time_ns))
>  		return false;
>  
> diff --git a/kernel/trace/rv/monitors/stall/stall.c
> b/kernel/trace/rv/monitors/stall/stall.c
> index 9ccfda6b0e73..1aa65d7e690d 100644
> --- a/kernel/trace/rv/monitors/stall/stall.c
> +++ b/kernel/trace/rv/monitors/stall/stall.c
> @@ -38,7 +38,7 @@ static inline bool ha_verify_invariants(struct ha_monitor
> *ha_mon,
>  					enum states next_state, u64 time_ns)
>  {
>  	if (curr_state == enqueued_stall)
> -		return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns);
> +		return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns,
> threshold_jiffies);
>  	return true;
>  }
>  


  reply	other threads:[~2026-05-06  9:15 UTC|newest]

Thread overview: 18+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2026-05-05  6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
2026-05-05  6:59 ` [PATCH 01/13] verification/rvgen: Switch LTL parser " Nam Cao
2026-05-06  7:37   ` Gabriele Monaco
2026-05-05  6:59 ` [PATCH 02/13] verification/rvgen: Introduce a parse tree for automata using Lark Nam Cao
2026-05-05  6:59 ` [PATCH 03/13] verification/rvgen: Implement state and transition parser based on Lark Nam Cao
2026-05-06 14:48   ` Gabriele Monaco
2026-05-05  6:59 ` [PATCH 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark Nam Cao
2026-05-05  6:59 ` [PATCH 05/13] verification/rvgen: Convert __fill_setup_invariants_func() " Nam Cao
2026-05-05  6:59 ` [PATCH 06/13] verification/rvgen: Convert __fill_verify_guards_func() " Nam Cao
2026-05-06 14:51   ` Gabriele Monaco
2026-05-05  6:59 ` [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables Nam Cao
2026-05-06  9:15   ` Gabriele Monaco [this message]
2026-05-05  6:59 ` [PATCH 08/13] verification/rvgen: Simplify the generation for " Nam Cao
2026-05-05  6:59 ` [PATCH 09/13] verification/rvgen: Delete __parse_constraint() Nam Cao
2026-05-05  6:59 ` [PATCH 10/13] verification/rvgen: Switch __get_event_variables() to Lark Nam Cao
2026-05-05  6:59 ` [PATCH 11/13] verification/rvgen: Switch __create_matrix() " Nam Cao
2026-05-05  6:59 ` [PATCH 12/13] verification/rvgen: Remove the old state variables Nam Cao
2026-05-05  6:59 ` [PATCH 13/13] verification/rvgen: Remove dead code Nam Cao

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=967f1cd8cd6e27aaa65d68194487306bc312caa0.camel@redhat.com \
    --to=gmonaco@redhat.com \
    --cc=linux-kernel@vger.kernel.org \
    --cc=linux-trace-kernel@vger.kernel.org \
    --cc=namcao@linutronix.de \
    --cc=rostedt@goodmis.org \
    --cc=wander@redhat.com \
    /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