rv/ltl_monitor.h is the template file used by all LTL monitors. But only
per-task monitor is supported.
Prepare to support for other monitor types:
- Change the monitored target type into an opaque type which will be
defined differently depending on the monitor type. This type is only
defined as struct task_struct * for now.
- Separate out the per-task-specific printf format and arguments, so that
rv_cond_react() can be shared with other monitor types.
No functional change intended.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
include/linux/rv.h | 1 +
include/rv/ltl_monitor.h | 85 +++++++++++--------
.../trace/rv/monitors/pagefault/pagefault.h | 2 +
kernel/trace/rv/monitors/sleep/sleep.h | 2 +
4 files changed, 55 insertions(+), 35 deletions(-)
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 14410a42faef..175438a22641 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -28,6 +28,7 @@ struct da_monitor {
#ifdef CONFIG_RV_LTL_MONITOR
+#define LTL_TASK_MONITOR 0
/*
* 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
diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
index 67031a774e3d..466155fd53e6 100644
--- a/include/rv/ltl_monitor.h
+++ b/include/rv/ltl_monitor.h
@@ -16,49 +16,63 @@
#error "Please include $(MODEL_NAME).h generated by rvgen"
#endif
+#if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
+
+#define TARGET_PRINT_FORMAT "%s[%d]"
+#define TARGET_PRINT_ARGS(task) task->comm, task->pid
+
+typedef struct task_struct *monitor_target;
+
+#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)
+static void rv_cond_react(monitor_target target)
{
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);
+
+ RV_MONITOR_NAME.react(
+ "rv: "__stringify(MONITOR_NAME)": "TARGET_PRINT_FORMAT": violation detected\n",
+ TARGET_PRINT_ARGS(target));
}
#else
-static void rv_cond_react(struct task_struct *task)
+static void rv_cond_react(monitor_target target)
{
}
#endif
-static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
+static void ltl_atoms_fetch(monitor_target target, struct ltl_monitor *mon);
+static void ltl_atoms_init(monitor_target target, struct ltl_monitor *mon, bool target_creation);
-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);
+#if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
+static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
-static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
+static struct ltl_monitor *ltl_get_monitor(monitor_target target)
{
- return &task->rv[ltl_monitor_slot].ltl_mon;
+ return &target->rv[ltl_monitor_slot].ltl_mon;
}
+#endif
-static void ltl_task_init(struct task_struct *task, bool task_creation)
+static void ltl_target_init(monitor_target target, bool target_creation)
{
- struct ltl_monitor *mon = ltl_get_monitor(task);
+ struct ltl_monitor *mon = ltl_get_monitor(target);
memset(&mon->states, 0, sizeof(mon->states));
for (int i = 0; i < LTL_NUM_ATOM; ++i)
__set_bit(i, mon->unknown_atoms);
- ltl_atoms_init(task, mon, task_creation);
- ltl_atoms_fetch(task, mon);
+ ltl_atoms_init(target, mon, target_creation);
+ ltl_atoms_fetch(target, mon);
}
+#if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags)
{
- ltl_task_init(task, true);
+ ltl_target_init(task, true);
}
static int ltl_monitor_init(void)
@@ -77,10 +91,10 @@ static int ltl_monitor_init(void)
read_lock(&tasklist_lock);
for_each_process_thread(g, p)
- ltl_task_init(p, false);
+ ltl_target_init(p, false);
for_each_present_cpu(cpu)
- ltl_task_init(idle_task(cpu), false);
+ ltl_target_init(idle_task(cpu), false);
read_unlock(&tasklist_lock);
@@ -94,17 +108,18 @@ static void ltl_monitor_destroy(void)
rv_put_task_monitor_slot(ltl_monitor_slot);
ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
}
+#endif
-static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+static void ltl_illegal_state(monitor_target target, struct ltl_monitor *mon)
{
- CONCATENATE(trace_error_, MONITOR_NAME)(task);
- rv_cond_react(task);
+ CONCATENATE(trace_error_, MONITOR_NAME)(target);
+ rv_cond_react(target);
}
-static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+static void ltl_attempt_start(monitor_target target, struct ltl_monitor *mon)
{
if (rv_ltl_all_atoms_known(mon))
- ltl_start(task, mon);
+ ltl_start(target, mon);
}
static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value)
@@ -117,7 +132,7 @@ static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, boo
}
static void
-ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state)
+ltl_trace_event(monitor_target target, struct ltl_monitor *mon, unsigned long *next_state)
{
const char *format_str = "%s";
DECLARE_SEQ_BUF(atoms, 64);
@@ -137,10 +152,10 @@ ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long
}
}
- CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer, next);
+ CONCATENATE(trace_event_, MONITOR_NAME)(target, states, atoms.buffer, next);
}
-static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)
+static void ltl_validate(monitor_target target, struct ltl_monitor *mon)
{
DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0};
@@ -152,35 +167,35 @@ static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)
ltl_possible_next_states(mon, i, next_states);
}
- ltl_trace_event(task, mon, next_states);
+ ltl_trace_event(target, mon, next_states);
memcpy(mon->states, next_states, sizeof(next_states));
if (!rv_ltl_valid_state(mon))
- ltl_illegal_state(task, mon);
+ ltl_illegal_state(target, mon);
}
-static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)
+static void ltl_atom_update(monitor_target target, enum ltl_atom atom, bool value)
{
- struct ltl_monitor *mon = ltl_get_monitor(task);
+ struct ltl_monitor *mon = ltl_get_monitor(target);
ltl_atom_set(mon, atom, value);
- ltl_atoms_fetch(task, mon);
+ ltl_atoms_fetch(target, mon);
if (!rv_ltl_valid_state(mon)) {
- ltl_attempt_start(task, mon);
+ ltl_attempt_start(target, mon);
return;
}
- ltl_validate(task, mon);
+ ltl_validate(target, mon);
}
-static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)
+static void __maybe_unused ltl_atom_pulse(monitor_target target, enum ltl_atom atom, bool value)
{
- struct ltl_monitor *mon = ltl_get_monitor(task);
+ struct ltl_monitor *mon = ltl_get_monitor(target);
- ltl_atom_update(task, atom, value);
+ ltl_atom_update(target, atom, value);
ltl_atom_set(mon, atom, !value);
- ltl_validate(task, mon);
+ ltl_validate(target, mon);
}
diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.h b/kernel/trace/rv/monitors/pagefault/pagefault.h
index c580ec194009..cc825be51ffc 100644
--- a/kernel/trace/rv/monitors/pagefault/pagefault.h
+++ b/kernel/trace/rv/monitors/pagefault/pagefault.h
@@ -11,6 +11,8 @@
#define MONITOR_NAME pagefault
+#define LTL_MONITOR_TYPE LTL_TASK_MONITOR
+
enum ltl_atom {
LTL_PAGEFAULT,
LTL_RT,
diff --git a/kernel/trace/rv/monitors/sleep/sleep.h b/kernel/trace/rv/monitors/sleep/sleep.h
index 2ab46fd218d2..c3752bc9f93f 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.h
+++ b/kernel/trace/rv/monitors/sleep/sleep.h
@@ -11,6 +11,8 @@
#define MONITOR_NAME sleep
+#define LTL_MONITOR_TYPE LTL_TASK_MONITOR
+
enum ltl_atom {
LTL_ABORT_SLEEP,
LTL_BLOCK_ON_RT_MUTEX,
--
2.39.5On Wed, 2025-07-30 at 14:45 +0200, Nam Cao wrote:
> rv/ltl_monitor.h is the template file used by all LTL monitors. But
> only per-task monitor is supported.
>
> No functional change intended.
>
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> include/linux/rv.h | 1 +
> include/rv/ltl_monitor.h | 85 +++++++++++------
> --
> .../trace/rv/monitors/pagefault/pagefault.h | 2 +
> kernel/trace/rv/monitors/sleep/sleep.h | 2 +
> 4 files changed, 55 insertions(+), 35 deletions(-)
>
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 14410a42faef..175438a22641 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -28,6 +28,7 @@ struct da_monitor {
>
> #ifdef CONFIG_RV_LTL_MONITOR
>
> +#define LTL_TASK_MONITOR 0
I stole your solution to get rid of macros for the DA as well (might
post it after this merge window or with the next changes) and I'm
currently running with this:
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 14410a42faef..6a7594080db1 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -13,6 +13,10 @@
#define MAX_DA_NAME_LEN 32
#define MAX_DA_RETRY_RACING_EVENTS 3
+#define RV_MON_GLOBAL 0
+#define RV_MON_PER_CPU 1
+#define RV_MON_PER_TASK 2
+
The numbers don't really matter and you don't need to implement all, of
course.
I'm not sure how are our patches going to coordinate, but I think it
may make sense to share those values for all monitor types.
What do you think?
For the rest this patch looks good to me, nice use of the typedef.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Thanks,
Gabriele
On Thu, Jul 31, 2025 at 11:04:44AM +0200, Gabriele Monaco wrote:
> I stole your solution to get rid of macros for the DA as well (might
> post it after this merge window or with the next changes) and I'm
> currently running with this:
Nice, glad you like it.
For global monitor, you could do
typdef struct {} monitor_target;
static monitor_target rv_global_target;
I didn't check clang, but gcc does not emit anything for this. So
effectively the compiled code does not have the "target" parameter.
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 14410a42faef..6a7594080db1 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -13,6 +13,10 @@
> #define MAX_DA_NAME_LEN 32
> #define MAX_DA_RETRY_RACING_EVENTS 3
>
> +#define RV_MON_GLOBAL 0
> +#define RV_MON_PER_CPU 1
> +#define RV_MON_PER_TASK 2
> +
>
> The numbers don't really matter and you don't need to implement all, of
> course.
That makes sense, will do.
> I'm not sure how are our patches going to coordinate,
Let's just post them. The one whose patches are not applied first will have
to rebase. It is a trivial rebase anyway.
Nam
On Thu, 2025-07-31 at 11:28 +0200, Nam Cao wrote:
> On Thu, Jul 31, 2025 at 11:04:44AM +0200, Gabriele Monaco wrote:
> > I stole your solution to get rid of macros for the DA as well
> > (might
> > post it after this merge window or with the next changes) and I'm
> > currently running with this:
>
> Nice, glad you like it.
>
> For global monitor, you could do
>
> typdef struct {} monitor_target;
>
> static monitor_target rv_global_target;
>
Well, implicit monitors (cpu and global for DA) don't really have a
target but I'll probably be using this for other types if necessary or
in case I'm unifying things. Which might be nice, if it didn't require
modifying all per-cpu monitors (where CPU is not passed because the
current one is assumed).
> I didn't check clang, but gcc does not emit anything for this. So
> effectively the compiled code does not have the "target" parameter.
>
> > diff --git a/include/linux/rv.h b/include/linux/rv.h
> > index 14410a42faef..6a7594080db1 100644
> > --- a/include/linux/rv.h
> > +++ b/include/linux/rv.h
> > @@ -13,6 +13,10 @@
> > #define MAX_DA_NAME_LEN 32
> > #define MAX_DA_RETRY_RACING_EVENTS 3
> >
> > +#define RV_MON_GLOBAL 0
> > +#define RV_MON_PER_CPU 1
> > +#define RV_MON_PER_TASK 2
> > +
> >
> > The numbers don't really matter and you don't need to implement
> > all, of
> > course.
>
> That makes sense, will do.
>
> > I'm not sure how are our patches going to coordinate,
>
> Let's just post them. The one whose patches are not applied first
> will have to rebase. It is a trivial rebase anyway.
Sure then, git may be smart enough to see there aren't conflicts.
Thanks,
Gabriele
© 2016 - 2025 Red Hat, Inc.