Re: [PATCH v2 10/20] rv: Add Hybrid Automata monitor type

[Nam Cao <namcao@linutronix.de>]

Gabriele Monaco <gmonaco@redhat.com> writes:
> diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
> new file mode 100644
> index 000000000000..fb885709b727
> --- /dev/null
> +++ b/include/rv/ha_monitor.h
> @@ -0,0 +1,469 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Copyright (C) 2025-2028 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com>
> + *
> + * Hybrid automata (HA) monitor functions, to be used together
> + * with automata models in C generated by the dot2k tool.
> + *
> + * This type of monitors extends the Deterministic automata (DA) class by
> + * adding a set of environment variables (e.g. clocks) that can be used to
> + * constraint the valid transitions.
> + *
> + * The dot2k tool is available at tools/verification/dot2k/
                                     ^^^^^^^^^^^^^^^^^^^^^^^^^
                                     non-existent
> +/*
> + * ktime_get_ns is expensive, since we usually don't require precise accounting
> + * of changes within the same event, cache the current time at the beginning of
> + * the constraint handler and use the cache for subsequent calls.
> + * Monitors without ns clocks automatically skip this.
> + */
> +#ifdef HA_CLK_NS
> +#define ha_update_ns_cache() ktime_get_ns()
> +#else
> +#define ha_update_ns_cache() 0
> +#endif /* HA_CLK_NS */

ha_update_ns_cache() itself does not cache, its caller does. So I think
it is misleading to name this "cache".

Why is "update" in the name? Isn't something like ha_get_ns() betters
describe this macro?

> +/*
> + * 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

Why does guard representation store the last reset?

For example, what if I specifiy the guard as "clk > 500ns". Shouldn't
the guard representation be "500ns"?

> +static inline u64 ha_get_passed_ns(struct ha_monitor *ha_mon, enum envs env,
> +				   u64 expire, 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);

The function is named *get*() which indicates that it only reads. But it
also writes.

> +/*
> + * Retrieve the last reset time (guard representation) from the invariant
> + * representation (expiration).
> + * It the caller's responsibility to make sure the storage was actually in the
> + * invariant representation (e.g. the current state has an invariant).
> + * The provided value must be the same used when starting the invariant.
> + *
> + * This function's access to the storage is NOT atomic, due to the rarity when
> + * this is used. If a monitor allows writes concurrent to this, likely
> + * other things are broken and need rethinking the model or additional locking.

Does atomic_sub() solves your "NOT atomic" problem?

> +static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
> +					u64 expire, u64 time_ns)
> +{
> +	u64 passed = ha_get_passed_jiffy(ha_mon, env, expire, time_ns);
> +
> +	mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
> +}

I don't understand this "passed" thing. I see this function being called
in ha_setup_invariants() of stall monitor. Stall monitor is validating
that the task does not stay in "enqueued" state for more than
"threshold_jiffies". If so, what is the purpose of "passed"? From my
understanding, it should be just 

static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
					u64 expire, u64 time_ns)
{
	mod_timer(&ha_mon->timer, get_jiffies_64() + expire);
}

what do I miss?

Nam