Re: [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor
From: Gabriele Monaco
Date: Wed Mar 12 2025 - 02:48:07 EST
On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> Prepare the infrastructure for linear temporal logic monitors:
>
> - add scripts for generating the monitors
> - implement data structures
>
> For details, see:
> Documentation/trace/rv/linear_temporal_logic.rst
>
> Signed-off-by: Nam Cao <namcao@xxxxxxxxxxxxx>
> ---
Thanks for this. It's great to have a new type of monitor!
I'll play with this a bit more, but please see my initial comments.
> .../trace/rv/linear_temporal_logic.rst | 73 +++
> include/linux/rv.h | 26 +-
> kernel/fork.c | 5 +-
> tools/verification/ltl2ba/.gitignore | 3 +
> tools/verification/ltl2ba/generate.py | 154 +++++
> tools/verification/ltl2ba/ltl.py | 556
> ++++++++++++++++++
> tools/verification/ltl2ba/template.c | 131 +++++
> tools/verification/ltl2ba/template.h | 157 +++++
> 8 files changed, 1097 insertions(+), 8 deletions(-)
> create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
> create mode 100644 tools/verification/ltl2ba/.gitignore
> create mode 100755 tools/verification/ltl2ba/generate.py
> create mode 100644 tools/verification/ltl2ba/ltl.py
> create mode 100644 tools/verification/ltl2ba/template.c
> create mode 100644 tools/verification/ltl2ba/template.h
>
> diff --git a/Documentation/trace/rv/linear_temporal_logic.rst
> b/Documentation/trace/rv/linear_temporal_logic.rst
> new file mode 100644
> index 000000000000..9b0ce6a143ec
> --- /dev/null
> +++ b/Documentation/trace/rv/linear_temporal_logic.rst
> [...]
>
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 5482651ed020..6de4f93b390e 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -10,6 +10,8 @@
> #define MAX_DA_NAME_LEN 24
>
> #ifdef CONFIG_RV
> +#include <linux/types.h>
> +
> /*
> * Deterministic automaton per-object variables.
> */
> @@ -18,6 +20,24 @@ struct da_monitor {
> unsigned int curr_state;
> };
>
> +enum ltl_truth_value {
> + LTL_FALSE,
> + LTL_TRUE,
> + LTL_UNDETERMINED,
> +};
> +
> +/*
> + * In the future, if the number of atomic propositions or the custom
> data size is larger, we can
> + * switch to dynamic allocation. For now, the code is simpler this
> way.
> + */
> +#define RV_MAX_LTL_ATOM 10
> +#define RV_MAX_DATA_SIZE 16
> +struct ltl_monitor {
> + unsigned int state;
> + enum ltl_truth_value atoms[RV_MAX_LTL_ATOM];
> + u8 data[RV_MAX_DATA_SIZE];
> +};
> +
> /*
> * 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 +47,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;
> };
This adds quite some memory overhead if we have multiple per-task
monitors (we might in the future) and we don't use this ltl monitors.
What about keeping it conditionally compiled out?
You could define the struct only if e.g. CONFIG_RV_LTL_MONITORS is set,
select it with any LTL monitor via Kconfig, then glue it somehow to
have it readable.
>
> #ifdef CONFIG_RV_REACTORS
> diff --git a/kernel/fork.c b/kernel/fork.c
> index 735405a9c5f3..5d6c1caca702 100644
> --- a/kernel/fork.c
> +++ b/kernel/fork.c
> @@ -2127,10 +2127,7 @@ static void copy_oom_score_adj(u64
> clone_flags, struct task_struct *tsk)
> #ifdef CONFIG_RV
> static void rv_task_fork(struct task_struct *p)
> {
> - int i;
> -
> - for (i = 0; i < RV_PER_TASK_MONITORS; i++)
> - p->rv[i].da_mon.monitoring = false;
> + memset(p->rv, 0, sizeof(p->rv));
> }
> #else
> #define rv_task_fork(p) do {} while (0)
> diff --git a/tools/verification/ltl2ba/.gitignore
> b/tools/verification/ltl2ba/.gitignore
> new file mode 100644
> index 000000000000..9c47b9724860
> --- /dev/null
> +++ b/tools/verification/ltl2ba/.gitignore
> @@ -0,0 +1,3 @@
> +__pycache__/
> +parsetab.py
> +parser.out
> diff --git a/tools/verification/ltl2ba/generate.py
> b/tools/verification/ltl2ba/generate.py
> new file mode 100755
> index 000000000000..52d5b3618e64
> --- /dev/null
> +++ b/tools/verification/ltl2ba/generate.py
You may want to rename this script to something more unique, just in
case one day we decide to make it possible to install this generator on
the system (like dot2k/dot2c).
>
> diff --git a/tools/verification/ltl2ba/ltl.py
> b/tools/verification/ltl2ba/ltl.py
> new file mode 100644
> index 000000000000..aa3a11d78a8e
> --- /dev/null
> +++ b/tools/verification/ltl2ba/ltl.py
>
> diff --git a/tools/verification/ltl2ba/template.c
> b/tools/verification/ltl2ba/template.c
> new file mode 100644
> index 000000000000..31c5a209d71d
> --- /dev/null
> +++ b/tools/verification/ltl2ba/template.c
> diff --git a/tools/verification/ltl2ba/template.h
> b/tools/verification/ltl2ba/template.h
> new file mode 100644
> index 000000000000..65d342891e70
> --- /dev/null
> +++ b/tools/verification/ltl2ba/template.h
> @@ -0,0 +1,157 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * This file is generated, do not edit.
> + *
> + * This file includes necessary functions to glue the Buchi
> automaton and the kernel together.
> + * Some of these functions must be manually implemented (look for
> "Must be implemented", or just
> + * let the compiler tells you).
> + *
> + * Essentially, you need to manually define the meaning of the
> atomic propositions in the LTL
> + * property. The primary function for that is
> rv_%%MODEL_NAME%%_atom_update(), which can be called
> + * in tracepoints' handlers for example. In some specific cases
> where
> + * rv_%%MODEL_NAME%%_atom_update() is not convenient,
> rv_%%MODEL_NAME%%_atoms_fetch() can be used.
> + *
> + * rv_%%MODEL_NAME%%_init()/rv_%%MODEL_NAME%%_destroy() must be
> called while enabling/disabling
> + * the monitor.
> + *
> + * If the fields in struct ltl_monitor is not enough, extra custom
> data can be used. See
> + * rv_%%MODEL_NAME%%_get_data().
> + */
> +
> +#include <linux/sched.h>
> +
> +enum %%MODEL_NAME%%_atom {
> +%%ATOM_LIST%%
> + NUM_ATOM
> +};
> +
> +/**
> + * rv_%%MODEL_NAME%%_init
> + * @data_size: required custom data size, can be zero
> + *
> + * Must be called while enabling the monitor
> + */
> +int rv_%%MODEL_NAME%%_init(size_t data_size);
> +
> +/**
> + * rv_%%MODEL_NAME%%_destroy
> + *
> + * must be called while disabling the monitor
> + */
> +void rv_%%MODEL_NAME%%_destroy(void);
> +
> +/**
> + * rv_%%MODEL_NAME%%_error - report violation of the LTL property
> + * @task: the task violating the LTL property
> + * @mon: the LTL monitor
> + *
> + * Must be implemented. This function should invoke the RV reactor
> and the monitor's tracepoints.
> + */
> +void rv_%%MODEL_NAME%%_error(struct task_struct *task, struct
> ltl_monitor *mon);
> +
> +extern int rv_%%MODEL_NAME%%_task_slot;
> +
> +/**
> + * rv_%%MODEL_NAME%%_get_monitor - get the struct ltl_monitor of a
> task
> + */
> +static inline struct ltl_monitor
> *rv_%%MODEL_NAME%%_get_monitor(struct task_struct *task)
> +{
> + return &task->rv[rv_%%MODEL_NAME%%_task_slot].ltl_mon;
> +}
> +
> +/**
> + * rv_%%MODEL_NAME%%_atoms_init - initialize the atomic propositions
> + * @task: the task
> + * @mon: the LTL monitor
> + *
> + * Must be implemented. This function is called during task
> creation, and should initialize all
> + * atomic propositions. rv_%%MODEL_NAME%%_atom_set() should be used
> to implement this function.
> + *
> + * This function does not have to initialize atomic propositions
> that are updated by
> + * rv_%%MODEL_NAME%%_atoms_fetch(), because the two functions are
> called together.
> + */
> +void rv_%%MODEL_NAME%%_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon);
> +
> +/**
> + * rv_%%MODEL_NAME%%_atoms_fetch - fetch the atomic propositions
> + * @task: the task
> + * @mon: the LTL monitor
> + *
> + * Must be implemented. This function is called anytime the Buchi
> automaton is triggered. Its
> + * intended purpose is to update the atomic propositions which are
> expensive to trace and can be
> + * easily read from @task. rv_%%MODEL_NAME%%_atom_set() should be
> used to implement this function.
> + *
> + * Using this function may cause incorrect verification result if it
> is important for the LTL that
> + * the atomic propositions must be updated at the correct time.
> Therefore, if it is possible,
> + * updating atomic propositions should be done with
> rv_%%MODEL_NAME%%_atom_update() instead.
> + *
> + * An example where this function is useful is with the LTL
> property:
> + * always (RT imply not PAGEFAULT)
> + * (a realtime task does not raise page faults)
> + *
> + * In this example, adding tracepoints to track RT is complicated,
> because it is changed in
> + * differrent places (mutex's priority boosting,
> sched_setscheduler). Furthermore, for this LTL
> + * property, we don't care exactly when RT changes, as long as we
> have its correct value when
> + * PAGEFAULT==true. Therefore, it is better to update RT in
> rv_%%MODEL_NAME%%_atoms_fetch(), as it
> + * can easily be retrieved from task_struct.
> + *
> + * This function can be empty.
> + */
> +void rv_%%MODEL_NAME%%_atoms_fetch(struct task_struct *task, struct
> ltl_monitor *mon);
> +
> +/**
> + * rv_%%MODEL_NAME%%_atom_update - update an atomic proposition
> + * @task: the task
> + * @atom: the atomic proposition, one of enum
> %%MODEL_NAME%%_atom
> + * @value: the new value for @atom
> + *
> + * Update an atomic proposition and trigger the Buchi atomaton to
> check for violation of the LTL
> + * property. This function can be called in tracepoints' handler,
> for example.
> + */
> +void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task,
> unsigned int atom, bool value);
> +
> +/**
> + * rv_%%MODEL_NAME%%_atom_get - get an atomic proposition
> + * @mon: the monitor
> + * @atom: the atomic proposition, one of enum
> %%MODEL_NAME%%_atom
> + *
> + * Returns the value of an atomic proposition.
> + */
> +static inline
> +enum ltl_truth_value rv_%%MODEL_NAME%%_atom_get(struct ltl_monitor
> *mon, unsigned int atom)
> +{
> + return mon->atoms[atom];
> +}
> +
> +/**
> + * rv_%%MODEL_NAME%%_atom_set - set an atomic proposition
> + * @mon: the monitor
> + * @atom: the atomic proposition, one of enum
> %%MODEL_NAME%%_atom
> + * @value: the new value for @atom
> + *
> + * Update an atomic proposition without triggering the Buchi
> automaton. This can be useful to
> + * implement rv_%%MODEL_NAME%%_atoms_fetch() and
> rv_%%MODEL_NAME%%_atoms_init().
> + *
> + * Another use case for this function is when multiple atomic
> propositions change at the same time,
> + * because calling rv_%%MODEL_NAME%%_atom_update() (and thus
> triggering the Buchi automaton)
> + * multiple times may be incorrect. In that case,
> rv_%%MODEL_NAME%%_atom_set() can be used to avoid
> + * triggering the Buchi automaton, and
> rv_%%MODEL_NAME%%_atom_update() is only used for the last
> + * atomic proposition.
> + */
> +static inline
> +void rv_%%MODEL_NAME%%_atom_set(struct ltl_monitor *mon, unsigned
> int atom, bool value)
> +{
> + mon->atoms[atom] = value;
> +}
> +
> +/**
> + * rv_%%MODEL_NAME%%_get_data - get the custom data of this monitor.
> + * @mon: the monitor
> + *
> + * If this function is used, rv_%%MODEL_NAME%%_init() must have been
> called with a positive
> + * data_size.
> + */
> +static inline void *rv_%%MODEL_NAME%%_get_data(struct ltl_monitor
> *mon)
> +{
> + return &mon->data;
> +}
Do we need all those functions defined here? We could have them
generated by the pre-processor just like with DA monitors.
Having a ltl_monitor.h defining all common utility functions and
variables (here I'm assuming most are, indeed, common) may save a lot
of maintenance.
Also I would rearrange monitors sources a bit differently, like putting
everything that doesn't need manual intervention (states and atoms
lists) in the header, remaining functions that may need tracepoint
wiring or more complex stuff can stay in a single c file, a bit like
current da monitors.
I see there seems to be more manual work in the main C file (e.g.
rtapp_block.c), but I think it would look cleaner if all other code was
generated by the preprocessor in a common header and all lists/inlined
functions created by the script stay in a separate header (why not call
it rtapp_block.h?).
What do you think?
Thanks,
Gabriele