[PATCH v2 00/22] RV: Linear temporal logic monitors for RT application

[PATCH v2 00/22] RV: Linear temporal logic monitors for RT application

[Nam Cao]

Real-time applications may have design flaws causing them to have
unexpected latency. For example, the applications may raise page faults, or
may be blocked trying to take a mutex without priority inheritance.

However, while attempting to implement DA monitors for these real-time
rules, 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 found to be more suitable. The
LTL is more concise and intuitive.

This series adds support for LTL RV monitor, and use it to implement two
monitors for reporting problems with real-time tasks.

Patch 1-7 do some cleanups to RV.

Patch 8-12 prepare the RV code for the integration of LTL monitors.

Patch 13 adds support for LTL monitors.

Patch 14 adds the container monitor "rtapp". This encapsulates the
sub-monitors for real-time.

Patch 15-18 prepares the pagefault tracepoints, so that patch 19 can add
the monitor which watches real-time tasks doing page faults.

Patch 20 adds the "sleep" monitor: it detects potential undesirable latency
with real-time threads.

Patch 21 adds documentation on the new monitors.

Patch 22 allows the number of per-task monitors to be configurable, so that
the two new monitors can be enabled simultaneously.

v1->v2 https://lore.kernel.org/lkml/cover.1741708239.git.namcao@linutronix.de/
  - Integrate the LTL scripts into the existing dot2k tool, taking
    advantage of the existing monitor generation scripts.
  - Switch the struct ltl_monitor to use bitmap instead of an array, to
    optimize memory usage.
  - Correct the generated code to be non-deterministic state machine,
    instead of deterministic state machine
  - Put common code for all LTL monitors into a single file
    (include/rv/ltl_monitor.h), reducing code duplication
  - Change the LTL monitors to make user of container. Add a bug fix to
    container while at it.
  - Make the number of per-task monitor configurable

Cc: Petr Mladek <pmladek@suse.com>
Cc: John Ogness <john.ogness@linutronix.de>
Cc: Sergey Senozhatsky <senozhatsky@chromium.org>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Waiman Long <longman@redhat.com>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: H. Peter Anvin <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: linux-arm-kernel@lists.infradead.org
Cc: Paul Walmsley <paul.walmsley@sifive.com>
Cc: Palmer Dabbelt <palmer@dabbelt.com>
Cc: Albert Ou <aou@eecs.berkeley.edu>
Cc: Alexandre Ghiti <alex@ghiti.fr>
Cc: linux-riscv@lists.infradead.org

Nam Cao (22):
  rv: Fix out-of-bound memory access in rv_is_container_monitor()
  rv: Add #undef TRACE_INCLUDE_FILE
  rv: Let the reactors take care of buffers
  verification/dot2k: Make it possible to invoke dot2k without
    installation
  verification/dot2k: Make a separate dot2k_templates/Kconfig_container
  verification/dot2k: Remove __buff_to_string()
  verification/dot2k: Replace is_container() hack with subparsers
  rv: rename CONFIG_DA_MON_EVENTS to CONFIG_RV_MON_EVENTS
  verification/dot2k: Prepare the frontend for LTL inclusion
  Documentation/rv: Prepare monitor synthesis document for LTL inclusion
  verification/rvgen: Prepare the templates for LTL inclusion
  verification/rvgen: Restructure the classes to prepare for LTL
    inclusion
  rv: Add support for LTL monitors
  rv: Add rtapp container monitor
  x86/tracing: Remove redundant trace_pagefault_key
  x86/tracing: Move page fault trace points to generic
  arm64: mm: Add page fault trace points
  riscv: mm: Add page fault trace points
  rv: Add rtapp_pagefault monitor
  rv: Add rtapp_sleep monitor
  rv: Add documentation for rtapp monitor
  rv: Allow to configure the number of per-task monitor

 .../trace/rv/da_monitor_synthesis.rst         | 147 -----
 Documentation/trace/rv/index.rst              |   3 +-
 .../trace/rv/linear_temporal_logic.rst        |  97 +++
 Documentation/trace/rv/monitor_rtapp.rst      | 105 ++++
 Documentation/trace/rv/monitor_synthesis.rst  | 256 ++++++++
 arch/arm64/mm/fault.c                         |   8 +
 arch/riscv/mm/fault.c                         |   8 +
 arch/x86/include/asm/trace/common.h           |  12 -
 arch/x86/include/asm/trace/irq_vectors.h      |   1 -
 arch/x86/kernel/Makefile                      |   1 -
 arch/x86/kernel/tracepoint.c                  |  21 -
 arch/x86/mm/fault.c                           |   5 +-
 include/linux/panic.h                         |   3 +
 include/linux/printk.h                        |   5 +
 include/linux/rv.h                            |  67 ++-
 include/linux/sched.h                         |   8 +-
 include/rv/da_monitor.h                       |  45 +-
 include/rv/ltl_monitor.h                      | 184 ++++++
 .../trace/events}/exceptions.h                |  27 +-
 kernel/fork.c                                 |   5 +-
 kernel/panic.c                                |  17 +-
 kernel/printk/internal.h                      |   1 -
 kernel/trace/rv/Kconfig                       |  27 +-
 kernel/trace/rv/Makefile                      |   3 +
 kernel/trace/rv/monitors/pagefault/Kconfig    |  11 +
 .../trace/rv/monitors/pagefault/pagefault.c   |  83 +++
 .../trace/rv/monitors/pagefault/pagefault.h   |  57 ++
 .../rv/monitors/pagefault/pagefault_trace.h   |  14 +
 kernel/trace/rv/monitors/rtapp/Kconfig        |   6 +
 kernel/trace/rv/monitors/rtapp/rtapp.c        |  34 ++
 kernel/trace/rv/monitors/rtapp/rtapp.h        |   3 +
 kernel/trace/rv/monitors/sleep/Kconfig        |  13 +
 kernel/trace/rv/monitors/sleep/sleep.c        | 217 +++++++
 kernel/trace/rv/monitors/sleep/sleep.h        | 293 ++++++++++
 kernel/trace/rv/monitors/sleep/sleep_trace.h  |  14 +
 kernel/trace/rv/reactor_panic.c               |   8 +-
 kernel/trace/rv/reactor_printk.c              |   8 +-
 kernel/trace/rv/rv.c                          |  17 +-
 kernel/trace/rv/rv_reactors.c                 |   2 +-
 kernel/trace/rv/rv_trace.h                    |  52 +-
 tools/verification/dot2/Makefile              |  26 -
 tools/verification/dot2/dot2k                 |  53 --
 tools/verification/models/rtapp/pagefault.ltl |   1 +
 tools/verification/models/rtapp/sleep.ltl     |  15 +
 tools/verification/rvgen/.gitignore           |   3 +
 tools/verification/rvgen/Makefile             |  30 +
 tools/verification/rvgen/__main__.py          |  67 +++
 tools/verification/{dot2 => rvgen}/dot2c      |   2 +-
 .../{dot2 => rvgen/rvgen}/automata.py         |   0
 tools/verification/rvgen/rvgen/container.py   |  22 +
 .../{dot2 => rvgen/rvgen}/dot2c.py            |   2 +-
 tools/verification/rvgen/rvgen/dot2k.py       | 129 ++++
 .../dot2k.py => rvgen/rvgen/generator.py}     | 233 ++------
 tools/verification/rvgen/rvgen/ltl2ba.py      | 552 ++++++++++++++++++
 tools/verification/rvgen/rvgen/ltl2k.py       | 242 ++++++++
 .../templates}/Kconfig                        |   0
 .../rvgen/templates/container/Kconfig         |   5 +
 .../templates/container/main.c}               |   0
 .../templates/container/main.h}               |   0
 .../templates/dot2k}/main.c                   |   0
 .../templates/dot2k}/trace.h                  |   0
 .../verification/rvgen/templates/ltl2k/main.c | 102 ++++
 .../rvgen/templates/ltl2k/trace.h             |  14 +
 63 files changed, 2857 insertions(+), 529 deletions(-)
 delete mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
 create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
 create mode 100644 Documentation/trace/rv/monitor_rtapp.rst
 create mode 100644 Documentation/trace/rv/monitor_synthesis.rst
 delete mode 100644 arch/x86/include/asm/trace/common.h
 delete mode 100644 arch/x86/kernel/tracepoint.c
 create mode 100644 include/rv/ltl_monitor.h
 rename {arch/x86/include/asm/trace => include/trace/events}/exceptions.h (55%)
 create mode 100644 kernel/trace/rv/monitors/pagefault/Kconfig
 create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.c
 create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.h
 create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault_trace.h
 create mode 100644 kernel/trace/rv/monitors/rtapp/Kconfig
 create mode 100644 kernel/trace/rv/monitors/rtapp/rtapp.c
 create mode 100644 kernel/trace/rv/monitors/rtapp/rtapp.h
 create mode 100644 kernel/trace/rv/monitors/sleep/Kconfig
 create mode 100644 kernel/trace/rv/monitors/sleep/sleep.c
 create mode 100644 kernel/trace/rv/monitors/sleep/sleep.h
 create mode 100644 kernel/trace/rv/monitors/sleep/sleep_trace.h
 delete mode 100644 tools/verification/dot2/Makefile
 delete mode 100644 tools/verification/dot2/dot2k
 create mode 100644 tools/verification/models/rtapp/pagefault.ltl
 create mode 100644 tools/verification/models/rtapp/sleep.ltl
 create mode 100644 tools/verification/rvgen/.gitignore
 create mode 100644 tools/verification/rvgen/Makefile
 create mode 100644 tools/verification/rvgen/__main__.py
 rename tools/verification/{dot2 => rvgen}/dot2c (97%)
 rename tools/verification/{dot2 => rvgen/rvgen}/automata.py (100%)
 create mode 100644 tools/verification/rvgen/rvgen/container.py
 rename tools/verification/{dot2 => rvgen/rvgen}/dot2c.py (99%)
 create mode 100644 tools/verification/rvgen/rvgen/dot2k.py
 rename tools/verification/{dot2/dot2k.py => rvgen/rvgen/generator.py} (56%)
 create mode 100644 tools/verification/rvgen/rvgen/ltl2ba.py
 create mode 100644 tools/verification/rvgen/rvgen/ltl2k.py
 rename tools/verification/{dot2/dot2k_templates => rvgen/templates}/Kconfig (100%)
 create mode 100644 tools/verification/rvgen/templates/container/Kconfig
 rename tools/verification/{dot2/dot2k_templates/main_container.c => rvgen/templates/container/main.c} (100%)
 rename tools/verification/{dot2/dot2k_templates/main_container.h => rvgen/templates/container/main.h} (100%)
 rename tools/verification/{dot2/dot2k_templates => rvgen/templates/dot2k}/main.c (100%)
 rename tools/verification/{dot2/dot2k_templates => rvgen/templates/dot2k}/trace.h (100%)
 create mode 100644 tools/verification/rvgen/templates/ltl2k/main.c
 create mode 100644 tools/verification/rvgen/templates/ltl2k/trace.h

-- 
2.39.5

[PATCH v2 01/22] rv: Fix out-of-bound memory access in rv_is_container_monitor()

[Nam Cao]

When rv_is_container_monitor() is called on the last monitor in
rv_monitors_list, KASAN yells:

  BUG: KASAN: global-out-of-bounds in rv_is_container_monitor+0x101/0x110
  Read of size 8 at addr ffffffff97c7c798 by task setup/221

  The buggy address belongs to the variable:
   rv_monitors_list+0x18/0x40

This is due to list_next_entry() is called on the last entry in the list.
It wraps around to the first list_head, and the first list_head is not
embedded in struct rv_monitor_def.

Fix it by checking if the monitor is last in the list.

Fixes: cb85c660fcd4 ("rv: Add option for nested monitors and include sched")
Signed-off-by: Nam Cao <namcao@linutronix.de>
Cc: stable@vger.kernel.org
---
 kernel/trace/rv/rv.c | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
index 50344aa9f7f9..544acb1f6a33 100644
--- a/kernel/trace/rv/rv.c
+++ b/kernel/trace/rv/rv.c
@@ -225,7 +225,12 @@ bool rv_is_nested_monitor(struct rv_monitor_def *mdef)
  */
 bool rv_is_container_monitor(struct rv_monitor_def *mdef)
 {
-	struct rv_monitor_def *next = list_next_entry(mdef, list);
+	struct rv_monitor_def *next;
+
+	if (list_is_last(&mdef->list, &rv_monitors_list))
+		return false;
+
+	next = list_next_entry(mdef, list);
 
 	return next->parent == mdef->monitor || !mdef->monitor->enable;
 }
-- 
2.39.5

[PATCH v2 02/22] rv: Add #undef TRACE_INCLUDE_FILE

[Nam Cao]

Without "#undef TRACE_INCLUDE_FILE", there could be a build error due to
TRACE_INCLUDE_FILE being redefined. Therefore add it.

Also fix a typo while at it.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 kernel/trace/rv/rv_trace.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 422b75f58891..99c3801616d4 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -129,8 +129,9 @@ DECLARE_EVENT_CLASS(error_da_monitor_id,
 #endif /* CONFIG_DA_MON_EVENTS_ID */
 #endif /* _TRACE_RV_H */
 
-/* This part ust be outside protection */
+/* This part must be outside protection */
 #undef TRACE_INCLUDE_PATH
 #define TRACE_INCLUDE_PATH .
+#undef TRACE_INCLUDE_FILE
 #define TRACE_INCLUDE_FILE rv_trace
 #include <trace/define_trace.h>
-- 
2.39.5

[PATCH v2 03/22] rv: Let the reactors take care of buffers

[Nam Cao]

Each RV monitor has one static buffer to send to the reactors. If multiple
errors are detected simultaneously, the one buffer could be overwritten.

Instead, leave it to the reactors to handle buffering.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Petr Mladek <pmladek@suse.com>
Cc: John Ogness <john.ogness@linutronix.de>
Cc: Sergey Senozhatsky <senozhatsky@chromium.org>
---
 include/linux/panic.h            |  3 +++
 include/linux/printk.h           |  5 ++++
 include/linux/rv.h               |  9 +++++--
 include/rv/da_monitor.h          | 45 +++++++-------------------------
 kernel/panic.c                   | 17 ++++++++----
 kernel/printk/internal.h         |  1 -
 kernel/trace/rv/reactor_panic.c  |  8 ++++--
 kernel/trace/rv/reactor_printk.c |  8 ++++--
 kernel/trace/rv/rv_reactors.c    |  2 +-
 9 files changed, 50 insertions(+), 48 deletions(-)

diff --git a/include/linux/panic.h b/include/linux/panic.h
index 54d90b6c5f47..3522f8c441f4 100644
--- a/include/linux/panic.h
+++ b/include/linux/panic.h
@@ -3,6 +3,7 @@
 #define _LINUX_PANIC_H
 
 #include <linux/compiler_attributes.h>
+#include <linux/stdarg.h>
 #include <linux/types.h>
 
 struct pt_regs;
@@ -10,6 +11,8 @@ struct pt_regs;
 extern long (*panic_blink)(int state);
 __printf(1, 2)
 void panic(const char *fmt, ...) __noreturn __cold;
+__printf(1, 0)
+void vpanic(const char *fmt, va_list args) __noreturn __cold;
 void nmi_panic(struct pt_regs *regs, const char *msg);
 void check_panic_on_warn(const char *origin);
 extern void oops_enter(void);
diff --git a/include/linux/printk.h b/include/linux/printk.h
index 4217a9f412b2..1b7eebe13f14 100644
--- a/include/linux/printk.h
+++ b/include/linux/printk.h
@@ -154,6 +154,7 @@ int vprintk_emit(int facility, int level,
 
 asmlinkage __printf(1, 0)
 int vprintk(const char *fmt, va_list args);
+__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args);
 
 asmlinkage __printf(1, 2) __cold
 int _printk(const char *fmt, ...);
@@ -213,6 +214,10 @@ int vprintk(const char *s, va_list args)
 {
 	return 0;
 }
+__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args)
+{
+	return 0;
+}
 static inline __printf(1, 2) __cold
 int _printk(const char *s, ...)
 {
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 3452b5e4b29e..c7c18c06911b 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -38,7 +38,7 @@ union rv_task_monitor {
 struct rv_reactor {
 	const char		*name;
 	const char		*description;
-	void			(*react)(char *msg);
+	__printf(1, 2) void	(*react)(const char *msg, ...);
 };
 #endif
 
@@ -50,7 +50,7 @@ struct rv_monitor {
 	void			(*disable)(void);
 	void			(*reset)(void);
 #ifdef CONFIG_RV_REACTORS
-	void			(*react)(char *msg);
+	__printf(1, 2) void	(*react)(const char *msg, ...);
 #endif
 };
 
@@ -64,6 +64,11 @@ void rv_put_task_monitor_slot(int slot);
 bool rv_reacting_on(void);
 int rv_unregister_reactor(struct rv_reactor *reactor);
 int rv_register_reactor(struct rv_reactor *reactor);
+#else
+bool rv_reacting_on(void)
+{
+	return false;
+}
 #endif /* CONFIG_RV_REACTORS */
 
 #endif /* CONFIG_RV */
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
index 510c88bfabd4..15f9ed4e4bb6 100644
--- a/include/rv/da_monitor.h
+++ b/include/rv/da_monitor.h
@@ -19,45 +19,22 @@
 #ifdef CONFIG_RV_REACTORS
 
 #define DECLARE_RV_REACTING_HELPERS(name, type)							\
-static char REACT_MSG_##name[1024];								\
-												\
-static inline char *format_react_msg_##name(type curr_state, type event)			\
-{												\
-	snprintf(REACT_MSG_##name, 1024,							\
-		 "rv: monitor %s does not allow event %s on state %s\n",			\
-		 #name,										\
-		 model_get_event_name_##name(event),						\
-		 model_get_state_name_##name(curr_state));					\
-	return REACT_MSG_##name;								\
-}												\
-												\
-static void cond_react_##name(char *msg)							\
+static void cond_react_##name(type curr_state, type event)					\
 {												\
-	if (rv_##name.react)									\
-		rv_##name.react(msg);								\
-}												\
-												\
-static bool rv_reacting_on_##name(void)								\
-{												\
-	return rv_reacting_on();								\
+	if (!rv_reacting_on() || !rv_##name.react)						\
+		return;										\
+	rv_##name.react("rv: monitor %s does not allow event %s on state %s\n",			\
+			#name,									\
+			model_get_event_name_##name(event),					\
+			model_get_state_name_##name(curr_state));				\
 }
 
 #else /* CONFIG_RV_REACTOR */
 
 #define DECLARE_RV_REACTING_HELPERS(name, type)							\
-static inline char *format_react_msg_##name(type curr_state, type event)			\
-{												\
-	return NULL;										\
-}												\
-												\
-static void cond_react_##name(char *msg)							\
+static void cond_react_##name(type curr_state, type event)					\
 {												\
 	return;											\
-}												\
-												\
-static bool rv_reacting_on_##name(void)								\
-{												\
-	return 0;										\
 }
 #endif
 
@@ -170,8 +147,7 @@ da_event_##name(struct da_monitor *da_mon, enum events_##name event)				\
 		return true;									\
 	}											\
 												\
-	if (rv_reacting_on_##name())								\
-		cond_react_##name(format_react_msg_##name(curr_state, event));			\
+	cond_react_##name(curr_state, event);							\
 												\
 	trace_error_##name(model_get_state_name_##name(curr_state),				\
 			   model_get_event_name_##name(event));					\
@@ -202,8 +178,7 @@ static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct
 		return true;									\
 	}											\
 												\
-	if (rv_reacting_on_##name())								\
-		cond_react_##name(format_react_msg_##name(curr_state, event));			\
+	cond_react_##name(curr_state, event);							\
 												\
 	trace_error_##name(tsk->pid,								\
 			   model_get_state_name_##name(curr_state),				\
diff --git a/kernel/panic.c b/kernel/panic.c
index d8635d5cecb2..df799d784b61 100644
--- a/kernel/panic.c
+++ b/kernel/panic.c
@@ -277,17 +277,16 @@ static void panic_other_cpus_shutdown(bool crash_kexec)
 }
 
 /**
- *	panic - halt the system
+ *	vpanic - halt the system
  *	@fmt: The text string to print
  *
  *	Display a message, then perform cleanups.
  *
  *	This function never returns.
  */
-void panic(const char *fmt, ...)
+void vpanic(const char *fmt, va_list args)
 {
 	static char buf[1024];
-	va_list args;
 	long i, i_next = 0, len;
 	int state = 0;
 	int old_cpu, this_cpu;
@@ -338,9 +337,7 @@ void panic(const char *fmt, ...)
 
 	console_verbose();
 	bust_spinlocks(1);
-	va_start(args, fmt);
 	len = vscnprintf(buf, sizeof(buf), fmt, args);
-	va_end(args);
 
 	if (len && buf[len - 1] == '\n')
 		buf[len - 1] = '\0';
@@ -477,7 +474,17 @@ void panic(const char *fmt, ...)
 		mdelay(PANIC_TIMER_STEP);
 	}
 }
+EXPORT_SYMBOL(vpanic);
 
+/* Identical to vpanic(), except it takes variadic arguments instead of va_list */
+void panic(const char *fmt, ...)
+{
+	va_list args;
+
+	va_start(args, fmt);
+	vpanic(fmt, args);
+	va_end(args);
+}
 EXPORT_SYMBOL(panic);
 
 #define TAINT_FLAG(taint, _c_true, _c_false, _module)			\
diff --git a/kernel/printk/internal.h b/kernel/printk/internal.h
index a91bdf802967..28afdeb58412 100644
--- a/kernel/printk/internal.h
+++ b/kernel/printk/internal.h
@@ -71,7 +71,6 @@ int vprintk_store(int facility, int level,
 		  const char *fmt, va_list args);
 
 __printf(1, 0) int vprintk_default(const char *fmt, va_list args);
-__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args);
 
 void __printk_safe_enter(void);
 void __printk_safe_exit(void);
diff --git a/kernel/trace/rv/reactor_panic.c b/kernel/trace/rv/reactor_panic.c
index 0186ff4cbd0b..2587f23db80b 100644
--- a/kernel/trace/rv/reactor_panic.c
+++ b/kernel/trace/rv/reactor_panic.c
@@ -13,9 +13,13 @@
 #include <linux/init.h>
 #include <linux/rv.h>
 
-static void rv_panic_reaction(char *msg)
+static void rv_panic_reaction(const char *msg, ...)
 {
-	panic(msg);
+	va_list args;
+
+	va_start(args, msg);
+	vpanic(msg, args);
+	va_end(args);
 }
 
 static struct rv_reactor rv_panic = {
diff --git a/kernel/trace/rv/reactor_printk.c b/kernel/trace/rv/reactor_printk.c
index 178759dbf89f..a15db3fc8b82 100644
--- a/kernel/trace/rv/reactor_printk.c
+++ b/kernel/trace/rv/reactor_printk.c
@@ -12,9 +12,13 @@
 #include <linux/init.h>
 #include <linux/rv.h>
 
-static void rv_printk_reaction(char *msg)
+static void rv_printk_reaction(const char *msg, ...)
 {
-	printk_deferred(msg);
+	va_list args;
+
+	va_start(args, msg);
+	vprintk_deferred(msg, args);
+	va_end(args);
 }
 
 static struct rv_reactor rv_printk = {
diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c
index 9501ca886d83..4ce6ebb9d095 100644
--- a/kernel/trace/rv/rv_reactors.c
+++ b/kernel/trace/rv/rv_reactors.c
@@ -490,7 +490,7 @@ void reactor_cleanup_monitor(struct rv_monitor_def *mdef)
 /*
  * Nop reactor register
  */
-static void rv_nop_reaction(char *msg)
+static void rv_nop_reaction(const char *msg, ...)
 {
 }
 
-- 
2.39.5

[PATCH v2 04/22] verification/dot2k: Make it possible to invoke dot2k without installation

[Nam Cao]

Without installation, dot2k doesn't work:

namcao@yellow:~/linux/tools/verification$ python3 ./dot2/dot2k
Traceback (most recent call last):
  File "/home/namcao/linux/tools/verification/./dot2/dot2k", line 12, in <module>
    from dot2.dot2k import dot2k
ModuleNotFoundError: No module named 'dot2'

Installing dot2k to the system is not always desirable. Sometimes it is not
even possible (e.g. no root permission).

Restructure the files to make it work without installing.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/dot2/Makefile               | 6 +++---
 tools/verification/dot2/{ => dot2}/automata.py | 0
 tools/verification/dot2/{ => dot2}/dot2c.py    | 0
 tools/verification/dot2/{ => dot2}/dot2k.py    | 0
 4 files changed, 3 insertions(+), 3 deletions(-)
 rename tools/verification/dot2/{ => dot2}/automata.py (100%)
 rename tools/verification/dot2/{ => dot2}/dot2c.py (100%)
 rename tools/verification/dot2/{ => dot2}/dot2k.py (100%)

diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile
index 021beb07a521..7a2ec30014b0 100644
--- a/tools/verification/dot2/Makefile
+++ b/tools/verification/dot2/Makefile
@@ -16,10 +16,10 @@ clean:
 
 .PHONY: install
 install:
-	$(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
-	$(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
+	$(INSTALL) dot2/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
+	$(INSTALL) dot2/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
 	$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
-	$(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py
+	$(INSTALL) dot2/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py
 	$(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/
 
 	mkdir -p ${miscdir}/
diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/dot2/automata.py
similarity index 100%
rename from tools/verification/dot2/automata.py
rename to tools/verification/dot2/dot2/automata.py
diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot2/dot2c.py
similarity index 100%
rename from tools/verification/dot2/dot2c.py
rename to tools/verification/dot2/dot2/dot2c.py
diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2/dot2k.py
similarity index 100%
rename from tools/verification/dot2/dot2k.py
rename to tools/verification/dot2/dot2/dot2k.py
-- 
2.39.5

[PATCH v2 05/22] verification/dot2k: Make a separate dot2k_templates/Kconfig_container

[Nam Cao]

A generated container's Kconfig has an incorrect line:

    select DA_MON_EVENTS_IMPLICIT

This is due to container generation uses the same template Kconfig file as
deterministic automaton monitor.

Therefore, make a separate Kconfig template for container which has only
the necessaries for container.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Alternatively, we could also modify the Python scripts. I tried both and
this solution seems cleaner.
---
 tools/verification/dot2/dot2/dot2k.py                     | 3 ++-
 tools/verification/dot2/dot2k_templates/Kconfig_container | 5 +++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 tools/verification/dot2/dot2k_templates/Kconfig_container

diff --git a/tools/verification/dot2/dot2/dot2k.py b/tools/verification/dot2/dot2/dot2k.py
index 745d35a4a379..dd4b5528a4f2 100644
--- a/tools/verification/dot2/dot2/dot2k.py
+++ b/tools/verification/dot2/dot2/dot2k.py
@@ -35,6 +35,7 @@ class dot2k(Dot2c):
             self.states = []
             self.main_c = self.__read_file(self.monitor_templates_dir + "main_container.c")
             self.main_h = self.__read_file(self.monitor_templates_dir + "main_container.h")
+            self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig_container")
         else:
             super().__init__(file_path, extra_params.get("model_name"))
 
@@ -44,7 +45,7 @@ class dot2k(Dot2c):
             self.monitor_type = MonitorType
             self.main_c = self.__read_file(self.monitor_templates_dir + "main.c")
             self.trace_h = self.__read_file(self.monitor_templates_dir + "trace.h")
-        self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig")
+            self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig")
         self.enum_suffix = "_%s" % self.name
         self.description = extra_params.get("description", self.name) or "auto-generated"
         self.auto_patch = extra_params.get("auto_patch")
diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/tools/verification/dot2/dot2k_templates/Kconfig_container
new file mode 100644
index 000000000000..a606111949c2
--- /dev/null
+++ b/tools/verification/dot2/dot2k_templates/Kconfig_container
@@ -0,0 +1,5 @@
+config RV_MON_%%MODEL_NAME_UP%%
+	depends on RV
+	bool "%%MODEL_NAME%% monitor"
+	help
+	  %%DESCRIPTION%%
-- 
2.39.5

[PATCH v2 06/22] verification/dot2k: Remove __buff_to_string()

[Nam Cao]

str.join() can do what __buff_to_string() does. Therefore replace
__buff_to_string() to make the scripts more pythonic.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/dot2/dot2/dot2k.py | 21 ++++++---------------
 1 file changed, 6 insertions(+), 15 deletions(-)

diff --git a/tools/verification/dot2/dot2/dot2k.py b/tools/verification/dot2/dot2/dot2k.py
index dd4b5528a4f2..0922754454b9 100644
--- a/tools/verification/dot2/dot2/dot2k.py
+++ b/tools/verification/dot2/dot2/dot2k.py
@@ -109,15 +109,6 @@ class dot2k(Dot2c):
         fd.close()
         return content
 
-    def __buff_to_string(self, buff):
-        string = ""
-
-        for line in buff:
-            string = string + line + "\n"
-
-        # cut off the last \n
-        return string[:-1]
-
     def fill_monitor_type(self):
         return self.monitor_type.upper()
 
@@ -148,19 +139,19 @@ class dot2k(Dot2c):
                 buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event, self.enum_suffix));
             buff.append("}")
             buff.append("")
-        return self.__buff_to_string(buff)
+        return '\n'.join(buff)
 
     def fill_tracepoint_attach_probe(self):
         buff = []
         for event in self.events:
             buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
-        return self.__buff_to_string(buff)
+        return '\n'.join(buff)
 
     def fill_tracepoint_detach_helper(self):
         buff = []
         for event in self.events:
             buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
-        return self.__buff_to_string(buff)
+        return '\n'.join(buff)
 
     def fill_main_c(self):
         main_c = self.main_c
@@ -210,7 +201,7 @@ class dot2k(Dot2c):
         buff = self.fill_model_h_header()
         buff += self.format_model()
 
-        return self.__buff_to_string(buff)
+        return '\n'.join(buff)
 
     def fill_monitor_class_type(self):
         if self.monitor_type == "per_task":
@@ -242,7 +233,7 @@ class dot2k(Dot2c):
         tp_args_c = ", ".join([b for a,b in tp_args])
         buff.append("	     TP_PROTO(%s)," % tp_proto_c)
         buff.append("	     TP_ARGS(%s)" % tp_args_c)
-        return self.__buff_to_string(buff)
+        return '\n'.join(buff)
 
     def fill_monitor_deps(self):
         buff = []
@@ -250,7 +241,7 @@ class dot2k(Dot2c):
         if self.parent:
             buff.append("	depends on RV_MON_%s" % self.parent.upper())
             buff.append("	default y")
-        return self.__buff_to_string(buff)
+        return '\n'.join(buff)
 
     def fill_trace_h(self):
         trace_h = self.trace_h
-- 
2.39.5

[PATCH v2 07/22] verification/dot2k: Replace is_container() hack with subparsers

[Nam Cao]

dot2k is used for both generating deterministic automaton (DA) monitor and
generating container monitor.

Generating DA monitor and generating container requires different
parameters. This is implemented by peeking at sys.argv and check whether
"--container" is specified, and use that information to make some
parameters optional or required.

This works, but is quite hacky and ugly.

Replace this hack with Python's built-in subparsers.

The old commands:

  python3 dot2/dot2k -d wip.dot -t per_cpu
  python3 dot2/dot2k -n sched --container

are equivalent to the new commands:

  python3 dot2/dot2k monitor -d wip.dot -t per_cpu
  python3 dot2/dot2k container -n sched

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/dot2/dot2/dot2k.py |  2 +-
 tools/verification/dot2/dot2k         | 37 +++++++++++++++------------
 2 files changed, 21 insertions(+), 18 deletions(-)

diff --git a/tools/verification/dot2/dot2/dot2k.py b/tools/verification/dot2/dot2/dot2k.py
index 0922754454b9..9ec99e297012 100644
--- a/tools/verification/dot2/dot2/dot2k.py
+++ b/tools/verification/dot2/dot2/dot2k.py
@@ -19,7 +19,7 @@ class dot2k(Dot2c):
     monitor_type = "per_cpu"
 
     def __init__(self, file_path, MonitorType, extra_params={}):
-        self.container = extra_params.get("container")
+        self.container = extra_params.get("subcmd") == "container"
         self.parent = extra_params.get("parent")
         self.__fill_rv_templates_dir()
 
diff --git a/tools/verification/dot2/dot2k b/tools/verification/dot2/dot2k
index 767064f415e7..133fb17d9d47 100644
--- a/tools/verification/dot2/dot2k
+++ b/tools/verification/dot2/dot2k
@@ -13,30 +13,33 @@ if __name__ == '__main__':
     import argparse
     import sys
 
-    def is_container():
-        """Should work even before parsing the arguments"""
-        return "-c" in sys.argv or "--container" in sys.argv
-
     parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor')
-    parser.add_argument('-d', "--dot", dest="dot_file", required=not is_container())
-    parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=not is_container(),
-                        help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
-    parser.add_argument('-n', "--model_name", dest="model_name", required=is_container())
     parser.add_argument("-D", "--description", dest="description", required=False)
     parser.add_argument("-a", "--auto_patch", dest="auto_patch",
                         action="store_true", required=False,
                         help="Patch the kernel in place")
-    parser.add_argument("-p", "--parent", dest="parent",
-                        required=False, help="Create a monitor nested to parent")
-    parser.add_argument("-c", "--container", dest="container",
-                        action="store_true", required=False,
-                        help="Create an empty monitor to be used as a container")
+
+    subparsers = parser.add_subparsers(dest="subcmd", required=True)
+
+    monitor_parser = subparsers.add_parser("monitor")
+    monitor_parser.add_argument('-n', "--model_name", dest="model_name")
+    monitor_parser.add_argument("-p", "--parent", dest="parent",
+                                required=False, help="Create a monitor nested to parent")
+    monitor_parser.add_argument('-d', "--dot", dest="dot_file")
+    monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
+                                help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
+
+    container_parser = subparsers.add_parser("container")
+    container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+
     params = parser.parse_args()
 
-    if not is_container():
-        print("Opening and parsing the dot file %s" % params.dot_file)
     try:
-        monitor=dot2k(params.dot_file, params.monitor_type, vars(params))
+        if params.subcmd == "monitor":
+            print("Opening and parsing the dot file %s" % params.dot_file)
+            monitor = dot2k(params.dot_file, params.monitor_type, vars(params))
+        else:
+            monitor = dot2k(None, None, vars(params))
     except Exception as e:
         print('Error: '+ str(e))
         print("Sorry : :-(")
@@ -45,7 +48,7 @@ if __name__ == '__main__':
     print("Writing the monitor into the directory %s" % monitor.name)
     monitor.print_files()
     print("Almost done, checklist")
-    if not is_container():
+    if params.subcmd == "monitor":
         print("  - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name))
         print(monitor.fill_tracepoint_tooltip())
     print(monitor.fill_makefile_tooltip())
-- 
2.39.5

[PATCH v2 08/22] rv: rename CONFIG_DA_MON_EVENTS to CONFIG_RV_MON_EVENTS

[Nam Cao]

CONFIG_DA_MON_EVENTS is not specific to deterministic automaton. It could
be used for other monitor types. Therefore rename it to
CONFIG_RV_MON_EVENTS.

This prepares for the introduction of linear temporal logic monitor.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 kernel/trace/rv/Kconfig | 6 +++---
 kernel/trace/rv/rv.c    | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index b39f36013ef2..6cdffc04b73c 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -1,14 +1,14 @@
 # SPDX-License-Identifier: GPL-2.0-only
 #
-config DA_MON_EVENTS
+config RV_MON_EVENTS
 	bool
 
 config DA_MON_EVENTS_IMPLICIT
-	select DA_MON_EVENTS
+	select RV_MON_EVENTS
 	bool
 
 config DA_MON_EVENTS_ID
-	select DA_MON_EVENTS
+	select RV_MON_EVENTS
 	bool
 
 menuconfig RV
diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
index 544acb1f6a33..d493fddf411f 100644
--- a/kernel/trace/rv/rv.c
+++ b/kernel/trace/rv/rv.c
@@ -143,7 +143,7 @@
 #include <linux/init.h>
 #include <linux/slab.h>
 
-#ifdef CONFIG_DA_MON_EVENTS
+#ifdef CONFIG_RV_MON_EVENTS
 #define CREATE_TRACE_POINTS
 #include <rv_trace.h>
 #endif
-- 
2.39.5

[PATCH v2 09/22] verification/dot2k: Prepare the frontend for LTL inclusion

[Nam Cao]

The dot2k tool has some code that can be reused for linear temporal logic
monitor. Prepare its frontend for LTL inclusion:

  1. Rename to be generic: rvgen

  2. Replace the parameter --dot with 2 parameters:
     --class: to specific the monitor class, can be 'da' or 'ltl'
     --spec: the monitor specification file, .dot file for DA, and .ltl
             file for LTL

The old command:

  python3 dot2/dot2k monitor -d wip.dot -t per_cpu

is equivalent to the new commands:

  python3 dot2/dot2k monitor -c da -s wip.dot -t per_cpu

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/{dot2 => rvgen}/Makefile    | 10 +++++-----
 .../{dot2/dot2k => rvgen/__main__.py}          | 18 +++++++++++++-----
 tools/verification/{dot2 => rvgen}/dot2c       |  2 +-
 .../{dot2 => rvgen}/dot2k_templates/Kconfig    |  0
 .../dot2k_templates/Kconfig_container          |  0
 .../{dot2 => rvgen}/dot2k_templates/main.c     |  0
 .../dot2k_templates/main_container.c           |  0
 .../dot2k_templates/main_container.h           |  0
 .../{dot2 => rvgen}/dot2k_templates/trace.h    |  0
 .../{dot2/dot2 => rvgen/rvgen}/automata.py     |  0
 .../{dot2/dot2 => rvgen/rvgen}/dot2c.py        |  2 +-
 .../{dot2/dot2 => rvgen/rvgen}/dot2k.py        | 10 +++++-----
 12 files changed, 25 insertions(+), 17 deletions(-)
 rename tools/verification/{dot2 => rvgen}/Makefile (55%)
 rename tools/verification/{dot2/dot2k => rvgen/__main__.py} (72%)
 rename tools/verification/{dot2 => rvgen}/dot2c (97%)
 rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig (100%)
 rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig_container (100%)
 rename tools/verification/{dot2 => rvgen}/dot2k_templates/main.c (100%)
 rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.c (100%)
 rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.h (100%)
 rename tools/verification/{dot2 => rvgen}/dot2k_templates/trace.h (100%)
 rename tools/verification/{dot2/dot2 => rvgen/rvgen}/automata.py (100%)
 rename tools/verification/{dot2/dot2 => rvgen/rvgen}/dot2c.py (99%)
 rename tools/verification/{dot2/dot2 => rvgen/rvgen}/dot2k.py (98%)

diff --git a/tools/verification/dot2/Makefile b/tools/verification/rvgen/Makefile
similarity index 55%
rename from tools/verification/dot2/Makefile
rename to tools/verification/rvgen/Makefile
index 7a2ec30014b0..cea9c21c3bce 100644
--- a/tools/verification/dot2/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -3,7 +3,7 @@ INSTALL=install
 prefix  ?= /usr
 bindir  ?= $(prefix)/bin
 mandir  ?= $(prefix)/share/man
-miscdir ?= $(prefix)/share/dot2
+miscdir ?= $(prefix)/share/rvgen
 srcdir  ?= $(prefix)/src
 
 PYLIB  ?= $(shell python3 -c 'import sysconfig;  print (sysconfig.get_path("purelib"))')
@@ -16,11 +16,11 @@ clean:
 
 .PHONY: install
 install:
-	$(INSTALL) dot2/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
-	$(INSTALL) dot2/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
+	$(INSTALL) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.py
+	$(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py
 	$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
-	$(INSTALL) dot2/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py
-	$(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/
+	$(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
+	$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
 
 	mkdir -p ${miscdir}/
 	cp -rp dot2k_templates $(DESTDIR)$(miscdir)/
diff --git a/tools/verification/dot2/dot2k b/tools/verification/rvgen/__main__.py
similarity index 72%
rename from tools/verification/dot2/dot2k
rename to tools/verification/rvgen/__main__.py
index 133fb17d9d47..994d320ad2d1 100644
--- a/tools/verification/dot2/dot2k
+++ b/tools/verification/rvgen/__main__.py
@@ -9,11 +9,11 @@
 #   Documentation/trace/rv/da_monitor_synthesis.rst
 
 if __name__ == '__main__':
-    from dot2.dot2k import dot2k
+    from rvgen.dot2k import dot2k
     import argparse
     import sys
 
-    parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor')
+    parser = argparse.ArgumentParser(description='Generate kernel rv monitor')
     parser.add_argument("-D", "--description", dest="description", required=False)
     parser.add_argument("-a", "--auto_patch", dest="auto_patch",
                         action="store_true", required=False,
@@ -25,7 +25,9 @@ if __name__ == '__main__':
     monitor_parser.add_argument('-n', "--model_name", dest="model_name")
     monitor_parser.add_argument("-p", "--parent", dest="parent",
                                 required=False, help="Create a monitor nested to parent")
-    monitor_parser.add_argument('-d', "--dot", dest="dot_file")
+    monitor_parser.add_argument('-c', "--class", dest="monitor_class",
+                                help="Monitor class, either \"da\" or \"ltl\"")
+    monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
     monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
                                 help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
 
@@ -36,8 +38,14 @@ if __name__ == '__main__':
 
     try:
         if params.subcmd == "monitor":
-            print("Opening and parsing the dot file %s" % params.dot_file)
-            monitor = dot2k(params.dot_file, params.monitor_type, vars(params))
+            print("Opening and parsing the specification file %s" % params.spec)
+            if params.monitor_class == "da":
+                monitor = dot2k(params.spec, params.monitor_type, vars(params))
+            elif params.monitor_class == "ltl":
+                raise NotImplementedError
+            else:
+                print("Unknown monitor class:", params.monitor_class)
+                sys.exit(1)
         else:
             monitor = dot2k(None, None, vars(params))
     except Exception as e:
diff --git a/tools/verification/dot2/dot2c b/tools/verification/rvgen/dot2c
similarity index 97%
rename from tools/verification/dot2/dot2c
rename to tools/verification/rvgen/dot2c
index 3fe89ab88b65..bf0c67c5b66c 100644
--- a/tools/verification/dot2/dot2c
+++ b/tools/verification/rvgen/dot2c
@@ -14,7 +14,7 @@
 #   Documentation/trace/rv/deterministic_automata.rst
 
 if __name__ == '__main__':
-    from dot2 import dot2c
+    from rvgen import dot2c
     import argparse
     import sys
 
diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verification/rvgen/dot2k_templates/Kconfig
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/Kconfig
rename to tools/verification/rvgen/dot2k_templates/Kconfig
diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/tools/verification/rvgen/dot2k_templates/Kconfig_container
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/Kconfig_container
rename to tools/verification/rvgen/dot2k_templates/Kconfig_container
diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verification/rvgen/dot2k_templates/main.c
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main.c
rename to tools/verification/rvgen/dot2k_templates/main.c
diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/tools/verification/rvgen/dot2k_templates/main_container.c
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main_container.c
rename to tools/verification/rvgen/dot2k_templates/main_container.c
diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/tools/verification/rvgen/dot2k_templates/main_container.h
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main_container.h
rename to tools/verification/rvgen/dot2k_templates/main_container.h
diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verification/rvgen/dot2k_templates/trace.h
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/trace.h
rename to tools/verification/rvgen/dot2k_templates/trace.h
diff --git a/tools/verification/dot2/dot2/automata.py b/tools/verification/rvgen/rvgen/automata.py
similarity index 100%
rename from tools/verification/dot2/dot2/automata.py
rename to tools/verification/rvgen/rvgen/automata.py
diff --git a/tools/verification/dot2/dot2/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
similarity index 99%
rename from tools/verification/dot2/dot2/dot2c.py
rename to tools/verification/rvgen/rvgen/dot2c.py
index fa2816ac7b61..6009caf568d9 100644
--- a/tools/verification/dot2/dot2/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -13,7 +13,7 @@
 # For further information, see:
 #   Documentation/trace/rv/deterministic_automata.rst
 
-from dot2.automata import Automata
+from .automata import Automata
 
 class Dot2c(Automata):
     enum_suffix = ""
diff --git a/tools/verification/dot2/dot2/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
similarity index 98%
rename from tools/verification/dot2/dot2/dot2k.py
rename to tools/verification/rvgen/rvgen/dot2k.py
index 9ec99e297012..e29462413194 100644
--- a/tools/verification/dot2/dot2/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -8,13 +8,13 @@
 # For further information, see:
 #   Documentation/trace/rv/da_monitor_synthesis.rst
 
-from dot2.dot2c import Dot2c
+from .dot2c import Dot2c
 import platform
 import os
 
 class dot2k(Dot2c):
     monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
-    monitor_templates_dir = "dot2/dot2k_templates/"
+    monitor_templates_dir = "rvgen/dot2k_templates/"
     rv_dir = "kernel/trace/rv"
     monitor_type = "per_cpu"
 
@@ -60,14 +60,14 @@ class dot2k(Dot2c):
         if platform.system() != "Linux":
             raise OSError("I can only run on Linux.")
 
-        kernel_path = "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % (platform.release())
+        kernel_path = "/lib/modules/%s/build/tools/verification/rvgen/dot2k_templates/" % (platform.release())
 
         if os.path.exists(kernel_path):
             self.monitor_templates_dir = kernel_path
             return
 
-        if os.path.exists("/usr/share/dot2/dot2k_templates/"):
-            self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/"
+        if os.path.exists("/usr/share/rvgen/dot2k_templates/"):
+            self.monitor_templates_dir = "/usr/share/rvgen/dot2k_templates/"
             return
 
         raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")
-- 
2.39.5

[PATCH v2 10/22] Documentation/rv: Prepare monitor synthesis document for LTL inclusion

[Nam Cao]

Monitor synthesis from deterministic automaton and linear temporal logic
have a lot in common. Therefore a single document should describe both.

Change da_monitor_synthesis.rst to monitor_synthesis.rst. LTL monitor
synthesis will be added to this file by a follow-up commit.

This makes the diff far easier to read. If renaming and adding LTL info is
done in a single commit, git wouldn't recognize it as a rename, but a file
removal and a file addition.

While at it, correct the old dot2k commands to the new rvgen commands.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 Documentation/trace/rv/index.rst              |  2 +-
 ...or_synthesis.rst => monitor_synthesis.rst} | 20 +++++++++----------
 2 files changed, 11 insertions(+), 11 deletions(-)
 rename Documentation/trace/rv/{da_monitor_synthesis.rst => monitor_synthesis.rst} (92%)

diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst
index e80e0057feb4..8e411b76ec82 100644
--- a/Documentation/trace/rv/index.rst
+++ b/Documentation/trace/rv/index.rst
@@ -8,7 +8,7 @@ Runtime Verification
 
    runtime-verification.rst
    deterministic_automata.rst
-   da_monitor_synthesis.rst
+   monitor_synthesis.rst
    da_monitor_instrumentation.rst
    monitor_wip.rst
    monitor_wwnr.rst
diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst b/Documentation/trace/rv/monitor_synthesis.rst
similarity index 92%
rename from Documentation/trace/rv/da_monitor_synthesis.rst
rename to Documentation/trace/rv/monitor_synthesis.rst
index 0a92729c8a9b..7d848e204687 100644
--- a/Documentation/trace/rv/da_monitor_synthesis.rst
+++ b/Documentation/trace/rv/monitor_synthesis.rst
@@ -1,5 +1,5 @@
-Deterministic Automata Monitor Synthesis
-========================================
+Runtime verification Monitor Synthesis
+======================================
 
 The starting point for the application of runtime verification (RV) techniques
 is the *specification* or *modeling* of the desired (or undesired) behavior
@@ -36,24 +36,24 @@ below::
                                   |  +----> panic ?
                                   +-------> <user-specified>
 
-DA monitor synthesis
+RV monitor synthesis
 --------------------
 
 The synthesis of automata-based models into the Linux *RV monitor* abstraction
-is automated by the dot2k tool and the rv/da_monitor.h header file that
+is automated by the rvgen tool and the rv/da_monitor.h header file that
 contains a set of macros that automatically generate the monitor's code.
 
-dot2k
+rvgen
 -----
 
-The dot2k utility leverages dot2c by converting an automaton model in
+The rvgen utility leverages dot2c by converting an automaton model in
 the DOT format into the C representation [1] and creating the skeleton of
 a kernel monitor in C.
 
 For example, it is possible to transform the wip.dot model present in
 [1] into a per-cpu monitor with the following command::
 
-  $ dot2k -d wip.dot -t per_cpu
+  $ rvgen monitor -c da -s wip.dot -t per_cpu
 
 This will create a directory named wip/ with the following files:
 
@@ -87,7 +87,7 @@ the second for monitors with per-cpu instances, and the third with per-task
 instances.
 
 In all cases, the 'name' argument is a string that identifies the monitor, and
-the 'type' argument is the data type used by dot2k on the representation of
+the 'type' argument is the data type used by rvgen on the representation of
 the model in C.
 
 For example, the wip model with two states and three events can be
@@ -134,7 +134,7 @@ Final remarks
 -------------
 
 With the monitor synthesis in place using the rv/da_monitor.h and
-dot2k, the developer's work should be limited to the instrumentation
+rvgen, the developer's work should be limited to the instrumentation
 of the system, increasing the confidence in the overall approach.
 
 [1] For details about deterministic automata format and the translation
@@ -142,6 +142,6 @@ from one representation to another, see::
 
   Documentation/trace/rv/deterministic_automata.rst
 
-[2] dot2k appends the monitor's name suffix to the events enums to
+[2] rvgen appends the monitor's name suffix to the events enums to
 avoid conflicting variables when exporting the global vmlinux.h
 use by BPF programs.
-- 
2.39.5

[PATCH v2 11/22] verification/rvgen: Prepare the templates for LTL inclusion

[Nam Cao]

To prepare for the inclusion of linear temporal logic monitor, prepare the
generation template files:

  - Rename the directory dot2k_templates to templates
  - Move the dot2k-specific files to templates/dot2k
  - Move the container-specific files to templates/container

(Kconfig can be shared with LTL, therefore leave it at templates/)

This new structure allows sharing code for reading Kconfig and main.c
templates between DA monitor, container monitor and LTL monitor.

The intention is to add template files for LTL to templates/ltl.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/Makefile             |  2 +-
 tools/verification/rvgen/rvgen/dot2k.py       | 33 +++++++++++++------
 .../{dot2k_templates => templates}/Kconfig    |  0
 .../container/Kconfig}                        |  0
 .../container/main.c}                         |  0
 .../container/main.h}                         |  0
 .../dot2k}/main.c                             |  0
 .../dot2k}/trace.h                            |  0
 8 files changed, 24 insertions(+), 11 deletions(-)
 rename tools/verification/rvgen/{dot2k_templates => templates}/Kconfig (100%)
 rename tools/verification/rvgen/{dot2k_templates/Kconfig_container => templates/container/Kconfig} (100%)
 rename tools/verification/rvgen/{dot2k_templates/main_container.c => templates/container/main.c} (100%)
 rename tools/verification/rvgen/{dot2k_templates/main_container.h => templates/container/main.h} (100%)
 rename tools/verification/rvgen/{dot2k_templates => templates/dot2k}/main.c (100%)
 rename tools/verification/rvgen/{dot2k_templates => templates/dot2k}/trace.h (100%)

diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
index cea9c21c3bce..c1a34fa49619 100644
--- a/tools/verification/rvgen/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -23,4 +23,4 @@ install:
 	$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
 
 	mkdir -p ${miscdir}/
-	cp -rp dot2k_templates $(DESTDIR)$(miscdir)/
+	cp -rp templates $(DESTDIR)$(miscdir)/
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e29462413194..ed40a2071ddc 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -14,13 +14,16 @@ import os
 
 class dot2k(Dot2c):
     monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
-    monitor_templates_dir = "rvgen/dot2k_templates/"
     rv_dir = "kernel/trace/rv"
     monitor_type = "per_cpu"
 
     def __init__(self, file_path, MonitorType, extra_params={}):
         self.container = extra_params.get("subcmd") == "container"
         self.parent = extra_params.get("parent")
+        if self.container:
+            self.monitor_templates_dir = "rvgen/templates/container"
+        else:
+            self.monitor_templates_dir = "rvgen/templates/dot2k"
         self.__fill_rv_templates_dir()
 
         if self.container:
@@ -33,9 +36,7 @@ class dot2k(Dot2c):
             self.name = extra_params.get("model_name")
             self.events = []
             self.states = []
-            self.main_c = self.__read_file(self.monitor_templates_dir + "main_container.c")
-            self.main_h = self.__read_file(self.monitor_templates_dir + "main_container.h")
-            self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig_container")
+            self.main_h = self._read_template_file("main.h")
         else:
             super().__init__(file_path, extra_params.get("model_name"))
 
@@ -43,9 +44,10 @@ class dot2k(Dot2c):
             if self.monitor_type is None:
                 raise ValueError("Unknown monitor type: %s" % MonitorType)
             self.monitor_type = MonitorType
-            self.main_c = self.__read_file(self.monitor_templates_dir + "main.c")
-            self.trace_h = self.__read_file(self.monitor_templates_dir + "trace.h")
-            self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig")
+            self.trace_h = self._read_template_file("trace.h")
+
+        self.main_c = self._read_template_file("main.c")
+        self.kconfig = self._read_template_file("Kconfig")
         self.enum_suffix = "_%s" % self.name
         self.description = extra_params.get("description", self.name) or "auto-generated"
         self.auto_patch = extra_params.get("auto_patch")
@@ -60,14 +62,15 @@ class dot2k(Dot2c):
         if platform.system() != "Linux":
             raise OSError("I can only run on Linux.")
 
-        kernel_path = "/lib/modules/%s/build/tools/verification/rvgen/dot2k_templates/" % (platform.release())
+        kernel_path = "/lib/modules/%s/build/tools/verification/%s/" \
+                      % (platform.release(), self.monitor_templates_dir)
 
         if os.path.exists(kernel_path):
             self.monitor_templates_dir = kernel_path
             return
 
-        if os.path.exists("/usr/share/rvgen/dot2k_templates/"):
-            self.monitor_templates_dir = "/usr/share/rvgen/dot2k_templates/"
+        if os.path.exists("/usr/share/%s/" % self.monitor_templates_dir):
+            self.monitor_templates_dir = "/usr/share/%s/" % self.monitor_templates_dir
             return
 
         raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")
@@ -109,6 +112,16 @@ class dot2k(Dot2c):
         fd.close()
         return content
 
+    def _read_template_file(self, file):
+        try:
+            path = os.path.join(self.monitor_templates_dir, file)
+            return self.__read_file(path)
+        except Exception:
+            # Specific template file not found. Try the generic template file in the template/
+            # directory, which is one level up
+            path = os.path.join(self.monitor_templates_dir, "..", file)
+            return self.__read_file(path)
+
     def fill_monitor_type(self):
         return self.monitor_type.upper()
 
diff --git a/tools/verification/rvgen/dot2k_templates/Kconfig b/tools/verification/rvgen/templates/Kconfig
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/Kconfig
rename to tools/verification/rvgen/templates/Kconfig
diff --git a/tools/verification/rvgen/dot2k_templates/Kconfig_container b/tools/verification/rvgen/templates/container/Kconfig
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/Kconfig_container
rename to tools/verification/rvgen/templates/container/Kconfig
diff --git a/tools/verification/rvgen/dot2k_templates/main_container.c b/tools/verification/rvgen/templates/container/main.c
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/main_container.c
rename to tools/verification/rvgen/templates/container/main.c
diff --git a/tools/verification/rvgen/dot2k_templates/main_container.h b/tools/verification/rvgen/templates/container/main.h
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/main_container.h
rename to tools/verification/rvgen/templates/container/main.h
diff --git a/tools/verification/rvgen/dot2k_templates/main.c b/tools/verification/rvgen/templates/dot2k/main.c
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/main.c
rename to tools/verification/rvgen/templates/dot2k/main.c
diff --git a/tools/verification/rvgen/dot2k_templates/trace.h b/tools/verification/rvgen/templates/dot2k/trace.h
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/trace.h
rename to tools/verification/rvgen/templates/dot2k/trace.h
-- 
2.39.5

[PATCH v2 12/22] verification/rvgen: Restructure the classes to prepare for LTL inclusion

[Nam Cao]

Both container generation and DA monitor generation is implemented in the
class dot2k. That requires some ugly "if is_container ... else ...". If
linear temporal logic support is added at the current state, the "if else"
chain is longer and uglier.

Furthermore, container generation is irrevelant to .dot files. It is
therefore illogical to be implemented in class "dot2k".

Clean it up, restructure the dot2k class into the following class
hierarchy:

         (RVGenerator)
              /\
             /  \
            /    \
           /      \
          /        \
    (Container)  (Monitor)
                    /\
                   /  \
                  /    \
                 /      \
              (dot2k)  [ltl2k] <- intended

This allows a simple and clean integration of LTL.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/Makefile           |   2 +
 tools/verification/rvgen/__main__.py        |   6 +-
 tools/verification/rvgen/rvgen/container.py |  22 ++
 tools/verification/rvgen/rvgen/dot2k.py     | 297 ++------------------
 tools/verification/rvgen/rvgen/generator.py | 284 +++++++++++++++++++
 5 files changed, 328 insertions(+), 283 deletions(-)
 create mode 100644 tools/verification/rvgen/rvgen/container.py
 create mode 100644 tools/verification/rvgen/rvgen/generator.py

diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
index c1a34fa49619..b86c35eea4a4 100644
--- a/tools/verification/rvgen/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -20,6 +20,8 @@ install:
 	$(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py
 	$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
 	$(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
+	$(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py
+	$(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py
 	$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
 
 	mkdir -p ${miscdir}/
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 994d320ad2d1..63ecf0c37034 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -10,6 +10,8 @@
 
 if __name__ == '__main__':
     from rvgen.dot2k import dot2k
+    from rvgen.generator import Monitor
+    from rvgen.container import Container
     import argparse
     import sys
 
@@ -29,7 +31,7 @@ if __name__ == '__main__':
                                 help="Monitor class, either \"da\" or \"ltl\"")
     monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
     monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
-                                help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
+                                help=f"Available options: {', '.join(Monitor.monitor_types.keys())}")
 
     container_parser = subparsers.add_parser("container")
     container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
@@ -47,7 +49,7 @@ if __name__ == '__main__':
                 print("Unknown monitor class:", params.monitor_class)
                 sys.exit(1)
         else:
-            monitor = dot2k(None, None, vars(params))
+            monitor = Container(vars(params))
     except Exception as e:
         print('Error: '+ str(e))
         print("Sorry : :-(")
diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py
new file mode 100644
index 000000000000..b8b482ea6e4b
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/container.py
@@ -0,0 +1,22 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# Generator for runtime verification monitor container
+
+from . import generator
+
+
+class Container(generator.RVGenerator):
+    monitor_templates_dir = "rvgen/templates/container"
+
+    def __init__(self, extra_params={}):
+        super().__init__(extra_params)
+        self.name = extra_params.get("model_name")
+        self.main_h = self._read_template_file("main.h")
+
+    def fill_model_h(self):
+        main_h = self.main_h
+        main_h = main_h.replace("%%MODEL_NAME%%", self.name)
+        return main_h
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index ed40a2071ddc..9b2ac9735449 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -9,130 +9,21 @@
 #   Documentation/trace/rv/da_monitor_synthesis.rst
 
 from .dot2c import Dot2c
-import platform
-import os
+from .generator import Monitor
 
-class dot2k(Dot2c):
-    monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
-    rv_dir = "kernel/trace/rv"
-    monitor_type = "per_cpu"
 
-    def __init__(self, file_path, MonitorType, extra_params={}):
-        self.container = extra_params.get("subcmd") == "container"
-        self.parent = extra_params.get("parent")
-        if self.container:
-            self.monitor_templates_dir = "rvgen/templates/container"
-        else:
-            self.monitor_templates_dir = "rvgen/templates/dot2k"
-        self.__fill_rv_templates_dir()
-
-        if self.container:
-            if file_path:
-                raise ValueError("A container does not require a dot file")
-            if MonitorType:
-                raise ValueError("A container does not require a monitor type")
-            if self.parent:
-                raise ValueError("A container cannot have a parent")
-            self.name = extra_params.get("model_name")
-            self.events = []
-            self.states = []
-            self.main_h = self._read_template_file("main.h")
-        else:
-            super().__init__(file_path, extra_params.get("model_name"))
-
-            self.monitor_type = self.monitor_types.get(MonitorType)
-            if self.monitor_type is None:
-                raise ValueError("Unknown monitor type: %s" % MonitorType)
-            self.monitor_type = MonitorType
-            self.trace_h = self._read_template_file("trace.h")
+class dot2k(Monitor, Dot2c):
+    monitor_templates_dir = "rvgen/templates/dot2k"
 
-        self.main_c = self._read_template_file("main.c")
-        self.kconfig = self._read_template_file("Kconfig")
+    def __init__(self, file_path, MonitorType, extra_params={}):
+        self.monitor_type = MonitorType
+        Monitor.__init__(self, extra_params)
+        Dot2c.__init__(self, file_path, extra_params.get("model_name"))
         self.enum_suffix = "_%s" % self.name
-        self.description = extra_params.get("description", self.name) or "auto-generated"
-        self.auto_patch = extra_params.get("auto_patch")
-        if self.auto_patch:
-            self.__fill_rv_kernel_dir()
-
-    def __fill_rv_templates_dir(self):
-
-        if os.path.exists(self.monitor_templates_dir):
-            return
-
-        if platform.system() != "Linux":
-            raise OSError("I can only run on Linux.")
-
-        kernel_path = "/lib/modules/%s/build/tools/verification/%s/" \
-                      % (platform.release(), self.monitor_templates_dir)
-
-        if os.path.exists(kernel_path):
-            self.monitor_templates_dir = kernel_path
-            return
-
-        if os.path.exists("/usr/share/%s/" % self.monitor_templates_dir):
-            self.monitor_templates_dir = "/usr/share/%s/" % self.monitor_templates_dir
-            return
-
-        raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")
-
-    def __fill_rv_kernel_dir(self):
-
-        # first try if we are running in the kernel tree root
-        if os.path.exists(self.rv_dir):
-            return
-
-        # offset if we are running inside the kernel tree from verification/dot2
-        kernel_path = os.path.join("../..", self.rv_dir)
-
-        if os.path.exists(kernel_path):
-            self.rv_dir = kernel_path
-            return
-
-        if platform.system() != "Linux":
-            raise OSError("I can only run on Linux.")
-
-        kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir)
-
-        # if the current kernel is from a distro this may not be a full kernel tree
-        # verify that one of the files we are going to modify is available
-        if os.path.exists(os.path.join(kernel_path, "rv_trace.h")):
-            self.rv_dir = kernel_path
-            return
-
-        raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
-
-    def __read_file(self, path):
-        try:
-            fd = open(path, 'r')
-        except OSError:
-            raise Exception("Cannot open the file: %s" % path)
-
-        content = fd.read()
-
-        fd.close()
-        return content
-
-    def _read_template_file(self, file):
-        try:
-            path = os.path.join(self.monitor_templates_dir, file)
-            return self.__read_file(path)
-        except Exception:
-            # Specific template file not found. Try the generic template file in the template/
-            # directory, which is one level up
-            path = os.path.join(self.monitor_templates_dir, "..", file)
-            return self.__read_file(path)
 
     def fill_monitor_type(self):
         return self.monitor_type.upper()
 
-    def fill_parent(self):
-        return "&rv_%s" % self.parent if self.parent else "NULL"
-
-    def fill_include_parent(self):
-        if self.parent:
-            return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent)
-        return ""
-
     def fill_tracepoint_handlers_skel(self):
         buff = []
         for event in self.events:
@@ -166,30 +57,6 @@ class dot2k(Dot2c):
             buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
         return '\n'.join(buff)
 
-    def fill_main_c(self):
-        main_c = self.main_c
-        monitor_type = self.fill_monitor_type()
-        min_type = self.get_minimun_type()
-        nr_events = len(self.events)
-        tracepoint_handlers = self.fill_tracepoint_handlers_skel()
-        tracepoint_attach = self.fill_tracepoint_attach_probe()
-        tracepoint_detach = self.fill_tracepoint_detach_helper()
-        parent = self.fill_parent()
-        parent_include = self.fill_include_parent()
-
-        main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type)
-        main_c = main_c.replace("%%MIN_TYPE%%", min_type)
-        main_c = main_c.replace("%%MODEL_NAME%%", self.name)
-        main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events))
-        main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers)
-        main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach)
-        main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach)
-        main_c = main_c.replace("%%DESCRIPTION%%", self.description)
-        main_c = main_c.replace("%%PARENT%%", parent)
-        main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include)
-
-        return main_c
-
     def fill_model_h_header(self):
         buff = []
         buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
@@ -248,147 +115,15 @@ class dot2k(Dot2c):
         buff.append("	     TP_ARGS(%s)" % tp_args_c)
         return '\n'.join(buff)
 
-    def fill_monitor_deps(self):
-        buff = []
-        buff.append("	# XXX: add dependencies if there")
-        if self.parent:
-            buff.append("	depends on RV_MON_%s" % self.parent.upper())
-            buff.append("	default y")
-        return '\n'.join(buff)
-
-    def fill_trace_h(self):
-        trace_h = self.trace_h
-        monitor_class = self.fill_monitor_class()
-        monitor_class_type = self.fill_monitor_class_type()
-        tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event")
-        tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error")
-        trace_h = trace_h.replace("%%MODEL_NAME%%", self.name)
-        trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper())
-        trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class)
-        trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
-        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event)
-        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error)
-        return trace_h
-
-    def fill_kconfig(self):
-        kconfig = self.kconfig
-        monitor_class_type = self.fill_monitor_class_type()
-        monitor_deps = self.fill_monitor_deps()
-        kconfig = kconfig.replace("%%MODEL_NAME%%", self.name)
-        kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper())
-        kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
-        kconfig = kconfig.replace("%%DESCRIPTION%%", self.description)
-        kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps)
-        return kconfig
-
-    def fill_main_container_h(self):
-        main_h = self.main_h
-        main_h = main_h.replace("%%MODEL_NAME%%", self.name)
-        return main_h
-
-    def __patch_file(self, file, marker, line):
-        file_to_patch = os.path.join(self.rv_dir, file)
-        content = self.__read_file(file_to_patch)
-        content = content.replace(marker, line + "\n" + marker)
-        self.__write_file(file_to_patch, content)
-
-    def fill_tracepoint_tooltip(self):
-        monitor_class_type = self.fill_monitor_class_type()
-        if self.auto_patch:
-            self.__patch_file("rv_trace.h",
-                            "// Add new monitors based on CONFIG_%s here" % monitor_class_type,
-                            "#include <monitors/%s/%s_trace.h>" % (self.name, self.name))
-            return "  - Patching %s/rv_trace.h, double check the result" % self.rv_dir
-
-        return """  - Edit %s/rv_trace.h:
-Add this line where other tracepoints are included and %s is defined:
-#include <monitors/%s/%s_trace.h>
-""" % (self.rv_dir, monitor_class_type, self.name, self.name)
-
-    def fill_kconfig_tooltip(self):
-        if self.auto_patch:
-            self.__patch_file("Kconfig",
-                            "# Add new monitors here",
-                            "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name))
-            return "  - Patching %s/Kconfig, double check the result" % self.rv_dir
-
-        return """  - Edit %s/Kconfig:
-Add this line where other monitors are included:
-source \"kernel/trace/rv/monitors/%s/Kconfig\"
-""" % (self.rv_dir, self.name)
-
-    def fill_makefile_tooltip(self):
-        name = self.name
-        name_up = name.upper()
-        if self.auto_patch:
-            self.__patch_file("Makefile",
-                            "# Add new monitors here",
-                            "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name))
-            return "  - Patching %s/Makefile, double check the result" % self.rv_dir
-
-        return """  - Edit %s/Makefile:
-Add this line where other monitors are included:
-obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
-""" % (self.rv_dir, name_up, name, name)
-
-    def fill_monitor_tooltip(self):
-        if self.auto_patch:
-            return "  - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name)
-        return "  - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir)
-
-    def __create_directory(self):
-        path = self.name
-        if self.auto_patch:
-            path = os.path.join(self.rv_dir, "monitors", path)
-        try:
-            os.mkdir(path)
-        except FileExistsError:
-            return
-        except:
-            print("Fail creating the output dir: %s" % self.name)
-
-    def __write_file(self, file_name, content):
-        try:
-            file = open(file_name, 'w')
-        except:
-            print("Fail writing to file: %s" % file_name)
-
-        file.write(content)
-
-        file.close()
-
-    def __create_file(self, file_name, content):
-        path = "%s/%s" % (self.name, file_name)
-        if self.auto_patch:
-            path = os.path.join(self.rv_dir, "monitors", path)
-        self.__write_file(path, content)
-
-    def __get_main_name(self):
-        path = "%s/%s" % (self.name, "main.c")
-        if not os.path.exists(path):
-            return "main.c"
-        return "__main.c"
-
-    def print_files(self):
-        main_c = self.fill_main_c()
-
-        self.__create_directory()
-
-        path = "%s.c" % self.name
-        self.__create_file(path, main_c)
+    def fill_main_c(self):
+        main_c = super().fill_main_c()
 
-        if self.container:
-            main_h = self.fill_main_container_h()
-            path = "%s.h" % self.name
-            self.__create_file(path, main_h)
-        else:
-            model_h = self.fill_model_h()
-            path = "%s.h" % self.name
-            self.__create_file(path, model_h)
+        min_type = self.get_minimun_type()
+        nr_events = len(self.events)
+        monitor_type = self.fill_monitor_type()
 
-            trace_h = self.fill_trace_h()
-            path = "%s_trace.h" % self.name
-            self.__create_file(path, trace_h)
+        main_c = main_c.replace("%%MIN_TYPE%%", min_type)
+        main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events))
+        main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type)
 
-        kconfig = self.fill_kconfig()
-        self.__create_file("Kconfig", kconfig)
+        return main_c
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
new file mode 100644
index 000000000000..2c929342d60f
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -0,0 +1,284 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# Abtract class for generating kernel runtime verification monitors from specification file
+
+import platform
+import os
+
+
+class RVGenerator:
+    rv_dir = "kernel/trace/rv"
+
+    def __init__(self, extra_params={}):
+        self.name = extra_params.get("model_name")
+        self.parent = extra_params.get("parent")
+        self.__fill_rv_templates_dir()
+        self.main_c = self._read_template_file("main.c")
+        self.kconfig = self._read_template_file("Kconfig")
+        self.description = extra_params.get("description", self.name) or "auto-generated"
+        self.auto_patch = extra_params.get("auto_patch")
+        if self.auto_patch:
+            self.__fill_rv_kernel_dir()
+
+    def __fill_rv_templates_dir(self):
+
+        if os.path.exists(self.monitor_templates_dir):
+            return
+
+        if platform.system() != "Linux":
+            raise OSError("I can only run on Linux.")
+
+        kernel_path = "/lib/modules/%s/build/tools/verification/%s/" \
+                      % (platform.release(), self.monitor_templates_dir)
+
+        if os.path.exists(kernel_path):
+            self.monitor_templates_dir = kernel_path
+            return
+
+        if os.path.exists("/usr/share/%s/" % self.monitor_templates_dir):
+            self.monitor_templates_dir = "/usr/share/%s/" % self.monitor_templates_dir
+            return
+
+        raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")
+
+    def __fill_rv_kernel_dir(self):
+
+        # first try if we are running in the kernel tree root
+        if os.path.exists(self.rv_dir):
+            return
+
+        # offset if we are running inside the kernel tree from verification/dot2
+        kernel_path = os.path.join("../..", self.rv_dir)
+
+        if os.path.exists(kernel_path):
+            self.rv_dir = kernel_path
+            return
+
+        if platform.system() != "Linux":
+            raise OSError("I can only run on Linux.")
+
+        kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir)
+
+        # if the current kernel is from a distro this may not be a full kernel tree
+        # verify that one of the files we are going to modify is available
+        if os.path.exists(os.path.join(kernel_path, "rv_trace.h")):
+            self.rv_dir = kernel_path
+            return
+
+        raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
+
+    def _read_file(self, path):
+        try:
+            fd = open(path, 'r')
+        except OSError:
+            raise Exception("Cannot open the file: %s" % path)
+
+        content = fd.read()
+
+        fd.close()
+        return content
+
+    def _read_template_file(self, file):
+        try:
+            path = os.path.join(self.monitor_templates_dir, file)
+            return self._read_file(path)
+        except Exception:
+            # Specific template file not found. Try the generic template file in the template/
+            # directory, which is one level up
+            path = os.path.join(self.monitor_templates_dir, "..", file)
+            return self._read_file(path)
+
+    def fill_parent(self):
+        return "&rv_%s" % self.parent if self.parent else "NULL"
+
+    def fill_include_parent(self):
+        if self.parent:
+            return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent)
+        return ""
+
+    def fill_tracepoint_handlers_skel(self):
+        return "NotImplemented"
+
+    def fill_tracepoint_attach_probe(self):
+        return "NotImplemented"
+
+    def fill_tracepoint_detach_helper(self):
+        return "NotImplemented"
+
+    def fill_main_c(self):
+        main_c = self.main_c
+        tracepoint_handlers = self.fill_tracepoint_handlers_skel()
+        tracepoint_attach = self.fill_tracepoint_attach_probe()
+        tracepoint_detach = self.fill_tracepoint_detach_helper()
+        parent = self.fill_parent()
+        parent_include = self.fill_include_parent()
+
+        main_c = main_c.replace("%%MODEL_NAME%%", self.name)
+        main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers)
+        main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach)
+        main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach)
+        main_c = main_c.replace("%%DESCRIPTION%%", self.description)
+        main_c = main_c.replace("%%PARENT%%", parent)
+        main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include)
+
+        return main_c
+
+    def fill_model_h(self):
+        return "NotImplemented"
+
+    def fill_monitor_class_type(self):
+        return "NotImplemented"
+
+    def fill_monitor_class(self):
+        return "NotImplemented"
+
+    def fill_tracepoint_args_skel(self, tp_type):
+        return "NotImplemented"
+
+    def fill_monitor_deps(self):
+        buff = []
+        buff.append("	# XXX: add dependencies if there")
+        if self.parent:
+            buff.append("	depends on RV_MON_%s" % self.parent.upper())
+            buff.append("	default y")
+        return '\n'.join(buff)
+
+    def fill_kconfig(self):
+        kconfig = self.kconfig
+        monitor_class_type = self.fill_monitor_class_type()
+        monitor_deps = self.fill_monitor_deps()
+        kconfig = kconfig.replace("%%MODEL_NAME%%", self.name)
+        kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper())
+        kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
+        kconfig = kconfig.replace("%%DESCRIPTION%%", self.description)
+        kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps)
+        return kconfig
+
+    def __patch_file(self, file, marker, line):
+        file_to_patch = os.path.join(self.rv_dir, file)
+        content = self._read_file(file_to_patch)
+        content = content.replace(marker, line + "\n" + marker)
+        self.__write_file(file_to_patch, content)
+
+    def fill_tracepoint_tooltip(self):
+        monitor_class_type = self.fill_monitor_class_type()
+        if self.auto_patch:
+            self.__patch_file("rv_trace.h",
+                            "// Add new monitors based on CONFIG_%s here" % monitor_class_type,
+                            "#include <monitors/%s/%s_trace.h>" % (self.name, self.name))
+            return "  - Patching %s/rv_trace.h, double check the result" % self.rv_dir
+
+        return """  - Edit %s/rv_trace.h:
+Add this line where other tracepoints are included and %s is defined:
+#include <monitors/%s/%s_trace.h>
+""" % (self.rv_dir, monitor_class_type, self.name, self.name)
+
+    def fill_kconfig_tooltip(self):
+        if self.auto_patch:
+            self.__patch_file("Kconfig",
+                            "# Add new monitors here",
+                            "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name))
+            return "  - Patching %s/Kconfig, double check the result" % self.rv_dir
+
+        return """  - Edit %s/Kconfig:
+Add this line where other monitors are included:
+source \"kernel/trace/rv/monitors/%s/Kconfig\"
+""" % (self.rv_dir, self.name)
+
+    def fill_makefile_tooltip(self):
+        name = self.name
+        name_up = name.upper()
+        if self.auto_patch:
+            self.__patch_file("Makefile",
+                            "# Add new monitors here",
+                            "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name))
+            return "  - Patching %s/Makefile, double check the result" % self.rv_dir
+
+        return """  - Edit %s/Makefile:
+Add this line where other monitors are included:
+obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
+""" % (self.rv_dir, name_up, name, name)
+
+    def fill_monitor_tooltip(self):
+        if self.auto_patch:
+            return "  - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name)
+        return "  - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir)
+
+    def __create_directory(self):
+        path = self.name
+        if self.auto_patch:
+            path = os.path.join(self.rv_dir, "monitors", path)
+        try:
+            os.mkdir(path)
+        except FileExistsError:
+            return
+        except:
+            print("Fail creating the output dir: %s" % self.name)
+
+    def __write_file(self, file_name, content):
+        try:
+            file = open(file_name, 'w')
+        except:
+            print("Fail writing to file: %s" % file_name)
+
+        file.write(content)
+
+        file.close()
+
+    def _create_file(self, file_name, content):
+        path = "%s/%s" % (self.name, file_name)
+        if self.auto_patch:
+            path = os.path.join(self.rv_dir, "monitors", path)
+        self.__write_file(path, content)
+
+    def __get_main_name(self):
+        path = "%s/%s" % (self.name, "main.c")
+        if not os.path.exists(path):
+            return "main.c"
+        return "__main.c"
+
+    def print_files(self):
+        main_c = self.fill_main_c()
+
+        self.__create_directory()
+
+        path = "%s.c" % self.name
+        self._create_file(path, main_c)
+
+        model_h = self.fill_model_h()
+        path = "%s.h" % self.name
+        self._create_file(path, model_h)
+
+        kconfig = self.fill_kconfig()
+        self._create_file("Kconfig", kconfig)
+
+
+class Monitor(RVGenerator):
+    monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
+
+    def __init__(self, extra_params={}):
+        super().__init__(extra_params)
+        self.trace_h = self._read_template_file("trace.h")
+
+    def fill_trace_h(self):
+        trace_h = self.trace_h
+        monitor_class = self.fill_monitor_class()
+        monitor_class_type = self.fill_monitor_class_type()
+        tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event")
+        tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error")
+        trace_h = trace_h.replace("%%MODEL_NAME%%", self.name)
+        trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper())
+        trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class)
+        trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
+        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event)
+        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error)
+        return trace_h
+
+    def print_files(self):
+        super().print_files()
+        trace_h = self.fill_trace_h()
+        path = "%s_trace.h" % self.name
+        self._create_file(path, trace_h)
-- 
2.39.5

[PATCH v2 13/22] rv: Add support for LTL monitors

[Nam Cao]

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
@@ -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`.
diff --git a/Documentation/trace/rv/monitor_synthesis.rst b/Documentation/trace/rv/monitor_synthesis.rst
index 7d848e204687..94caf66d3ba6 100644
--- a/Documentation/trace/rv/monitor_synthesis.rst
+++ b/Documentation/trace/rv/monitor_synthesis.rst
@@ -39,16 +39,17 @@ below::
 RV monitor synthesis
 --------------------
 
-The synthesis of automata-based models into the Linux *RV monitor* abstraction
-is automated by the rvgen tool and the rv/da_monitor.h header file that
-contains a set of macros that automatically generate the monitor's code.
+The synthesis of a specification into the Linux *RV monitor* abstraction is automated by the rvgen
+tool and the header file containing common code for creating monitors. The header files are:
+
+  * rv/da_monitor.h for deterministic automaton monitor.
+  * rv/ltl_monitor.h for linear temporal logic monitor.
 
 rvgen
 -----
 
-The rvgen utility leverages dot2c by converting an automaton model in
-the DOT format into the C representation [1] and creating the skeleton of
-a kernel monitor in C.
+The rvgen utility converts a specification into the C presentation and creating the skeleton of a
+kernel monitor in C.
 
 For example, it is possible to transform the wip.dot model present in
 [1] into a per-cpu monitor with the following command::
@@ -63,18 +64,34 @@ This will create a directory named wip/ with the following files:
 The wip.c file contains the monitor declaration and the starting point for
 the system instrumentation.
 
-Monitor macros
---------------
+Similarly, a linear temporal logic monitor can be generated with the following command::
+
+  $ rvgen monitor -c ltl -s pagefault.ltl -t per_task
+
+This generates pagefault/ directory with:
+
+- pagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)
+- pagefault.c: The skeleton for the RV monitor
+
+Monitor header files
+--------------------
+
+The header files:
+
+- `rv/da_monitor.h` for deterministic automaton monitor
+- `rv/ltl_monitor` for linear temporal logic monitor
+
+include common macros and static functions for implementing *Monitor Instance(s)*.
 
-The rv/da_monitor.h enables automatic code generation for the *Monitor
-Instance(s)* using C macros.
+The benefits of having all common functionalities in a single header file are 3-fold:
 
-The benefits of the usage of macro for monitor synthesis are 3-fold as it:
+  - Reduce the code duplication;
+  - Facilitate the bug fix/improvement;
+  - Avoid the case of developers changing the core of the monitor code to manipulate the model in a
+    (let's say) non-standard way.
 
-- Reduces the code duplication;
-- Facilitates the bug fix/improvement;
-- Avoids the case of developers changing the core of the monitor code
-  to manipulate the model in a (let's say) non-standard way.
+rv/da_monitor.h
++++++++++++++++
 
 This initial implementation presents three different types of monitor instances:
 
@@ -130,10 +147,102 @@ While the event "preempt_enabled" will use::
 To notify the monitor that the system will be returning to the initial state,
 so the system and the monitor should be in sync.
 
+rv/ltl_monitor.h
+++++++++++++++++
+This file must be combined with the $(MODEL_NAME).h file (generated by `rvgen`) to be complete. For
+example, for the `pagefault` monitor, the `pagefault.c` source file must include::
+
+  #include "pagefault.h"
+  #include <rv/ltl_monitor.h>
+
+(the skeleton monitor file generated by `rvgen` already does this).
+
+`$(MODEL_NAME).h` (`pagefault.h` in the above example) includes the implementation of the Buchi
+automaton - a non-deterministic state machine that verifies the LTL specification. While
+`rv/ltl_monitor.h` includes the common helper functions to interact with the Buchi automaton and to
+implement an RV monitor. An important definition in `$(MODEL_NAME).h` is::
+
+  enum ltl_atom {
+      LTL_$(FIRST_ATOMIC_PROPOSITION),
+      LTL_$(SECOND_ATOMIC_PROPOSITION),
+      ...
+      LTL_NUM_ATOM
+  };
+
+which is the list of atomic propositions present in the LTL specification (prefixed with "LTL\_" to
+avoid name collision). This `enum` is passed to the functions interacting with the Buchi automaton.
+
+While generating code, `rvgen` cannot understand the meaning of the atomic propositions. Thus, that
+task is left for manual work. The recommended pratice is adding tracepoints to places where the
+atomic propositions change; and in the tracepoints' handlers: the Buchi automaton is executed
+using::
+
+  void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)
+
+which tells the Buchi automaton that the atomic proposition `atom` is now `value`. The Buchi
+automaton checks whether the LTL specification is still satisfied, and invokes the monitor's error
+tracepoint and the reactor if violation is detected.
+
+Tracepoints and `ltl_atom_update()` should be used whenever possible. However, it is sometimes not
+the most convenient. For some atomic propositions which are changed in multiple places in the
+kernel, it is cumbersome to trace all those places. Furthermore, it may not be important that the
+atomic propositions are updated at precise times. For example, considering the following linear
+temporal logic::
+
+  RULE = always (RT imply not PAGEFAULT)
+
+This LTL states that a real-time task does not raise page faults. For this specification, it is not
+important when `RT` changes, as long as it has the correct value when `PAGEFAULT` is true.
+Motivated by this case, another function is introduced::
+
+  void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
+
+This function is called whenever the Buchi automaton is triggered. Therefore, it can be manually
+implemented to "fetch" `RT`::
+
+  void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
+  {
+      ltl_atom_set(mon, LTL_RT, rt_task(task));
+  }
+
+Effectively, whenever `PAGEFAULT` is updated with a call to `ltl_atom_update()`, `RT` is also
+fetched. Thus, the LTL specification can be verified without tracing `RT` everywhere.
+
+For atomic propositions which act like events, they usually need to be set (or cleared) and then
+immediately cleared (or set). A convenient function is provided::
+
+  void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)
+
+which is equivalent to::
+
+  ltl_atom_update(task, atom, value);
+  ltl_atom_update(task, atom, !value);
+
+To initialize the atomic propositions, the following function must be implemented::
+
+  ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+
+This function is called for all running tasks when the monitor is enabled. It is also called for new
+tasks created after the enabling the monitor. It should initialize as many atomic propositions as
+possible, for example::
+
+  void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+  {
+      ltl_atom_set(mon, LTL_RT, rt_task(task));
+      if (task_creation)
+          ltl_atom_set(mon, LTL_PAGEFAULT, false);
+  }
+
+Atomic propositions not initialized by `ltl_atom_init()` will stay in the unknown state until
+relevant tracepoints are hit, which can take some time. As monitoring for a task cannot be done
+until all atomic propositions is known for the task, the monitor may need some time to start
+validating tasks which have been running before the monitor is enabled. Therefore, it is recommended
+to start the tasks of interest after enabling the monitor.
+
 Final remarks
 -------------
 
-With the monitor synthesis in place using the rv/da_monitor.h and
+With the monitor synthesis in place using the header files and
 rvgen, the developer's work should be limited to the instrumentation
 of the system, increasing the confidence in the overall approach.
 
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
+};
+
+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
@@ -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;
+}
+
+static void ltl_task_init(struct task_struct *task, bool task_creation)
+{
+	struct ltl_monitor *mon = ltl_get_monitor(task);
+
+	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);
+}
+
+static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags)
+{
+	ltl_task_init(task, true);
+}
+
+static int ltl_monitor_init(void)
+{
+	struct task_struct *g, *p;
+	int ret, cpu;
+
+	ret = rv_get_task_monitor_slot();
+	if (ret < 0)
+		return ret;
+
+	ltl_monitor_slot = ret;
+
+	rv_attach_trace_probe(name, task_newtask, handle_task_newtask);
+
+	read_lock(&tasklist_lock);
+
+	for_each_process_thread(g, p)
+		ltl_task_init(p, false);
+
+	for_each_present_cpu(cpu)
+		ltl_task_init(idle_task(cpu), false);
+
+	read_unlock(&tasklist_lock);
+
+	return 0;
+}
+
+static void ltl_monitor_destroy(void)
+{
+	rv_detach_trace_probe(name, task_newtask, handle_task_newtask);
+
+	rv_put_task_monitor_slot(ltl_monitor_slot);
+	ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
+}
+
+static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+{
+	CONCATENATE(trace_error_, MONITOR_NAME)(task);
+	rv_cond_react(task);
+}
+
+static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	if (rv_ltl_all_atoms_known(mon))
+		ltl_start(task, mon);
+}
+
+static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value)
+{
+	__clear_bit(atom, mon->unknown_atoms);
+	if (value)
+		__set_bit(atom, mon->atoms);
+	else
+		__clear_bit(atom, mon->atoms);
+}
+
+static void
+ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state)
+{
+	const char *format_str = "%s";
+	DECLARE_SEQ_BUF(atoms, 64);
+	char states[32], next[32];
+	int i;
+
+	if (!CONCATENATE(CONCATENATE(trace_event_, MONITOR_NAME), _enabled)())
+		return;
+
+	snprintf(states, sizeof(states), "%*pbl", RV_MAX_BA_STATES, mon->states);
+	snprintf(next, sizeof(next), "%*pbl", RV_MAX_BA_STATES, next_state);
+
+	for (i = 0; i < LTL_NUM_ATOM; ++i) {
+		if (test_bit(i, mon->atoms)) {
+			seq_buf_printf(&atoms, format_str, ltl_atom_str(i));
+			format_str = ",%s";
+		}
+	}
+
+	CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer, next);
+}
+
+static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)
+{
+	DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0};
+
+	if (!rv_ltl_valid_state(mon))
+		return;
+
+	for (unsigned int i = 0; i < RV_NUM_BA_STATES; ++i) {
+		if (test_bit(i, mon->states))
+			ltl_possible_next_states(mon, i, next_states);
+	}
+
+	ltl_trace_event(task, mon, next_states);
+
+	memcpy(mon->states, next_states, sizeof(next_states));
+
+	if (!rv_ltl_valid_state(mon))
+		ltl_illegal_state(task, mon);
+}
+
+static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)
+{
+	struct ltl_monitor *mon = ltl_get_monitor(task);
+
+	ltl_atom_set(mon, atom, value);
+	ltl_atoms_fetch(task, mon);
+
+	if (!rv_ltl_valid_state(mon))
+		ltl_attempt_start(task, mon);
+
+	ltl_validate(task, mon);
+}
+
+static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)
+{
+	struct ltl_monitor *mon = ltl_get_monitor(task);
+
+	ltl_atom_update(task, atom, value);
+
+	ltl_atom_set(mon, atom, !value);
+	ltl_validate(task, mon);
+}
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/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 6cdffc04b73c..6e157f964991 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -11,6 +11,13 @@ config DA_MON_EVENTS_ID
 	select RV_MON_EVENTS
 	bool
 
+config LTL_MON_EVENTS_ID
+	select RV_MON_EVENTS
+	bool
+
+config RV_LTL_MONITOR
+	bool
+
 menuconfig RV
 	bool "Runtime Verification"
 	depends on TRACING
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 99c3801616d4..f9fb848bae91 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -127,6 +127,53 @@ DECLARE_EVENT_CLASS(error_da_monitor_id,
 // Add new monitors based on CONFIG_DA_MON_EVENTS_ID here
 
 #endif /* CONFIG_DA_MON_EVENTS_ID */
+#if CONFIG_LTL_MON_EVENTS_ID
+TRACE_EVENT(event_ltl_monitor_id,
+
+	TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+
+	TP_ARGS(task, states, atoms, next),
+
+	TP_STRUCT__entry(
+		__string(comm, task->comm)
+		__field(pid_t, pid)
+		__string(states, states)
+		__string(atoms, atoms)
+		__string(next, next)
+	),
+
+	TP_fast_assign(
+		__assign_str(comm);
+		__entry->pid = task->pid;
+		__assign_str(states);
+		__assign_str(atoms);
+		__assign_str(next);
+	),
+
+	TP_printk("%s[%d]: (%s) x (%s) -> (%s)", __get_str(comm), __entry->pid, __get_str(states),
+		  __get_str(atoms), __get_str(next))
+);
+
+TRACE_EVENT(error_ltl_monitor_id,
+
+	TP_PROTO(struct task_struct *task),
+
+	TP_ARGS(task),
+
+	TP_STRUCT__entry(
+		__string(comm, task->comm)
+		__field(pid_t, pid)
+	),
+
+	TP_fast_assign(
+		__assign_str(comm);
+		__entry->pid = task->pid;
+	),
+
+	TP_printk("%s[%d]: violation detected", __get_str(comm), __entry->pid)
+);
+// Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here
+#endif /* CONFIG_LTL_MON_EVENTS_ID */
 #endif /* _TRACE_RV_H */
 
 /* This part must be outside protection */
diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore
new file mode 100644
index 000000000000..1e288a076560
--- /dev/null
+++ b/tools/verification/rvgen/.gitignore
@@ -0,0 +1,3 @@
+__pycache__/
+parser.out
+parsetab.py
diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
index b86c35eea4a4..a76a5cdd0c7e 100644
--- a/tools/verification/rvgen/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -22,6 +22,8 @@ install:
 	$(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
 	$(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py
 	$(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py
+	$(INSTALL) rvgen/ltl2ba.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2ba.py
+	$(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py
 	$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
 
 	mkdir -p ${miscdir}/
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 63ecf0c37034..fa6fc1f4de2f 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -12,6 +12,7 @@ if __name__ == '__main__':
     from rvgen.dot2k import dot2k
     from rvgen.generator import Monitor
     from rvgen.container import Container
+    from rvgen.ltl2k import ltl2k
     import argparse
     import sys
 
@@ -44,7 +45,7 @@ if __name__ == '__main__':
             if params.monitor_class == "da":
                 monitor = dot2k(params.spec, params.monitor_type, vars(params))
             elif params.monitor_class == "ltl":
-                raise NotImplementedError
+                monitor = ltl2k(params.spec, params.monitor_type, vars(params))
             else:
                 print("Unknown monitor class:", params.monitor_class)
                 sys.exit(1)
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
new file mode 100644
index 000000000000..163f192190aa
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -0,0 +1,552 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Implementation based on
+# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996).
+# Simple On-the-fly Automatic Verification of Linear Temporal Logic.
+# https://doi.org/10.1007/978-0-387-34892-6_1
+# With extra optimizations
+
+from ply.lex import lex
+from ply.yacc import yacc
+
+# Grammar:
+# 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+#
+# Operands (opd):
+# 	true, false, user-defined names
+#
+# Unary Operators (unop):
+#       always
+#       eventually
+#       not
+#
+# Binary Operators (binop):
+#       until
+#       and
+#       or
+#       imply
+#       equivalent
+
+tokens = (
+   'AND',
+   'OR',
+   'IMPLY',
+   'UNTIL',
+   'ALWAYS',
+   'EVENTUALLY',
+   'VARIABLE',
+   'LITERAL',
+   'NOT',
+   'LPAREN',
+   'RPAREN',
+   'ASSIGN',
+)
+
+t_AND     = r'and'
+t_OR      = r'or'
+t_IMPLY   = r'imply'
+t_UNTIL   = r'until'
+t_ALWAYS = r'always'
+t_EVENTUALLY = r'eventually'
+t_VARIABLE = r'[A-Z_0-9]+'
+t_LITERAL = r'true|false'
+t_NOT = r'not'
+t_LPAREN = r'\('
+t_RPAREN = r'\)'
+t_ASSIGN = r'='
+t_ignore_COMMENT = r'\#.*'
+t_ignore  = ' \t\n'
+
+def t_error(t):
+    raise ValueError("Illegal character '%s'" % t.value[0])
+
+lexer = lex()
+
+class GraphNode:
+    def __init__(self, incoming: set['GraphNode'], new, old, _next):
+        self.init = False
+        self.outgoing = set()
+        self.labels = set()
+        self.incoming = incoming
+        self.new = new.copy()
+        self.old = old.copy()
+        self.next = _next.copy()
+        self.id = None
+
+    def expand(self, node_set):
+        if not self.new:
+            for nd in node_set:
+                if nd.old == self.old and nd.next == self.next:
+                    nd.incoming |= self.incoming
+                    for i in self.incoming:
+                        i.outgoing.add(nd)
+                    return node_set
+
+            new_current_node = GraphNode({self}, self.next, set(), set())
+            return new_current_node.expand({self} | node_set)
+        n = self.new.pop()
+        return n.expand(self, node_set)
+
+    def __lt__(self, other):
+        return self.id < other.id
+
+class ASTNode:
+    uid = 1
+    def __init__(self,op):
+        self.op = op
+        self.id = ASTNode.uid
+        ASTNode.uid += 1
+
+    def __hash__(self):
+        return hash(self.op)
+
+    def __eq__(self, other):
+        return self is other
+
+    def __iter__(self):
+        yield self
+        yield from self.op
+
+    def negate(self):
+        self.op = self.op.negate()
+        return self
+
+    def expand(self, node, node_set):
+        return self.op.expand(self, node, node_set)
+
+    def __str__(self):
+        if isinstance(self.op, Literal):
+            return str(self.op.value)
+        elif isinstance(self.op, Variable):
+            return self.op.name.lower()
+        return "val" + str(self.id)
+
+    def normalize(self):
+        # Get rid of:
+        #   - ALWAYS
+        #   - EVENTUALLY
+        #   - IMPLY
+        # And move all the NOT to be inside
+        self.op = self.op.normalize()
+        return self
+
+class BinaryOp:
+    op_str = "not_supported"
+
+    def __init__(self, left: ASTNode, right: ASTNode):
+        self.left = left
+        self.right = right
+
+    def __hash__(self):
+        return hash((self.left, self.right))
+
+    def __iter__(self):
+        yield from self.left
+        yield from self.right
+
+    def normalize(self):
+        raise NotImplemented
+
+    def negate(self):
+        raise NotImplemented
+
+    def _is_temporal(self):
+        raise NotImplemented
+
+    def is_temporal(self):
+        if self.left.op.is_temporal():
+            return True
+        if self.right.op.is_temporal():
+            return True
+        return self._is_temporal()
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        raise NotImplemented
+
+class AndOp(BinaryOp):
+    op_str = '&&'
+
+    def __init__(self, left, right):
+        super().__init__(left, right)
+
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return OrOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        if not n.op.is_temporal():
+            node.old.add(n)
+            return node.expand(node_set)
+
+        tmp = GraphNode(node.incoming,
+                        node.new | ({n.op.left, n.op.right} - node.old),
+                        node.old | {n},
+                        node.next)
+        return tmp.expand(node_set)
+
+class OrOp(BinaryOp):
+    op_str = '||'
+
+    def __init__(self, left, right):
+        super().__init__(left, right)
+
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return AndOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        if not n.op.is_temporal():
+            node.old |= {n}
+            return node.expand(node_set)
+
+        node1 = GraphNode( node.incoming,
+                          node.new | ({n.op.left} - node.old),
+                          node.old | {n},
+                          node.next)
+        node2 = GraphNode( node.incoming,
+                          node.new | ({n.op.right} - node.old),
+                          node.old | {n},
+                          node.next)
+        return node2.expand(node1.expand(node_set))
+
+class UntilOp(BinaryOp):
+    def __init__(self, left, right):
+        super().__init__(left, right)
+
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return VOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return True
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        node1 = GraphNode( node.incoming,
+                          node.new | ({n.op.left} - node.old),
+                          node.old | {n},
+                          node.next | {n})
+        node2 = GraphNode(node.incoming,
+                          node.new | ({n.op.right} - node.old),
+                          node.old | {n},
+                          node.next)
+        return node2.expand(node1.expand(node_set))
+
+class VOp(BinaryOp):
+    def __init__(self, left, right):
+        super().__init__(left, right)
+
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return UntilOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return True
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        node1 = GraphNode(node.incoming,
+                          node.new | ({n.op.right} - node.old),
+                          node.old | {n},
+                          node.next | {n})
+        node2 = GraphNode(node.incoming,
+                          node.new | ({n.op.left, n.op.right} - node.old),
+                          node.old | {n},
+                          node.next)
+        return node2.expand(node1.expand(node_set))
+
+class ImplyOp(BinaryOp):
+    def __init__(self, left, right):
+        super().__init__(left, right)
+
+    def normalize(self):
+        # P -> Q === !P | Q
+        return OrOp(self.left.negate(), self.right)
+
+    def _is_temporal(self):
+        return False
+
+    def negate():
+        # !(P -> Q) === !(!P | Q) === P & !Q
+        return AndOp(self.left, self.right.negate())
+
+class UnaryOp:
+    def __init__(self, child: ASTNode):
+        self.child = child
+
+    def __iter__(self):
+        yield from self.child
+
+    def __hash__(self):
+        return hash(self.child)
+
+    def normalize(self):
+        raise NotImplemented
+
+    def _is_temporal(self):
+        raise NotImplemented
+
+    def is_temporal(self):
+        if self.child.op.is_temporal():
+            return True
+        return self._is_temporal()
+
+    def negate(self):
+        raise NotImplemented
+
+class EventuallyOp(UnaryOp):
+    def __init__(self, child):
+        super().__init__(child)
+
+    def __str__(self):
+        return "eventually " + str(self.child)
+
+    def normalize(self):
+        # <>F == true U F
+        return UntilOp(Literal(True), self.right)
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # !<>F == [](!F)
+        return AlwaysOp(self.right.negate()).normalize()
+
+class AlwaysOp(UnaryOp):
+    def __init__(self, child):
+        super().__init__(child)
+
+    def normalize(self):
+        #[]F === !(true U !F) == false V F
+        new = ASTNode(Literal(False))
+        return VOp(new, self.child)
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # ![]F == <>(!F)
+        return EventuallyOp(self.left, self.right.negate()).normalize()
+
+class NotOp(UnaryOp):
+    def __init__(self, child):
+        super().__init__(child)
+
+    def __str__(self):
+        return "!" + str(self.child)
+
+    def normalize(self):
+        return self.child.op.negate()
+
+    def negate(self):
+        return self.child.op
+
+    def _is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        for f in node.old:
+            if n.op.child is f:
+                return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+class Variable:
+    def __init__(self, name: str):
+        self.name = name
+
+    def __hash__(self):
+        return hash(self.name)
+
+    def __iter__(self):
+        yield from ()
+
+    def negate(self):
+        new = ASTNode(self)
+        return NotOp(new)
+
+    def normalize(self):
+        return self
+
+    def is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        for f in node.old:
+            if isinstance(f, NotOp) and f.op.child is n:
+                return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+class Literal:
+    def __init__(self, value: bool):
+        self.value = value
+
+    def __iter__(self):
+        yield from ()
+
+    def __hash__(self):
+        return hash(self.value)
+
+    def __str__(self):
+        if self.value:
+            return "true"
+        return "false"
+
+    def negate(self):
+        self.value = not self.value
+        return self
+
+    def normalize(self):
+        return self
+
+    def is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        if not n.op.value:
+            return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+def p_spec(p):
+    '''
+    spec : assign
+         | assign spec
+    '''
+    if len(p) == 3:
+        p[2].append(p[1])
+        p[0] = p[2]
+    else:
+        p[0] = [p[1]]
+
+def p_assign(p):
+    '''
+    assign : VARIABLE ASSIGN ltl
+    '''
+    p[0] = (p[1], p[3])
+
+def p_ltl(p):
+    '''
+    ltl : opd
+        | binop
+        | unop
+    '''
+    p[0] = p[1]
+
+def p_opd(p):
+    '''
+    opd : VARIABLE
+        | LITERAL
+        | LPAREN ltl RPAREN
+    '''
+    if p[1] == "true":
+        p[0] = ASTNode(Literal(True))
+    elif p[1] == "false":
+        p[0] = ASTNode(Literal(False))
+    elif p[1] == '(':
+        p[0] = p[2]
+    else:
+        p[0] = ASTNode(Variable(p[1]))
+
+def p_unop(p):
+    '''
+    unop : ALWAYS ltl
+         | EVENTUALLY ltl
+         | NOT ltl
+    '''
+    if p[1] == "always":
+        op = AlwaysOp(p[2])
+    if p[1] == "eventually":
+        op = EventuallyOp(p[2])
+    if p[1] == "not":
+        op = NotOp(p[2])
+
+    p[0] = ASTNode(op)
+
+def p_binop(p):
+    '''
+    binop : opd UNTIL ltl
+          | opd AND ltl
+          | opd OR ltl
+          | opd IMPLY ltl
+    '''
+    if p[2] == "and":
+        op = AndOp(p[1], p[3])
+    elif p[2] == "until":
+        op = UntilOp(p[1], p[3])
+    elif p[2] == "or":
+        op = OrOp(p[1], p[3])
+    elif p[2] == "imply":
+        op = ImplyOp(p[1], p[3])
+    else:
+        raise ValueError("Invalid binary operator: %s" % p[2])
+
+    p[0] = ASTNode(op)
+
+parser = yacc()
+
+def parse_ltl(s: str) -> ASTNode:
+    spec = parser.parse(s)
+
+    subexpr = dict()
+
+    for assign in spec:
+        if assign[0] == "RULE":
+            rule = assign[1]
+        else:
+            subexpr[assign[0]] = assign[1]
+
+    for node in rule:
+        if not isinstance(node.op, Variable):
+            continue
+        replace = subexpr.get(node.op.name)
+        if replace is not None:
+            node.op = replace.op
+
+    return rule
+
+def create_graph(s: str):
+    atoms = set()
+
+    ltl = parse_ltl(s)
+    for c in ltl:
+        c.normalize()
+        if isinstance(c.op, Variable):
+            atoms.add(c.op.name)
+
+    init = GraphNode(set(), set(), set(), set())
+    head = GraphNode({init}, {ltl}, set(), set())
+    graph = head.expand(set())
+
+    for i, node in enumerate(graph):
+        node.id = i
+        for incoming in node.incoming:
+            if incoming is init:
+                node.init = True
+        for o in node.old:
+            if not o.op.is_temporal():
+                node.labels.add(str(o))
+
+    return sorted(atoms), sorted(graph), ltl
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
new file mode 100644
index 000000000000..e82d3f4bbee9
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -0,0 +1,242 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+
+from pathlib import Path
+from . import generator
+from . import ltl2ba
+
+COLUMN_LIMIT = 100
+
+def line_len(line: str) -> int:
+    tabs = line.count('\t')
+    return tabs * 7 + len(line)
+
+def break_long_line(line: str, indent='') -> list[str]:
+    result = []
+    while line_len(line) > COLUMN_LIMIT:
+        i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ')
+        result.append(line[:i])
+        line = indent + line[i + 1:]
+    if line:
+        result.append(line)
+    return result
+
+def build_condition_string(node: ltl2ba.GraphNode):
+    if not node.labels:
+        return "(true)"
+
+    result = "("
+
+    first = True
+    for label in sorted(node.labels):
+        if not first:
+            result += " && "
+        result += label
+        first = False
+
+    result += ")"
+
+    return result
+
+def abbreviate_atoms(atoms: list[str]) -> list[str]:
+    abbrs = list()
+    for atom in atoms:
+        size = 1
+        while True:
+            abbr = atom[:size]
+            if sum(a.startswith(abbr) for a in atoms) == 1:
+                break
+            size += 1
+        abbrs.append(abbr.lower())
+    return abbrs
+
+class ltl2k(generator.Monitor):
+    monitor_templates_dir = "rvgen/templates/ltl2k"
+
+    def __init__(self, file_path, MonitorType, extra_params={}):
+        if MonitorType != "per_task":
+            raise NotImplementedError("Only per_task monitor is supported for LTL")
+        super().__init__(extra_params)
+        with open(file_path) as f:
+            self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
+        self.atoms_abbr = abbreviate_atoms(self.atoms)
+        self.name = extra_params.get("model_name")
+        if not self.name:
+            self.name = Path(file_path).stem
+
+    def _fill_states(self) -> str:
+        buf = [
+            "enum ltl_buchi_state {",
+        ]
+
+        for node in self.ba:
+            buf.append("\tS%i," % node.id)
+        buf.append("\tRV_NUM_BA_STATES")
+        buf.append("};")
+        buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
+        return buf
+
+    def _fill_atoms(self):
+        buf = ["enum ltl_atom {"]
+        for a in sorted(self.atoms):
+            buf.append("\tLTL_%s," % a)
+        buf.append("\tLTL_NUM_ATOM")
+        buf.append("};")
+        buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
+        return buf
+
+    def _fill_atoms_to_string(self):
+        buf = [
+            "static const char *ltl_atom_str(enum ltl_atom atom)",
+            "{",
+            "\tstatic const char *const names[] = {"
+        ]
+
+        for name in self.atoms_abbr:
+            buf.append("\t\t\"%s\"," % name)
+
+        buf.extend([
+            "\t};",
+            "",
+            "\treturn names[atom];",
+            "}"
+        ])
+        return buf
+
+    def _fill_atom_values(self):
+        buf = []
+        for node in self.ltl:
+            if node.op.is_temporal():
+                continue
+
+            if isinstance(node.op, ltl2ba.Variable):
+                buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (node, node.op.name))
+            elif isinstance(node.op, ltl2ba.AndOp):
+                buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right))
+            elif isinstance(node.op, ltl2ba.OrOp):
+                buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right))
+            elif isinstance(node.op, ltl2ba.NotOp):
+                buf.append("\tbool %s = !%s;" % (node, node.op.child))
+        buf.reverse()
+
+        buf2 = []
+        for line in buf:
+            buf2.extend(break_long_line(line, "\t     "))
+        return buf2
+
+    def _fill_transitions(self):
+        buf = [
+            "static void",
+            "ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)",
+            "{"
+        ]
+        buf.extend(self._fill_atom_values())
+        buf.extend([
+            "",
+            "\tswitch (state) {"
+        ])
+
+        for node in self.ba:
+            buf.append("\tcase S%i:" % node.id)
+
+            for o in sorted(node.outgoing):
+                line   = "\t\tif "
+                indent = "\t\t   "
+
+                line += build_condition_string(o)
+                lines = break_long_line(line, indent)
+                buf.extend(lines)
+
+                buf.append("\t\t\t__set_bit(S%i, next);" % o.id)
+            buf.append("\t\tbreak;")
+        buf.extend([
+            "\t}",
+            "}"
+        ])
+
+        return buf
+
+    def _fill_start(self):
+        buf = [
+            "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)",
+            "{"
+        ]
+        buf.extend(self._fill_atom_values())
+        buf.append("")
+
+        for node in self.ba:
+            if not node.init:
+                continue
+
+            line   = "\tif "
+            indent = "\t   "
+
+            line += build_condition_string(node)
+            lines = break_long_line(line, indent)
+            buf.extend(lines)
+
+            buf.append("\t\t__set_bit(S%i, mon->states);" % node.id)
+        buf.append("}")
+        return buf
+
+    def fill_tracepoint_handlers_skel(self):
+        buff = []
+        buff.append("static void handle_example_event(void *data, /* XXX: fill header */)")
+        buff.append("{")
+        buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.atoms[0])
+        buff.append("}")
+        buff.append("")
+        return '\n'.join(buff)
+
+    def fill_tracepoint_attach_probe(self):
+        return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_example_event);" \
+                % self.name
+
+    def fill_tracepoint_detach_helper(self):
+        return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_sample_event);" \
+                % self.name
+
+    def fill_atoms_init(self):
+        buff = []
+        for a in self.atoms:
+            buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a)
+        return '\n'.join(buff)
+
+    def fill_model_h(self):
+        buf = [
+            "/* SPDX-License-Identifier: GPL-2.0 */",
+            "",
+            "#include <linux/rv.h>",
+            "",
+            "#define MONITOR_NAME " + self.name,
+            ""
+        ]
+
+        buf.extend(self._fill_atoms())
+        buf.append('')
+
+        buf.extend(self._fill_atoms_to_string())
+        buf.append('')
+
+        buf.extend(self._fill_states())
+        buf.append('')
+
+        buf.extend(self._fill_start())
+        buf.append('')
+
+        buf.extend(self._fill_transitions())
+        buf.append('')
+
+        return '\n'.join(buf)
+
+    def fill_monitor_class_type(self):
+        return "LTL_MON_EVENTS_ID"
+
+    def fill_monitor_class(self):
+        return "ltl_monitor_id"
+
+    def fill_main_c(self):
+        main_c = super().fill_main_c()
+        main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init())
+
+        return main_c
diff --git a/tools/verification/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/templates/ltl2k/main.c
new file mode 100644
index 000000000000..2f3c4d642746
--- /dev/null
+++ b/tools/verification/rvgen/templates/ltl2k/main.c
@@ -0,0 +1,102 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "%%MODEL_NAME%%"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+%%INCLUDE_PARENT%%
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "%%MODEL_NAME%%.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which are expensive to
+	 * trace. It is possible only if the atomic proposition does not need to be updated at
+	 * precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is false if the task is
+	 * already running before the monitor is enabled.
+	 */
+%%ATOMS_INIT%%
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+%%TRACEPOINT_HANDLERS_SKEL%%
+static int enable_%%MODEL_NAME%%(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+%%TRACEPOINT_ATTACH%%
+
+	return 0;
+}
+
+static void disable_%%MODEL_NAME%%(void)
+{
+%%TRACEPOINT_DETACH%%
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_%%MODEL_NAME%% = {
+	.name = "%%MODEL_NAME%%",
+	.description = "%%DESCRIPTION%%",
+	.enable = enable_%%MODEL_NAME%%,
+	.disable = disable_%%MODEL_NAME%%,
+};
+
+static int __init register_%%MODEL_NAME%%(void)
+{
+	return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%);
+}
+
+static void __exit unregister_%%MODEL_NAME%%(void)
+{
+	rv_unregister_monitor(&rv_%%MODEL_NAME%%);
+}
+
+module_init(register_%%MODEL_NAME%%);
+module_exit(unregister_%%MODEL_NAME%%);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR(/* TODO */);
+MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/templates/ltl2k/trace.h b/tools/verification/rvgen/templates/ltl2k/trace.h
new file mode 100644
index 000000000000..49394c4b0f1c
--- /dev/null
+++ b/tools/verification/rvgen/templates/ltl2k/trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%%
+DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
-- 
2.39.5

[PATCH v2 14/22] rv: Add rtapp container monitor

[Nam Cao]

Add the container "rtapp" which is the monitor collection for detecting
problems with real-time applications. The monitors will be added in the
follow-up commits.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 kernel/trace/rv/Kconfig                |  1 +
 kernel/trace/rv/Makefile               |  1 +
 kernel/trace/rv/monitors/rtapp/Kconfig |  6 +++++
 kernel/trace/rv/monitors/rtapp/rtapp.c | 34 ++++++++++++++++++++++++++
 kernel/trace/rv/monitors/rtapp/rtapp.h |  3 +++
 5 files changed, 45 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/rtapp/Kconfig
 create mode 100644 kernel/trace/rv/monitors/rtapp/rtapp.c
 create mode 100644 kernel/trace/rv/monitors/rtapp/rtapp.h

diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 6e157f964991..5c407d291661 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -41,6 +41,7 @@ source "kernel/trace/rv/monitors/snroc/Kconfig"
 source "kernel/trace/rv/monitors/scpd/Kconfig"
 source "kernel/trace/rv/monitors/snep/Kconfig"
 source "kernel/trace/rv/monitors/sncid/Kconfig"
+source "kernel/trace/rv/monitors/rtapp/Kconfig"
 # Add new monitors here
 
 config RV_REACTORS
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index f9b2cd0483c3..9b28c2419995 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -12,6 +12,7 @@ obj-$(CONFIG_RV_MON_SNROC) += monitors/snroc/snroc.o
 obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o
 obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o
 obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o
+obj-$(CONFIG_RV_MON_RTAPP) += monitors/rtapp/rtapp.o
 # Add new monitors here
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
diff --git a/kernel/trace/rv/monitors/rtapp/Kconfig b/kernel/trace/rv/monitors/rtapp/Kconfig
new file mode 100644
index 000000000000..94689d66a79c
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp/Kconfig
@@ -0,0 +1,6 @@
+config RV_MON_RTAPP
+	depends on RV
+	bool "rtapp monitor"
+	help
+	  Collection of monitors to check for common problems with real-time application that cause
+	  unexpected latency.
diff --git a/kernel/trace/rv/monitors/rtapp/rtapp.c b/kernel/trace/rv/monitors/rtapp/rtapp.c
new file mode 100644
index 000000000000..193c9d8dc0af
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp/rtapp.c
@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+
+#define MODULE_NAME "rtapp"
+
+#include "rtapp.h"
+
+struct rv_monitor rv_rtapp;
+
+struct rv_monitor rv_rtapp = {
+	.name = "rtapp",
+	.description = "Collection of monitors for detecting problems with real-time applications",
+};
+
+static int __init register_rtapp(void)
+{
+	rv_register_monitor(&rv_rtapp, NULL);
+	return 0;
+}
+
+static void __exit unregister_rtapp(void)
+{
+	rv_unregister_monitor(&rv_rtapp);
+}
+
+module_init(register_rtapp);
+module_exit(unregister_rtapp);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>");
+MODULE_DESCRIPTION("Collection of monitors for detecting problems with real-time applications");
diff --git a/kernel/trace/rv/monitors/rtapp/rtapp.h b/kernel/trace/rv/monitors/rtapp/rtapp.h
new file mode 100644
index 000000000000..4c200d67c7f6
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp/rtapp.h
@@ -0,0 +1,3 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+extern struct rv_monitor rv_rtapp;
-- 
2.39.5

[PATCH v2 15/22] x86/tracing: Remove redundant trace_pagefault_key

[Nam Cao]

trace_pagefault_key is used to optimize the pagefault tracepoints when it
is disabled. However, tracepoints already have built-in static_key for this
exact purpose.

Remove this redundant key.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: H. Peter Anvin <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
---
 arch/x86/include/asm/trace/common.h      | 12 ------------
 arch/x86/include/asm/trace/exceptions.h  | 18 ++++++------------
 arch/x86/include/asm/trace/irq_vectors.h |  1 -
 arch/x86/kernel/Makefile                 |  1 -
 arch/x86/kernel/tracepoint.c             | 21 ---------------------
 arch/x86/mm/fault.c                      |  3 ---
 6 files changed, 6 insertions(+), 50 deletions(-)
 delete mode 100644 arch/x86/include/asm/trace/common.h
 delete mode 100644 arch/x86/kernel/tracepoint.c

diff --git a/arch/x86/include/asm/trace/common.h b/arch/x86/include/asm/trace/common.h
deleted file mode 100644
index f0f9bcdb74d9..000000000000
--- a/arch/x86/include/asm/trace/common.h
+++ /dev/null
@@ -1,12 +0,0 @@
-#ifndef _ASM_TRACE_COMMON_H
-#define _ASM_TRACE_COMMON_H
-
-#ifdef CONFIG_TRACING
-DECLARE_STATIC_KEY_FALSE(trace_pagefault_key);
-#define trace_pagefault_enabled()			\
-	static_branch_unlikely(&trace_pagefault_key)
-#else
-static inline bool trace_pagefault_enabled(void) { return false; }
-#endif
-
-#endif
diff --git a/arch/x86/include/asm/trace/exceptions.h b/arch/x86/include/asm/trace/exceptions.h
index 6b1e87194809..34bc8214a2d7 100644
--- a/arch/x86/include/asm/trace/exceptions.h
+++ b/arch/x86/include/asm/trace/exceptions.h
@@ -6,10 +6,6 @@
 #define _TRACE_PAGE_FAULT_H
 
 #include <linux/tracepoint.h>
-#include <asm/trace/common.h>
-
-extern int trace_pagefault_reg(void);
-extern void trace_pagefault_unreg(void);
 
 DECLARE_EVENT_CLASS(x86_exceptions,
 
@@ -34,15 +30,13 @@ DECLARE_EVENT_CLASS(x86_exceptions,
 		  (void *)__entry->address, (void *)__entry->ip,
 		  __entry->error_code) );
 
-#define DEFINE_PAGE_FAULT_EVENT(name)				\
-DEFINE_EVENT_FN(x86_exceptions, name,				\
-	TP_PROTO(unsigned long address,	struct pt_regs *regs,	\
-		 unsigned long error_code),			\
-	TP_ARGS(address, regs, error_code),			\
-	trace_pagefault_reg, trace_pagefault_unreg);
+DEFINE_EVENT(x86_exceptions, page_fault_user,
+	TP_PROTO(unsigned long address,	struct pt_regs *regs, unsigned long error_code),
+	TP_ARGS(address, regs, error_code));
 
-DEFINE_PAGE_FAULT_EVENT(page_fault_user);
-DEFINE_PAGE_FAULT_EVENT(page_fault_kernel);
+DEFINE_EVENT(x86_exceptions, page_fault_kernel,
+	TP_PROTO(unsigned long address,	struct pt_regs *regs, unsigned long error_code),
+	TP_ARGS(address, regs, error_code));
 
 #undef TRACE_INCLUDE_PATH
 #undef TRACE_INCLUDE_FILE
diff --git a/arch/x86/include/asm/trace/irq_vectors.h b/arch/x86/include/asm/trace/irq_vectors.h
index 88e7f0f3bf62..7408bebdfde0 100644
--- a/arch/x86/include/asm/trace/irq_vectors.h
+++ b/arch/x86/include/asm/trace/irq_vectors.h
@@ -6,7 +6,6 @@
 #define _TRACE_IRQ_VECTORS_H
 
 #include <linux/tracepoint.h>
-#include <asm/trace/common.h>
 
 #ifdef CONFIG_X86_LOCAL_APIC
 
diff --git a/arch/x86/kernel/Makefile b/arch/x86/kernel/Makefile
index b43eb7e384eb..e8e33ec684ba 100644
--- a/arch/x86/kernel/Makefile
+++ b/arch/x86/kernel/Makefile
@@ -139,7 +139,6 @@ obj-$(CONFIG_OF)			+= devicetree.o
 obj-$(CONFIG_UPROBES)			+= uprobes.o
 
 obj-$(CONFIG_PERF_EVENTS)		+= perf_regs.o
-obj-$(CONFIG_TRACING)			+= tracepoint.o
 obj-$(CONFIG_SCHED_MC_PRIO)		+= itmt.o
 obj-$(CONFIG_X86_UMIP)			+= umip.o
 
diff --git a/arch/x86/kernel/tracepoint.c b/arch/x86/kernel/tracepoint.c
deleted file mode 100644
index 03ae1caaa878..000000000000
--- a/arch/x86/kernel/tracepoint.c
+++ /dev/null
@@ -1,21 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0
-/*
- * Copyright (C) 2013 Seiji Aguchi <seiji.aguchi@hds.com>
- */
-#include <linux/jump_label.h>
-#include <linux/atomic.h>
-
-#include <asm/trace/exceptions.h>
-
-DEFINE_STATIC_KEY_FALSE(trace_pagefault_key);
-
-int trace_pagefault_reg(void)
-{
-	static_branch_inc(&trace_pagefault_key);
-	return 0;
-}
-
-void trace_pagefault_unreg(void)
-{
-	static_branch_dec(&trace_pagefault_key);
-}
diff --git a/arch/x86/mm/fault.c b/arch/x86/mm/fault.c
index 296d294142c8..7e3e51fa1f95 100644
--- a/arch/x86/mm/fault.c
+++ b/arch/x86/mm/fault.c
@@ -1455,9 +1455,6 @@ static __always_inline void
 trace_page_fault_entries(struct pt_regs *regs, unsigned long error_code,
 			 unsigned long address)
 {
-	if (!trace_pagefault_enabled())
-		return;
-
 	if (user_mode(regs))
 		trace_page_fault_user(address, regs, error_code);
 	else
-- 
2.39.5

[PATCH v2 16/22] x86/tracing: Move page fault trace points to generic

[Nam Cao]

Page fault trace points are interesting for other architectures as well.
Move them to be generic.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: "H. Peter Anvin" <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
---
 arch/x86/mm/fault.c                                 |  2 +-
 .../asm/trace => include/trace/events}/exceptions.h | 13 ++++---------
 2 files changed, 5 insertions(+), 10 deletions(-)
 rename {arch/x86/include/asm/trace => include/trace/events}/exceptions.h (79%)

diff --git a/arch/x86/mm/fault.c b/arch/x86/mm/fault.c
index 7e3e51fa1f95..ad4cb1502316 100644
--- a/arch/x86/mm/fault.c
+++ b/arch/x86/mm/fault.c
@@ -38,7 +38,7 @@
 #include <asm/sev.h>			/* snp_dump_hva_rmpentry()	*/
 
 #define CREATE_TRACE_POINTS
-#include <asm/trace/exceptions.h>
+#include <trace/events/exceptions.h>
 
 /*
  * Returns 0 if mmiotrace is disabled, or if the fault is not
diff --git a/arch/x86/include/asm/trace/exceptions.h b/include/trace/events/exceptions.h
similarity index 79%
rename from arch/x86/include/asm/trace/exceptions.h
rename to include/trace/events/exceptions.h
index 34bc8214a2d7..a631f8de8917 100644
--- a/arch/x86/include/asm/trace/exceptions.h
+++ b/include/trace/events/exceptions.h
@@ -7,7 +7,7 @@
 
 #include <linux/tracepoint.h>
 
-DECLARE_EVENT_CLASS(x86_exceptions,
+DECLARE_EVENT_CLASS(exceptions,
 
 	TP_PROTO(unsigned long address, struct pt_regs *regs,
 		 unsigned long error_code),
@@ -22,7 +22,7 @@ DECLARE_EVENT_CLASS(x86_exceptions,
 
 	TP_fast_assign(
 		__entry->address = address;
-		__entry->ip = regs->ip;
+		__entry->ip = instruction_pointer(regs);
 		__entry->error_code = error_code;
 	),
 
@@ -30,18 +30,13 @@ DECLARE_EVENT_CLASS(x86_exceptions,
 		  (void *)__entry->address, (void *)__entry->ip,
 		  __entry->error_code) );
 
-DEFINE_EVENT(x86_exceptions, page_fault_user,
+DEFINE_EVENT(exceptions, page_fault_user,
 	TP_PROTO(unsigned long address,	struct pt_regs *regs, unsigned long error_code),
 	TP_ARGS(address, regs, error_code));
-
-DEFINE_EVENT(x86_exceptions, page_fault_kernel,
+DEFINE_EVENT(exceptions, page_fault_kernel,
 	TP_PROTO(unsigned long address,	struct pt_regs *regs, unsigned long error_code),
 	TP_ARGS(address, regs, error_code));
 
-#undef TRACE_INCLUDE_PATH
-#undef TRACE_INCLUDE_FILE
-#define TRACE_INCLUDE_PATH .
-#define TRACE_INCLUDE_FILE exceptions
 #endif /*  _TRACE_PAGE_FAULT_H */
 
 /* This part must be outside protection */
-- 
2.39.5

[PATCH v2 17/22] arm64: mm: Add page fault trace points

[Nam Cao]

Add page fault trace points, which are useful to implement RV monitor which
watches page faults.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Will Deacon <will@kernel.org>
Cc: linux-arm-kernel@lists.infradead.org
---
 arch/arm64/mm/fault.c | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/arch/arm64/mm/fault.c b/arch/arm64/mm/fault.c
index ef63651099a9..e3f096b0dffd 100644
--- a/arch/arm64/mm/fault.c
+++ b/arch/arm64/mm/fault.c
@@ -44,6 +44,9 @@
 #include <asm/tlbflush.h>
 #include <asm/traps.h>
 
+#define CREATE_TRACE_POINTS
+#include <trace/events/exceptions.h>
+
 struct fault_info {
 	int	(*fn)(unsigned long far, unsigned long esr,
 		      struct pt_regs *regs);
@@ -559,6 +562,11 @@ static int __kprobes do_page_fault(unsigned long far, unsigned long esr,
 	if (kprobe_page_fault(regs, esr))
 		return 0;
 
+	if (user_mode(regs))
+		trace_page_fault_user(addr, regs, esr);
+	else
+		trace_page_fault_kernel(addr, regs, esr);
+
 	/*
 	 * If we're in an interrupt or have no user context, we must not take
 	 * the fault.
-- 
2.39.5

[PATCH v2 18/22] riscv: mm: Add page fault trace points

[Nam Cao]

Add page fault trace points, which are useful to implement RV monitor that
watches page faults.

Signed-off-by: Nam Cao <namcao@linutronix.de>
Acked-by: Alexandre Ghiti <alexghiti@rivosinc.com>
---
Cc: Paul Walmsley <paul.walmsley@sifive.com>
Cc: Palmer Dabbelt <palmer@dabbelt.com>
Cc: Albert Ou <aou@eecs.berkeley.edu>
Cc: linux-riscv@lists.infradead.org
---
 arch/riscv/mm/fault.c | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/arch/riscv/mm/fault.c b/arch/riscv/mm/fault.c
index 0194324a0c50..04ed6f8acae4 100644
--- a/arch/riscv/mm/fault.c
+++ b/arch/riscv/mm/fault.c
@@ -20,6 +20,9 @@
 #include <asm/ptrace.h>
 #include <asm/tlbflush.h>
 
+#define CREATE_TRACE_POINTS
+#include <trace/events/exceptions.h>
+
 #include "../kernel/head.h"
 
 static void show_pte(unsigned long addr)
@@ -291,6 +294,11 @@ void handle_page_fault(struct pt_regs *regs)
 	if (kprobe_page_fault(regs, cause))
 		return;
 
+	if (user_mode(regs))
+		trace_page_fault_user(addr, regs, cause);
+	else
+		trace_page_fault_kernel(addr, regs, cause);
+
 	/*
 	 * Fault-in kernel-space virtual memory on-demand.
 	 * The 'reference' page table is init_mm.pgd.
-- 
2.39.5

[PATCH v2 19/22] rv: Add rtapp_pagefault monitor

[Nam Cao]

Userspace real-time applications may have design flaws that they raise
page faults in real-time threads, and thus have unexpected latencies.

Add an linear temporal logic monitor to detect this scenario.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Will Deacon <will@kernel.org>
Cc: Paul Walmsley <paul.walmsley@sifive.com>
Cc: Palmer Dabbelt <palmer@dabbelt.com>
Cc: Albert Ou <aou@eecs.berkeley.edu>
Cc: Alexandre Ghiti <alex@ghiti.fr>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: H. Peter Anvin <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: linux-arm-kernel@lists.infradead.org
Cc: linux-riscv@lists.infradead.org
---
 kernel/trace/rv/Kconfig                       |  1 +
 kernel/trace/rv/Makefile                      |  1 +
 kernel/trace/rv/monitors/pagefault/Kconfig    | 11 +++
 .../trace/rv/monitors/pagefault/pagefault.c   | 83 +++++++++++++++++++
 .../trace/rv/monitors/pagefault/pagefault.h   | 57 +++++++++++++
 .../rv/monitors/pagefault/pagefault_trace.h   | 14 ++++
 kernel/trace/rv/rv_trace.h                    |  1 +
 tools/verification/models/rtapp/pagefault.ltl |  1 +
 8 files changed, 169 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/pagefault/Kconfig
 create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.c
 create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.h
 create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault_trace.h
 create mode 100644 tools/verification/models/rtapp/pagefault.ltl

diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 5c407d291661..6f86d8501e87 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -42,6 +42,7 @@ source "kernel/trace/rv/monitors/scpd/Kconfig"
 source "kernel/trace/rv/monitors/snep/Kconfig"
 source "kernel/trace/rv/monitors/sncid/Kconfig"
 source "kernel/trace/rv/monitors/rtapp/Kconfig"
+source "kernel/trace/rv/monitors/pagefault/Kconfig"
 # Add new monitors here
 
 config RV_REACTORS
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 9b28c2419995..353ecf939d0e 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -13,6 +13,7 @@ obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o
 obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o
 obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o
 obj-$(CONFIG_RV_MON_RTAPP) += monitors/rtapp/rtapp.o
+obj-$(CONFIG_RV_MON_PAGEFAULT) += monitors/pagefault/pagefault.o
 # Add new monitors here
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
diff --git a/kernel/trace/rv/monitors/pagefault/Kconfig b/kernel/trace/rv/monitors/pagefault/Kconfig
new file mode 100644
index 000000000000..b31dee208459
--- /dev/null
+++ b/kernel/trace/rv/monitors/pagefault/Kconfig
@@ -0,0 +1,11 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_PAGEFAULT
+	depends on RV
+	select RV_LTL_MONITOR
+	depends on RV_MON_RTAPP
+	default y
+	select LTL_MON_EVENTS_ID
+	bool "pagefault monitor"
+	help
+	  Monitor that real-time tasks do not raise page faults
diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.c b/kernel/trace/rv/monitors/pagefault/pagefault.c
new file mode 100644
index 000000000000..9f7a4cba39a1
--- /dev/null
+++ b/kernel/trace/rv/monitors/pagefault/pagefault.c
@@ -0,0 +1,83 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "pagefault"
+
+#include <rv_trace.h>
+#include <trace/events/exceptions.h>
+#include <monitors/rtapp/rtapp.h>
+
+#include "pagefault.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	ltl_atom_set(mon, LTL_RT, rt_task(task));
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	if (task_creation)
+		ltl_atom_set(mon, LTL_PAGEFAULT, false);
+}
+
+static void handle_page_fault(void *data, unsigned long address, struct pt_regs *regs,
+			      unsigned long error_code)
+{
+	ltl_atom_pulse(current, LTL_PAGEFAULT, true);
+}
+
+static int enable_pagefault(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("pagefault", page_fault_kernel, handle_page_fault);
+	rv_attach_trace_probe("pagefault", page_fault_user, handle_page_fault);
+
+	return 0;
+}
+
+static void disable_pagefault(void)
+{
+	rv_pagefault.enabled = 0;
+
+	rv_detach_trace_probe("rtapp_pagefault", page_fault_kernel, handle_page_fault);
+	rv_detach_trace_probe("rtapp_pagefault", page_fault_user, handle_page_fault);
+
+	ltl_monitor_destroy();
+}
+
+static struct rv_monitor rv_pagefault = {
+	.name = "pagefault",
+	.description = "Monitor that RT tasks do not raise page faults",
+	.enable = enable_pagefault,
+	.disable = disable_pagefault,
+};
+
+static int __init register_pagefault(void)
+{
+	rv_register_monitor(&rv_pagefault, &rv_rtapp);
+	return 0;
+}
+
+static void __exit unregister_pagefault(void)
+{
+	rv_unregister_monitor(&rv_pagefault);
+}
+
+module_init(register_pagefault);
+module_exit(unregister_pagefault);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>");
+MODULE_DESCRIPTION("pagefault: Monitor that RT tasks do not raise page faults");
diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.h b/kernel/trace/rv/monitors/pagefault/pagefault.h
new file mode 100644
index 000000000000..f4535c83f7d1
--- /dev/null
+++ b/kernel/trace/rv/monitors/pagefault/pagefault.h
@@ -0,0 +1,57 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME pagefault
+
+enum ltl_atom {
+	LTL_PAGEFAULT,
+	LTL_RT,
+	LTL_NUM_ATOM
+};
+static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+static const char *ltl_atom_str(enum ltl_atom atom)
+{
+	static const char *const names[] = {
+		"p",
+		"r",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
+	bool val3 = !pagefault;
+	bool rt = test_bit(LTL_RT, mon->atoms);
+	bool val1 = !rt;
+	bool val4 = val1 || val3;
+
+	if (val4)
+		__set_bit(S0, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
+	bool val3 = !pagefault;
+	bool rt = test_bit(LTL_RT, mon->atoms);
+	bool val1 = !rt;
+	bool val4 = val1 || val3;
+
+	switch (state) {
+	case S0:
+		if (val4)
+			__set_bit(S0, next);
+		break;
+	}
+}
diff --git a/kernel/trace/rv/monitors/pagefault/pagefault_trace.h b/kernel/trace/rv/monitors/pagefault/pagefault_trace.h
new file mode 100644
index 000000000000..fe1f82597b1a
--- /dev/null
+++ b/kernel/trace/rv/monitors/pagefault/pagefault_trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_PAGEFAULT
+DEFINE_EVENT(event_ltl_monitor_id, event_pagefault,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_pagefault,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_PAGEFAULT */
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index f9fb848bae91..02c906c9745b 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -172,6 +172,7 @@ TRACE_EVENT(error_ltl_monitor_id,
 
 	TP_printk("%s[%d]: violation detected", __get_str(comm), __entry->pid)
 );
+#include <monitors/pagefault/pagefault_trace.h>
 // Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here
 #endif /* CONFIG_LTL_MON_EVENTS_ID */
 #endif /* _TRACE_RV_H */
diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl
new file mode 100644
index 000000000000..d7ce62102733
--- /dev/null
+++ b/tools/verification/models/rtapp/pagefault.ltl
@@ -0,0 +1 @@
+RULE = always (RT imply not PAGEFAULT)
-- 
2.39.5

[PATCH v2 20/22] rv: Add rtapp_sleep monitor

[Nam Cao]

Add a monitor for checking that real-time tasks do not go to sleep in a
manner that may cause undesirable latency.

Also change
	RV depends on TRACING
to
	RV select TRACING
to avoid the following recursive dependency:

 error: recursive dependency detected!
	symbol TRACING is selected by PREEMPTIRQ_TRACEPOINTS
	symbol PREEMPTIRQ_TRACEPOINTS depends on TRACE_IRQFLAGS
	symbol TRACE_IRQFLAGS is selected by RV_MON_SLEEP
	symbol RV_MON_SLEEP depends on RV
	symbol RV depends on TRACING

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 kernel/trace/rv/Kconfig                      |   3 +-
 kernel/trace/rv/Makefile                     |   1 +
 kernel/trace/rv/monitors/sleep/Kconfig       |  13 +
 kernel/trace/rv/monitors/sleep/sleep.c       | 217 ++++++++++++++
 kernel/trace/rv/monitors/sleep/sleep.h       | 293 +++++++++++++++++++
 kernel/trace/rv/monitors/sleep/sleep_trace.h |  14 +
 kernel/trace/rv/rv_trace.h                   |   1 +
 tools/verification/models/rtapp/sleep.ltl    |  15 +
 8 files changed, 556 insertions(+), 1 deletion(-)
 create mode 100644 kernel/trace/rv/monitors/sleep/Kconfig
 create mode 100644 kernel/trace/rv/monitors/sleep/sleep.c
 create mode 100644 kernel/trace/rv/monitors/sleep/sleep.h
 create mode 100644 kernel/trace/rv/monitors/sleep/sleep_trace.h
 create mode 100644 tools/verification/models/rtapp/sleep.ltl

diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 6f86d8501e87..942d57575e67 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -20,7 +20,7 @@ config RV_LTL_MONITOR
 
 menuconfig RV
 	bool "Runtime Verification"
-	depends on TRACING
+	select TRACING
 	help
 	  Enable the kernel runtime verification infrastructure. RV is a
 	  lightweight (yet rigorous) method that complements classical
@@ -43,6 +43,7 @@ source "kernel/trace/rv/monitors/snep/Kconfig"
 source "kernel/trace/rv/monitors/sncid/Kconfig"
 source "kernel/trace/rv/monitors/rtapp/Kconfig"
 source "kernel/trace/rv/monitors/pagefault/Kconfig"
+source "kernel/trace/rv/monitors/sleep/Kconfig"
 # Add new monitors here
 
 config RV_REACTORS
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 353ecf939d0e..13ec2944c665 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -14,6 +14,7 @@ obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o
 obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o
 obj-$(CONFIG_RV_MON_RTAPP) += monitors/rtapp/rtapp.o
 obj-$(CONFIG_RV_MON_PAGEFAULT) += monitors/pagefault/pagefault.o
+obj-$(CONFIG_RV_MON_SLEEP) += monitors/sleep/sleep.o
 # Add new monitors here
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
diff --git a/kernel/trace/rv/monitors/sleep/Kconfig b/kernel/trace/rv/monitors/sleep/Kconfig
new file mode 100644
index 000000000000..d00aa1aae069
--- /dev/null
+++ b/kernel/trace/rv/monitors/sleep/Kconfig
@@ -0,0 +1,13 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_SLEEP
+	depends on RV
+	select RV_LTL_MONITOR
+	depends on HAVE_SYSCALL_TRACEPOINTS
+	depends on RV_MON_RTAPP
+	select TRACE_IRQFLAGS
+	default y
+	select LTL_MON_EVENTS_ID
+	bool "sleep monitor"
+	help
+	  Monitor that real-time tasks do not sleep in a manner that may cause undesirable latency.
diff --git a/kernel/trace/rv/monitors/sleep/sleep.c b/kernel/trace/rv/monitors/sleep/sleep.c
new file mode 100644
index 000000000000..c31b02921823
--- /dev/null
+++ b/kernel/trace/rv/monitors/sleep/sleep.c
@@ -0,0 +1,217 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/irqflags.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "sleep"
+
+#include <trace/events/syscalls.h>
+#include <trace/events/sched.h>
+#include <trace/events/lock.h>
+#include <uapi/linux/futex.h>
+#include <rv_trace.h>
+#include <monitors/rtapp/rtapp.h>
+
+#include "sleep.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	ltl_atom_set(mon, LTL_RT, rt_task(task));
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/* event-like atomic propositions */
+	ltl_atom_set(mon, LTL_SLEEP, false);
+	ltl_atom_set(mon, LTL_WAKE, false);
+	ltl_atom_set(mon, LTL_WOKEN_BY_HARDIRQ, false);
+	ltl_atom_set(mon, LTL_WOKEN_BY_NMI, false);
+	ltl_atom_set(mon, LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, false);
+
+	if (task_creation) {
+		ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false);
+		ltl_atom_set(mon, LTL_NANOSLEEP, false);
+		ltl_atom_set(mon, LTL_PI_FUTEX, false);
+		ltl_atom_set(mon, LTL_BLOCK_ON_RT_MUTEX, false);
+	}
+
+	if (task->flags & PF_KTHREAD) {
+		ltl_atom_set(mon, LTL_KERNEL_THREAD, true);
+
+		/* kernel tasks do not do syscall */
+		ltl_atom_set(mon, LTL_PI_FUTEX, false);
+		ltl_atom_set(mon, LTL_NANOSLEEP, false);
+
+		if (strstarts(task->comm, "migration/"))
+			ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, true);
+		else
+			ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, false);
+
+		if (strstarts(task->comm, "rcu"))
+			ltl_atom_set(mon, LTL_TASK_IS_RCU, true);
+		else
+			ltl_atom_set(mon, LTL_TASK_IS_RCU, false);
+	} else {
+		ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false);
+		ltl_atom_set(mon, LTL_KERNEL_THREAD, false);
+		ltl_atom_set(mon, LTL_TASK_IS_RCU, false);
+		ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, false);
+	}
+
+}
+
+static void handle_sched_switch(void *data, bool preempt, struct task_struct *prev,
+				struct task_struct *next, unsigned int prev_state)
+{
+	if (prev_state & TASK_INTERRUPTIBLE)
+		ltl_atom_pulse(prev, LTL_SLEEP, true);
+	ltl_atom_pulse(next, LTL_WAKE, true);
+}
+
+static void handle_sched_waking(void *data, struct task_struct *task)
+{
+	if (this_cpu_read(hardirq_context)) {
+		ltl_atom_pulse(task, LTL_WOKEN_BY_HARDIRQ, true);
+	} else if (in_task()) {
+		if (current->prio <= task->prio)
+			ltl_atom_pulse(task, LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, true);
+	} else if (in_nmi()) {
+		ltl_atom_pulse(task, LTL_WOKEN_BY_NMI, true);
+	}
+}
+
+static void handle_contention_begin(void *data, void *lock, unsigned int flags)
+{
+	if (flags & LCB_F_RT)
+		ltl_atom_update(current, LTL_BLOCK_ON_RT_MUTEX, true);
+}
+
+static void handle_contention_end(void *data, void *lock, int ret)
+{
+	ltl_atom_update(current, LTL_BLOCK_ON_RT_MUTEX, false);
+}
+
+static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
+{
+	struct ltl_monitor *mon;
+	unsigned long args[6];
+	int op, cmd;
+
+	mon = ltl_get_monitor(current);
+
+	/*
+	 * We do have the lock contention tracepoints for this atomic proposition. However, it
+	 * can take a long time for a task to hit those tracepoints, and the task won't be monitored
+	 * for a long time because an atomic proposition is still unknown.
+	 *
+	 * Therefore, set this here to allow monitoring to begin sooner. We know that at syscall
+	 * enter, a task cannot be blocked by rt_mutex.
+	 *
+	 * This is only necessary for tasks starting before enabling the monitor. It is not a
+	 * problem for tasks starting after enabling the monitor, because we know
+	 * LTL_BLOCK_ON_RT_MUTEX is false for new tasks.
+	 */
+	ltl_atom_set(mon, LTL_BLOCK_ON_RT_MUTEX, false);
+
+	switch (id) {
+	case __NR_nanosleep:
+	case __NR_clock_nanosleep:
+#ifdef __NR_clock_nanosleep_time64
+	case __NR_clock_nanosleep_time64:
+#endif
+		ltl_atom_update(current, LTL_NANOSLEEP, true);
+		break;
+
+	case __NR_futex:
+#ifdef __NR_futex_time64
+	case __NR_futex_time64:
+#endif
+		syscall_get_arguments(current, regs, args);
+		op = args[1];
+		cmd = op & FUTEX_CMD_MASK;
+
+		switch (cmd) {
+		case FUTEX_LOCK_PI:
+		case FUTEX_LOCK_PI2:
+		case FUTEX_WAIT_REQUEUE_PI:
+			ltl_atom_update(current, LTL_PI_FUTEX, true);
+		}
+		break;
+	}
+}
+
+static void handle_sys_exit(void *data, struct pt_regs *regs, long ret)
+{
+	struct ltl_monitor *mon = ltl_get_monitor(current);
+
+	ltl_atom_set(mon, LTL_PI_FUTEX, false);
+	ltl_atom_update(current, LTL_NANOSLEEP, false);
+}
+
+static void handle_kthread_stop(void *data, struct task_struct *task)
+{
+	/* FIXME: this could race with other tracepoint handlers */
+	ltl_atom_update(task, LTL_KTHREAD_SHOULD_STOP, true);
+}
+
+static int enable_sleep(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("rtapp_sleep", sched_waking, handle_sched_waking);
+	rv_attach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin);
+	rv_attach_trace_probe("rtapp_sleep", contention_end, handle_contention_end);
+	rv_attach_trace_probe("rtapp_sleep", sched_switch, handle_sched_switch);
+	rv_attach_trace_probe("rtapp_sleep", sys_enter, handle_sys_enter);
+	rv_attach_trace_probe("rtapp_sleep", sys_exit, handle_sys_exit);
+	rv_attach_trace_probe("rtapp_sleep", sched_kthread_stop, handle_kthread_stop);
+	return 0;
+}
+
+static void disable_sleep(void)
+{
+	rv_detach_trace_probe("rtapp_sleep", sched_waking, handle_sched_waking);
+	rv_detach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin);
+	rv_detach_trace_probe("rtapp_sleep", contention_end, handle_contention_end);
+	rv_detach_trace_probe("rtapp_sleep", sched_switch, handle_sched_switch);
+	rv_detach_trace_probe("rtapp_sleep", sys_enter, handle_sys_enter);
+	rv_detach_trace_probe("rtapp_sleep", sys_exit, handle_sys_exit);
+	rv_detach_trace_probe("rtapp_sleep", sched_kthread_stop, handle_kthread_stop);
+
+	ltl_monitor_destroy();
+}
+
+static struct rv_monitor rv_sleep = {
+	.name = "sleep",
+	.description = "Monitor that RT tasks do not undesirably sleep",
+	.enable = enable_sleep,
+	.disable = disable_sleep,
+};
+
+static int __init register_sleep(void)
+{
+	rv_register_monitor(&rv_sleep, &rv_rtapp);
+	return 0;
+}
+
+static void __exit unregister_sleep(void)
+{
+	rv_unregister_monitor(&rv_sleep);
+}
+
+module_init(register_sleep);
+module_exit(unregister_sleep);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>");
+MODULE_DESCRIPTION("sleep: Monitor that RT tasks do not undesirably sleep");
diff --git a/kernel/trace/rv/monitors/sleep/sleep.h b/kernel/trace/rv/monitors/sleep/sleep.h
new file mode 100644
index 000000000000..6df134739286
--- /dev/null
+++ b/kernel/trace/rv/monitors/sleep/sleep.h
@@ -0,0 +1,293 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME sleep
+
+enum ltl_atom {
+	LTL_BLOCK_ON_RT_MUTEX,
+	LTL_KERNEL_THREAD,
+	LTL_KTHREAD_SHOULD_STOP,
+	LTL_NANOSLEEP,
+	LTL_PI_FUTEX,
+	LTL_RT,
+	LTL_SLEEP,
+	LTL_TASK_IS_MIGRATION,
+	LTL_TASK_IS_RCU,
+	LTL_WAKE,
+	LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
+	LTL_WOKEN_BY_HARDIRQ,
+	LTL_WOKEN_BY_NMI,
+	LTL_NUM_ATOM
+};
+static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+static const char *ltl_atom_str(enum ltl_atom atom)
+{
+	static const char *const names[] = {
+		"b",
+		"ke",
+		"kt",
+		"n",
+		"p",
+		"r",
+		"s",
+		"task_is_m",
+		"task_is_r",
+		"wa",
+		"woken_by_e",
+		"woken_by_h",
+		"woken_by_n",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	S5,
+	S6,
+	S7,
+	S8,
+	S9,
+	S10,
+	RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
+	bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
+	bool val29 = task_is_migration || kthread_should_stop;
+	bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
+	bool val30 = task_is_rcu || val29;
+	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
+	bool val4 = block_on_rt_mutex || val30;
+	bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
+	bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
+	bool val23 = woken_by_hardirq || woken_by_nmi;
+	bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
+	     mon->atoms);
+	bool val14 = woken_by_equal_or_higher_prio || val23;
+	bool wake = test_bit(LTL_WAKE, mon->atoms);
+	bool val13 = !wake;
+	bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
+	bool nanosleep = test_bit(LTL_NANOSLEEP, mon->atoms);
+	bool pi_futex = test_bit(LTL_PI_FUTEX, mon->atoms);
+	bool val9 = pi_futex || nanosleep;
+	bool val11 = val9 || kernel_thread;
+	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
+	bool val2 = !sleep;
+	bool rt = test_bit(LTL_RT, mon->atoms);
+	bool val1 = !rt;
+
+	if (val4)
+		__set_bit(S0, mon->states);
+	if (val2)
+		__set_bit(S3, mon->states);
+	if (val11 && val13)
+		__set_bit(S4, mon->states);
+	if (val11 && val14)
+		__set_bit(S7, mon->states);
+	if (val1)
+		__set_bit(S10, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
+	bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
+	bool val29 = task_is_migration || kthread_should_stop;
+	bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
+	bool val30 = task_is_rcu || val29;
+	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
+	bool val4 = block_on_rt_mutex || val30;
+	bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
+	bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
+	bool val23 = woken_by_hardirq || woken_by_nmi;
+	bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
+	     mon->atoms);
+	bool val14 = woken_by_equal_or_higher_prio || val23;
+	bool wake = test_bit(LTL_WAKE, mon->atoms);
+	bool val13 = !wake;
+	bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
+	bool nanosleep = test_bit(LTL_NANOSLEEP, mon->atoms);
+	bool pi_futex = test_bit(LTL_PI_FUTEX, mon->atoms);
+	bool val9 = pi_futex || nanosleep;
+	bool val11 = val9 || kernel_thread;
+	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
+	bool val2 = !sleep;
+	bool rt = test_bit(LTL_RT, mon->atoms);
+	bool val1 = !rt;
+
+	switch (state) {
+	case S0:
+		if (val4)
+			__set_bit(S0, next);
+		if (val2)
+			__set_bit(S3, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val1)
+			__set_bit(S10, next);
+		break;
+	case S1:
+		if (val4)
+			__set_bit(S0, next);
+		if (val13 && val2)
+			__set_bit(S1, next);
+		if (val1 && val13)
+			__set_bit(S2, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val1 && val14)
+			__set_bit(S5, next);
+		if (val13 && val4)
+			__set_bit(S6, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val14 && val2)
+			__set_bit(S8, next);
+		if (val14 && val4)
+			__set_bit(S9, next);
+		break;
+	case S2:
+		if (val4)
+			__set_bit(S0, next);
+		if (val13 && val2)
+			__set_bit(S1, next);
+		if (val1 && val13)
+			__set_bit(S2, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val1 && val14)
+			__set_bit(S5, next);
+		if (val13 && val4)
+			__set_bit(S6, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val14 && val2)
+			__set_bit(S8, next);
+		if (val14 && val4)
+			__set_bit(S9, next);
+		break;
+	case S3:
+		if (val4)
+			__set_bit(S0, next);
+		if (val2)
+			__set_bit(S3, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val1)
+			__set_bit(S10, next);
+		break;
+	case S4:
+		if (val4)
+			__set_bit(S0, next);
+		if (val13 && val2)
+			__set_bit(S1, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val1 && val14)
+			__set_bit(S5, next);
+		if (val13 && val4)
+			__set_bit(S6, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val14 && val2)
+			__set_bit(S8, next);
+		if (val14 && val4)
+			__set_bit(S9, next);
+		break;
+	case S5:
+		if (val4)
+			__set_bit(S0, next);
+		if (val2)
+			__set_bit(S3, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val1)
+			__set_bit(S10, next);
+		break;
+	case S6:
+		if (val4)
+			__set_bit(S0, next);
+		if (val13 && val2)
+			__set_bit(S1, next);
+		if (val1 && val13)
+			__set_bit(S2, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val1 && val14)
+			__set_bit(S5, next);
+		if (val13 && val4)
+			__set_bit(S6, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val14 && val2)
+			__set_bit(S8, next);
+		if (val14 && val4)
+			__set_bit(S9, next);
+		break;
+	case S7:
+		if (val4)
+			__set_bit(S0, next);
+		if (val2)
+			__set_bit(S3, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val1)
+			__set_bit(S10, next);
+		break;
+	case S8:
+		if (val4)
+			__set_bit(S0, next);
+		if (val2)
+			__set_bit(S3, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val1)
+			__set_bit(S10, next);
+		break;
+	case S9:
+		if (val4)
+			__set_bit(S0, next);
+		if (val2)
+			__set_bit(S3, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val1)
+			__set_bit(S10, next);
+		break;
+	case S10:
+		if (val4)
+			__set_bit(S0, next);
+		if (val2)
+			__set_bit(S3, next);
+		if (val11 && val13)
+			__set_bit(S4, next);
+		if (val11 && val14)
+			__set_bit(S7, next);
+		if (val1)
+			__set_bit(S10, next);
+		break;
+	}
+}
diff --git a/kernel/trace/rv/monitors/sleep/sleep_trace.h b/kernel/trace/rv/monitors/sleep/sleep_trace.h
new file mode 100644
index 000000000000..22eaf31da987
--- /dev/null
+++ b/kernel/trace/rv/monitors/sleep/sleep_trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_SLEEP
+DEFINE_EVENT(event_ltl_monitor_id, event_sleep,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_sleep,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_SLEEP */
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 02c906c9745b..283d5c2fd055 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -173,6 +173,7 @@ TRACE_EVENT(error_ltl_monitor_id,
 	TP_printk("%s[%d]: violation detected", __get_str(comm), __entry->pid)
 );
 #include <monitors/pagefault/pagefault_trace.h>
+#include <monitors/sleep/sleep_trace.h>
 // Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here
 #endif /* CONFIG_LTL_MON_EVENTS_ID */
 #endif /* _TRACE_RV_H */
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl
new file mode 100644
index 000000000000..5479a3a3b164
--- /dev/null
+++ b/tools/verification/models/rtapp/sleep.ltl
@@ -0,0 +1,15 @@
+RULE = always (RT imply (SLEEP imply (RT_FRIENDLY_SLEEP or ALLOWLIST)))
+
+RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
+                and ((not WAKE) until RT_FRIENDLY_WAKE)
+
+RT_VALID_SLEEP_REASON = PI_FUTEX or NANOSLEEP
+
+RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
+                or WOKEN_BY_HARDIRQ
+                or WOKEN_BY_NMI
+
+ALLOWLIST = BLOCK_ON_RT_MUTEX
+         or TASK_IS_RCU
+         or TASK_IS_MIGRATION
+         or KTHREAD_SHOULD_STOP
-- 
2.39.5

[PATCH v2 21/22] rv: Add documentation for rtapp monitor

[Nam Cao]

Add documentation describing the rtapp monitor.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 Documentation/trace/rv/monitor_rtapp.rst | 105 +++++++++++++++++++++++
 1 file changed, 105 insertions(+)
 create mode 100644 Documentation/trace/rv/monitor_rtapp.rst

diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace/rv/monitor_rtapp.rst
new file mode 100644
index 000000000000..1cd188039a7e
--- /dev/null
+++ b/Documentation/trace/rv/monitor_rtapp.rst
@@ -0,0 +1,105 @@
+Scheduler monitors
+==================
+
+- Name: rtapp
+- Type: container for multiple monitors
+- Author: Nam Cao <namcao@linutronix.de>
+
+Description
+-----------
+
+Real-time applications may have design flaws such that they experience unexpected latency and fail
+to meet their time requirements. Often, these flaws follow a few patterns:
+
+  - Page faults: A real-time thread may access memory that does not have a mapped physical backing
+    or must first be copied (such as for copy-on-write). Thus a page fault is raised and the kernel
+    must first perform the expensive action. This causes significant delays to the real-time thread
+  - Priority inversion: A real-time thread blocks waiting for a lower-priority thread. This causes
+    the real-time thread to effectively take on the scheduling priority of the lower-priority
+    thread. For example, the real-time thread needs to access a shared resource that is protected by
+    a non-pi-mutex, but the mutex is currently owned by a non-real-time thread.
+
+The `rtapp` monitor detects these patterns. It aids developers to identify reasons for unexpected
+latency with real-time applications. It is a container of multiple sub-monitors described in the
+following sections.
+
+Monitor pagefault
++++++++++++++++++
+
+The `pagefault` monitor reports real-time tasks raising page faults. Its specification is::
+
+  RULE = always (RT imply not PAGEFAULT)
+
+To fix warnings reported by this monitor, `mlockall()` or `mlock()` can be used to ensure physical
+backing for memory.
+
+This monitor may have false negatives because the pages used by the real-time threads may just
+happen to be directly available during testing. To minimize this, the system can be put under memory
+pressure (e.g. invoking the OOM killer using a program that does `ptr = malloc(SIZE_OF_RAM);
+memset(ptr, 0, SIZE_OF_RAM);`) so that the kernel executes aggressive strategies to recycle as much
+physical memory as possible.
+
+Monitor sleep
++++++++++++++
+
+The `sleep` monitor reports real-time threads sleeping in a manner that may cause undesirable
+latency. Real-time applications should only put a real-time thread to sleep for one of the following
+reasons:
+
+  - Cyclic work: real-time thread sleeps waiting for the next cycle. For this case, only the
+    `nanosleep` syscall should be used. No other method is safe for real-time. For example, threads
+    waiting for timerfd can be woken by softirq which provides no real-time guarantee.
+  - Real-time thread waiting for something to happen (e.g. another thread releasing shared
+    resources, or a completion signal from another thread). In this case, only futexes with priority
+    inheritance (PI) should be used. Applications usually do not use futexes directly, but use PI
+    mutexes and PI condition variables which are built on top of futexes. Be aware that the C
+    library might not implement conditional variables as safe for real-time. As an alternative, the
+    librtpi library exists to provide a conditional variable implementation that is correct for
+    real-time applications in Linux.
+
+Beside the reason for sleeping, the eventual waker should also be real-time-safe. Namely, one of:
+
+  - An equal-or-higher-priority thread
+  - Hard interrupt handler
+  - Non-maskable interrupt handler
+
+This monitor's warning usually means one of the following:
+
+  - Real-time thread is blocked by a non-real-time thread (e.g. due to contention on a mutex without
+    priority inheritance). This is priority inversion.
+  - Time-critical work waits for something which is not safe for real-time (e.g. timerfd).
+  - The work executed by the real-time thread does not need to run at real-time priority at all.
+    This is not a problem for the real-time thread itself, but it is potentially taking the CPU away
+    from other important real-time work.
+
+Application developers may purposely choose to have their real-time application sleep in a way that
+is not safe for real-time. It is debatable whether that is a problem. Application developers must
+analyze the warnings to make a proper assessment.
+
+The monitor's specification is::
+
+  RULE = always (RT imply (SLEEP imply (RT_FRIENDLY_SLEEP or ALLOWLIST)))
+
+  RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
+                  and ((not WAKE) until RT_FRIENDLY_WAKE)
+
+  RT_VALID_SLEEP_REASON = PI_FUTEX or NANOSLEEP
+
+  RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
+                  or WOKEN_BY_HARDIRQ
+                  or WOKEN_BY_NMI
+
+  ALLOWLIST = BLOCK_ON_RT_MUTEX
+           or TASK_IS_RCU
+           or TASK_IS_MIGRATION
+           or KTHREAD_SHOULD_STOP
+
+Beside the scenarios described above, this specification also handle some special cases:
+
+  - `KERNEL_THREAD`: kernel tasks do not have any pattern that can be recognized as valid real-time
+    sleeping reasons. Therefore sleeping reason is not checked for kernel tasks.
+  - `RT_SLEEP_WHITELIST`: to handle known false positives with kernel tasks.
+  - `BLOCK_ON_RT_MUTEX` is included in the allowlist due to its implementation. In the release path
+    of rt_mutex, a boosted task is de-boosted before waking the rt_mutex's waiter. Consequently, the
+    monitor may see a real-time-unsafe wakeup (e.g. non-real-time task waking real-time task). This
+    is actually real-time-safe because preemption is disable for the duration.
-- 
2.39.5

[PATCH v2 22/22] rv: Allow to configure the number of per-task monitor

[Nam Cao]

Now that there are 2 monitors for real-time applications, users may want to
enable both of them simultaneously. Make the number of per-task monitor
configurable. Default it to 2 for now.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 include/linux/rv.h      | 2 +-
 include/linux/sched.h   | 8 +++-----
 kernel/trace/rv/Kconfig | 9 +++++++++
 kernel/trace/rv/rv.c    | 8 ++++----
 4 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/include/linux/rv.h b/include/linux/rv.h
index c8320fa3a94b..204436a73bee 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -75,7 +75,7 @@ static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
  * these are justified.
  */
 #define RV_PER_TASK_MONITORS		1
-#define RV_PER_TASK_MONITOR_INIT	(RV_PER_TASK_MONITORS)
+#define RV_PER_TASK_MONITOR_INIT	(CONFIG_RV_PER_TASK_MONITORS)
 
 union rv_task_monitor {
 	struct da_monitor	da_mon;
diff --git a/include/linux/sched.h b/include/linux/sched.h
index 45be0fa7a5cc..560782493292 100644
--- a/include/linux/sched.h
+++ b/include/linux/sched.h
@@ -1623,12 +1623,10 @@ struct task_struct {
 
 #ifdef CONFIG_RV
 	/*
-	 * Per-task RV monitor. Nowadays fixed in RV_PER_TASK_MONITORS.
-	 * If we find justification for more monitors, we can think
-	 * about adding more or developing a dynamic method. So far,
-	 * none of these are justified.
+	 * Per-task RV monitor, fixed in CONFIG_RV_PER_TASK_MONITORS.
+	 * If memory becomes a concern, we can think about a dynamic method.
 	 */
-	union rv_task_monitor		rv[RV_PER_TASK_MONITORS];
+	union rv_task_monitor		rv[CONFIG_RV_PER_TASK_MONITORS];
 #endif
 
 #ifdef CONFIG_USER_EVENTS
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 942d57575e67..c11bf7e61ebf 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -32,6 +32,15 @@ menuconfig RV
 	  For further information, see:
 	    Documentation/trace/rv/runtime-verification.rst
 
+config RV_PER_TASK_MONITORS
+	int "Maximum number of per-task monitor"
+	depends on RV
+	range 1 8
+	default 2
+	help
+	  This option configures the maximum number of per-task RV monitors that can run
+	  simultaneously.
+
 source "kernel/trace/rv/monitors/wip/Kconfig"
 source "kernel/trace/rv/monitors/wwnr/Kconfig"
 source "kernel/trace/rv/monitors/sched/Kconfig"
diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
index d493fddf411f..ebd4b4b228bf 100644
--- a/kernel/trace/rv/rv.c
+++ b/kernel/trace/rv/rv.c
@@ -165,7 +165,7 @@ struct dentry *get_monitors_root(void)
 LIST_HEAD(rv_monitors_list);
 
 static int task_monitor_count;
-static bool task_monitor_slots[RV_PER_TASK_MONITORS];
+static bool task_monitor_slots[CONFIG_RV_PER_TASK_MONITORS];
 
 int rv_get_task_monitor_slot(void)
 {
@@ -173,12 +173,12 @@ int rv_get_task_monitor_slot(void)
 
 	lockdep_assert_held(&rv_interface_lock);
 
-	if (task_monitor_count == RV_PER_TASK_MONITORS)
+	if (task_monitor_count == CONFIG_RV_PER_TASK_MONITORS)
 		return -EBUSY;
 
 	task_monitor_count++;
 
-	for (i = 0; i < RV_PER_TASK_MONITORS; i++) {
+	for (i = 0; i < CONFIG_RV_PER_TASK_MONITORS; i++) {
 		if (task_monitor_slots[i] == false) {
 			task_monitor_slots[i] = true;
 			return i;
@@ -194,7 +194,7 @@ void rv_put_task_monitor_slot(int slot)
 {
 	lockdep_assert_held(&rv_interface_lock);
 
-	if (slot < 0 || slot >= RV_PER_TASK_MONITORS) {
+	if (slot < 0 || slot >= CONFIG_RV_PER_TASK_MONITORS) {
 		WARN_ONCE(1, "RV releasing an invalid slot!: %d\n", slot);
 		return;
 	}
-- 
2.39.5

Re: [PATCH v2 03/22] rv: Let the reactors take care of buffers

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> Each RV monitor has one static buffer to send to the reactors. If
> multiple
> errors are detected simultaneously, the one buffer could be
> overwritten.
> 
> Instead, leave it to the reactors to handle buffering.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> Cc: Petr Mladek <pmladek@suse.com>
> Cc: John Ogness <john.ogness@linutronix.de>
> Cc: Sergey Senozhatsky <senozhatsky@chromium.org>
> ---
>  include/linux/panic.h            |  3 +++
>  include/linux/printk.h           |  5 ++++
>  include/linux/rv.h               |  9 +++++--
>  include/rv/da_monitor.h          | 45 +++++++-----------------------
> --
>  kernel/panic.c                   | 17 ++++++++----
>  kernel/printk/internal.h         |  1 -
>  kernel/trace/rv/reactor_panic.c  |  8 ++++--
>  kernel/trace/rv/reactor_printk.c |  8 ++++--
>  kernel/trace/rv/rv_reactors.c    |  2 +-
>  9 files changed, 50 insertions(+), 48 deletions(-)
> 
> diff --git a/include/linux/panic.h b/include/linux/panic.h
> index 54d90b6c5f47..3522f8c441f4 100644
> --- a/include/linux/panic.h
> +++ b/include/linux/panic.h
> @@ -3,6 +3,7 @@
>  #define _LINUX_PANIC_H
>  
>  #include <linux/compiler_attributes.h>
> +#include <linux/stdarg.h>
>  #include <linux/types.h>
>  
>  struct pt_regs;
> @@ -10,6 +11,8 @@ struct pt_regs;
>  extern long (*panic_blink)(int state);
>  __printf(1, 2)
>  void panic(const char *fmt, ...) __noreturn __cold;
> +__printf(1, 0)
> +void vpanic(const char *fmt, va_list args) __noreturn __cold;
>  void nmi_panic(struct pt_regs *regs, const char *msg);
>  void check_panic_on_warn(const char *origin);
>  extern void oops_enter(void);
> diff --git a/include/linux/printk.h b/include/linux/printk.h
> index 4217a9f412b2..1b7eebe13f14 100644
> --- a/include/linux/printk.h
> +++ b/include/linux/printk.h
> @@ -154,6 +154,7 @@ int vprintk_emit(int facility, int level,
>  
>  asmlinkage __printf(1, 0)
>  int vprintk(const char *fmt, va_list args);
> +__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args);
>  
>  asmlinkage __printf(1, 2) __cold
>  int _printk(const char *fmt, ...);
> @@ -213,6 +214,10 @@ int vprintk(const char *s, va_list args)
>  {
>  	return 0;
>  }
> +__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args)
> +{
> +	return 0;
> +}
>  static inline __printf(1, 2) __cold
>  int _printk(const char *s, ...)
>  {

From the RV perspective this patch looks really good to me, although
you're doing a bit more than just RV here.
I hate to be the one telling you to split patches (22 is already scary
as it is!) but probably the vpanic and vprintk_deferred belong in
separate patches.

Feel free to mark the RV part (and also 1/22 2/22)

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

Thanks,
Gabriele

> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 3452b5e4b29e..c7c18c06911b 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -38,7 +38,7 @@ union rv_task_monitor {
>  struct rv_reactor {
>  	const char		*name;
>  	const char		*description;
> -	void			(*react)(char *msg);
> +	__printf(1, 2) void	(*react)(const char *msg, ...);
>  };
>  #endif
>  
> @@ -50,7 +50,7 @@ struct rv_monitor {
>  	void			(*disable)(void);
>  	void			(*reset)(void);
>  #ifdef CONFIG_RV_REACTORS
> -	void			(*react)(char *msg);
> +	__printf(1, 2) void	(*react)(const char *msg, ...);
>  #endif
>  };
>  
> @@ -64,6 +64,11 @@ void rv_put_task_monitor_slot(int slot);
>  bool rv_reacting_on(void);
>  int rv_unregister_reactor(struct rv_reactor *reactor);
>  int rv_register_reactor(struct rv_reactor *reactor);
> +#else
> +bool rv_reacting_on(void)
> +{
> +	return false;
> +}
>  #endif /* CONFIG_RV_REACTORS */
>  
>  #endif /* CONFIG_RV */
> diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
> index 510c88bfabd4..15f9ed4e4bb6 100644
> --- a/include/rv/da_monitor.h
> +++ b/include/rv/da_monitor.h
> @@ -19,45 +19,22 @@
>  #ifdef CONFIG_RV_REACTORS
>  
>  #define DECLARE_RV_REACTING_HELPERS(name,
> type)							\
> -static char
> REACT_MSG_##name[1024];								\
> -
> 												\
> -static inline char *format_react_msg_##name(type curr_state, type
> event)			\
> -
> {												\
> -	snprintf(REACT_MSG_##name,
> 1024,							\
> -		 "rv: monitor %s does not allow event %s on state
> %s\n",			\
> -		
> #name,										\
> -		
> model_get_event_name_##name(event),						\
> -		
> model_get_state_name_##name(curr_state));					\
> -	return
> REACT_MSG_##name;								\
> -
> }												\
> -
> 												\
> -static void cond_react_##name(char
> *msg)							\
> +static void cond_react_##name(type curr_state, type
> event)					\
>  {								
> 				\
> -	if
> (rv_##name.react)									\
> -
> 		rv_##name.react(msg);								\
> -
> }												\
> -
> 												\
> -static bool
> rv_reacting_on_##name(void)								\
> -
> {												\
> -	return
> rv_reacting_on();								\
> +	if (!rv_reacting_on() ||
> !rv_##name.react)						\
> +		return;					
> 					\
> +	rv_##name.react("rv: monitor %s does not allow event %s on
> state %s\n",			\
> +			#name,					
> 				\
> +			model_get_event_name_##name(event),	
> 				\
> +			model_get_state_name_##name(curr_state));
> 				\
>  }
>  
>  #else /* CONFIG_RV_REACTOR */
>  
>  #define DECLARE_RV_REACTING_HELPERS(name,
> type)							\
> -static inline char *format_react_msg_##name(type curr_state, type
> event)			\
> -
> {												\
> -	return
> NULL;										\
> -
> }												\
> -
> 												\
> -static void cond_react_##name(char
> *msg)							\
> +static void cond_react_##name(type curr_state, type
> event)					\
>  {								
> 				\
>  	return;						
> 					\
> -
> }												\
> -
> 												\
> -static bool
> rv_reacting_on_##name(void)								\
> -
> {												\
> -	return
> 0;										\
>  }
>  #endif
>  
> @@ -170,8 +147,7 @@ da_event_##name(struct da_monitor *da_mon, enum
> events_##name event)				\
>  		return
> true;									\
>  	}							
> 				\
>  								
> 				\
> -	if
> (rv_reacting_on_##name())								\
> -
> 		cond_react_##name(format_react_msg_##name(curr_state, event));			\
> +	cond_react_##name(curr_state,
> event);							\
>  								
> 				\
>  	trace_error_##name(model_get_state_name_##name(curr_state),
> 				\
>  			  
> model_get_event_name_##name(event));					\
> @@ -202,8 +178,7 @@ static inline bool da_event_##name(struct
> da_monitor *da_mon, struct task_struct
>  		return
> true;									\
>  	}							
> 				\
>  								
> 				\
> -	if
> (rv_reacting_on_##name())								\
> -
> 		cond_react_##name(format_react_msg_##name(curr_state, event));			\
> +	cond_react_##name(curr_state,
> event);							\
>  								
> 				\
>  	trace_error_##name(tsk-
> >pid,								\
>  			  
> model_get_state_name_##name(curr_state),				\
> diff --git a/kernel/panic.c b/kernel/panic.c
> index d8635d5cecb2..df799d784b61 100644
> --- a/kernel/panic.c
> +++ b/kernel/panic.c
> @@ -277,17 +277,16 @@ static void panic_other_cpus_shutdown(bool
> crash_kexec)
>  }
>  
>  /**
> - *	panic - halt the system
> + *	vpanic - halt the system
>   *	@fmt: The text string to print
>   *
>   *	Display a message, then perform cleanups.
>   *
>   *	This function never returns.
>   */
> -void panic(const char *fmt, ...)
> +void vpanic(const char *fmt, va_list args)
>  {
>  	static char buf[1024];
> -	va_list args;
>  	long i, i_next = 0, len;
>  	int state = 0;
>  	int old_cpu, this_cpu;
> @@ -338,9 +337,7 @@ void panic(const char *fmt, ...)
>  
>  	console_verbose();
>  	bust_spinlocks(1);
> -	va_start(args, fmt);
>  	len = vscnprintf(buf, sizeof(buf), fmt, args);
> -	va_end(args);
>  
>  	if (len && buf[len - 1] == '\n')
>  		buf[len - 1] = '\0';
> @@ -477,7 +474,17 @@ void panic(const char *fmt, ...)
>  		mdelay(PANIC_TIMER_STEP);
>  	}
>  }
> +EXPORT_SYMBOL(vpanic);
>  
> +/* Identical to vpanic(), except it takes variadic arguments instead
> of va_list */
> +void panic(const char *fmt, ...)
> +{
> +	va_list args;
> +
> +	va_start(args, fmt);
> +	vpanic(fmt, args);
> +	va_end(args);
> +}
>  EXPORT_SYMBOL(panic);
>  
>  #define TAINT_FLAG(taint, _c_true, _c_false,
> _module)			\
> diff --git a/kernel/printk/internal.h b/kernel/printk/internal.h
> index a91bdf802967..28afdeb58412 100644
> --- a/kernel/printk/internal.h
> +++ b/kernel/printk/internal.h
> @@ -71,7 +71,6 @@ int vprintk_store(int facility, int level,
>  		  const char *fmt, va_list args);
>  
>  __printf(1, 0) int vprintk_default(const char *fmt, va_list args);
> -__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args);
>  
>  void __printk_safe_enter(void);
>  void __printk_safe_exit(void);
> diff --git a/kernel/trace/rv/reactor_panic.c
> b/kernel/trace/rv/reactor_panic.c
> index 0186ff4cbd0b..2587f23db80b 100644
> --- a/kernel/trace/rv/reactor_panic.c
> +++ b/kernel/trace/rv/reactor_panic.c
> @@ -13,9 +13,13 @@
>  #include <linux/init.h>
>  #include <linux/rv.h>
>  
> -static void rv_panic_reaction(char *msg)
> +static void rv_panic_reaction(const char *msg, ...)
>  {
> -	panic(msg);
> +	va_list args;
> +
> +	va_start(args, msg);
> +	vpanic(msg, args);
> +	va_end(args);
>  }
>  
>  static struct rv_reactor rv_panic = {
> diff --git a/kernel/trace/rv/reactor_printk.c
> b/kernel/trace/rv/reactor_printk.c
> index 178759dbf89f..a15db3fc8b82 100644
> --- a/kernel/trace/rv/reactor_printk.c
> +++ b/kernel/trace/rv/reactor_printk.c
> @@ -12,9 +12,13 @@
>  #include <linux/init.h>
>  #include <linux/rv.h>
>  
> -static void rv_printk_reaction(char *msg)
> +static void rv_printk_reaction(const char *msg, ...)
>  {
> -	printk_deferred(msg);
> +	va_list args;
> +
> +	va_start(args, msg);
> +	vprintk_deferred(msg, args);
> +	va_end(args);
>  }
>  
>  static struct rv_reactor rv_printk = {
> diff --git a/kernel/trace/rv/rv_reactors.c
> b/kernel/trace/rv/rv_reactors.c
> index 9501ca886d83..4ce6ebb9d095 100644
> --- a/kernel/trace/rv/rv_reactors.c
> +++ b/kernel/trace/rv/rv_reactors.c
> @@ -490,7 +490,7 @@ void reactor_cleanup_monitor(struct
> rv_monitor_def *mdef)
>  /*
>   * Nop reactor register
>   */
> -static void rv_nop_reaction(char *msg)
> +static void rv_nop_reaction(const char *msg, ...)
>  {
>  }
>  

Re: [PATCH v2 06/22] verification/dot2k: Remove __buff_to_string()

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> str.join() can do what __buff_to_string() does. Therefore replace
> __buff_to_string() to make the scripts more pythonic.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
>  tools/verification/dot2/dot2/dot2k.py | 21 ++++++---------------
>  1 file changed, 6 insertions(+), 15 deletions(-)
> 
> diff --git a/tools/verification/dot2/dot2/dot2k.py
> b/tools/verification/dot2/dot2/dot2k.py
> index dd4b5528a4f2..0922754454b9 100644
> --- a/tools/verification/dot2/dot2/dot2k.py
> +++ b/tools/verification/dot2/dot2/dot2k.py
> @@ -109,15 +109,6 @@ class dot2k(Dot2c):
>          fd.close()
>          return content
>  
> -    def __buff_to_string(self, buff):
> -        string = ""
> -
> -        for line in buff:
> -            string = string + line + "\n"
> -
> -        # cut off the last \n
> -        return string[:-1]
> -
>      def fill_monitor_type(self):
>          return self.monitor_type.upper()
>  
> @@ -148,19 +139,19 @@ class dot2k(Dot2c):
>                  buff.append("\tda_%s_%s(%s%s);" % (handle,
> self.name, event, self.enum_suffix));
>              buff.append("}")
>              buff.append("")
> -        return self.__buff_to_string(buff)
> +        return '\n'.join(buff)
>  
>      def fill_tracepoint_attach_probe(self):
>          buff = []
>          for event in self.events:
>              buff.append("\trv_attach_trace_probe(\"%s\", /* XXX:
> tracepoint */, handle_%s);" % (self.name, event))
> -        return self.__buff_to_string(buff)
> +        return '\n'.join(buff)
>  
>      def fill_tracepoint_detach_helper(self):
>          buff = []
>          for event in self.events:
>              buff.append("\trv_detach_trace_probe(\"%s\", /* XXX:
> tracepoint */, handle_%s);" % (self.name, event))
> -        return self.__buff_to_string(buff)
> +        return '\n'.join(buff)
>  
>      def fill_main_c(self):
>          main_c = self.main_c
> @@ -210,7 +201,7 @@ class dot2k(Dot2c):
>          buff = self.fill_model_h_header()
>          buff += self.format_model()
>  
> -        return self.__buff_to_string(buff)
> +        return '\n'.join(buff)
>  
>      def fill_monitor_class_type(self):
>          if self.monitor_type == "per_task":
> @@ -242,7 +233,7 @@ class dot2k(Dot2c):
>          tp_args_c = ", ".join([b for a,b in tp_args])
>          buff.append("	     TP_PROTO(%s)," % tp_proto_c)
>          buff.append("	     TP_ARGS(%s)" % tp_args_c)
> -        return self.__buff_to_string(buff)
> +        return '\n'.join(buff)
>  
>      def fill_monitor_deps(self):
>          buff = []
> @@ -250,7 +241,7 @@ class dot2k(Dot2c):
>          if self.parent:
>              buff.append("	depends on RV_MON_%s" %
> self.parent.upper())
>              buff.append("	default y")
> -        return self.__buff_to_string(buff)
> +        return '\n'.join(buff)
>  
>      def fill_trace_h(self):
>          trace_h = self.trace_h

Good one, I've been too lazy to do it. Thanks!

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

Re: [PATCH v2 05/22] verification/dot2k: Make a separate dot2k_templates/Kconfig_container

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> A generated container's Kconfig has an incorrect line:
> 
>     select DA_MON_EVENTS_IMPLICIT
> 
> This is due to container generation uses the same template Kconfig
> file as
> deterministic automaton monitor.
> 
> Therefore, make a separate Kconfig template for container which has
> only
> the necessaries for container.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> Alternatively, we could also modify the Python scripts. I tried both
> and
> this solution seems cleaner.
> ---
>  tools/verification/dot2/dot2/dot2k.py                     | 3 ++-
>  tools/verification/dot2/dot2k_templates/Kconfig_container | 5 +++++
>  2 files changed, 7 insertions(+), 1 deletion(-)
>  create mode 100644
> tools/verification/dot2/dot2k_templates/Kconfig_container
> 
> diff --git a/tools/verification/dot2/dot2/dot2k.py
> b/tools/verification/dot2/dot2/dot2k.py
> index 745d35a4a379..dd4b5528a4f2 100644
> --- a/tools/verification/dot2/dot2/dot2k.py
> +++ b/tools/verification/dot2/dot2/dot2k.py
> @@ -35,6 +35,7 @@ class dot2k(Dot2c):
>              self.states = []
>              self.main_c =
> self.__read_file(self.monitor_templates_dir + "main_container.c")
>              self.main_h =
> self.__read_file(self.monitor_templates_dir + "main_container.h")
> +            self.kconfig =
> self.__read_file(self.monitor_templates_dir + "Kconfig_container")
>          else:
>              super().__init__(file_path,
> extra_params.get("model_name"))
>  
> @@ -44,7 +45,7 @@ class dot2k(Dot2c):
>              self.monitor_type = MonitorType
>              self.main_c =
> self.__read_file(self.monitor_templates_dir + "main.c")
>              self.trace_h =
> self.__read_file(self.monitor_templates_dir + "trace.h")
> -        self.kconfig = self.__read_file(self.monitor_templates_dir +
> "Kconfig")
> +            self.kconfig =
> self.__read_file(self.monitor_templates_dir + "Kconfig")
>          self.enum_suffix = "_%s" % self.name
>          self.description = extra_params.get("description",
> self.name) or "auto-generated"
>          self.auto_patch = extra_params.get("auto_patch")
> diff --git
> a/tools/verification/dot2/dot2k_templates/Kconfig_container
> b/tools/verification/dot2/dot2k_templates/Kconfig_container
> new file mode 100644
> index 000000000000..a606111949c2
> --- /dev/null
> +++ b/tools/verification/dot2/dot2k_templates/Kconfig_container
> @@ -0,0 +1,5 @@
> +config RV_MON_%%MODEL_NAME_UP%%
> +	depends on RV
> +	bool "%%MODEL_NAME%% monitor"
> +	help
> +	  %%DESCRIPTION%%

Good catch

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

Re: [PATCH v2 07/22] verification/dot2k: Replace is_container() hack with subparsers

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> dot2k is used for both generating deterministic automaton (DA)
> monitor and
> generating container monitor.
> 
> Generating DA monitor and generating container requires different
> parameters. This is implemented by peeking at sys.argv and check
> whether
> "--container" is specified, and use that information to make some
> parameters optional or required.
> 
> This works, but is quite hacky and ugly.
> 
> Replace this hack with Python's built-in subparsers.
> 

Yeah, that's much neater, thanks!

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> The old commands:
> 
>   python3 dot2/dot2k -d wip.dot -t per_cpu
>   python3 dot2/dot2k -n sched --container
> 
> are equivalent to the new commands:
> 
>   python3 dot2/dot2k monitor -d wip.dot -t per_cpu
>   python3 dot2/dot2k container -n sched
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
>  tools/verification/dot2/dot2/dot2k.py |  2 +-
>  tools/verification/dot2/dot2k         | 37 +++++++++++++++----------
> --
>  2 files changed, 21 insertions(+), 18 deletions(-)
> 
> diff --git a/tools/verification/dot2/dot2/dot2k.py
> b/tools/verification/dot2/dot2/dot2k.py
> index 0922754454b9..9ec99e297012 100644
> --- a/tools/verification/dot2/dot2/dot2k.py
> +++ b/tools/verification/dot2/dot2/dot2k.py
> @@ -19,7 +19,7 @@ class dot2k(Dot2c):
>      monitor_type = "per_cpu"
>  
>      def __init__(self, file_path, MonitorType, extra_params={}):
> -        self.container = extra_params.get("container")
> +        self.container = extra_params.get("subcmd") == "container"
>          self.parent = extra_params.get("parent")
>          self.__fill_rv_templates_dir()
>  
> diff --git a/tools/verification/dot2/dot2k
> b/tools/verification/dot2/dot2k
> index 767064f415e7..133fb17d9d47 100644
> --- a/tools/verification/dot2/dot2k
> +++ b/tools/verification/dot2/dot2k
> @@ -13,30 +13,33 @@ if __name__ == '__main__':
>      import argparse
>      import sys
>  
> -    def is_container():
> -        """Should work even before parsing the arguments"""
> -        return "-c" in sys.argv or "--container" in sys.argv
> -
>      parser = argparse.ArgumentParser(description='transform .dot
> file into kernel rv monitor')
> -    parser.add_argument('-d', "--dot", dest="dot_file", required=not
> is_container())
> -    parser.add_argument('-t', "--monitor_type", dest="monitor_type",
> required=not is_container(),
> -                        help=f"Available options: {',
> '.join(dot2k.monitor_types.keys())}")
> -    parser.add_argument('-n', "--model_name", dest="model_name",
> required=is_container())
>      parser.add_argument("-D", "--description", dest="description",
> required=False)
>      parser.add_argument("-a", "--auto_patch", dest="auto_patch",
>                          action="store_true", required=False,
>                          help="Patch the kernel in place")
> -    parser.add_argument("-p", "--parent", dest="parent",
> -                        required=False, help="Create a monitor
> nested to parent")
> -    parser.add_argument("-c", "--container", dest="container",
> -                        action="store_true", required=False,
> -                        help="Create an empty monitor to be used as
> a container")
> +
> +    subparsers = parser.add_subparsers(dest="subcmd", required=True)
> +
> +    monitor_parser = subparsers.add_parser("monitor")
> +    monitor_parser.add_argument('-n', "--model_name",
> dest="model_name")
> +    monitor_parser.add_argument("-p", "--parent", dest="parent",
> +                                required=False, help="Create a
> monitor nested to parent")
> +    monitor_parser.add_argument('-d', "--dot", dest="dot_file")
> +    monitor_parser.add_argument('-t', "--monitor_type",
> dest="monitor_type",
> +                                help=f"Available options: {',
> '.join(dot2k.monitor_types.keys())}")
> +
> +    container_parser = subparsers.add_parser("container")
> +    container_parser.add_argument('-n', "--model_name",
> dest="model_name", required=True)
> +
>      params = parser.parse_args()
>  
> -    if not is_container():
> -        print("Opening and parsing the dot file %s" %
> params.dot_file)
>      try:
> -        monitor=dot2k(params.dot_file, params.monitor_type,
> vars(params))
> +        if params.subcmd == "monitor":
> +            print("Opening and parsing the dot file %s" %
> params.dot_file)
> +            monitor = dot2k(params.dot_file, params.monitor_type,
> vars(params))
> +        else:
> +            monitor = dot2k(None, None, vars(params))
>      except Exception as e:
>          print('Error: '+ str(e))
>          print("Sorry : :-(")
> @@ -45,7 +48,7 @@ if __name__ == '__main__':
>      print("Writing the monitor into the directory %s" %
> monitor.name)
>      monitor.print_files()
>      print("Almost done, checklist")
> -    if not is_container():
> +    if params.subcmd == "monitor":
>          print("  - Edit the %s/%s.c to add the instrumentation" %
> (monitor.name, monitor.name))
>          print(monitor.fill_tracepoint_tooltip())
>      print(monitor.fill_makefile_tooltip())

Re: [PATCH v2 04/22] verification/dot2k: Make it possible to invoke dot2k without installation

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> Without installation, dot2k doesn't work:
> 
> namcao@yellow:~/linux/tools/verification$ python3 ./dot2/dot2k
> Traceback (most recent call last):
>   File "/home/namcao/linux/tools/verification/./dot2/dot2k", line 12,
> in <module>
>     from dot2.dot2k import dot2k
> ModuleNotFoundError: No module named 'dot2'
> 
> Installing dot2k to the system is not always desirable. Sometimes it
> is not
> even possible (e.g. no root permission).
> 
> Restructure the files to make it work without installing.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>

Mmh, the workflow

pushd tools/verification
...
popd

has always been working in my case, but probably that's because I have
PYTHONPATH="." , not sure how much of a good practice that is.

Anyway, since you're already moving things around in 9/22
("verification/dot2k: Prepare the frontend for LTL inclusion"), does it
make sense to keep the commits separated? Or you could directly move to
rvgen here and just add the ltl related changes in the later commit.

Also, after your changes on my system, I can run the script from the
kernel directory too, which is much better than having to cd to
tools/verification .
If that's something portable, I'd change the default definition of
monitor_templates_dir and allow the user to run the script only from
the kernel root.

What do you think?

Thanks,
Gabriele

> ---
>  tools/verification/dot2/Makefile               | 6 +++---
>  tools/verification/dot2/{ => dot2}/automata.py | 0
>  tools/verification/dot2/{ => dot2}/dot2c.py    | 0
>  tools/verification/dot2/{ => dot2}/dot2k.py    | 0
>  4 files changed, 3 insertions(+), 3 deletions(-)
>  rename tools/verification/dot2/{ => dot2}/automata.py (100%)
>  rename tools/verification/dot2/{ => dot2}/dot2c.py (100%)
>  rename tools/verification/dot2/{ => dot2}/dot2k.py (100%)
> 
> diff --git a/tools/verification/dot2/Makefile
> b/tools/verification/dot2/Makefile
> index 021beb07a521..7a2ec30014b0 100644
> --- a/tools/verification/dot2/Makefile
> +++ b/tools/verification/dot2/Makefile
> @@ -16,10 +16,10 @@ clean:
>  
>  .PHONY: install
>  install:
> -	$(INSTALL) automata.py -D -m 644
> $(DESTDIR)$(PYLIB)/dot2/automata.py
> -	$(INSTALL) dot2c.py -D -m 644
> $(DESTDIR)$(PYLIB)/dot2/dot2c.py
> +	$(INSTALL) dot2/automata.py -D -m 644
> $(DESTDIR)$(PYLIB)/dot2/automata.py
> +	$(INSTALL) dot2/dot2c.py -D -m 644
> $(DESTDIR)$(PYLIB)/dot2/dot2c.py
>  	$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
> -	$(INSTALL) dot2k.py -D -m 644
> $(DESTDIR)$(PYLIB)/dot2/dot2k.py
> +	$(INSTALL) dot2/dot2k.py -D -m 644
> $(DESTDIR)$(PYLIB)/dot2/dot2k.py
>  	$(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/
>  
>  	mkdir -p ${miscdir}/
> diff --git a/tools/verification/dot2/automata.py
> b/tools/verification/dot2/dot2/automata.py
> similarity index 100%
> rename from tools/verification/dot2/automata.py
> rename to tools/verification/dot2/dot2/automata.py
> diff --git a/tools/verification/dot2/dot2c.py
> b/tools/verification/dot2/dot2/dot2c.py
> similarity index 100%
> rename from tools/verification/dot2/dot2c.py
> rename to tools/verification/dot2/dot2/dot2c.py
> diff --git a/tools/verification/dot2/dot2k.py
> b/tools/verification/dot2/dot2/dot2k.py
> similarity index 100%
> rename from tools/verification/dot2/dot2k.py
> rename to tools/verification/dot2/dot2/dot2k.py

Re: [PATCH v2 10/22] Documentation/rv: Prepare monitor synthesis document for LTL inclusion

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> Monitor synthesis from deterministic automaton and linear temporal
> logic
> have a lot in common. Therefore a single document should describe
> both.
> 
> Change da_monitor_synthesis.rst to monitor_synthesis.rst. LTL monitor
> synthesis will be added to this file by a follow-up commit.
> 
> This makes the diff far easier to read. If renaming and adding LTL
> info is
> done in a single commit, git wouldn't recognize it as a rename, but a
> file
> removal and a file addition.
> 
> While at it, correct the old dot2k commands to the new rvgen
> commands.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
>  Documentation/trace/rv/index.rst              |  2 +-
>  ...or_synthesis.rst => monitor_synthesis.rst} | 20 +++++++++--------
> --
>  2 files changed, 11 insertions(+), 11 deletions(-)
>  rename Documentation/trace/rv/{da_monitor_synthesis.rst =>
> monitor_synthesis.rst} (92%)
> 
> diff --git a/Documentation/trace/rv/index.rst
> b/Documentation/trace/rv/index.rst
> index e80e0057feb4..8e411b76ec82 100644
> --- a/Documentation/trace/rv/index.rst
> +++ b/Documentation/trace/rv/index.rst
> @@ -8,7 +8,7 @@ Runtime Verification
>  
>     runtime-verification.rst
>     deterministic_automata.rst
> -   da_monitor_synthesis.rst
> +   monitor_synthesis.rst
>     da_monitor_instrumentation.rst
>     monitor_wip.rst
>     monitor_wwnr.rst
> diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst
> b/Documentation/trace/rv/monitor_synthesis.rst
> similarity index 92%
> rename from Documentation/trace/rv/da_monitor_synthesis.rst
> rename to Documentation/trace/rv/monitor_synthesis.rst
> index 0a92729c8a9b..7d848e204687 100644
> --- a/Documentation/trace/rv/da_monitor_synthesis.rst
> +++ b/Documentation/trace/rv/monitor_synthesis.rst
> @@ -1,5 +1,5 @@
> -Deterministic Automata Monitor Synthesis
> -========================================
> +Runtime verification Monitor Synthesis
> +======================================

+Runtime Verification Monitor Synthesis

The title is capitalised here.

The rest looks good, thanks.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

>  
>  The starting point for the application of runtime verification (RV)
> techniques
>  is the *specification* or *modeling* of the desired (or undesired)
> behavior
> @@ -36,24 +36,24 @@ below::
>                                    |  +----> panic ?
>                                    +-------> <user-specified>
>  
> -DA monitor synthesis
> +RV monitor synthesis
>  --------------------
>  
>  The synthesis of automata-based models into the Linux *RV monitor*
> abstraction
> -is automated by the dot2k tool and the rv/da_monitor.h header file
> that
> +is automated by the rvgen tool and the rv/da_monitor.h header file
> that
>  contains a set of macros that automatically generate the monitor's
> code.
>  
> -dot2k
> +rvgen
>  -----
>  
> -The dot2k utility leverages dot2c by converting an automaton model
> in
> +The rvgen utility leverages dot2c by converting an automaton model
> in
>  the DOT format into the C representation [1] and creating the
> skeleton of
>  a kernel monitor in C.
>  
>  For example, it is possible to transform the wip.dot model present
> in
>  [1] into a per-cpu monitor with the following command::
>  
> -  $ dot2k -d wip.dot -t per_cpu
> +  $ rvgen monitor -c da -s wip.dot -t per_cpu
>  
>  This will create a directory named wip/ with the following files:
>  
> @@ -87,7 +87,7 @@ the second for monitors with per-cpu instances, and
> the third with per-task
>  instances.
>  
>  In all cases, the 'name' argument is a string that identifies the
> monitor, and
> -the 'type' argument is the data type used by dot2k on the
> representation of
> +the 'type' argument is the data type used by rvgen on the
> representation of
>  the model in C.
>  
>  For example, the wip model with two states and three events can be
> @@ -134,7 +134,7 @@ Final remarks
>  -------------
>  
>  With the monitor synthesis in place using the rv/da_monitor.h and
> -dot2k, the developer's work should be limited to the instrumentation
> +rvgen, the developer's work should be limited to the instrumentation
>  of the system, increasing the confidence in the overall approach.
>  
>  [1] For details about deterministic automata format and the
> translation
> @@ -142,6 +142,6 @@ from one representation to another, see::
>  
>    Documentation/trace/rv/deterministic_automata.rst
>  
> -[2] dot2k appends the monitor's name suffix to the events enums to
> +[2] rvgen appends the monitor's name suffix to the events enums to
>  avoid conflicting variables when exporting the global vmlinux.h
>  use by BPF programs.

Re: [PATCH v2 08/22] rv: rename CONFIG_DA_MON_EVENTS to CONFIG_RV_MON_EVENTS

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> CONFIG_DA_MON_EVENTS is not specific to deterministic automaton. It
> could
> be used for other monitor types. Therefore rename it to
> CONFIG_RV_MON_EVENTS.
> 
> This prepares for the introduction of linear temporal logic monitor.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

Re: [PATCH v2 13/22] rv: Add support for LTL monitors

[Gabriele Monaco]

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

Re: [PATCH v2 22/22] rv: Allow to configure the number of per-task monitor

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> Now that there are 2 monitors for real-time applications, users may
> want to
> enable both of them simultaneously. Make the number of per-task
> monitor
> configurable. Default it to 2 for now.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
>  include/linux/rv.h      | 2 +-
>  include/linux/sched.h   | 8 +++-----
>  kernel/trace/rv/Kconfig | 9 +++++++++
>  kernel/trace/rv/rv.c    | 8 ++++----
>  4 files changed, 17 insertions(+), 10 deletions(-)
> 
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index c8320fa3a94b..204436a73bee 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -75,7 +75,7 @@ static inline bool rv_ltl_all_atoms_known(struct
> ltl_monitor *mon)
>   * these are justified.
>   */
>  #define RV_PER_TASK_MONITORS		1

We could get rid of RV_PER_TASK_MONITORS too I guess.

Rest looks good, thanks.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> -#define RV_PER_TASK_MONITOR_INIT	(RV_PER_TASK_MONITORS)
> +#define
> RV_PER_TASK_MONITOR_INIT	(CONFIG_RV_PER_TASK_MONITORS)
>  
>  union rv_task_monitor {
>  	struct da_monitor	da_mon;
> diff --git a/include/linux/sched.h b/include/linux/sched.h
> index 45be0fa7a5cc..560782493292 100644
> --- a/include/linux/sched.h
> +++ b/include/linux/sched.h
> @@ -1623,12 +1623,10 @@ struct task_struct {
>  
>  #ifdef CONFIG_RV
>  	/*
> -	 * Per-task RV monitor. Nowadays fixed in
> RV_PER_TASK_MONITORS.
> -	 * If we find justification for more monitors, we can think
> -	 * about adding more or developing a dynamic method. So far,
> -	 * none of these are justified.
> +	 * Per-task RV monitor, fixed in
> CONFIG_RV_PER_TASK_MONITORS.
> +	 * If memory becomes a concern, we can think about a dynamic
> method.
>  	 */
> -	union rv_task_monitor		rv[RV_PER_TASK_MONITORS];
> +	union
> rv_task_monitor		rv[CONFIG_RV_PER_TASK_MONITORS];
>  #endif
>  
>  #ifdef CONFIG_USER_EVENTS
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 942d57575e67..c11bf7e61ebf 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -32,6 +32,15 @@ menuconfig RV
>  	  For further information, see:
>  	    Documentation/trace/rv/runtime-verification.rst
>  
> +config RV_PER_TASK_MONITORS
> +	int "Maximum number of per-task monitor"
> +	depends on RV
> +	range 1 8
> +	default 2
> +	help
> +	  This option configures the maximum number of per-task RV
> monitors that can run
> +	  simultaneously.
> +
>  source "kernel/trace/rv/monitors/wip/Kconfig"
>  source "kernel/trace/rv/monitors/wwnr/Kconfig"
>  source "kernel/trace/rv/monitors/sched/Kconfig"
> diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
> index d493fddf411f..ebd4b4b228bf 100644
> --- a/kernel/trace/rv/rv.c
> +++ b/kernel/trace/rv/rv.c
> @@ -165,7 +165,7 @@ struct dentry *get_monitors_root(void)
>  LIST_HEAD(rv_monitors_list);
>  
>  static int task_monitor_count;
> -static bool task_monitor_slots[RV_PER_TASK_MONITORS];
> +static bool task_monitor_slots[CONFIG_RV_PER_TASK_MONITORS];
>  
>  int rv_get_task_monitor_slot(void)
>  {
> @@ -173,12 +173,12 @@ int rv_get_task_monitor_slot(void)
>  
>  	lockdep_assert_held(&rv_interface_lock);
>  
> -	if (task_monitor_count == RV_PER_TASK_MONITORS)
> +	if (task_monitor_count == CONFIG_RV_PER_TASK_MONITORS)
>  		return -EBUSY;
>  
>  	task_monitor_count++;
>  
> -	for (i = 0; i < RV_PER_TASK_MONITORS; i++) {
> +	for (i = 0; i < CONFIG_RV_PER_TASK_MONITORS; i++) {
>  		if (task_monitor_slots[i] == false) {
>  			task_monitor_slots[i] = true;
>  			return i;
> @@ -194,7 +194,7 @@ void rv_put_task_monitor_slot(int slot)
>  {
>  	lockdep_assert_held(&rv_interface_lock);
>  
> -	if (slot < 0 || slot >= RV_PER_TASK_MONITORS) {
> +	if (slot < 0 || slot >= CONFIG_RV_PER_TASK_MONITORS) {
>  		WARN_ONCE(1, "RV releasing an invalid slot!: %d\n",
> slot);
>  		return;
>  	}

Re: [PATCH v2 04/22] verification/dot2k: Make it possible to invoke dot2k without installation

[Nam Cao]

On Fri, Apr 11, 2025 at 11:23:25AM +0200, Gabriele Monaco wrote:
> On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > Without installation, dot2k doesn't work:
> >
> > namcao@yellow:~/linux/tools/verification$ python3 ./dot2/dot2k
> > Traceback (most recent call last):
> >   File "/home/namcao/linux/tools/verification/./dot2/dot2k", line 12,
> > in <module>
> >     from dot2.dot2k import dot2k
> > ModuleNotFoundError: No module named 'dot2'
> > 
> > Installing dot2k to the system is not always desirable. Sometimes it
> > is not
> > even possible (e.g. no root permission).
> > 
> > Restructure the files to make it work without installing.
> > 
> > Signed-off-by: Nam Cao <namcao@linutronix.de>
> 
> Mmh, the workflow
> 
> pushd tools/verification
> ...
> popd
>
> 
> has always been working in my case, but probably that's because I have
> PYTHONPATH="." , not sure how much of a good practice that is.

Ahh, PYTHONPATH is the trick. But that shouldn't be required. The scripts
should work out of the box without any environment setup.

> Anyway, since you're already moving things around in 9/22
> ("verification/dot2k: Prepare the frontend for LTL inclusion"), does it
> make sense to keep the commits separated? Or you could directly move to
> rvgen here and just add the ltl related changes in the later commit.

Yes, it makes sense to move them to rvgen here.

> Also, after your changes on my system, I can run the script from the
> kernel directory too, which is much better than having to cd to
> tools/verification .
> If that's something portable, I'd change the default definition of
> monitor_templates_dir and allow the user to run the script only from
> the kernel root.
> 
> What do you think?

I actually prefer running the script from tools/verification. We can allow
user to run from anywhere, with something like:

 class dot2k(Monitor, Dot2c):
-    monitor_templates_dir = "rvgen/templates/dot2k"
+    monitor_templates_dir = os.path.join(os.path.dirname(__file__), "../../rvgen/templates/dot2k")

Best regards,
Nam

Re: [PATCH v2 13/22] rv: Add support for LTL monitors

[Nam Cao]

On Fri, Apr 11, 2025 at 01:17:30PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > +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

I have no preference for either, so sure!

> > 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? :)

YES!

> Anyway I really like your approach, very neat.

Thank you! I'm very happy to have found a way to escape the macros.

> > +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?

Yes.

> 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

Yes, either can work.

> 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.

Thank you,
Nam

Re: [PATCH v2 04/22] verification/dot2k: Make it possible to invoke dot2k without installation

[Gabriele Monaco]

On Fri, 2025-04-11 at 16:04 +0200, Nam Cao wrote:
> On Fri, Apr 11, 2025 at 11:23:25AM +0200, Gabriele Monaco wrote:
> > On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > > Without installation, dot2k doesn't work:
> > > 
> > > namcao@yellow:~/linux/tools/verification$ python3 ./dot2/dot2k
> > > Traceback (most recent call last):
> > >   File "/home/namcao/linux/tools/verification/./dot2/dot2k", line
> > > 12,
> > > in <module>
> > >     from dot2.dot2k import dot2k
> > > ModuleNotFoundError: No module named 'dot2'
> > > 
> > > Installing dot2k to the system is not always desirable. Sometimes
> > > it
> > > is not
> > > even possible (e.g. no root permission).
> > > 
> > > Restructure the files to make it work without installing.
> > > 
> > > Signed-off-by: Nam Cao <namcao@linutronix.de>
> > 
> > Mmh, the workflow
> > 
> > pushd tools/verification
> > ...
> > popd
> > 
> > 
> > has always been working in my case, but probably that's because I
> > have
> > PYTHONPATH="." , not sure how much of a good practice that is.
> 
> Ahh, PYTHONPATH is the trick. But that shouldn't be required. The
> scripts
> should work out of the box without any environment setup.
> 
> > Anyway, since you're already moving things around in 9/22
> > ("verification/dot2k: Prepare the frontend for LTL inclusion"),
> > does it
> > make sense to keep the commits separated? Or you could directly
> > move to
> > rvgen here and just add the ltl related changes in the later
> > commit.
> 
> Yes, it makes sense to move them to rvgen here.
> 
> > Also, after your changes on my system, I can run the script from
> > the
> > kernel directory too, which is much better than having to cd to
> > tools/verification .
> > If that's something portable, I'd change the default definition of
> > monitor_templates_dir and allow the user to run the script only
> > from
> > the kernel root.
> > 
> > What do you think?
> 
> I actually prefer running the script from tools/verification. We can
> allow
> user to run from anywhere, with something like:
> 
>  class dot2k(Monitor, Dot2c):
> -    monitor_templates_dir = "rvgen/templates/dot2k"
> +    monitor_templates_dir = os.path.join(os.path.dirname(__file__),
> "../../rvgen/templates/dot2k")

That looks like a good option!

Thanks,
Gabriele

Re: [PATCH v2 03/22] rv: Let the reactors take care of buffers

[Petr Mladek]

On Fri 2025-04-11 09:37:19, Nam Cao wrote:
> Each RV monitor has one static buffer to send to the reactors. If multiple
> errors are detected simultaneously, the one buffer could be overwritten.
> 
> Instead, leave it to the reactors to handle buffering.
> 
>  include/linux/panic.h            |  3 +++
>  include/linux/printk.h           |  5 ++++
>  include/linux/rv.h               |  9 +++++--
>  include/rv/da_monitor.h          | 45 +++++++-------------------------
>  kernel/panic.c                   | 17 ++++++++----
>  kernel/printk/internal.h         |  1 -
>  kernel/trace/rv/reactor_panic.c  |  8 ++++--
>  kernel/trace/rv/reactor_printk.c |  8 ++++--
>  kernel/trace/rv/rv_reactors.c    |  2 +-
>  9 files changed, 50 insertions(+), 48 deletions(-)

For the changes in the printk and panic code:

Reviewed-by: Petr Mladek <pmladek@suse.com>    # printk, panic

I have just briefly looked at the changes in the rv code.
I wonder if a __printf(1, 2) declaration might be needed
in the printk and panic reactors code, see below.

> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -38,7 +38,7 @@ union rv_task_monitor {
>  struct rv_reactor {
>  	const char		*name;
>  	const char		*description;
> -	void			(*react)(char *msg);
> +	__printf(1, 2) void	(*react)(const char *msg, ...);
>  };
>  #endif
>  
> @@ -50,7 +50,7 @@ struct rv_monitor {
>  	void			(*disable)(void);
>  	void			(*reset)(void);
>  #ifdef CONFIG_RV_REACTORS
> -	void			(*react)(char *msg);
> +	__printf(1, 2) void	(*react)(const char *msg, ...);
>  #endif
>  };
>  
> --- a/kernel/trace/rv/reactor_printk.c
> +++ b/kernel/trace/rv/reactor_printk.c
> @@ -12,9 +12,13 @@
>  #include <linux/init.h>
>  #include <linux/rv.h>
>  
> -static void rv_printk_reaction(char *msg)
> +static void rv_printk_reaction(const char *msg, ...)

I wonder whether "make W=1 kernel/trace/rv/reactor_printk.o" would
start complaining about that this function is a candidate for
‘gnu_printf’ format attribute.

I am not sure. Maybe it is enough that this function is later assigned to
the .react callback in struct rv_reactor.

I wanted to tried it myself. But I was not able to compile the
code in linux-next. I got something like:

./include/linux/rv.h: In function ‘rv_ltl_valid_state’:
./include/linux/rv.h:55:43: error: ‘struct ltl_monitor’ has no member named ‘states’
   55 |         for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
      |                                           ^~
...

I am actually not sure against which tree I should apply this patchset.
It did apply on linux-next after skipping the 1st patch.
But it does not compile there.

And there are more conflicts when I tried to apply it
on Linus' master.

>  {
> -	printk_deferred(msg);
> +	va_list args;
> +
> +	va_start(args, msg);
> +	vprintk_deferred(msg, args);
> +	va_end(args);
>  }

The __printf statement might be missing also in the other two
reactors (panic, nop).

Best Regards,
Petr

Re: [PATCH v2 03/22] rv: Let the reactors take care of buffers

[Nam Cao]

On Tue, Apr 15, 2025 at 11:32:44AM +0200, Petr Mladek wrote:
> On Fri 2025-04-11 09:37:19, Nam Cao wrote:
> > -static void rv_printk_reaction(char *msg)
> > +static void rv_printk_reaction(const char *msg, ...)
> 
> I wonder whether "make W=1 kernel/trace/rv/reactor_printk.o" would
> start complaining about that this function is a candidate for
> ‘gnu_printf’ format attribute.

I checked, it does. Thanks for pointing it out.

> I am not sure. Maybe it is enough that this function is later assigned to
> the .react callback in struct rv_reactor.
> 
> I wanted to tried it myself. But I was not able to compile the
> code in linux-next. I got something like:
> 
> ./include/linux/rv.h: In function ‘rv_ltl_valid_state’:
> ./include/linux/rv.h:55:43: error: ‘struct ltl_monitor’ has no member named ‘states’
>    55 |         for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
>       |                                           ^~

This is a problem with the series. For now, you could "fix" this error with
CONFIG_RV_MON_RTAPP=y. I will fix it up properly in the next version.
> ...
> 
> I am actually not sure against which tree I should apply this patchset.
> It did apply on linux-next after skipping the 1st patch.
> But it does not compile there.

linux-next is supposed to be fine. It doesn't build due to a problem
introduced by this series.

> The __printf statement might be missing also in the other two
> reactors (panic, nop).

Yes. Will be fixed.

Thanks for the review!
Nam

Re: [PATCH v2 19/22] rv: Add rtapp_pagefault monitor

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> Userspace real-time applications may have design flaws that they
> raise
> page faults in real-time threads, and thus have unexpected latencies.
> 
> Add an linear temporal logic monitor to detect this scenario.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> Cc: Catalin Marinas <catalin.marinas@arm.com>
> Cc: Will Deacon <will@kernel.org>
> Cc: Paul Walmsley <paul.walmsley@sifive.com>
> Cc: Palmer Dabbelt <palmer@dabbelt.com>
> Cc: Albert Ou <aou@eecs.berkeley.edu>
> Cc: Alexandre Ghiti <alex@ghiti.fr>
> Cc: Thomas Gleixner <tglx@linutronix.de>
> Cc: Ingo Molnar <mingo@redhat.com>
> Cc: Borislav Petkov <bp@alien8.de>
> Cc: Dave Hansen <dave.hansen@linux.intel.com>
> Cc: x86@kernel.org
> Cc: H. Peter Anvin <hpa@zytor.com>
> Cc: Andy Lutomirski <luto@kernel.org>
> Cc: Peter Zijlstra <peterz@infradead.org>
> Cc: linux-arm-kernel@lists.infradead.org
> Cc: linux-riscv@lists.infradead.org
> ---
>  kernel/trace/rv/Kconfig                       |  1 +
>  kernel/trace/rv/Makefile                      |  1 +
>  kernel/trace/rv/monitors/pagefault/Kconfig    | 11 +++
>  .../trace/rv/monitors/pagefault/pagefault.c   | 83
> +++++++++++++++++++
>  .../trace/rv/monitors/pagefault/pagefault.h   | 57 +++++++++++++
>  .../rv/monitors/pagefault/pagefault_trace.h   | 14 ++++
>  kernel/trace/rv/rv_trace.h                    |  1 +
>  tools/verification/models/rtapp/pagefault.ltl |  1 +
>  8 files changed, 169 insertions(+)
>  create mode 100644 kernel/trace/rv/monitors/pagefault/Kconfig
>  create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.c
>  create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.h
>  create mode 100644
> kernel/trace/rv/monitors/pagefault/pagefault_trace.h
>  create mode 100644 tools/verification/models/rtapp/pagefault.ltl
> 
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 5c407d291661..6f86d8501e87 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -42,6 +42,7 @@ source "kernel/trace/rv/monitors/scpd/Kconfig"
>  source "kernel/trace/rv/monitors/snep/Kconfig"
>  source "kernel/trace/rv/monitors/sncid/Kconfig"
>  source "kernel/trace/rv/monitors/rtapp/Kconfig"
> +source "kernel/trace/rv/monitors/pagefault/Kconfig"
>  # Add new monitors here
>  
>  config RV_REACTORS
> diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
> index 9b28c2419995..353ecf939d0e 100644
> --- a/kernel/trace/rv/Makefile
> +++ b/kernel/trace/rv/Makefile
> @@ -13,6 +13,7 @@ obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o
>  obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o
>  obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o
>  obj-$(CONFIG_RV_MON_RTAPP) += monitors/rtapp/rtapp.o
> +obj-$(CONFIG_RV_MON_PAGEFAULT) += monitors/pagefault/pagefault.o
>  # Add new monitors here
>  obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
>  obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
> diff --git a/kernel/trace/rv/monitors/pagefault/Kconfig
> b/kernel/trace/rv/monitors/pagefault/Kconfig
> new file mode 100644
> index 000000000000..b31dee208459
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/pagefault/Kconfig
> @@ -0,0 +1,11 @@
> +# SPDX-License-Identifier: GPL-2.0-only
> +#
> +config RV_MON_PAGEFAULT
> +	depends on RV
> +	select RV_LTL_MONITOR
> +	depends on RV_MON_RTAPP
> +	default y
> +	select LTL_MON_EVENTS_ID
> +	bool "pagefault monitor"
> +	help
> +	  Monitor that real-time tasks do not raise page faults
> diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.c
> b/kernel/trace/rv/monitors/pagefault/pagefault.c
> new file mode 100644
> index 000000000000..9f7a4cba39a1
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/pagefault/pagefault.c
> @@ -0,0 +1,83 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/ftrace.h>
> +#include <linux/tracepoint.h>
> +#include <linux/kernel.h>
> +#include <linux/module.h>
> +#include <linux/init.h>
> +#include <linux/rv.h>
> +#include <rv/instrumentation.h>
> +
> +#define MODULE_NAME "pagefault"
> +
> +#include <rv_trace.h>
> +#include <trace/events/exceptions.h>
> +#include <monitors/rtapp/rtapp.h>
> +
> +#include "pagefault.h"
> +#include <rv/ltl_monitor.h>
> +
> +static void ltl_atoms_fetch(struct task_struct *task, struct
> ltl_monitor *mon)
> +{
> +	ltl_atom_set(mon, LTL_RT, rt_task(task));
> +}
> +
> +static void ltl_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon, bool task_creation)
> +{
> +	if (task_creation)
> +		ltl_atom_set(mon, LTL_PAGEFAULT, false);
> +}
> +
> +static void handle_page_fault(void *data, unsigned long address,
> struct pt_regs *regs,
> +			      unsigned long error_code)
> +{
> +	ltl_atom_pulse(current, LTL_PAGEFAULT, true);
> +}
> +
> +static int enable_pagefault(void)
> +{
> +	int retval;
> +
> +	retval = ltl_monitor_init();
> +	if (retval)
> +		return retval;
> +
> +	rv_attach_trace_probe("pagefault", page_fault_kernel,
> handle_page_fault);
> +	rv_attach_trace_probe("pagefault", page_fault_user,
> handle_page_fault);
> +
> +	return 0;
> +}
> +
> +static void disable_pagefault(void)
> +{
> +	rv_pagefault.enabled = 0;
> +
> +	rv_detach_trace_probe("rtapp_pagefault", page_fault_kernel,
> handle_page_fault);
> +	rv_detach_trace_probe("rtapp_pagefault", page_fault_user,
> handle_page_fault);
> +
> +	ltl_monitor_destroy();
> +}
> +
> +static struct rv_monitor rv_pagefault = {
> +	.name = "pagefault",
> +	.description = "Monitor that RT tasks do not raise page
> faults",
> +	.enable = enable_pagefault,
> +	.disable = disable_pagefault,
> +};
> +
> +static int __init register_pagefault(void)
> +{
> +	rv_register_monitor(&rv_pagefault, &rv_rtapp);
> +	return 0;

Any reason why you aren't returning the error value from the monitor
registration?

Other than that, the monitor seems neat and reasonably easy to
generate.

May not be necessary in this series, but try to keep compatibility with
the userspace RV tool as well, you need to have some special case in
its tracing components because fields are not matching:
 # rv mon sleep -t
         rcuc/11-108      [011] event <CANT FIND FIELD final_state>   
(null) x (null)                   -> (null)                   Y
         rcuc/11-108      [011] event <CANT FIND FIELD final_state>   
(null) x (null)                   -> (null)                   Y
      ktimers/11-109      [011] event <CANT FIND FIELD final_state>   
(null) x (null)                   -> (null)                   Y
 
Thanks,
Gabriele

Re: [PATCH v2 19/22] rv: Add rtapp_pagefault monitor

[Nam Cao]

On Tue, Apr 15, 2025 at 02:31:43PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > +static int __init register_pagefault(void)
> > +{
> > +	rv_register_monitor(&rv_pagefault, &rv_rtapp);
> > +	return 0;
> 
> Any reason why you aren't returning the error value from the monitor
> registration?

Copy-paste from dot2k :P

> Other than that, the monitor seems neat and reasonably easy to
> generate.
> 
> May not be necessary in this series, but try to keep compatibility with
> the userspace RV tool as well, you need to have some special case in
> its tracing components because fields are not matching:
>  # rv mon sleep -t
>          rcuc/11-108      [011] event <CANT FIND FIELD final_state>   
> (null) x (null)                   -> (null)                   Y
>          rcuc/11-108      [011] event <CANT FIND FIELD final_state>   
> (null) x (null)                   -> (null)                   Y
>       ktimers/11-109      [011] event <CANT FIND FIELD final_state>   
> (null) x (null)                   -> (null)                   Y

I have this userspace RV tool in my "later" TODO list, if that's okay.

Honestly, I haven't looked at what it does yet. perf already does what I
need.

Best regards,
Nam

Re: [PATCH v2 19/22] rv: Add rtapp_pagefault monitor

[Gabriele Monaco]

On Tue, 2025-04-15 at 14:38 +0200, Nam Cao wrote:
> On Tue, Apr 15, 2025 at 02:31:43PM +0200, Gabriele Monaco wrote:
> > On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > > +static int __init register_pagefault(void)
> > > +{
> > > +	rv_register_monitor(&rv_pagefault, &rv_rtapp);
> > > +	return 0;
> > 
> > Any reason why you aren't returning the error value from the
> > monitor
> > registration?
> 
> Copy-paste from dot2k :P

Mmh, you're right! All other monitors are broken in this sense..

> 
> > Other than that, the monitor seems neat and reasonably easy to
> > generate.
> > 
> > May not be necessary in this series, but try to keep compatibility
> > with
> > the userspace RV tool as well, you need to have some special case
> > in
> > its tracing components because fields are not matching:
> >  # rv mon sleep -t
> >          rcuc/11-108      [011] event <CANT FIND FIELD
> > final_state>   
> > (null) x (null)                   -> (null)                   Y
> >          rcuc/11-108      [011] event <CANT FIND FIELD
> > final_state>   
> > (null) x (null)                   -> (null)                   Y
> >       ktimers/11-109      [011] event <CANT FIND FIELD
> > final_state>   
> > (null) x (null)                   -> (null)                   Y
> 
> I have this userspace RV tool in my "later" TODO list, if that's
> okay.
> 
> Honestly, I haven't looked at what it does yet. perf already does
> what I
> need.

Yeah, no rush, the tool is mostly for enabling the monitor and reactors
in a single command, the rest (tracing) you can already do with perf,
trace-cmd and friends, after enabling the monitor manually, of course.

We may even consider integrating RV in other tools instead of
maintaining a separate one, but that's for another day.

Thanks,
Gabriele

Re: [PATCH v2 21/22] rv: Add documentation for rtapp monitor

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> Add documentation describing the rtapp monitor.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
>  Documentation/trace/rv/monitor_rtapp.rst | 105
> +++++++++++++++++++++++
>  1 file changed, 105 insertions(+)
>  create mode 100644 Documentation/trace/rv/monitor_rtapp.rst
> 
> diff --git a/Documentation/trace/rv/monitor_rtapp.rst
> b/Documentation/trace/rv/monitor_rtapp.rst
> new file mode 100644
> index 000000000000..1cd188039a7e
> --- /dev/null
> +++ b/Documentation/trace/rv/monitor_rtapp.rst
> @@ -0,0 +1,105 @@
> +Scheduler monitors
> +==================
> +
> +- Name: rtapp
> +- Type: container for multiple monitors
> +- Author: Nam Cao <namcao@linutronix.de>
> +
> +Description
> +-----------
> +
> +Real-time applications may have design flaws such that they
> experience unexpected latency and fail
> +to meet their time requirements. Often, these flaws follow a few
> patterns:
> +
> +  - Page faults: A real-time thread may access memory that does not
> have a mapped physical backing
> +    or must first be copied (such as for copy-on-write). Thus a page
> fault is raised and the kernel
> +    must first perform the expensive action. This causes significant
> delays to the real-time thread
> +  - Priority inversion: A real-time thread blocks waiting for a
> lower-priority thread. This causes
> +    the real-time thread to effectively take on the scheduling
> priority of the lower-priority
> +    thread. For example, the real-time thread needs to access a
> shared resource that is protected by
> +    a non-pi-mutex, but the mutex is currently owned by a non-real-
> time thread.
> +
> +The `rtapp` monitor detects these patterns. It aids developers to
> identify reasons for unexpected
> +latency with real-time applications. It is a container of multiple
> sub-monitors described in the
> +following sections.
> +
> +Monitor pagefault
> ++++++++++++++++++
> +
> +The `pagefault` monitor reports real-time tasks raising page faults.
> Its specification is::
> +
> +  RULE = always (RT imply not PAGEFAULT)
> +
> +To fix warnings reported by this monitor, `mlockall()` or `mlock()`
> can be used to ensure physical
> +backing for memory.
> +
> +This monitor may have false negatives because the pages used by the
> real-time threads may just
> +happen to be directly available during testing. To minimize this,
> the system can be put under memory
> +pressure (e.g. invoking the OOM killer using a program that does
> `ptr = malloc(SIZE_OF_RAM);
> +memset(ptr, 0, SIZE_OF_RAM);`) so that the kernel executes
> aggressive strategies to recycle as much
> +physical memory as possible.
> +
> +Monitor sleep
> ++++++++++++++
> +
> +The `sleep` monitor reports real-time threads sleeping in a manner
> that may cause undesirable
> +latency. Real-time applications should only put a real-time thread
> to sleep for one of the following
> +reasons:
> +
> +  - Cyclic work: real-time thread sleeps waiting for the next cycle.
> For this case, only the
> +    `nanosleep` syscall should be used. No other method is safe for
> real-time. For example, threads
> +    waiting for timerfd can be woken by softirq which provides no
> real-time guarantee.
> +  - Real-time thread waiting for something to happen (e.g. another
> thread releasing shared
> +    resources, or a completion signal from another thread). In this
> case, only futexes with priority
> +    inheritance (PI) should be used. Applications usually do not use
> futexes directly, but use PI
> +    mutexes and PI condition variables which are built on top of
> futexes. Be aware that the C
> +    library might not implement conditional variables as safe for
> real-time. As an alternative, the
> +    librtpi library exists to provide a conditional variable
> implementation that is correct for
> +    real-time applications in Linux.
> +
> +Beside the reason for sleeping, the eventual waker should also be
> real-time-safe. Namely, one of:
> +
> +  - An equal-or-higher-priority thread
> +  - Hard interrupt handler
> +  - Non-maskable interrupt handler
> +
> +This monitor's warning usually means one of the following:
> +
> +  - Real-time thread is blocked by a non-real-time thread (e.g. due
> to contention on a mutex without
> +    priority inheritance). This is priority inversion.
> +  - Time-critical work waits for something which is not safe for
> real-time (e.g. timerfd).
> +  - The work executed by the real-time thread does not need to run
> at real-time priority at all.
> +    This is not a problem for the real-time thread itself, but it is
> potentially taking the CPU away
> +    from other important real-time work.
> +
> +Application developers may purposely choose to have their real-time
> application sleep in a way that
> +is not safe for real-time. It is debatable whether that is a
> problem. Application developers must
> +analyze the warnings to make a proper assessment.
> +
> +The monitor's specification is::
> +
> +  RULE = always (RT imply (SLEEP imply (RT_FRIENDLY_SLEEP or
> ALLOWLIST)))
> +
> +  RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
> +                  and ((not WAKE) until RT_FRIENDLY_WAKE)
> +
> +  RT_VALID_SLEEP_REASON = PI_FUTEX or NANOSLEEP
> +
> +  RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
> +                  or WOKEN_BY_HARDIRQ
> +                  or WOKEN_BY_NMI
> +
> +  ALLOWLIST = BLOCK_ON_RT_MUTEX
> +           or TASK_IS_RCU
> +           or TASK_IS_MIGRATION
> +           or KTHREAD_SHOULD_STOP
> +
> +Beside the scenarios described above, this specification also handle
> some special cases:
> +
> +  - `KERNEL_THREAD`: kernel tasks do not have any pattern that can
> be recognized as valid real-time
> +    sleeping reasons. Therefore sleeping reason is not checked for
> kernel tasks.
> +  - `RT_SLEEP_WHITELIST`: to handle known false positives with
> kernel tasks.

Is this what you call ALLOWLIST?

Just out of curiosity, normal kernel threads are not forced to follow a
VALID_SLEEP_REASON but need RT_FRIENDLY_WAKE, how are tasks like RCU
and migration not following this?

The monitors are not designed for deadline tasks, any plan to extend to
those too?

Other than this, nice explanation and monitors, thanks.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> +  - `BLOCK_ON_RT_MUTEX` is included in the allowlist due to its
> implementation. In the release path
> +    of rt_mutex, a boosted task is de-boosted before waking the
> rt_mutex's waiter. Consequently, the
> +    monitor may see a real-time-unsafe wakeup (e.g. non-real-time
> task waking real-time task). This
> +    is actually real-time-safe because preemption is disable for the
> duration.
Typo:

+    is actually real-time-safe because preemption is disable**d** for
the duration.

Re: [PATCH v2 13/22] rv: Add support for LTL monitors

[Gabriele Monaco]

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
> @@ -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

Re: [PATCH v2 13/22] rv: Add support for LTL monitors

[Nam Cao]

On Tue, Apr 15, 2025 at 03:22:09PM +0200, Gabriele Monaco wrote:
> You probably read a lot to write this, do you mind adding a brief
> Reference section for the curious reader? Asking for a friend ;)

I actually learned lots of it during university.

But I certainly can link some materials.

Best regards,
Nam

Re: [PATCH v2 21/22] rv: Add documentation for rtapp monitor

[Nam Cao]

On Tue, Apr 15, 2025 at 03:12:23PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > +  - `RT_SLEEP_WHITELIST`: to handle known false positives with
> > kernel tasks.
> 
> Is this what you call ALLOWLIST?

Yes. A colleague already poked me off-list about this error :(

> Just out of curiosity, normal kernel threads are not forced to follow a
> VALID_SLEEP_REASON but need RT_FRIENDLY_WAKE, how are tasks like RCU
> and migration not following this?

Because that's how RCU and migration works, they are intended to be woken
by anything.

It is also possible that people deliberately design their userspace
real-time threads to be woken by non-real-time threads. For example,
pipewire has a non-real-time thread waking a real-time thread to do some
non-critical work. That's still okayish from real-time perspective (but it
is better if the non-real-time thread just does the work itself).

This monitor's warning is not exactly a "here's a bug, fix it". But more
like "something seems really wrong here, please investigate". People can
decide whether this particular suspicious instance is acceptable for their
case.

The initial implementation of the monitor didn't have this allowlist. And
we had a bunch of warnings on the rcu_preempt and migration/ threads. We
decided that due to how rcu and migration works, these warnings are okay.

> The monitors are not designed for deadline tasks, any plan to extend to
> those too?

I haven't thought much about deadline tasks. But it could be extended by
changing "RT" into "RT or DL", if needed.

> Other than this, nice explanation and monitors, thanks.
> 
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

Thanks so much for the review!
Nam