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
> ...
>  
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index c7c18c06911b..c8320fa3a94b 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -10,6 +10,10 @@
>  #define MAX_DA_NAME_LEN	32
>  
>  #ifdef CONFIG_RV
> +#include <linux/bitops.h>
> +#include <linux/types.h>
> +#include <linux/array_size.h>
> +
>  /*
>   * Deterministic automaton per-object variables.
>   */
> @@ -18,6 +22,52 @@ struct da_monitor {
>  	unsigned int	curr_state;
>  };
>  
> +/*
> + * In the future, if the number of atomic propositions or the size
> of Buchi automaton is larger, we
> + * can switch to dynamic allocation. For now, the code is simpler
> this way.
> + */
> +#define RV_MAX_LTL_ATOM 32
> +#define RV_MAX_BA_STATES 32
> +
> +/**
> + * struct ltl_monitor - A linear temporal logic runtime verification
> monitor
> + * @states:	States in the Buchi automaton. As Buchi automaton is
> a
> + *		non-deterministic state machine, the monitor can be
> in multiple states
> + *		simultaneously. This is a bitmask of all possible
> states.
> + *		If this is zero, that means either:
> + *		    - The monitor has not started yet (e.g. because
> not all atomic propositions are
> + *		      known).
> + *		    - there is no possible state to be in. In other
> words, a violation of the
> + *		      LTL property is detected.
> + * @atoms:	The values of atomic propositions.
> + * @unknown_atoms: Atomic propositions which are still unknown.
> + */
> +struct ltl_monitor {
> +#ifdef CONFIG_RV_LTL_MONITOR
> +	DECLARE_BITMAP(states, RV_MAX_BA_STATES);
> +	DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
> +	DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
> +#endif
> +};

Mmh, we have a lot of those ifdefs in quite inappropriate places, but I
think we can do better than this.

What about something like:

#ifdef CONFIG_RV_LTL_MONITOR

struct ltl_monitor {
	DECLARE_BITMAP(states, RV_MAX_BA_STATES);
	DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
	DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
};

static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
{
	...
}

static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
{
	...
}

#else

/*
 * Leave the struct empty not to use up space
 * In a later patch we could do the same for DAs..
 */
struct ltl_monitor { };

#endif

> +
> +static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
> +{
> +	for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
> +		if (mon->states[i])
> +			return true;
> +	}
> +	return false;
> +}
> +
> +static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
> +{
> +	for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) {
> +		if (mon->unknown_atoms[i])
> +			return false;
> +	}
> +	return true;
> +}
> +
>  /*
>   * Per-task RV monitors count. Nowadays fixed in
> RV_PER_TASK_MONITORS.
>   * If we find justification for more monitors, we can think about
> @@ -27,11 +77,9 @@ struct da_monitor {
>  #define RV_PER_TASK_MONITORS		1
>  #define RV_PER_TASK_MONITOR_INIT	(RV_PER_TASK_MONITORS)
>  
> -/*
> - * Futher monitor types are expected, so make this a union.
> - */
>  union rv_task_monitor {
> -	struct da_monitor da_mon;
> +	struct da_monitor	da_mon;
> +	struct ltl_monitor	ltl_mon;
>  };
>  
>  #ifdef CONFIG_RV_REACTORS
> diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
> new file mode 100644
> index 000000000000..78f5a1197665
> --- /dev/null
> +++ b/include/rv/ltl_monitor.h

You hate macros don't you? :)
Anyway I really like your approach, very neat.

> @@ -0,0 +1,184 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/**
> + * This file must be combined with the $(MODEL_NAME).h file
> generated by
> + * tools/verification/rvgen.
> + */
> +
> +#include <linux/args.h>
> +#include <linux/rv.h>
> +#include <linux/stringify.h>
> +#include <linux/seq_buf.h>
> +#include <rv/instrumentation.h>
> +#include <trace/events/task.h>
> +#include <trace/events/sched.h>
> +
> +#ifndef MONITOR_NAME
> +#error "MONITOR_NAME macro is not defined. Did you include
> $(MODEL_NAME).h generated by rvgen?"
> +#endif
> +
> +#ifdef CONFIG_RV_REACTORS
> +#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
> +static struct rv_monitor RV_MONITOR_NAME;
> +
> +static void rv_cond_react(struct task_struct *task)
> +{
> +	if (!rv_reacting_on() || !RV_MONITOR_NAME.react)
> +		return;
> +	RV_MONITOR_NAME.react("rv: "__stringify(MONITOR_NAME)":
> %s[%d]: violation detected\n",
> +			      task->comm, task->pid);
> +}
> +#else
> +static void rv_cond_react(struct task_struct *task)
> +{
> +}
> +#endif
> +
> +static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
> +
> +static void ltl_atoms_fetch(struct task_struct *task, struct
> ltl_monitor *mon);
> +static void ltl_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon, bool task_creation);
> +
> +static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
> +{
> +	return &task->rv[ltl_monitor_slot].ltl_mon;
> +}

This means ltl monitors only support per-task, right?
It shouldn't take much effort putting an ifdef chain here and defining e.g.
PER_CPU in the header file to choose a different get_monitor.
Or directly an ltl_monitor_implicit.h

I think this patch is ready without it, just trying to brainstorm how we could
potentially extend this.

I need more time to play with these, but it looks promising.

Thanks,
Gabriele