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

[Nam Cao <namcao@linutronix.de>]

Gabriele Monaco <gmonaco@redhat.com> writes:
> Alright, this is the simplest way I could think to represent clocks, still it
> seems confusing.
>
> Let's start from guards (invariants are not special but I'm trying to do
> something to keep precision), the value of a clock is the time that passed since
> the last reset, as that's when the value is set to 0. Storing that timestamp and
> just comparing the difference whenever you need to know the valuation of said
> clock seemed the most straightforward thing to me. The clock representation
> doesn't include the guard constraint, that is validated during the event using
> the current valuation (i.e. now - reset_time).
>
> What is important to note is that, at time of reset, you don't know what guard
> is going to fire, you may as well have a state with event A asking for clk<10
> and event B requiring clk<20, also the guard may be in a later state and may
> depend on the path.
>
> Invariants are bound to the form clk < N, and get "armed" when we reach the
> state, from there we know exactly when the invariant is going to expire, so we
> can save that (very important when using the timer wheel). Note here that the
> expiration isn't exactly N from now, but it's the valuation of the clock (reset
> might have occurred a few states earlier, see the nomiss case) subtracted by N,
> this is what the "passed" means later.
>
> That said, I couldn't think of a simpler implementation but any suggestion is
> welcome, of course.

Ok, now things start to make sense. Thanks for the explanation.

At least to me, using the same variable to store different time values
is a bit confusing.

Is it possible that we always store the timestamp of the last clock reset?

The invariant bound value (N) is fixed for each state, so we can have
the bound value in ha_verify_invariants() instead. For example, the
Python script can generate something like

static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
                                       enum states curr_state, enum events event,
                                       enum states next_state, u64 time_ns)
{
       if (curr_state == enqueued_stall)
               return ha_check_invariant_jiffy(ha_mon, threshold_jiffies, time_ns);
       return true;
}

Is that possible?

> Kinda, it would solve the problem for this specific subtraction, but racing
> handlers could still lead to problems although the subtraction is "correct".
>
> Since this is the only time the env storage needs to be an atomic_t and it's
> fairly rare (only complicated models require calling this function at all,
> others are happy with READ_ONCE/WRITE_ONCE) I didn't want to change the storage
> implementation for some perceived safety.
>
> I wrote that comment exactly to motivate why we aren't using atomic_t, but I
> should probably reword that. Does this make sense to you?

I think if we always store the timestamp since last reset, we can get
rid of this function. Let's see how that discussion go..

> As mentioned before, this is true for the stall case, where the reset occurred
> when reaching the state with the invariant (passed is close to 0), if you look
> at the nomiss case, reset happens before being ready (its invariant would have
> passed close to 0), but the same invariant is enforced in running, here we will
> see a passed far from 0 and need to take that into account when setting the
> invariant.

Make sense, thanks!

Nam