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 <[email protected]> > --- > 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
