Message-ID: <a85dcc1c6b493838abdc8716ae35fe4ad734db2b.camel@redhat.com>
Date: Wed, 16 Apr 2025 16:29:53 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Nam Cao <namcao@...utronix.de>, Steven Rostedt <rostedt@...dmis.org>, 
	linux-trace-kernel@...r.kernel.org, linux-kernel@...r.kernel.org
Cc: john.ogness@...utronix.de
Subject: Re: [PATCH v3 13/22] rv: Add support for LTL monitors

On Wed, 2025-04-16 at 08:51 +0200, Nam Cao wrote:
> diff --git a/Documentation/trace/rv/linear_temporal_logic.rst
> b/Documentation/trace/rv/linear_temporal_logic.rst
> new file mode 100644
> index 000000000000..232f9700cbaa
> --- /dev/null
> +++ b/Documentation/trace/rv/linear_temporal_logic.rst
> @@ -0,0 +1,119 @@
> +Introduction
> +============
> +

Just noticed you misplaced the sections in this file, it should be like:

Linear Temporal Logic
=====================

Introduction
------------

[...]

Grammar
-------

[...]

Example linear temporal logic
-----------------------------

[...]

E.g. use === only for the page's title (which is missing) and --- for
the sections, otherwise you get it oddly integrated in the index.

Thanks,
Gabriele

> +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.
> +
> +Many materials explain LTL in details. One book is::
> +
> +  Christel Baier aund Joost-Pieter Katoen: Principles of Model
> Checking, The MIT Press, 2008.
> +
> +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`.
> +
> +References
> +==========
> +
> +One book covering model checking and linear temporal logic is::
> +
> +  Christel Baier aund Joost-Pieter Katoen: Principles of Model
> Checking, The MIT Press, 2008.
> +
> +For an example of using linear temporal logic in software testing,
> see::
> +
> +  Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik
> Roychoudhury. 2022. Linear-time
> +  temporal logic guided greybox fuzzing. In Proceedings of the 44th
> International Conference on
> +  Software Engineering (ICSE '22). Association for Computing
> Machinery, New York, NY, USA,
> +  1343–1355. https://doi.org/10.1145/3510003.3510082
> +
> +The kernel's LTL monitor implementation is based on::
> +
> +  Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-
> the-fly Automatic Verification of
> +  Linear Temporal Logic. In: Dembiński, P., Średniawa, M. (eds)
> Protocol Specification, Testing and
> +  Verification XV. PSTV 1995. IFIP Advances in Information and
> Communication Technology. Springer,
> +  Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_1

Powered by blists - more mailing lists