Re: [PATCH v2 13/20] Documentation/rv: Add documentation about hybrid automata

[Gabriele Monaco <gmonaco@redhat.com>]

On Fri, 2025-10-10 at 15:46 +0200, Nam Cao wrote:
> Gabriele Monaco <gmonaco@redhat.com> writes:
> > Describe theory and implementation of hybrid automata in the dedicated
> > page hybrid_automata.rst
> > Include a section on how to integrate a hybrid automaton in
> > monitor_synthesis.rst
> > Also remove a hanging $ in deterministic_automata.rst
> > 
> > Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
> > ---
> This brings back bad memories from university..

:')

> > +It is important to note that any valid hybrid automaton is a valid
> > +deterministic automaton
> 
> Perhaps remove the double "valid". Usually people use the phrase "any
> valid A is a valid B" to say that B is a superset of A, but it is
> opposite here.

Alright, will do.

> > +This is a combination of both iterations of the stall example::
> > +
> > +  /* enum representation of X (set of states) to be used as index */
> > +  enum states {
> > +	dequeued = 0,
> 
> I think you already removed this " = 0" in an earlier patch?

Right, missed that.

> > +	/* Validate invariants in i */
> > +    if (next_state == curr_state || !res)
>    ^^^^
>    indentation error ;)

Good catch.

> > +Due to the complex nature of environment variables, the user needs to
> > provide
> > +functions to get and reset environment variables, although we provide some
> > +helpers for common types (e.g. clocks with ns or jiffy granularity).
> 
> Is there theoretical reason that functions to get/set variables cannot
> be generated? Or you just do not have time for it yet?

Not theoretical but practical, the monitor cannot always define /what/ an
environment variable is. In case of clocks (jiffy and ns) that's easy and the
parser does in fact generate get and reset functions, the user only needs to
specify the measure unit as explained somewhere else.

It is possible to add more exotic variables that don't follow common clock rules
and need different get/reset definitions. Now, in practice, that may not happen
with clocks (I cannot think of an alternative clock definition), but can happen
for other variables. For instance if the variable describes the preempt count,
the model cannot know in advance and the user will need to supply how to read
that in the kernel (just like we do with tracepoints, although event names
/might/ hint something).

As I get it, this isn't so clear so I should probably try and reword it.

I might just assume variables without unit but with a reset are, say, jiffy
clocks and never expect manual definition of the reset function, but that might
be misleading at times: e.g. if a user wants a ns clock but forgets the unit,
the monitor would still build.

> 
> > +Since invariants are only defined as clock expirations (e.g. *clk <
> > +threshold*), the callback for timers armed when entering the state is in
> > fact a
> > +failure in the model and triggers a reaction. Leaving the state stops the
> > timer
> > +and checks for its expiration, in case the callback was late.
> 
> "callback for timers armed when entering the state is in fact a failure
> in the model and triggers a reaction." - I have problem parsing this
> sentence. How can "callback for timers" be armed? Or do you mean arming
> timers while entering a state is a failure in the model? What is it a failure?

Right, that sentence doesn't make sense.
We arm a timer when entering the state, expiration of such timer is a failure.
The timer is cancelled when leaving the state, so in fact leaving the state
before the timer expiration is the only valid behaviour.

> > +It is important to note that timers introduce overhead, if the monitor has
> > +several instances (e.g. all tasks) this can become an issue.
> > +If the monitor is guaranteed to *eventually* leave the state and the
> > incurred
> > +delay to wait for the next event is acceptable, guards can be use to lower
> > the
> > +monitor's overhead.
> 
> How about having some sort of a "background task" which periodically
> verifies the invariants?

I didn't update this part, but now timers can work also via timer wheel, which
is cutting down costs by sacrificing some reactivity (not correctness though). I
assume the background thread would be quite similar to what the timer wheel
already does.

But I definitely need to mention this because the timer wheel is not as heavy as
the hrtimers and its overhead is usually acceptable (unless proven otherwise for
a specific monitor/workload, I'd say).

> > +This is the full example of the last version of the 'stall' model in DOT::
> > +
> > +  digraph state_automaton {
> > +      {node [shape = circle] "enqueued"};
> > +      {node [shape = plaintext, style=invis, label=""] "__init_dequeued"};
> > +      {node [shape = doublecircle] "dequeued"};
> > +      {node [shape = circle] "running"};
> > +      "__init_dequeued" -> "dequeued";
> > +      "enqueued" [label = "enqueued\nclk < threshold_jiffies"];
> > +      "running" [label = "running"];
> > +      "dequeued" [label = "dequeued"];
> > +      "enqueued" -> "running" [ label = "switch_in" ];
> > +      "running" -> "dequeued" [ label = "dequeue" ];
> > +      "dequeued" -> "enqueued" [ label = "enqueue;reset(clk)" ];
> > +      { rank = min ;
> > +          "__init_dequeued";
> > +          "dequeued";
> > +      }
> 
> Btw, the last block (rank = min) doesn't seem to serve any purpose. But
> the last time I checked months ago, the parser explodes if it is
> removed, not sure if it still does now. But this is another reason that
> I would like a rewrite.

Mmh, that's automatically generated by Supremica and, I believe, in some models
it's tuning a bit the position of nodes. Quite strange that the parser exploded,
those lines should be completely ignored.. Still, we know the parser needs this
big refactor.

Thanks,
Gabriele