Re: [PATCH v2 13/22] rv: Add support for LTL monitors
From: Gabriele Monaco
Date: Tue Apr 15 2025 - 09:22:31 EST
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@xxxxxxxxxxxxx>
> ---
> 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