Re: [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables

[Gabriele Monaco <gmonaco@redhat.com>]

On Mon, 2026-05-11 at 13:55 +0200, Nam Cao wrote:
> Gabriele Monaco <gmonaco@redhat.com> writes:
> > Well, this is roughly what we discussed in [1].
> > Now, I didn't submit the throttle monitor yet because it depends on unacked
> > tracepoints.
> 
> Thanks for bringing that up. I had no memory of that discussion.
> 
> > 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.
> 
> I believe you are referring to this:
> 
>                                      |
>                                      |
>       dl_replenish;reset(clk)        v
>               sched_switch_in   #=========================# sched_switch_in;
>                +--------------- H                         H   reset(clk)
>                |                H                         H <----------------+
>                +--------------> H         running         H                  |
>     dl_throttle;reset(clk)      H clk < runtime_left_ns() H                  |
>    +--------------------------- H                         H sched_switch_out |
>    |       +------------------> H                         H -------------+   |
>    | dl_replenish;reset(clk)    #=========================#              |   |
>    |       |                         |             ^                     |   |
>    v       |                  dl_defer_arm         |                     |   |
> 
> Now that I stared at this again, I think we already deviate from theory
> here. Our documentation mentions that the invariant must be in the form
> 
>         g = v < c | true
> 
> with "c [being] a numerical value".
> 
> The invariant "clk < runtime_left_ns()" means clk must not exceed the
> remaining runtime, which is sampled by calling runtime_left_ns() when
> the state is entered. This is not in the theory. Additionally, I think
> this interpretation is ambiguous; one could also interpret that as "the
> clk value must never exceed the *current* value returned by
> runtime_left_ns()".

Well, that's a fair point. Using functions here is kind of pushing it, but if we
assume the runtime constant for the duration of the invariant (which is what
happens in practice), I don't see that huge difference. Then sure, I'm still
twisting the theory here.

But that's right, it's quite ambiguous. The function is technically syntactic
sugar in RV to allow monitor-specific values, I should probably make it clear it
doesn't make it a dynamic value (at least within the same constraint
validation).

> I digged into the cited academic papers, but couldn't find anything that
> can describe this. The closest I see is the "init" label for states, but
> that is the condition for entering the states.
> 
> > 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.
> 
> That can work, but not ideal, because hrtimer will not be usable.

Why not? If we have HA_TIMER_WHEEL , we'd use timer and expire, if we have
HA_TIMER_HRTIMER we'd only need hrtimer with it's hrtimer_get_expires():

 union {
 struct hrtimer hrtimer;
 struct {
 struct timer_list timer;
 u64 expire; /* Explicitly store the armed budget */
 };

we already can't use timer and hrtimer interchangeably.
What am I missing here?

> Looking at the throttle monitor again, is it possible to rewrite
> runtime_left_ns() to read .dl_runtime instead of .runtime? I don't know
> the deadline schedule very well, but I think .dl_runtime is not changing
> like .runtime?

In theory yes, but since the runtime is consumed only when running, we cannot
just set the timeout once. We either save how much was consumed somewhere or do
some start/pause mechanism.
Neither looks simpler to me.

Thanks,
Gabriele