diff mbox series

[RFC,V3,10/20] rv/monitor: Add the wwnr monitor skeleton created by dot2k

Message ID 6ba97ca1d6bd265a573b39e9efe2a0c039e722f7.1651766361.git.bristot@kernel.org (mailing list archive)
State Superseded
Headers show
Series The Runtime Verification (RV) interface | expand

Commit Message

Daniel Bristot de Oliveira May 5, 2022, 4:06 p.m. UTC
Per task wakeup while not running (wwnr) monitor, generated by dot2k
with this command line:

  $ dot2k -d wwnr.dot -t per_task

The model is:
 ----- %< -----
digraph state_automaton {
	center = true;
	size = "7,11";
	{node [shape = plaintext, style=invis, label=""] "__init_not_running"};
	{node [shape = ellipse] "not_running"};
	{node [shape = plaintext] "not_running"};
	{node [shape = plaintext] "running"};
	"__init_not_running" -> "not_running";
	"not_running" [label = "not_running", color = green3];
	"not_running" -> "not_running" [ label = "wakeup" ];
	"not_running" -> "running" [ label = "switch_in" ];
	"running" [label = "running"];
	"running" -> "not_running" [ label = "switch_out" ];
	{ rank = min ;
		"__init_not_running";
		"not_running";
	}
}
 ----- >% -----

This model is broken, the reason is that a task can be running in the
processor without being set as RUNNABLE. Think about a task about to
sleep:

1:	set_current_state(TASK_UNINTERRUPTIBLE);
2:	schedule();

And then imagine an IRQ happening in between the lines one and two,
waking the task up. BOOM, the wakeup will happen while the task is
running.

Q: Why do we need this model, so?
A: To test the reactors.

Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Steven Rostedt <rostedt@goodmis.org>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Will Deacon <will@kernel.org>
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Marco Elver <elver@google.com>
Cc: Dmitry Vyukov <dvyukov@google.com>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Shuah Khan <skhan@linuxfoundation.org>
Cc: Gabriele Paoloni <gpaoloni@redhat.com>
Cc: Juri Lelli <juri.lelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Cc: linux-trace-devel@vger.kernel.org
Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org>
---
 kernel/trace/rv/monitor_wwnr/model.h |  38 +++++++++
 kernel/trace/rv/monitor_wwnr/wwnr.c  | 118 +++++++++++++++++++++++++++
 kernel/trace/rv/monitor_wwnr/wwnr.h  |  70 ++++++++++++++++
 3 files changed, 226 insertions(+)
 create mode 100644 kernel/trace/rv/monitor_wwnr/model.h
 create mode 100644 kernel/trace/rv/monitor_wwnr/wwnr.c
 create mode 100644 kernel/trace/rv/monitor_wwnr/wwnr.h
diff mbox series

Patch

diff --git a/kernel/trace/rv/monitor_wwnr/model.h b/kernel/trace/rv/monitor_wwnr/model.h
new file mode 100644
index 000000000000..7840ffbda98d
--- /dev/null
+++ b/kernel/trace/rv/monitor_wwnr/model.h
@@ -0,0 +1,38 @@ 
+enum states_wwnr {
+	not_running = 0,
+	running,
+	state_max
+};
+
+enum events_wwnr {
+	switch_in = 0,
+	switch_out,
+	wakeup,
+	event_max
+};
+
+struct automaton_wwnr {
+	char *state_names[state_max];
+	char *event_names[event_max];
+	char function[state_max][event_max];
+	char initial_state;
+	char final_states[state_max];
+};
+
+struct automaton_wwnr automaton_wwnr = {
+	.state_names = {
+		"not_running",
+		"running"
+	},
+	.event_names = {
+		"switch_in",
+		"switch_out",
+		"wakeup"
+	},
+	.function = {
+		{     running,          -1, not_running },
+		{          -1, not_running,          -1 },
+	},
+	.initial_state = not_running,
+	.final_states = { 1, 0 },
+};
\ No newline at end of file
diff --git a/kernel/trace/rv/monitor_wwnr/wwnr.c b/kernel/trace/rv/monitor_wwnr/wwnr.c
new file mode 100644
index 000000000000..1ad3365c0d22
--- /dev/null
+++ b/kernel/trace/rv/monitor_wwnr/wwnr.c
@@ -0,0 +1,118 @@ 
+// 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>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "wwnr"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <linux/trace/events/sched.h>
+ */
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_wwnr;
+DECLARE_DA_MON_PER_TASK(wwnr, char);
+
+#define CREATE_TRACE_POINTS
+#include "wwnr.h"
+
+/*
+ * 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.
+ *
+ */
+static void handle_switch_in(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event_wwnr(p, switch_in);
+}
+
+static void handle_switch_out(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event_wwnr(p, switch_out);
+}
+
+static void handle_wakeup(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event_wwnr(p, wakeup);
+}
+
+
+static int start_wwnr(void)
+{
+	int retval;
+
+	retval = da_monitor_init_wwnr();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in);
+	rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out);
+	rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup);
+
+	return 0;
+}
+
+static void stop_wwnr(void)
+{
+	rv_wwnr.enabled = 0;
+
+	rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in);
+	rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out);
+	rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup);
+
+	da_monitor_destroy_wwnr();
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_wwnr = {
+	.name = "wwnr",
+	.description = "auto-generated wwnr",
+	.start = start_wwnr,
+	.stop = stop_wwnr,
+	.reset = da_monitor_reset_all_wwnr,
+	.enabled = 0,
+};
+
+int register_wwnr(void)
+{
+	rv_register_monitor(&rv_wwnr);
+	return 0;
+}
+
+void unregister_wwnr(void)
+{
+	if (rv_wwnr.enabled)
+		stop_wwnr();
+
+	rv_unregister_monitor(&rv_wwnr);
+}
+
+module_init(register_wwnr);
+module_exit(unregister_wwnr);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("wwnr");
diff --git a/kernel/trace/rv/monitor_wwnr/wwnr.h b/kernel/trace/rv/monitor_wwnr/wwnr.h
new file mode 100644
index 000000000000..4af1827d2f16
--- /dev/null
+++ b/kernel/trace/rv/monitor_wwnr/wwnr.h
@@ -0,0 +1,70 @@ 
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_WWNR_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _WWNR_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_wwnr,
+
+	TP_PROTO(pid_t pid, char state, char event, char next_state, bool safe),
+
+	TP_ARGS(pid, state, event, next_state, safe),
+
+	TP_STRUCT__entry(
+		__field(	pid_t,		pid		)
+		__field(	char,		state		)
+		__field(	char,		event		)
+		__field(	char,		next_state	)
+		__field(	bool,		safe		)
+	),
+
+	TP_fast_assign(
+		__entry->pid = pid;
+		__entry->state = state;
+		__entry->event = event;
+		__entry->next_state = next_state;
+		__entry->safe = safe;
+	),
+
+	TP_printk("%d: %s x %s -> %s %s",
+		__entry->pid,
+		model_get_state_name_wwnr(__entry->state),
+		model_get_event_name_wwnr(__entry->event),
+		model_get_state_name_wwnr(__entry->next_state),
+		__entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_wwnr,
+
+	TP_PROTO(pid_t pid, char state, char event),
+
+	TP_ARGS(pid, state, event),
+
+	TP_STRUCT__entry(
+		__field(	pid_t,		pid		)
+		__field(	char,		state		)
+		__field(	char,		event		)
+	),
+
+	TP_fast_assign(
+		__entry->pid = pid;
+		__entry->state = state;
+		__entry->event = event;
+	),
+
+	TP_printk("%d event %s not expected in the state %s",
+		__entry->pid,
+		model_get_event_name_wwnr(__entry->event),
+		model_get_state_name_wwnr(__entry->state))
+);
+
+#endif /* _WWNR_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_FILE wwnr
+#include <trace/define_trace.h>