rv: Simplify hybrid automata monitors's clock variables

Browse source

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.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/c0f600dcbf3d8b487c944406851a39146f4d91fa.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

...

This commit is contained in:

Nam Cao 2026-06-19 07:52:10 +02:00 • committed by Gabriele Monaco

parent e0235729b0

commit ab2900ae25

3 changed files with 19 additions and 65 deletions

Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL

Download patch file Download diff file Expand all files Collapse all files

64

include/rv/ha_monitor.h

View file

18

kernel/trace/rv/monitors/nomiss/nomiss.c

View file

2

kernel/trace/rv/monitors/stall/stall.c

View file