Existing scheduler events do not identify the task that owns a
preempt_schedule_irq() invocation after it switches out.
Add irqexit, a per-task hybrid-automaton monitor that follows an
invocation through entry, suspension, migration, resumption, and return.
Its guards check hardirq context, local interrupt state, and task
ownership.
The monitor covers preempt_schedule_irq() only. It does not cover
architecture-specific interrupt-return work or establish that the helper
was reached from a physical interrupt.
The generated model header is reproducible from the included DOT file
with the unmodified rvgen tool.
Assisted-by: LLM
---
kernel/trace/rv/Kconfig | 1 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitors/irqexit/Kconfig | 14 ++
kernel/trace/rv/monitors/irqexit/irqexit.c | 159 ++++++++++++++++++
kernel/trace/rv/monitors/irqexit/irqexit.h | 85 ++++++++++
.../trace/rv/monitors/irqexit/irqexit_trace.h | 19 +++
kernel/trace/rv/rv_trace.h | 1 +
.../verification/models/irqentry/irqexit.dot | 21 +++
8 files changed, 301 insertions(+)
create mode 100644 kernel/trace/rv/monitors/irqexit/Kconfig
create mode 100644 kernel/trace/rv/monitors/irqexit/irqexit.c
create mode 100644 kernel/trace/rv/monitors/irqexit/irqexit.h
create mode 100644 kernel/trace/rv/monitors/irqexit/irqexit_trace.h
create mode 100644 tools/verification/models/irqentry/irqexit.dot
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index e7b30668a559b..12854fc9643f9 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -75,6 +75,7 @@ source "kernel/trace/rv/monitors/opid/Kconfig"
source "kernel/trace/rv/monitors/irqentry/Kconfig"
source "kernel/trace/rv/monitors/irqstate/Kconfig"
+source "kernel/trace/rv/monitors/irqexit/Kconfig"
# Add new irqentry monitors here
source "kernel/trace/rv/monitors/rtapp/Kconfig"
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index f39a9f8815764..c9a0bf8d9f9b8 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -19,6 +19,7 @@ obj-$(CONFIG_RV_MON_SSSW) += monitors/sssw/sssw.o
obj-$(CONFIG_RV_MON_OPID) += monitors/opid/opid.o
obj-$(CONFIG_RV_MON_IRQENTRY) += monitors/irqentry/irqentry.o
obj-$(CONFIG_RV_MON_IRQSTATE) += monitors/irqstate/irqstate.o
+obj-$(CONFIG_RV_MON_IRQEXIT) += monitors/irqexit/irqexit.o
obj-$(CONFIG_RV_MON_STALL) += monitors/stall/stall.o
obj-$(CONFIG_RV_MON_DEADLINE) += monitors/deadline/deadline.o
obj-$(CONFIG_RV_MON_NOMISS) += monitors/nomiss/nomiss.o
diff --git a/kernel/trace/rv/monitors/irqexit/Kconfig
b/kernel/trace/rv/monitors/irqexit/Kconfig
new file mode 100644
index 0000000000000..55d85e3aa3fca
--- /dev/null
+++ b/kernel/trace/rv/monitors/irqexit/Kconfig
@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_IRQEXIT
+ depends on RV
+ depends on RV_MON_IRQENTRY
+ default y
+ select HA_MON_EVENTS_ID
+ bool "irqexit monitor"
+ help
+ Verify that IRQ-exit scheduling starts outside hardirq context
+ with interrupts disabled and returns to its original task.
+
+ For further information, see:
+ Documentation/trace/rv/monitor_irqentry.rst
diff --git a/kernel/trace/rv/monitors/irqexit/irqexit.c
b/kernel/trace/rv/monitors/irqexit/irqexit.c
new file mode 100644
index 0000000000000..a088b28b62b17
--- /dev/null
+++ b/kernel/trace/rv/monitors/irqexit/irqexit.c
@@ -0,0 +1,159 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/hardirq.h>
+#include <linux/init.h>
+#include <linux/irqflags.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/rv.h>
+#include <linux/tracepoint.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "irqexit"
+
+#include <trace/events/sched.h>
+#include <rv_trace.h>
+#include <monitors/irqentry/irqentry.h>
+
+#define RV_MON_TYPE RV_MON_PER_TASK
+#include "irqexit.h"
+#include <rv/ha_monitor.h>
+
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_irqexit env, u64
time_ns)
+{
+ switch (env) {
+ case hardirq_irqexit:
+ return hardirq_count();
+ case irq_off_irqexit:
+ return !!irqs_disabled();
+ case owner_current_irqexit:
+ return ha_get_target(ha_mon) == rv_get_current();
+ default:
+ return ENV_INVALID_VALUE;
+ }
+}
+
+static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+ enum states curr_state, enum events event,
+ enum states next_state, u64 time_ns)
+{
+ bool res = true;
+
+ if (curr_state == idle_irqexit && event == resched_entry_irqexit)
+ res = ha_get_env(ha_mon, hardirq_irqexit, time_ns) == 0ull &&
+ ha_get_env(ha_mon, irq_off_irqexit, time_ns) == 1ull &&
+ ha_get_env(ha_mon, owner_current_irqexit, time_ns) ==
1ull;
+ else if (curr_state == idle_irqexit && event == switch_in_irqexit)
+ res = ha_get_env(ha_mon, hardirq_irqexit, time_ns) == 0ull &&
+ ha_get_env(ha_mon, irq_off_irqexit, time_ns) == 1ull;
+ else if (curr_state == idle_irqexit && event == switch_out_irqexit)
+ res = ha_get_env(ha_mon, hardirq_irqexit, time_ns) == 0ull &&
+ ha_get_env(ha_mon, irq_off_irqexit, time_ns) == 1ull;
+ else if (curr_state == rescheduling_irqexit && event ==
resched_exit_irqexit)
+ res = ha_get_env(ha_mon, hardirq_irqexit, time_ns) == 0ull &&
+ ha_get_env(ha_mon, irq_off_irqexit, time_ns) == 1ull &&
+ ha_get_env(ha_mon, owner_current_irqexit, time_ns) ==
1ull;
+ else if (curr_state == rescheduling_irqexit && event ==
switch_out_irqexit)
+ res = ha_get_env(ha_mon, hardirq_irqexit, time_ns) == 0ull &&
+ ha_get_env(ha_mon, irq_off_irqexit, time_ns) == 1ull &&
+ ha_get_env(ha_mon, owner_current_irqexit, time_ns) ==
1ull;
+ else if (curr_state == suspended_irqexit && event == switch_in_irqexit)
+ res = ha_get_env(ha_mon, hardirq_irqexit, time_ns) == 0ull &&
+ ha_get_env(ha_mon, irq_off_irqexit, time_ns) == 1ull;
+ return res;
+}
+
+static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+ enum states curr_state, enum events event,
+ enum states next_state, u64 time_ns)
+{
+ return ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns);
+}
+
+static void handle_resched_entry(void *data, struct task_struct *owner)
+{
+ da_handle_start_run_event(owner, resched_entry_irqexit);
+}
+
+static void handle_resched_exit(void *data, struct task_struct *owner)
+{
+ /* Do not hide an invalid return behind enable-mid-invocation sync. */
+ if (owner != rv_get_current() || hardirq_count() || !irqs_disabled())
+ da_handle_start_run_event(owner, resched_exit_irqexit);
+ else
+ da_handle_start_event(owner, resched_exit_irqexit);
+}
+
+static void probe_resched_entry(void *data, struct task_struct *owner,
+ unsigned long pc, bool irq_off)
+{
+ handle_resched_entry(data, owner);
+}
+
+static void probe_resched_exit(void *data, struct task_struct *owner,
+ unsigned long pc, bool irq_off)
+{
+ handle_resched_exit(data, owner);
+}
+
+static void handle_sched_switch(void *data, bool preempt,
+ struct task_struct *prev,
+ struct task_struct *next,
+ unsigned int prev_state)
+{
+ /* current is still prev; the incoming task must not use that guard. */
+ da_handle_event(prev, switch_out_irqexit);
+ da_handle_event(next, switch_in_irqexit);
+}
+
+static int enable_irqexit(void)
+{
+ int retval;
+
+ retval = ha_monitor_init();
+ if (retval)
+ return retval;
+
+ rv_attach_trace_probe("irqexit", sched_irq_preempt_entry,
probe_resched_entry);
+ rv_attach_trace_probe("irqexit", sched_irq_preempt_exit,
probe_resched_exit);
+ rv_attach_trace_probe("irqexit", sched_switch, handle_sched_switch);
+
+ return 0;
+}
+
+static void disable_irqexit(void)
+{
+ rv_this.enabled = 0;
+
+ rv_detach_trace_probe("irqexit", sched_irq_preempt_entry,
probe_resched_entry);
+ rv_detach_trace_probe("irqexit", sched_irq_preempt_exit,
probe_resched_exit);
+ rv_detach_trace_probe("irqexit", sched_switch, handle_sched_switch);
+
+ ha_monitor_destroy();
+}
+
+static struct rv_monitor rv_this = {
+ .name = "irqexit",
+ .description = "Verify IRQ-exit scheduling ownership.",
+ .enable = enable_irqexit,
+ .disable = disable_irqexit,
+ .reset = da_monitor_reset_all,
+ .enabled = 0,
+};
+
+static int __init register_irqexit(void)
+{
+ return rv_register_monitor(&rv_this, &rv_irqentry);
+}
+
+static void __exit unregister_irqexit(void)
+{
+ rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_irqexit);
+module_exit(unregister_irqexit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Karl Mehltretter <[email protected]>");
+MODULE_DESCRIPTION("irqexit: verify IRQ-exit scheduling ownership");
diff --git a/kernel/trace/rv/monitors/irqexit/irqexit.h
b/kernel/trace/rv/monitors/irqexit/irqexit.h
new file mode 100644
index 0000000000000..f48d44d1dff73
--- /dev/null
+++ b/kernel/trace/rv/monitors/irqexit/irqexit.h
@@ -0,0 +1,85 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of irqexit automaton
+ * For further information about this format, see kernel documentation:
+ * Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME irqexit
+
+enum states_irqexit {
+ idle_irqexit,
+ rescheduling_irqexit,
+ suspended_irqexit,
+ state_max_irqexit,
+};
+
+#define INVALID_STATE state_max_irqexit
+
+enum events_irqexit {
+ resched_entry_irqexit,
+ resched_exit_irqexit,
+ switch_in_irqexit,
+ switch_out_irqexit,
+ event_max_irqexit,
+};
+
+enum envs_irqexit {
+ hardirq_irqexit,
+ irq_off_irqexit,
+ owner_current_irqexit,
+ env_max_irqexit,
+ env_max_stored_irqexit = hardirq_irqexit,
+};
+
+_Static_assert(env_max_stored_irqexit <= MAX_HA_ENV_LEN, "Not enough slots");
+
+struct automaton_irqexit {
+ char *state_names[state_max_irqexit];
+ char *event_names[event_max_irqexit];
+ char *env_names[env_max_irqexit];
+ unsigned char function[state_max_irqexit][event_max_irqexit];
+ unsigned char initial_state;
+ bool final_states[state_max_irqexit];
+};
+
+static const struct automaton_irqexit automaton_irqexit = {
+ .state_names = {
+ "idle",
+ "rescheduling",
+ "suspended",
+ },
+ .event_names = {
+ "resched_entry",
+ "resched_exit",
+ "switch_in",
+ "switch_out",
+ },
+ .env_names = {
+ "hardirq",
+ "irq_off",
+ "owner_current",
+ },
+ .function = {
+ {
+ rescheduling_irqexit,
+ INVALID_STATE,
+ idle_irqexit,
+ idle_irqexit,
+ },
+ {
+ INVALID_STATE,
+ idle_irqexit,
+ INVALID_STATE,
+ suspended_irqexit,
+ },
+ {
+ INVALID_STATE,
+ INVALID_STATE,
+ rescheduling_irqexit,
+ INVALID_STATE,
+ },
+ },
+ .initial_state = idle_irqexit,
+ .final_states = { 1, 0, 0 },
+};
diff --git a/kernel/trace/rv/monitors/irqexit/irqexit_trace.h
b/kernel/trace/rv/monitors/irqexit/irqexit_trace.h
new file mode 100644
index 0000000000000..f35366875feff
--- /dev/null
+++ b/kernel/trace/rv/monitors/irqexit/irqexit_trace.h
@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_IRQEXIT
+DEFINE_EVENT(event_da_monitor_id, event_irqexit,
+ TP_PROTO(int id, char *state, char *event, char *next_state, bool
final_state),
+ TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_irqexit,
+ TP_PROTO(int id, char *state, char *event),
+ TP_ARGS(id, state, event));
+
+DEFINE_EVENT(error_env_da_monitor_id, error_env_irqexit,
+ TP_PROTO(int id, char *state, char *event, char *env),
+ TP_ARGS(id, state, event, env));
+#endif /* CONFIG_RV_MON_IRQEXIT */
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 040b3635ef289..c90dae4338bcc 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -190,6 +190,7 @@ DECLARE_EVENT_CLASS(error_env_da_monitor_id,
#include <monitors/stall/stall_trace.h>
#include <monitors/nomiss/nomiss_trace.h>
+#include <monitors/irqexit/irqexit_trace.h>
// Add new monitors based on CONFIG_HA_MON_EVENTS_ID here
#endif
diff --git a/tools/verification/models/irqentry/irqexit.dot
b/tools/verification/models/irqentry/irqexit.dot
new file mode 100644
index 0000000000000..eb2e5499ad7a7
--- /dev/null
+++ b/tools/verification/models/irqentry/irqexit.dot
@@ -0,0 +1,21 @@
+digraph state_automaton {
+ center = true;
+ size = "7,11";
+ {node [shape = plaintext, style=invis, label=""] "__init_idle"};
+ {node [shape = doublecircle] "idle"};
+ {node [shape = circle] "rescheduling"};
+ {node [shape = circle] "suspended"};
+ "__init_idle" -> "idle";
+ "idle" [label = "idle", color = green3];
+ "idle" -> "idle" [ label = "switch_in;hardirq == 0 && irq_off ==
1\nswitch_out;hardirq == 0 && irq_off == 1" ];
+ "idle" -> "rescheduling" [ label = "resched_entry;hardirq == 0 &&
irq_off == 1 && owner_current == 1" ];
+ "rescheduling" [label = "rescheduling"];
+ "rescheduling" -> "idle" [ label = "resched_exit;hardirq == 0 &&
irq_off == 1 && owner_current == 1" ];
+ "rescheduling" -> "suspended" [ label = "switch_out;hardirq == 0 &&
irq_off == 1 && owner_current == 1" ];
+ "suspended" [label = "suspended"];
+ "suspended" -> "rescheduling" [ label = "switch_in;hardirq == 0 &&
irq_off == 1" ];
+ { rank = min ;
+ "__init_idle";
+ "idle";
+ }
+}
--
2.39.5 (Apple Git-154)
