Re: [PATCH v2 13/22] rv: Add support for LTL monitors

[Gabriele Monaco <gmonaco@redhat.com>]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> While attempting to implement DA monitors for some complex
> specifications,
> deterministic automaton is found to be inappropriate as the
> specification
> language. The automaton is complicated, hard to understand, and
> error-prone.
> 
> For these cases, linear temporal logic is more suitable as the
> specification language.
> 
> Add support for linear temporal logic runtime verification monitor.
> 
> For all the details, see the documentations added by this commit.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
>  Documentation/trace/rv/index.rst              |   1 +
>  .../trace/rv/linear_temporal_logic.rst        |  97 +++
>  Documentation/trace/rv/monitor_synthesis.rst  | 141 ++++-
>  include/linux/rv.h                            |  56 +-
>  include/rv/ltl_monitor.h                      | 184 ++++++
>  kernel/fork.c                                 |   5 +-
>  kernel/trace/rv/Kconfig                       |   7 +
>  kernel/trace/rv/rv_trace.h                    |  47 ++
>  tools/verification/rvgen/.gitignore           |   3 +
>  tools/verification/rvgen/Makefile             |   2 +
>  tools/verification/rvgen/__main__.py          |   3 +-
>  tools/verification/rvgen/rvgen/ltl2ba.py      | 552
> ++++++++++++++++++
>  tools/verification/rvgen/rvgen/ltl2k.py       | 242 ++++++++
>  .../verification/rvgen/templates/ltl2k/main.c | 102 ++++
>  .../rvgen/templates/ltl2k/trace.h             |  14 +
>  15 files changed, 1431 insertions(+), 25 deletions(-)
>  create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
>  create mode 100644 include/rv/ltl_monitor.h
>  create mode 100644 tools/verification/rvgen/.gitignore
>  create mode 100644 tools/verification/rvgen/rvgen/ltl2ba.py
>  create mode 100644 tools/verification/rvgen/rvgen/ltl2k.py
>  create mode 100644 tools/verification/rvgen/templates/ltl2k/main.c
>  create mode 100644 tools/verification/rvgen/templates/ltl2k/trace.h
> 
> diff --git a/Documentation/trace/rv/index.rst
> b/Documentation/trace/rv/index.rst
> index 8e411b76ec82..2a27f6bc9429 100644
> --- a/Documentation/trace/rv/index.rst
> +++ b/Documentation/trace/rv/index.rst
> @@ -8,6 +8,7 @@ Runtime Verification
>  
>     runtime-verification.rst
>     deterministic_automata.rst
> +   linear_temporal_logic.rst
>     monitor_synthesis.rst
>     da_monitor_instrumentation.rst
>     monitor_wip.rst
> diff --git a/Documentation/trace/rv/linear_temporal_logic.rst
> b/Documentation/trace/rv/linear_temporal_logic.rst
> new file mode 100644
> index 000000000000..68574370eec3
> --- /dev/null
> +++ b/Documentation/trace/rv/linear_temporal_logic.rst
> @@ -0,0 +1,97 @@
> +Introduction
> +============
> +
> +Runtime verification monitor is a verification technique which
> checks that the kernel follows a
> +specification. It does so by using tracepoints to monitor the
> kernel's execution trace, and
> +verifying that the execution trace sastifies the specification.
> +
> +Initially, the specification can only be written in the form of
> deterministic automaton (DA).
> +However, while attempting to implement DA monitors for some complex
> specifications, deterministic
> +automaton is found to be inappropriate as the specification
> language. The automaton is complicated,
> +hard to understand, and error-prone.
> +
> +Thus, RV monitors based on linear temporal logic (LTL) are
> introduced. This type of monitor uses LTL
> +as specification instead of DA. For some cases, writing the
> specification as LTL is more concise and
> +intuitive.
> +
> +Documents regarding LTL are widely available on the internet, this
> document will not go into
> +details.
> +
> +Grammar
> +========
> +
> +Unlike some existing syntax, kernel's implementation of LTL is more
> verbose. This is motivated by
> +considering that the people who read the LTL specifications may not
> be well-versed in LTL.
> +
> +Grammar:
> +    ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
> +
> +Operands (opd):
> +    true, false, user-defined names consisting of upper-case
> characters, digits, and underscore.
> +
> +Unary Operators (unop):
> +    always
> +    eventually
> +    not
> +
> +Binary Operators (binop):
> +    until
> +    and
> +    or
> +    imply
> +    equivalent
> +
> +This grammar is ambiguous: operator precedence is not defined.
> Parentheses must be used.
> +
> +Example linear temporal logic
> +=============================
> +.. code-block::
> +
> +   RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA)
> +
> +means: if it is raining, going outside means having an umbrella.
> +
> +.. code-block::
> +
> +   RAIN imply (WET until not RAIN)
> +
> +means: if it is raining, it is going to be wet until the rain stops.
> +
> +.. code-block::
> +
> +   RAIN imply eventually not RAIN
> +
> +means: if it is raining, rain will eventually stop.
> +
> +The above examples are referring to the current time instance only.
> For kernel verification, the
> +`always` operator is usually desirable, to specify that something is
> always true at the present and
> +for all future. For example::
> +
> +    always (RAIN imply eventually not RAIN)
> +
> +means: *all* rain eventually stops.
> +
> +In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and
> `WET` are the "atomic
> +propositions".
> +
> +Monitor synthesis
> +=================
> +
> +To synthesize an LTL into a kernel monitor, the `rvgen` tool can be
> used:
> +`tools/verification/rvgen`. The specification needs to be provided
> as a file, and it must have a
> +"RULE = LTL" assignment. For example::
> +
> +    RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until
> RELEASE))
> +
> +which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED`
> or `CRASHED`.
> +
> +The LTL can be broken down using sub-expressions. The above is
> equivalent to:
> +
> +   .. code-block::
> +
> +    RULE = always (ACQUIRE imply (ALIVE until RELEASE))
> +    ALIVE = not KILLED and not CRASHED
> +
> +From this specification, `rvgen` generates the C implementation of a
> Buchi automaton - a
> +non-deterministic state machine which checks the satisfiability of
> the LTL. See
> +Documentation/trace/rv/monitor_synthesis.rst for details on using
> `rvgen`.

You probably read a lot to write this, do you mind adding a brief
Reference section for the curious reader? Asking for a friend ;)

Something like
https://docs.kernel.org/trace/rv/deterministic_automata.html#references
would do.

Thanks,
Gabriele