The Runtime Verification (RV) interface

Over the last years, I've been exploring the possibility of verifying the Linux kernel behavior using Runtime Verification.

Runtime Verification (RV) is a lightweight (yet rigorous) method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach for complex systems.

Instead of relying on a fine-grained model of a system (e.g., a re-implementation a instruction level), RV works by analyzing the trace of the system's actual execution, comparing it against a formal specification of the system behavior.

The usage of deterministic automaton for RV is a well-established approach. In the specific case of the Linux kernel, you can check how to model complex behavior of the Linux kernel with this paper:

De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Efficient formal verification for the Linux kernel.* In: International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. p. 315-332.

And how efficient is this approach here:

De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *A thread synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems Architecture, 2020, 107: 101729.

tlrd: it is possible to model complex behaviors in a modular way, with an acceptable overhead (even for production systems). See this presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg

Here I am proposing a more practical approach for the usage of deterministic automata for runtime verification, and it includes:

- An interface for controlling the verification;
- A tool and set of headers that enables the automatic code generation of the RV monitor (Monitor Synthesis);
- Sample monitors to evaluate the interface;

Given that RV is a tracing consumer, the code is being placed inside the tracing subsystem (Steven and I have been talking about it for a while).

Features to be added after this patchset:
- safe_wtd monitor (requires further discussion with watchdog maintainers)
- Export symbols for external modules
- dot2bpf
- Add a reactor that enables the visualization of the visited states via KCOV (Marco Elver & Dmitry Vyukov)
- Add a CRC method to check from user-space if the values exported by the monitor were not corrupted by any other kernel task (Gabriele Paoloni)

Changes from v8:
- Change the da_monitor curr state type from int to
unsigned int (Daniel)
- Fix a compilation problem because of the usage of a function from patch 2 in patch 1 (last minute change) (Tao).
Changes from v7:
- Optmize the check for monitor enabled (Tao)
- add lockdep checks on rv_enable/disable_monitor (Steven)
- Adjusted the "------" of documentation titles (Steven)
- Adjusted turn_monitoring_on(), and added a turn_monitoring_on_with_reset() (Steven)
- Moved all tracepoint_synchronize_unregister() to run with interface lock taken, and added a comment about it (Steven)
- lockdep, WARN, and call reactor_cleanup_monitor() (Steven)
- Improve comments on synchronization (Steven)
Changes from v6:
- Remove lock protection when reading static data (Steven)
- Add lock protection in disable_all_monitors() (Steven)
- Re-arrange enable_monitor (Steven/Tao)
- Fix monitor_desc_read_data() Description (Tao)
- Wait for tracepoint_synchronize_unregister() anytime a monitor is Disabled (daniel)
- Add memory barriers around monitoring_on and reacting_on (Steven)
- Make rv reactor name and description const char * (Tao)
- Append missing _##name for some da_automata functions/variables (Steven)
- rv_unregister_monitor() will disable the monitor if necessary, and take care of synchronization (Daniel)
- Fixed da_monitor_instrumentation.rst (Tao)
- Fix !CONFIG_Rv_REACTORS (kbuild test)
- Moved struct rv/rv.h to linux/rv.h (Daniel)
- Add rv_ prefix on get/put task slot (Daniel)
Changes from v5:
- Add task monitor slot checks (Daniel/Tao)
- Reset the monitors only after initializing the data (Daniel)
- Add static for static data (Daniel/0-day)
- Change start/stop *functions to enable/disable (like the user- interface (Daniel)
- s/init/start/ for the functions starting the monitoring (Daniel)
- Access monitoring_on and reacting_on via functions (Daniel)
- Improved vector access checks (Tao)
- cleanups (Daniel/Tao)
Changes from v4:
- The watchdog monitor will be discussed on another thread (Daniel)
- s/safe/final/ in the tracepoint definition (Daniel)
- Improved error handling at __init functions (Daniel)
- Remove the hostname from example of commands in a shell (Bagas Sanjaya)
- Added documentation about automata representation in C/DOT/Formal and this documentation is cited in a comment on all model.h (Steven)
- Make wwnr a single patch (Daniel/Steven)
- Add the .dot file for each monitor (Daniel)
- Add a document for each monitor (Daniel)
- Add an order for documentation in the index.rst (Daniel)
- Add wip/wwnr/... long description (Steven/Randy)
- Add comments for helper functions (Steven)
- Improve checks in da_monitor.h (Tao Zhou)
- Change final states set to bool (Tao/Daniel)
- Adjust indentation on enabling monitor/reactor (Steven)
- Use strim on buffers from user-space (Steven)
- Remove ifdefs inside functions (Steven)
- Adjust depends on RV in Kconfig (Steven)
- Check empty enabled monitor list (Tao Zhou)
- Fixed Copyright (Steven)
- Adjusted structures' indentation (Steven)
- Fix rv/monitors/$monitor/enabled return value (Song Liu)
- Typos (Punit Agrawal/Randy)
- Improved python scripts w.r.t. consistency (Steve)
- Blamed myself for so many problems :-) (Daniel's mind)
Changes from v3:
- Rebased on 5.19
(rostedt's request were made on 1x1 meetings)
- Moved monitors to monitors/$name/ (Rostedt)
- Consolidate the tracepoints into a single include file in the default directory (trace/events/rv.h) (Rostedt)
- The tracepoints now record the entire string to the buffer.
- Change the enable_monitors to disable monitors with ! (instead of -). (Rostedt)
- Add a suffix to the state/events enums, to avoid conflict in the vmlinux.h used by eBPF.
- The models are now placed in the $name.h (it used to store the tracepoints, but they are now consolidated in a single file)
- dot2c and dot2k updated to the changes
- models re-generated with these new standards.
- user-space tools moved to an directory outside of tools/tracing as other methods of verification/log sources are planned.
Changes from v2:
- Tons of checkpatch and kernel test robot
- Moved files to better places
- Adjusted watchdog tracepoints patch (Guenter Roeck)
- Added pretimeout watchdog events (Peter Enderborg)
- Used task struct to store per-task monitors (Peter Zijlstra)
- Changed the instrumentation to use internal definition of tracepoint and check the callback signature (Steven Rostedt)
- Used printk_deferred() and removed the comment about deadlocks (Shuah Khan/John Ogness)
- Some simplifications:
- Removed the safe watchdog nowayout for now (myself)
- Removed export symbols for now (myself)
Changes from V1:
- rebased to the latest kernel;
- code cleanup;
- the watchdog dev monitor;
- safety app;

Daniel Bristot de Oliveira (16):
rv: Add Runtime Verification (RV) interface
rv: Add runtime reactors interface
rv/include: Add helper functions for deterministic automata rv/include: Add deterministic automata monitor definition via C macros rv/include: Add instrumentation helper functions Documentation/rv: Add a basic documentation
tools/rv: Add dot2c
Documentation/rv: Add deterministic automaton documentation tools/rv: Add dot2k
Documentation/rv: Add deterministic automata monitor synthesis
documentation
Documentation/rv: Add deterministic automata instrumentation
documentation
rv/monitor: Add the wip monitor skeleton created by dot2k rv/monitor: Add the wip monitor
rv/monitor: Add the wwnr monitor
rv/reactor: Add the printk reactor
rv/reactor: Add the panic reactor

 Documentation/trace/index.rst                 |   1 +
 .../trace/rv/da_monitor_instrumentation.rst   | 171 ++++
 .../trace/rv/da_monitor_synthesis.rst         | 147 ++++
 .../trace/rv/deterministic_automata.rst       | 184 ++++
 Documentation/trace/rv/index.rst              |  14 +
 Documentation/trace/rv/monitor_wip.rst        |  55 ++
 Documentation/trace/rv/monitor_wwnr.rst       |  45 +
 .../trace/rv/runtime-verification.rst         | 231 +++++
 include/linux/rv.h                            |  70 ++
 include/linux/sched.h                         |  11 +
 include/rv/automata.h                         |  75 ++
 include/rv/da_monitor.h                       | 544 ++++++++++++
 include/rv/instrumentation.h                  |  29 +
 include/trace/events/rv.h                     | 142 ++++
 kernel/fork.c                                 |  14 +
 kernel/trace/Kconfig                          |   2 +
 kernel/trace/Makefile                         |   1 +
 kernel/trace/rv/Kconfig                       |  78 ++
 kernel/trace/rv/Makefile                      |   8 +
 kernel/trace/rv/monitors/wip/wip.c            |  88 ++
 kernel/trace/rv/monitors/wip/wip.h            |  46 +
 kernel/trace/rv/monitors/wwnr/wwnr.c          |  87 ++
 kernel/trace/rv/monitors/wwnr/wwnr.h          |  46 +
 kernel/trace/rv/reactor_panic.c               |  43 +
 kernel/trace/rv/reactor_printk.c              |  42 +
 kernel/trace/rv/rv.c                          | 799 ++++++++++++++++++
 kernel/trace/rv/rv.h                          |  68 ++
 kernel/trace/rv/rv_reactors.c                 | 508 +++++++++++
 kernel/trace/trace.c                          |   2 +
 kernel/trace/trace.h                          |   9 +
 tools/verification/dot2/Makefile              |  26 +
 tools/verification/dot2/automata.py           | 174 ++++
 tools/verification/dot2/dot2c                 |  26 +
 tools/verification/dot2/dot2c.py              | 254 ++++++
 tools/verification/dot2/dot2k                 |  47 ++
 tools/verification/dot2/dot2k.py              | 177 ++++
 .../dot2/dot2k_templates/main_global.c        |  91 ++
 .../dot2/dot2k_templates/main_per_cpu.c       |  91 ++
 .../dot2/dot2k_templates/main_per_task.c      |  91 ++
 tools/verification/models/wip.dot             |  16 +
 tools/verification/models/wwnr.dot            |  16 +
 41 files changed, 4569 insertions(+)
 create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst
 create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
 create mode 100644 Documentation/trace/rv/deterministic_automata.rst
 create mode 100644 Documentation/trace/rv/index.rst
 create mode 100644 Documentation/trace/rv/monitor_wip.rst
 create mode 100644 Documentation/trace/rv/monitor_wwnr.rst
 create mode 100644 Documentation/trace/rv/runtime-verification.rst
 create mode 100644 include/linux/rv.h
 create mode 100644 include/rv/automata.h
 create mode 100644 include/rv/da_monitor.h
 create mode 100644 include/rv/instrumentation.h
 create mode 100644 include/trace/events/rv.h
 create mode 100644 kernel/trace/rv/Kconfig
 create mode 100644 kernel/trace/rv/Makefile
 create mode 100644 kernel/trace/rv/monitors/wip/wip.c
 create mode 100644 kernel/trace/rv/monitors/wip/wip.h
 create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c
 create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h
 create mode 100644 kernel/trace/rv/reactor_panic.c
 create mode 100644 kernel/trace/rv/reactor_printk.c
 create mode 100644 kernel/trace/rv/rv.c
 create mode 100644 kernel/trace/rv/rv.h
 create mode 100644 kernel/trace/rv/rv_reactors.c
 create mode 100644 tools/verification/dot2/Makefile
 create mode 100644 tools/verification/dot2/automata.py
 create mode 100644 tools/verification/dot2/dot2c
 create mode 100644 tools/verification/dot2/dot2c.py
 create mode 100644 tools/verification/dot2/dot2k
 create mode 100644 tools/verification/dot2/dot2k.py
 create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c
 create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c
 create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c
 create mode 100644 tools/verification/models/wip.dot
 create mode 100644 tools/verification/models/wwnr.dot

2.35.1

RV is a lightweight (yet rigorous) method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach to complex systems.

RV works by analyzing the trace of the system's actual execution, comparing it against a formal specification of the system behavior. RV can give precise information on the runtime behavior of the monitored system while enabling the reaction for unexpected events, avoiding, for example, the propagation of a failure on safety-critical systems.

The development of this interface roots in the development of the paper:

De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. Efficient formal verification for the Linux kernel. In:
International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. p. 315-332.

And:

De Oliveira, Daniel Bristot. Automata-based formal analysis and verification of the real-time Linux kernel. PhD Thesis, 2020.

The RV interface resembles the tracing/ interface on purpose. The current path for the RV interface is /sys/kernel/tracing/rv/.

It presents these files:

"available_monitors"
- List the available monitors, one per line.

For example:

     # cat available_monitors
     wip
     wwnr

"enabled_monitors"
- Lists the enabled monitors, one per line;
- Writing to it enables a given monitor;
- Writing a monitor name with a '!' prefix disables it;
- Truncating the file disables all enabled monitors.

For example:

     # cat enabled_monitors
     # echo wip > enabled_monitors
     # echo wwnr >> enabled_monitors
     # cat enabled_monitors
     wip
     wwnr
     # echo '!wip' >> enabled_monitors
     # cat enabled_monitors
     wwnr
     # echo > enabled_monitors
     # cat enabled_monitors
     #

Note that more than one monitor can be enabled concurrently.

"monitoring_on"
- It is an on/off general switcher for monitoring. Note that it does not disable enabled monitors or detach events, but stop the per-entity monitors of monitoring the events received from the system. It resembles the "tracing_on" switcher.

"monitors/"
Each monitor will have its one directory inside "monitors/". There the monitor specific files will be presented.
The "monitors/" directory resembles the "events" directory on tracefs.

For example:

     # cd monitors/wip/
     # ls
     desc  enable
     # cat desc
     wakeup in preemptive per-cpu testing monitor.
     # cat enable
     0

For further information, see the comments in the header of kernel/trace/rv/rv.c from this patch.

---
 include/linux/rv.h       |  43 +++
 include/linux/sched.h    |  11 +
 kernel/trace/Kconfig     |   2 +
 kernel/trace/Makefile    |   1 +
 kernel/trace/rv/Kconfig  |  12 +
 kernel/trace/rv/Makefile |   3 +
 kernel/trace/rv/rv.c     | 782 +++++++++++++++++++++++++++++++++++++++
 kernel/trace/rv/rv.h     |  33 ++
 kernel/trace/trace.c     |   2 +
 kernel/trace/trace.h     |   9 +
 10 files changed, 898 insertions(+)
 create mode 100644 include/linux/rv.h
 create mode 100644 kernel/trace/rv/Kconfig
 create mode 100644 kernel/trace/rv/Makefile
 create mode 100644 kernel/trace/rv/rv.c
 create mode 100644 kernel/trace/rv/rv.h

new file mode 100644
index 000000000000..d8fa9e8be94a
@@ -0,0 +1,43 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Runtime Verification.
+ *
+ * For futher information, see: kernel/trace/rv/rv.c.
+ */
+#ifndef _LINUX_RV_H
+#define _LINUX_RV_H
+
+#ifdef CONFIG_RV
+
+/*
+ * Per-task RV monitors count. 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.
+ */
+#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 rv_monitor {
+	const char		*name;
+	const char		*description;
+	bool			enabled;
+	int			(*enable)(void);
+	void			(*disable)(void);
+	void			(*reset)(void);
+};
+
+bool rv_monitoring_on(void);
+int rv_unregister_monitor(struct rv_monitor *monitor);
+int rv_register_monitor(struct rv_monitor *monitor);
+int rv_get_task_monitor_slot(void);
+void rv_put_task_monitor_slot(int slot);
+
+#endif /* CONFIG_RV */
+#endif /* _LINUX_RV_H */

index c46f3a63b758..b5da3e7c3a04 100644
@@ -34,6 +34,7 @@
 #include <linux/rseq.h>
 #include <linux/seqlock.h>
 #include <linux/kcsan.h>
+#include <linux/rv.h>
 #include <asm/kmap_size.h>
 
 /* task_struct member predeclarations (sorted alphabetically): */

@@ -1500,6 +1501,16 @@ struct task_struct {
 	struct callback_head		l1d_flush_kill;
 #endif
 
+#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.
+	 */
+	union rv_task_monitor		rv[RV_PER_TASK_MONITORS];
+#endif
+
 	/*
 	 * New fields for task_struct should be added above here, so that
 	 * they are included in the randomized portion of task_struct.

index ccd6a5ade3e9..1052126bdca2 100644
@@ -1106,4 +1106,6 @@ config HIST_TRIGGERS_DEBUG
 
           If unsure, say N.
 
+source "kernel/trace/rv/Kconfig"
+
 endif # FTRACE

index 0d261774d6f3..c6651e16b557 100644
@@ -106,5 +106,6 @@ obj-$(CONFIG_FPROBE) += fprobe.o
 obj-$(CONFIG_RETHOOK) += rethook.o
 
 obj-$(CONFIG_TRACEPOINT_BENCHMARK) += trace_benchmark.o
+obj-$(CONFIG_RV) += rv/
 
 libftrace-y := ftrace.o

new file mode 100644
index 000000000000..6d127cdb00dd
@@ -0,0 +1,12 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+menuconfig RV
+	bool "Runtime Verification"
+	depends on TRACING
+	help
+	  Enable the kernel runtime verification infrastructure. RV is a
+	  lightweight (yet rigorous) method that complements classical
+	  exhaustive verification techniques (such as model checking and
+	  theorem proving). RV works by analyzing the trace of the system's
+	  actual execution, comparing it against a formal specification of
+	  the system behavior.

new file mode 100644
index 000000000000..fd995379df67
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: GPL-2.0
+
+obj-$(CONFIG_RV) += rv.o

new file mode 100644
index 000000000000..50014aa224a7
@@ -0,0 +1,33 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#include <linux/mutex.h>
+
+struct rv_interface {
+	struct dentry		*root_dir;
+	struct dentry		*monitors_dir;
+};
+
+#include "../trace.h"
+#include <linux/tracefs.h>
+#include <linux/rv.h>
+
+#define RV_MODE_WRITE			TRACE_MODE_WRITE
+#define RV_MODE_READ			TRACE_MODE_READ
+
+#define rv_create_dir			tracefs_create_dir
+#define rv_create_file			tracefs_create_file
+#define rv_remove			tracefs_remove
+
+#define MAX_RV_MONITOR_NAME_SIZE	32
+
+extern struct mutex rv_interface_lock;
+
+struct rv_monitor_def {
+	struct list_head	list;
+	struct rv_monitor	*monitor;
+	struct dentry		*root_d;
+	bool			task_monitor;
+};
+
+struct dentry *get_monitors_root(void);
+int rv_disable_monitor(struct rv_monitor_def *mdef);
+int rv_enable_monitor(struct rv_monitor_def *mdef);

index b8dd54627075..062423371741 100644
@@ -9772,6 +9772,8 @@ static __init int tracer_init_tracefs(void)
 		tracer_init_tracefs_work_func(NULL);
 	}
 
+	rv_init_interface();
+
 	return 0;
 }
 

index ff816fb41e48..900e75d96c84 100644
@@ -2005,4 +2005,13 @@ struct trace_min_max_param {
 
 extern const struct file_operations trace_min_max_fops;
 
+#ifdef CONFIG_RV
+extern int rv_init_interface(void);
+#else
+static inline int rv_init_interface(void)
+{
+	return 0;
+}
+#endif
+
 #endif /* _LINUX_KERNEL_TRACE_H */

2.35.1

Perhaps that is not a given. I'm guessing that ->disable() can not fail.

negative is usually unsuccessful. 1 and 0 can be anything we really choose it to be. But should be commented at the top for clarification.

As for now, disable can not fail. But OK to return a status in that case that changes in the future.

Both rv_enable_monitor() and rv_disable_monitor() return either 0 on success or negative on failure. Do not confuse the internal callers (that start with "__") as the return values of these.

User space will only see 0 or negative.

Yes, the enable callbacks should return negative on error.

Probably want this to be "retval = 0;"

And this to be "retval |= "

where rv_attach_trace_probe() returns 0 on success and something else on error.

Well, the above is not true. If any "succeed" and return zero, with the "&=" it will be zero if only one succeeds and then rest fail. That's why you want the "|=" and set the flag on error.

We could change the macro to:

#define rv_attach_trace_probe(monitor, tp, rv_handler)                                  \
        ({                                                                            \
                check_trace_callback_type_##tp(rv_handler);                             \
                WARN_ONCE(register_trace_##tp(rv_handler, NULL),                        \
                                "fail attaching " #monitor " " #tp "handler");          \
        })

Where the macro returns the result of the WARN_ONCE() which is zero on success (no warning) and non-zero otherwise.

Correct. Because strlen() does not include the nul byte.

-- Steve

The modification of macro make sense to me even though I do not know trace enough. Thanks,

Which is correct.

No, 1 indicates that *disable was called, 0 did not call disable function.

This is a "static __function", which alerts for internal aspects.

It has a specific purpose of counting if the disable function was actually called.

Disabling a disabled monitor is not a problem.

So all your argumentation based on this is not correct, and it is breaking other parts of the code... see where it is called.

This is not a problem. Actually, disable functions often return void. I am keeping an int just in case.

All things above are misled by the first interpretation but,,,

so I checked

The way that rv_attach_trace_probe() is attaching a probe is not different from the way other *in kernel* tracing does.

No, that is not the most robust way to do this. A better way is to do it like in the early versions of this patch set, where it was searching for the existence of the tracepoint from the module perspective, taking notes of the ones that were enabled, and then actually disabling all events that were enabled before the failure.

and here the system state is even worse than WARNING and doing nothing: the monitor is disabled, but the tracepoints that were registered are still hooked to the system... and you cannot unhook them because the monitor is not enabled.

You still can unhook in current implementation.

So, for the in-kernel version, the current method is equivalent to the the way we do on other tracers, and the monitors only compile if the tracepoints exist, the callback has the correct signature and WARNs in case of problems in the tracepoint.

There will be a more robust way to do this, and it will be included in the "add module support" patch set. But is its better to add it in a patch set because we can analyze change by change instead of adding on top of this initial implementation - which is quite large already.

Yep, this can be improved. But it is not a BUG, as it is allowing monitor
with (MAX_RV_MONITOR_NAME_SIZE - 1) size, which is safe.

Given that neither 'wip' or 'wwnr' are >= MAX_RV_MONITOR_NAME_SIZE, this problem is not happening - and no other monitor can hit it because modules are not yet supported.

I took note and will patch it.

Thanks!
-- Daniel

Yeah, this is not that clear from my above words expression. I said the return value of da_monitor_init_*() will be 0, but it is not right. Global and per-cpu monitor will return 0, per-task monitor may return a positive value when the slot is equal or greater than RV_PER_TASK_MONITOR_INIT(how possible this will happen I do know yet). This is from reading the current code implementation.
I just want to say that there may be a bug here.
If rv_enable_monitor() return a positive value and the error happened(as above said), user space will not know this is a error return value, but regard it as a right writing. Even if the return value(the slot value not in [0..RV_PER_TASK_MONITOR_INIT)) is equal to count of charaters that are writen to the file(the string length of monitor name), it will still be not a right writing.

Even if we check the return value of rv_attach_trace_probe() in current implementation, once error happened from one register the previous trace pointers will not be unregistered.

Yes.

Thanks,
Tao

goto my previous email;

goto my previous email; see other tracers.

If you increment RV_PER_TASK_MONITORS to 2, I believe Tao is correct.

-- Steve

Well, rv_get_monitor_slot() can currently only return 0 or negative. This is because PER_TASK_MONITORS is just 1 and we can not return that or greater.

With the current code this can not happen, as we only allow for a single PER_TASK_MONITORS.

But in the future, if we increment this, then you are correct. We can not just check retval, but need to check retval < 0.

This does need to be fixed. But because it currently isn't an issue because we they can only return 0 or negative, I'm going to pull this series in.

But Daniel, these checks do need to be updated. Please send patches on top of this series to address it.

-- Steve

I believe what Tao is trying to say is this:

If we set RV_PER_TASKS_MONITORS greater than 1 we have:

int rv_enable_monitor(struct rv_monitor_def *mdef)

{
        int retval;

        lockdep_assert_held(&rv_interface_lock);

        if (mdef->monitor->enabled)
                return 0;

        retval = mdef->monitor->enable();  <- if that returns positive, then things break.

        if (!retval)
                mdef->monitor->enabled = 1;  <- this is not set.

        return retval;
}

static int enable_wip(void)

{
        int retval;

        retval = da_monitor_init_wip();  <- if that returns positive, things break
        if (retval)
                return retval;

static int da_monitor_init_##name(void)                                                         \
{                                                                                               \
        int slot;                                                                               \
                                                                                                \
        slot = rv_get_task_monitor_slot();  <- if this returns positive, things break           \
        if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT)                                       \

And we probably need slot to be negative if it is greater or equal to RV_PER_TASK_MONITOR_INIT.

                return slot;                                                                    \

int rv_get_task_monitor_slot(void)

{
        int i;

        lockdep_assert_held(&rv_interface_lock);

        if (task_monitor_count == RV_PER_TASK_MONITORS)
                return -EBUSY;

        task_monitor_count++;

        for (i = 0; i < RV_PER_TASK_MONITORS; i++) {
                if (task_monitor_slots[i] == false) {
                        task_monitor_slots[i] = true;
                        return i;  <- if RV_PER_TASK_MONITORS > 1 then it can return positive!
                }
        }

-- Steve

ok, there will be a problem when RV_PER_TASK_MONITOR_INIT changes to > 1. This will need to be patched to return negative. So far we have only one because there is only one per task monitor.

-- Daniel

Exactly. And reviewers like Tao and myself are going to continue to flag it as a bug as we don't assume that RV_PER_TASK_MONITOR_INIT will stay 1 ;-)

-- Steve

A runtime monitor can cause a reaction to the detection of an exception on the model's execution. By default, the monitors have tracing reactions, printing the monitor output via tracepoints. But other reactions can be added (on-demand) via this interface.

The user interface resembles the kernel tracing interface and presents these files:

"available_reactors"
- Reading shows the available reactors, one per line.

For example:

     # cat available_reactors
     nop
     panic
     printk

"reacting_on"
- It is an on/off general switch for reactors, disabling all reactions.

"monitors/MONITOR/reactors"
- List available reactors, with the select reaction for the given MONITOR inside []. The default one is the nop (no operation) reactor.
- Writing the name of a reactor enables it to the given MONITOR.

For example:

     # cat monitors/wip/reactors
     [nop]
     panic
     printk
     # echo panic > monitors/wip/reactors
     # cat monitors/wip/reactors
     nop
     [panic]
     printk

---
 include/linux/rv.h            |  17 ++
 kernel/trace/rv/Kconfig       |  11 +
 kernel/trace/rv/Makefile      |   1 +
 kernel/trace/rv/rv.c          |   9 +
 kernel/trace/rv/rv.h          |  35 +++
 kernel/trace/rv/rv_reactors.c | 508 ++++++++++++++++++++++++++++++++++
 6 files changed, 581 insertions(+)
 create mode 100644 kernel/trace/rv/rv_reactors.c

index d8fa9e8be94a..dcce56987cf7 100644
@@ -24,6 +24,14 @@
 union rv_task_monitor {
 };
 
+#ifdef CONFIG_RV_REACTORS
+struct rv_reactor {
+	const char		*name;
+	const char		*description;
+	void			(*react)(char *msg);
+};
+#endif
+
 struct rv_monitor {
 	const char		*name;
 	const char		*description;

@@ -31,6 +39,9 @@ struct rv_monitor {
 	int			(*enable)(void);
 	void			(*disable)(void);
 	void			(*reset)(void);
+#ifdef CONFIG_RV_REACTORS
+	void			(*react)(char *msg);
+#endif
 };
 
 bool rv_monitoring_on(void);

@@ -39,5 +50,11 @@ int rv_register_monitor(struct rv_monitor *monitor);
 int rv_get_task_monitor_slot(void);
 void rv_put_task_monitor_slot(int slot);
 
+#ifdef CONFIG_RV_REACTORS
+bool rv_reacting_on(void);
+int rv_unregister_reactor(struct rv_reactor *reactor);
+int rv_register_reactor(struct rv_reactor *reactor);
+#endif /* CONFIG_RV_REACTORS */
+
 #endif /* CONFIG_RV */
 #endif /* _LINUX_RV_H */

index 6d127cdb00dd..3eb5d48ab4f6 100644
@@ -10,3 +10,14 @@ menuconfig RV
 	  theorem proving). RV works by analyzing the trace of the system's
 	  actual execution, comparing it against a formal specification of
 	  the system behavior.
+
+config RV_REACTORS
+	bool "Runtime verification reactors"
+	default y
+	depends on RV
+	help
+	  Enables the online runtime verification reactors. A runtime
+	  monitor can cause a reaction to the detection of an exception
+	  on the model's execution. By default, the monitors have
+	  tracing reactions, printing the monitor output via tracepoints,
+	  but other reactions can be added (on-demand) via this interface.

index fd995379df67..8944274d9b41 100644
@@ -1,3 +1,4 @@
 # SPDX-License-Identifier: GPL-2.0
 
 obj-$(CONFIG_RV) += rv.o
+obj-$(CONFIG_RV_REACTORS) += rv_reactors.o

index 731cc961cc70..45cf64eb2600 100644
@@ -353,6 +353,10 @@ static int create_monitor_dir(struct rv_monitor_def *mdef)
 		goto out_remove_root;
 	}
 
+	retval = reactor_populate_monitor(mdef);
+	if (retval)
+		goto out_remove_root;
+
 	return 0;
 
 out_remove_root:

@@ -669,6 +673,7 @@ static const struct file_operations monitoring_on_fops = {
 
 static void destroy_monitor_dir(struct rv_monitor_def *mdef)
 {
+	reactor_cleanup_monitor(mdef);
 	rv_remove(mdef->root_d);
 }
 

@@ -747,6 +752,7 @@ int rv_unregister_monitor(struct rv_monitor *monitor)
 int __init rv_init_interface(void)
 {
 	struct dentry *tmp;
+	int retval;
 
 	rv_root.root_dir = rv_create_dir("rv", NULL);
 	if (!rv_root.root_dir)

@@ -770,6 +776,9 @@ int __init rv_init_interface(void)
 			     &monitoring_on_fops);
 	if (!tmp)
 		goto out_err;
+	retval = init_rv_reactors(rv_root.root_dir);
+	if (retval)
+		goto out_err;
 
 	turn_monitoring_on();
 

index 50014aa224a7..db6cb0913dbd 100644
@@ -18,16 +18,51 @@ struct rv_interface {
 #define rv_remove			tracefs_remove
 
 #define MAX_RV_MONITOR_NAME_SIZE	32
+#define MAX_RV_REACTOR_NAME_SIZE	32
 
 extern struct mutex rv_interface_lock;
 
+#ifdef CONFIG_RV_REACTORS
+struct rv_reactor_def {
+	struct list_head	list;
+	struct rv_reactor	*reactor;
+	/* protected by the monitor interface lock */
+	int			counter;
+};
+#endif
+
 struct rv_monitor_def {
 	struct list_head	list;
 	struct rv_monitor	*monitor;
 	struct dentry		*root_d;
+#ifdef CONFIG_RV_REACTORS
+	struct rv_reactor_def	*rdef;
+	bool			reacting;
+#endif
 	bool			task_monitor;
 };
 
 struct dentry *get_monitors_root(void);
 int rv_disable_monitor(struct rv_monitor_def *mdef);
 int rv_enable_monitor(struct rv_monitor_def *mdef);
+
+#ifdef CONFIG_RV_REACTORS
+int reactor_populate_monitor(struct rv_monitor_def *mdef);
+void reactor_cleanup_monitor(struct rv_monitor_def *mdef);
+int init_rv_reactors(struct dentry *root_dir);
+#else
+static inline int reactor_populate_monitor(struct rv_monitor_def *mdef)
+{
+	return 0;
+}
+
+static inline void reactor_cleanup_monitor(struct rv_monitor_def *mdef)
+{
+	return;
+}
+
+static inline int init_rv_reactors(struct dentry *root_dir)
+{
+	return 0;
+}
+#endif

2.35.1

Formally, a deterministic automaton, denoted by G, is defined as a quintuple:

G = { X, E, f, x_0, X_m }

where:
- X is the set of states;
- E is the finite set of events;
- x_0 is the initial state;
- X_m (subset of X) is the set of marked states.
- f : X x E -> X $ is the transition function. It defines the state transition in the occurrence of a event from E in the state X. In the special case of deterministic automata, the occurrence of the event in E in a state in X has a deterministic next state from X.

An automaton can also be represented using a graphical format of vertices (nodes) and edges. The open-source tool Graphviz can produce this graphic format using the (textual) DOT language as the source code.

The dot2c tool presented in this paper:

De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. Efficient formal verification for the Linux kernel. In:
International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. p. 315-332.

Translates a deterministic automaton in the DOT format into a C source code representation that to be used for monitoring.

This header file implements helper functions to facilitate the usage of the C output from dot2c/k for monitoring.

---
 include/rv/automata.h | 75 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 include/rv/automata.h

new file mode 100644
index 000000000000..eb9e636809a0
@@ -0,0 +1,75 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira  <[email protected]>
+ *
+ * Deterministic automata helper functions, to be used with the automata
+ * models in C generated by the dot2k tool.
+ */
+
+/*
+ * DECLARE_AUTOMATA_HELPERS - define a set of helper functions for automata
+ *
+ * Define a set of helper functions for automata. The 'name' argument is used
+ * as suffix for the functions and data. These functions will handle automaton
+ * with data type 'type'.
+ */
+#define DECLARE_AUTOMATA_HELPERS(name, type)					\
+										\
+/*										\
+ * model_get_state_name_##name - return the (string) name of the given state	\
+ */ 										\
+static char *model_get_state_name_##name(enum states_##name state)		\
+{										\
+	if ((state < 0) || (state >= state_max_##name))				\
+		return "INVALID";						\
+										\
+	return automaton_##name.state_names[state];				\
+}										\
+										\
+/*										\
+ * model_get_event_name_##name - return the (string) name of the given event	\
+ */										\
+static char *model_get_event_name_##name(enum events_##name event)		\
+{										\
+	if ((event < 0) || (event >= event_max_##name))				\
+		return "INVALID";						\
+										\
+	return automaton_##name.event_names[event];				\
+}										\
+										\
+/*										\
+ * model_get_initial_state_##name - return the automaton's initial state		\
+ */										\
+static inline type model_get_initial_state_##name(void)				\
+{										\
+	return automaton_##name.initial_state;					\
+}										\
+										\
+/*										\
+ * model_get_next_state_##name - process an automaton event occurrence		\
+ *										\
+ * Given the current state (curr_state) and the event (event), returns		\
+ * the next state, or INVALID_STATE in case of error.				\
+ */										\
+static inline type model_get_next_state_##name(enum states_##name curr_state,	\
+					       enum events_##name event)	\
+{										\
+	if ((curr_state < 0) || (curr_state >= state_max_##name))		\
+		return INVALID_STATE;						\
+										\
+	if ((event < 0) || (event >= event_max_##name))				\
+		return INVALID_STATE;						\
+										\
+	return automaton_##name.function[curr_state][event];			\
+}										\
+										\
+/*										\
+ * model_is_final_state_##name - check if the given state is a final state	\
+ */										\
+static inline bool model_is_final_state_##name(enum states_##name state)	\
+{										\
+	if ((state < 0) || (state >= state_max_##name))				\
+		return 0;							\
+										\
+	return automaton_##name.final_states[state];				\
+}

2.35.1

On Fri, Jul 29, 2022 at 11:38:42AM +0200, Daniel Bristot de Oliveira wrote:

[...]

no.

-- Daniel

Absolutly I lost here, this is for *get next state*, must return a state info.

In Linux terms, the runtime verification monitors are encapsulated inside the "RV monitor" abstraction. The "RV monitor" includes a set of instances of the monitor (per-cpu monitor, per-task monitor, and so on), the helper functions that glue the monitor to the system reference model, and the trace output as a reaction for event parsing and exceptions, as depicted below:

Linux +----- RV Monitor ----------------------------------+ Formal
Realm | | Realm

 +-------------------+     +----------------+     +-----------------+
 |   Linux kernel    |     |     Monitor    |     |     Reference   |
 |     Tracing       |  -> |   Instance(s)  | <-  |       Model     |
 | (instrumentation) |     | (verification) |     | (specification) |
 +-------------------+     +----------------+     +-----------------+
        |                          |                       |
        |                          V                       |
        |                     +----------+                 |
        |                     | Reaction |                 |
        |                     +--+--+--+-+                 |
        |                        |  |  |                   |
        |                        |  |  +-> trace output ?  |
        +------------------------|--|----------------------+
                                 |  +----> panic ?
                                 +-------> <user-specified>

Add the rv/da_monitor.h, enabling automatic code generation for the *Monitor Instance(s)* using C macros, and code to support it.

The benefits of the usage of macro for monitor synthesis are 3-fold as it:

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

This initial implementation presents three different types of monitor instances:

- DECLARE_DA_MON_GLOBAL(name, type)
- DECLARE_DA_MON_PER_CPU(name, type)
- DECLARE_DA_MON_PER_TASK(name, type)

The first declares the functions for a global deterministic automata monitor, the second for monitors with per-cpu instances, and the third with per-task instances.

---
 include/linux/rv.h        |  10 +
 include/rv/da_monitor.h   | 541 ++++++++++++++++++++++++++++++++++++++
 include/trace/events/rv.h | 120 +++++++++
 kernel/fork.c             |  14 +
 kernel/trace/rv/Kconfig   |  11 +
 kernel/trace/rv/rv.c      |   5 +
 6 files changed, 701 insertions(+)
 create mode 100644 include/rv/da_monitor.h
 create mode 100644 include/trace/events/rv.h

index dcce56987cf7..8883b41d88ec 100644
@@ -7,7 +7,16 @@
 #ifndef _LINUX_RV_H
 #define _LINUX_RV_H
 
+#define MAX_DA_NAME_LEN	24
+
 #ifdef CONFIG_RV
+/*
+ * Deterministic automaton per-object variables.
+ */
+struct da_monitor {
+	bool		monitoring;
+	unsigned int	curr_state;
+};
 
 /*
  * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS.

@@ -22,6 +31,7 @@
  * Futher monitor types are expected, so make this a union.
  */
 union rv_task_monitor {
+	struct da_monitor da_mon;
 };
 
 #ifdef CONFIG_RV_REACTORS

index 9d44f2d46c69..6f1f82ccd5f2 100644
@@ -1964,6 +1964,18 @@ static void copy_oom_score_adj(u64 clone_flags, struct task_struct *tsk)
 	mutex_unlock(&oom_adj_mutex);
 }
 
+#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;
+}
+#else
+#define rv_task_fork(p) do {} while (0)
+#endif
+
 /*
  * This creates a new process as a copy of the old one,
  * but does not actually start it yet.

@@ -2399,6 +2411,8 @@ static __latent_entropy struct task_struct *copy_process(
 	 */
 	copy_seccomp(p);
 
+	rv_task_fork(p);
+
 	rseq_fork(p, clone_flags);
 
 	/* Don't start children in a dying pid namespace */

index 3eb5d48ab4f6..8714800e22ad 100644
@@ -1,5 +1,16 @@
 # SPDX-License-Identifier: GPL-2.0-only
 #
+config DA_MON_EVENTS
+	bool
+
+config DA_MON_EVENTS_IMPLICIT
+	select DA_MON_EVENTS
+	bool
+
+config DA_MON_EVENTS_ID
+	select DA_MON_EVENTS
+	bool
+
 menuconfig RV
 	bool "Runtime Verification"
 	depends on TRACING

index 45cf64eb2600..df6678c86334 100644
@@ -140,6 +140,11 @@
 #include <linux/init.h>
 #include <linux/slab.h>
 
+#ifdef CONFIG_DA_MON_EVENTS
+#define CREATE_TRACE_POINTS
+#include <trace/events/rv.h>
+#endif
+
 #include "rv.h"
 
 DEFINE_MUTEX(rv_interface_lock);

2.35.1

Instrumentation helper functions to facilitate the instrumentation of auto-generated RV monitors create by dot2k.

---
 include/rv/instrumentation.h | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 include/rv/instrumentation.h

new file mode 100644
index 000000000000..d4e7a02ede1a
@@ -0,0 +1,29 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
+ *
+ * Helper functions to facilitate the instrumentation of auto-generated
+ * RV monitors create by dot2k.
+ *
+ * The dot2k tool is available at tools/verification/dot2/
+ */
+
+#include <linux/ftrace.h>
+
+/*
+ * rv_attach_trace_probe - check and attach a handler function to a tracepoint
+ */
+#define rv_attach_trace_probe(monitor, tp, rv_handler)					\
+	do {										\
+		check_trace_callback_type_##tp(rv_handler);				\
+		WARN_ONCE(register_trace_##tp(rv_handler, NULL),			\
+				"fail attaching " #monitor " " #tp "handler");		\
+	} while (0)
+
+/*
+ * rv_detach_trace_probe - detach a handler function to a tracepoint
+ */
+#define rv_detach_trace_probe(monitor, tp, rv_handler)					\
+	do {										\
+		unregister_trace_##tp(rv_handler, NULL);				\
+	} while (0)

2.35.1

Add the runtime-verification.rst document, explaining the basics of RV and how to use the interface.

---
 Documentation/trace/index.rst                 |   1 +
 Documentation/trace/rv/index.rst              |   9 +
 .../trace/rv/runtime-verification.rst         | 231 ++++++++++++++++++
 kernel/trace/rv/Kconfig                       |   3 +
 kernel/trace/rv/rv.c                          |   3 +
 5 files changed, 247 insertions(+)
 create mode 100644 Documentation/trace/rv/index.rst
 create mode 100644 Documentation/trace/rv/runtime-verification.rst

index f9b7bcb5a630..2d73e8697523 100644
@@ -32,3 +32,4 @@ Linux Tracing Technologies
    sys-t
    coresight/index
    user_events
+   rv/index

new file mode 100644
index 000000000000..b54e49b1d0de
@@ -0,0 +1,9 @@
+====================
+Runtime Verification
+====================
+
+.. toctree::
+   :maxdepth: 2
+   :glob:
+
+   runtime-verification.rst

index 8714800e22ad..0d9552b406c6 100644
@@ -22,6 +22,9 @@ menuconfig RV
 	  actual execution, comparing it against a formal specification of
 	  the system behavior.
 
+	  For further information, see:
+	    Documentation/trace/rv/runtime-verification.rst
+
 config RV_REACTORS
 	bool "Runtime verification reactors"
 	default y

index df6678c86334..6c97cc2d754a 100644
@@ -133,6 +133,9 @@
  *      auto-generated wakeup in preemptive monitor.
  *      # cat enable
  *      0
+ *
+ *  For further information, see:
+ *   Documentation/trace/rv/runtime-verification.rst
  */
 
 #include <linux/kernel.h>

2.35.1

dot2c is a tool that transforms an automata in the graphiviz .dot file into an C representation of the automata.

usage: dot2c [-h] dot_file

dot2c: converts a .dot file into a C structure

positional arguments:
dot_file The dot file to be converted

optional arguments:
-h, --help show this help message and exit

---
 tools/verification/dot2/Makefile    |  21 +++
 tools/verification/dot2/automata.py | 171 +++++++++++++++++++
 tools/verification/dot2/dot2c       |  23 +++
 tools/verification/dot2/dot2c.py    | 251 ++++++++++++++++++++++++++++
 4 files changed, 466 insertions(+)
 create mode 100644 tools/verification/dot2/Makefile
 create mode 100644 tools/verification/dot2/automata.py
 create mode 100644 tools/verification/dot2/dot2c
 create mode 100644 tools/verification/dot2/dot2c.py

new file mode 100644
index 000000000000..235d182f6b2c
@@ -0,0 +1,21 @@
+INSTALL=install
+
+prefix  ?= /usr
+bindir  ?= $(prefix)/bin
+mandir  ?= $(prefix)/share/man
+miscdir ?= $(prefix)/share/dot2
+srcdir  ?= $(prefix)/src
+
+PYLIB  ?= $(shell python3 -c 'import sysconfig;  print (sysconfig.get_path("purelib"))')
+
+.PHONY: all
+all:
+
+.PHONY: clean
+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) dot2c -D -m 755 $(DESTDIR)$(bindir)/

new file mode 100644
index 000000000000..8a8cd84bdfcf
@@ -0,0 +1,23 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
+#
+# dot2c: parse an automata in dot file digraph format into a C
+#
+# This program was written in the development of this paper:
+#  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+#  "Efficient Formal Verification for the Linux Kernel." International
+#  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+
+if __name__ == '__main__':
+    from dot2 import dot2c
+    import argparse
+    import sys
+
+    parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
+    parser.add_argument('dot_file',  help='The dot file to be converted')
+
+    args = parser.parse_args()
+    d = dot2c.Dot2c(args.dot_file)
+    d.print_model_classic()

2.35.1

Add documentation about deterministic automaton and its possible representations (formal, graphic, .dot and C).

---
 .../trace/rv/deterministic_automata.rst       | 184 ++++++++++++++++++
 Documentation/trace/rv/index.rst              |   1 +
 tools/verification/dot2/automata.py           |   3 +
 tools/verification/dot2/dot2c                 |   3 +
 tools/verification/dot2/dot2c.py              |   3 +
 5 files changed, 194 insertions(+)
 create mode 100644 Documentation/trace/rv/deterministic_automata.rst

new file mode 100644
index 000000000000..d0638f95a455
@@ -0,0 +1,184 @@
+Deterministic Automata
+======================
+
+Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
+
+        *G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
+
+where:
+
+- *X* is the set of states;
+- *E* is the finite set of events;
+- x\ :subscript:`0` is the initial state;
+- X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
+- *f* : *X* x *E* -> *X* $ is the transition function. It defines the state
+  transition in the occurrence of an event from *E* in the state *X*. In the
+  special case of deterministic automata, the occurrence of the event in *E*
+  in a state in *X* has a deterministic next state from *X*.
+
+For example, a given automaton named 'wip' (wakeup in preemptive) can
+be defined as:
+
+- *X* = { ``preemptive``, ``non_preemptive``}
+- *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
+- x\ :subscript:`0` = ``preemptive``
+- X\ :subscript:`m` = {``preemptive``}
+- *f* =
+   - *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
+   - *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
+   - *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
+
+One of the benefits of this formal definition is that it can be presented
+in multiple formats. For example, using a *graphical representation*, using
+vertices (nodes) and edges, which is very intuitive for *operating system*
+practitioners, without any loss.
+
+The previous 'wip' automaton can also be represented as::
+
+                       preempt_enable
+          +---------------------------------+
+          v                                 |
+        #============#  preempt_disable   +------------------+
+    --> H preemptive H -----------------> |  non_preemptive  |
+        #============#                    +------------------+
+                                            ^              |
+                                            | sched_waking |
+                                            +--------------+
+
+Deterministic Automaton in C
+----------------------------
+
+In the paper "Efficient formal verification for the Linux kernel",
+the authors present a simple way to represent an automaton in C that can
+be used as regular code in the Linux kernel.
+
+For example, the 'wip' automata can be presented as (augmented with comments)::
+
+  /* enum representation of X (set of states) to be used as index */
+  enum states {
+	preemptive = 0,
+	non_preemptive,
+	state_max
+  };
+
+  #define INVALID_STATE state_max
+
+  /* enum representation of E (set of events) to be used as index */
+  enum events {
+	preempt_disable = 0,
+	preempt_enable,
+	sched_waking,
+	event_max
+  };
+
+  struct automaton {
+	char *state_names[state_max];                   // X: the set of states
+	char *event_names[event_max];                   // E: the finite set of events
+	unsigned char function[state_max][event_max];   // f: transition function
+	unsigned char initial_state;                    // x_0: the initial state
+	bool final_states[state_max];                   // X_m: the set of marked states
+  };
+
+  struct automaton aut = {
+	.state_names = {
+		"preemptive",
+		"non_preemptive"
+	},
+	.event_names = {
+		"preempt_disable",
+		"preempt_enable",
+		"sched_waking"
+	},
+	.function = {
+		{ non_preemptive,  INVALID_STATE,  INVALID_STATE },
+		{  INVALID_STATE,     preemptive, non_preemptive },
+	},
+	.initial_state = preemptive,
+	.final_states = { 1, 0 },
+  };
+
+The *transition function* is represented as a matrix of states (lines) and
+events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
+in O(1). For example::
+
+  next_state = automaton_wip.function[curr_state][event];
+
+Graphviz .dot format
+--------------------
+
+The Graphviz open-source tool can produce the graphical representation
+of an automaton using the (textual) DOT language as the source code.
+The DOT format is widely used and can be converted to many other formats.
+
+For example, this is the 'wip' model in DOT::
+
+  digraph state_automaton {
+        {node [shape = circle] "non_preemptive"};
+        {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
+        {node [shape = doublecircle] "preemptive"};
+        {node [shape = circle] "preemptive"};
+        "__init_preemptive" -> "preemptive";
+        "non_preemptive" [label = "non_preemptive"];
+        "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
+        "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
+        "preemptive" [label = "preemptive"];
+        "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
+        { rank = min ;
+                "__init_preemptive";
+                "preemptive";
+        }
+  }
+
+This DOT format can be transformed into a bitmap or vectorial image
+using the dot utility, or into an ASCII art using graph-easy. For
+instance::
+
+  $ dot -Tsvg -o wip.svg wip.dot
+  $ graph-easy wip.dot > wip.txt
+
+dot2c
+-----
+
+dot2c is a utility that can parse a .dot file containing an automaton as
+in the example above and automatically convert it to the C representation
+presented in [3].
+
+For example, having the previous 'wip' model into a file named 'wip.dot',
+the following command will transform the .dot file into the C
+representation (previously shown) in the 'wip.h' file::
+
+  $ dot2c wip.dot > wip.h
+
+The 'wip.h' content is the code sample in section 'Deterministic Automaton
+in C'.
+
+Remarks
+-------
+
+The automata formalism allows modeling discrete event systems (DES) in
+multiple formats, suitable for different applications/users.
+
+For example, the formal description using set theory is better suitable
+for automata operations, while the graphical format for human interpretation;
+and computer languages for machine execution.
+
+References
+----------
+
+Many textbooks cover automata formalism. For a brief introduction see::
+
+  O'Regan, Gerard. Concise guide to software engineering. Springer,
+  Cham, 2017.
+
+For a detailed description, including operations, and application on Discrete
+Event Systems (DES), see::
+
+  Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
+  event systems. Boston, MA: Springer US, 2008.
+
+For the C representation in kernel, see::
+
+  De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
+  Silva. Efficient formal verification for the Linux kernel. In:
+  International Conference on Software Engineering and Formal Methods.
+  Springer, Cham, 2019. p. 315-332.

index b54e49b1d0de..013a41a410cf 100644
@@ -7,3 +7,4 @@ Runtime Verification
    :glob:
 
    runtime-verification.rst
+   deterministic_automata.rst

index f22e1dff19ce..baffeb960ff0 100644
@@ -4,6 +4,9 @@
 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
 #
 # Automata object: parse an automata in dot file digraph format into a python object
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
 
 import ntpath
 

index 8a8cd84bdfcf..3fe89ab88b65 100644
@@ -9,6 +9,9 @@
 #  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
 #  "Efficient Formal Verification for the Linux Kernel." International
 #  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
 
 if __name__ == '__main__':
     from dot2 import dot2c

index bca902eec483..fa73353f7e56 100644
@@ -9,6 +9,9 @@
 #  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
 #  "Efficient Formal Verification for the Linux Kernel." International
 #  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
 
 from dot2.automata import Automata
 

2.35.1

transform .dot file into kernel rv monitor

usage: dot2k [-h] -d DOT_FILE -t MONITOR_TYPE [-n MODEL_NAME] [-D DESCRIPTION]

optional arguments:
-h, --help show this help message and exit
-d DOT_FILE, --dot DOT_FILE
-t MONITOR_TYPE, --monitor_type MONITOR_TYPE
-n MODEL_NAME, --model_name MODEL_NAME
-D DESCRIPTION, --description DESCRIPTION

---
 tools/verification/dot2/Makefile              |   5 +
 tools/verification/dot2/dot2k                 |  44 +++++
 tools/verification/dot2/dot2k.py              | 174 ++++++++++++++++++
 .../dot2/dot2k_templates/main_global.c        |  91 +++++++++
 .../dot2/dot2k_templates/main_per_cpu.c       |  91 +++++++++
 .../dot2/dot2k_templates/main_per_task.c      |  91 +++++++++
 6 files changed, 496 insertions(+)
 create mode 100644 tools/verification/dot2/dot2k
 create mode 100644 tools/verification/dot2/dot2k.py
 create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c
 create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c
 create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c

index 235d182f6b2c..021beb07a521 100644
@@ -19,3 +19,8 @@ install:
 	$(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
 	$(INSTALL) 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) dot2k -D -m 755 $(DESTDIR)$(bindir)/
+
+	mkdir -p ${miscdir}/
+	cp -rp dot2k_templates $(DESTDIR)$(miscdir)/

2.35.1

Add the da_monitor_synthesis.rst introduces some concepts behind the Deterministic Automata (DA) monitor synthesis and interface.

---
 .../trace/rv/da_monitor_synthesis.rst         | 147 ++++++++++++++++++
 Documentation/trace/rv/index.rst              |   1 +
 include/rv/da_monitor.h                       |   3 +
 tools/verification/dot2/dot2k                 |   3 +
 tools/verification/dot2/dot2k.py              |   3 +
 5 files changed, 157 insertions(+)
 create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst

new file mode 100644
index 000000000000..0dbdcd1e62b9
@@ -0,0 +1,147 @@
+Deterministic Automata Monitor Synthesis
+========================================
+
+The starting point for the application of runtime verification (RV) technics
+is the *specification* or *modeling* of the desired (or undesired) behavior
+of the system under scrutiny.
+
+The formal representation needs to be then *synthesized* into a *monitor*
+that can then be used in the analysis of the trace of the system. The
+*monitor* connects to the system via an *instrumentation* that converts
+the events from the *system* to the events of the *specification*.
+
+
+In Linux terms, the runtime verification monitors are encapsulated inside
+the *RV monitor* abstraction. The RV monitor includes a set of instances
+of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
+functions that glue the monitor to the system reference model, and the
+trace output as a reaction to event parsing and exceptions, as depicted
+below::
+
+ Linux  +----- RV Monitor ----------------------------------+ Formal
+  Realm |                                                   |  Realm
+  +-------------------+     +----------------+     +-----------------+
+  |   Linux kernel    |     |     Monitor    |     |     Reference   |
+  |     Tracing       |  -> |   Instance(s)  | <-  |       Model     |
+  | (instrumentation) |     | (verification) |     | (specification) |
+  +-------------------+     +----------------+     +-----------------+
+         |                          |                       |
+         |                          V                       |
+         |                     +----------+                 |
+         |                     | Reaction |                 |
+         |                     +--+--+--+-+                 |
+         |                        |  |  |                   |
+         |                        |  |  +-> trace output ?  |
+         +------------------------|--|----------------------+
+                                  |  +----> panic ?
+                                  +-------> <user-specified>
+
+DA 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
+contains a set of macros that automatically generate the monitor's code.
+
+dot2k
+-----
+
+The dot2k 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
+
+This will create a directory named wip/ with the following files:
+
+- wip.h: the wip model in C
+- wip.c: the RV monitor
+
+The wip.c file contains the monitor declaration and the starting point for
+the system instrumentation.
+
+Monitor macros
+--------------
+
+The rv/da_monitor.h enables automatic code generation for the *Monitor
+Instance(s)* using C macros.
+
+The benefits of the usage of macro for monitor synthesis are 3-fold as it:
+
+- 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.
+
+This initial implementation presents three different types of monitor instances:
+
+- ``#define DECLARE_DA_MON_GLOBAL(name, type)``
+- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
+- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
+
+The first declares the functions for a global deterministic automata monitor,
+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 model in C.
+
+For example, the wip model with two states and three events can be
+stored in an 'unsigned char' type. Considering that the preemption control
+is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
+
+  DECLARE_DA_MON_PER_CPU(wip, unsigned char);
+
+The monitor is executed by sending events to be processed via the functions
+presented below::
+
+  da_handle_event_$(MONITOR_NAME)($(event from event enum));
+  da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
+  da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
+
+The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
+the event will be processed if the monitor is processing events.
+
+When a monitor is enabled, it is placed in the initial state of the automata.
+However, the monitor does not know if the system is in the *initial state*.
+
+The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
+monitor that the system is returning to the initial state, so the monitor can
+start monitoring the next event.
+
+The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
+the monitor that the system is known to be in the initial state, so the
+monitor can start monitoring and monitor the current event.
+
+Using the wip model as example, the events "preempt_disable" and
+"sched_waking" should be sent to monitor, respectively, via [2]::
+
+  da_handle_event_wip(preempt_disable_wip);
+  da_handle_event_wip(sched_waking_wip);
+
+While the event "preempt_enabled" will use::
+
+  da_handle_start_event_wip(preempt_enable_wip);
+
+To notify the monitor that the system will be returning to the initial state,
+so the system and the monitor should be in sync.
+
+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
+of the system, increasing the confidence in the overall approach.
+
+[1] For details about deterministic automata format and the translation
+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
+avoid conflicting variables when exporting the global vmlinux.h
+use by BPF programs.

index 013a41a410cf..46d47f33052c 100644
@@ -8,3 +8,4 @@ Runtime Verification
 
    runtime-verification.rst
    deterministic_automata.rst
+   da_monitor_synthesis.rst

index 001bc298289f..9eb75683e012 100644
@@ -6,6 +6,9 @@
  * with automata models in C generated by the dot2k tool.
  *
  * The dot2k tool is available at tools/verification/dot2k/
+ *
+ * For further information, see:
+ *   Documentation/trace/rv/da_monitor_synthesis.rst
  */
 
 #include <rv/automata.h>

index 69106f4b7682..9dcd38abe20a 100644
@@ -4,6 +4,9 @@
 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
 #
 # dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For further information, see:
+#   Documentation/trace/rv/da_monitor_synthesis.rst
 
 if __name__ == '__main__':
     from dot2.dot2k import dot2k

index d85f755e3bc7..016550fccf1f 100644
@@ -4,6 +4,9 @@
 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
 #
 # dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For further information, see:
+#   Documentation/trace/rv/da_monitor_synthesis.rst
 
 from dot2.dot2c import Dot2c
 import platform

2.35.1

Add the da_monitor_instrumentation.rst. It describes the basics of RV monitor instrumentation.

---
 .../trace/rv/da_monitor_instrumentation.rst   | 171 ++++++++++++++++++
 Documentation/trace/rv/index.rst              |   1 +
 2 files changed, 172 insertions(+)
 create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst

new file mode 100644
index 000000000000..6c67c7b57811
@@ -0,0 +1,171 @@
+Deterministic Automata Instrumentation
+======================================
+
+The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
+includes a section dedicated to instrumentation.
+
+In the example of the wip.dot monitor created on [1], it will look like::
+
+  /*
+   * 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_preempt_disable(void *data, /* XXX: fill header */)
+  {
+	da_handle_event_wip(preempt_disable_wip);
+  }
+
+  static void handle_preempt_enable(void *data, /* XXX: fill header */)
+  {
+	da_handle_event_wip(preempt_enable_wip);
+  }
+
+  static void handle_sched_waking(void *data, /* XXX: fill header */)
+  {
+	da_handle_event_wip(sched_waking_wip);
+  }
+
+  static int enable_wip(void)
+  {
+	int retval;
+
+	retval = da_monitor_init_wip();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
+
+	return 0;
+  }
+
+The comment at the top of the section explains the general idea: the
+instrumentation section translates *kernel events* into the *model's
+event*.
+
+Tracing callback functions
+--------------------------
+
+The first three functions are the starting point of the callback *handler
+functions* for each of the three events from the wip model. The developer
+does not necessarily need to use them: they are just starting points.
+
+Using the example of::
+
+ void handle_preempt_disable(void *data, /* XXX: fill header */)
+ {
+        da_handle_event_wip(preempt_disable_wip);
+ }
+
+The preempt_disable event from the model connects directly to the
+preemptirq:preempt_disable. The preemptirq:preempt_disable event
+has the following signature, from include/trace/events/preemptirq.h::
+
+  TP_PROTO(unsigned long ip, unsigned long parent_ip)
+
+Hence, the handle_preempt_disable() function will look like::
+
+  void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
+
+In this case, the kernel event translates one to one with the automata
+event, and indeed, no other change is required for this function.
+
+The next handler function, handle_preempt_enable() has the same argument
+list from the handle_preempt_disable(). The difference is that the
+preempt_enable event will be used to synchronize the system to the model.
+
+Initially, the *model* is placed in the initial state. However, the *system*
+might or might not be in the initial state. The monitor cannot start
+processing events until it knows that the system has reached the initial state.
+Otherwise, the monitor and the system could be out-of-sync.
+
+Looking at the automata definition, it is possible to see that the system
+and the model are expected to return to the initial state after the
+preempt_enable execution. Hence, it can be used to synchronize the
+system and the model at the initialization of the monitoring section.
+
+The start is informed via a special handle function, the
+"da_handle_start_event_$(MONITOR_NAME)(event)", in this case::
+
+  da_handle_start_event_wip(preempt_enable_wip);
+
+So, the callback function will look like::
+
+  void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
+  {
+        da_handle_start_event_wip(preempt_enable_wip);
+  }
+
+Finally, the "handle_sched_waking()" will look like::
+
+  void handle_sched_waking(void *data, struct task_struct *task)
+  {
+        da_handle_event_wip(sched_waking_wip);
+  }
+
+And the explanation is left for the reader as an exercise.
+
+enable and disable functions
+----------------------------
+
+dot2k automatically creates two special functions::
+
+  enable_$(MONITOR_NAME)()
+  disable_$(MONITOR_NAME)()
+
+These functions are called when the monitor is enabled and disabled,
+respectively.
+
+They should be used to *attach* and *detach* the instrumentation to the running
+system. The developer must add to the relative function all that is needed to
+*attach* and *detach* its monitor to the system.
+
+For the wip case, these functions were named::
+
+ enable_wip()
+ disable_wip()
+
+But no change was required because: by default, these functions *attach* and
+*detach* the tracepoints_to_attach, which was enough for this case.
+
+Instrumentation helpers
+-----------------------
+
+To complete the instrumentation, the *handler functions* need to be attached to a
+kernel event, at the monitoring enable phase.
+
+The RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()"
+is used to connect the wip model events to the relative kernel event. dot2k automatically
+adds "rv_attach_trace_probe()" function call for each model event in the enable phase, as
+a suggestion.
+
+For example, from the wip sample model::
+
+  static int enable_wip(void)
+  {
+        int retval;
+
+        retval = da_monitor_init_wip();
+        if (retval)
+                return retval;
+
+        rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
+        rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
+        rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
+
+        return 0;
+  }
+
+The probes then need to be detached at the disable phase.
+
+[1] The wip model is presented in::
+
+  Documentation/trace/rv/deterministic_automata.rst
+
+The wip monitor is presented in::
+
+  Documentation/trace/rv/da_monitor_synthesis.rst

index 46d47f33052c..db2ae3f90b90 100644
@@ -9,3 +9,4 @@ Runtime Verification
    runtime-verification.rst
    deterministic_automata.rst
    da_monitor_synthesis.rst
+   da_monitor_instrumentation.rst

2.35.1

THIS CODE IS NOT LINKED TO THE MAKEFILE.

This model does not compile because it lacks the instrumentation part, which will be added next. In the typical case, there will be only one patch, but it was split into two patches for educational purposes.

This is the direct output this command line:

  $ dot2k -d tools/verification/models/wip.dot -t per_cpu

---
 kernel/trace/rv/monitors/wip/wip.c | 109 +++++++++++++++++++++++++++++
 kernel/trace/rv/monitors/wip/wip.h |  46 ++++++++++++
 2 files changed, 155 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/wip/wip.c
 create mode 100644 kernel/trace/rv/monitors/wip/wip.h

new file mode 100644
index 000000000000..79a054ca0cde
@@ -0,0 +1,109 @@
+// 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 "wip"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <linux/trace/events/sched.h>
+ */
+#include <trace/events/rv.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "wip.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_wip;
+DECLARE_DA_MON_PER_CPU(wip, unsigned char);
+
+/*
+ * 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_preempt_disable(void *data, /* XXX: fill header */)
+{
+	da_handle_event_wip(preempt_disable_wip);
+}
+
+static void handle_preempt_enable(void *data, /* XXX: fill header */)
+{
+	da_handle_event_wip(preempt_enable_wip);
+}
+
+static void handle_sched_waking(void *data, /* XXX: fill header */)
+{
+	da_handle_event_wip(sched_waking_wip);
+}
+
+static int enable_wip(void)
+{
+	int retval;
+
+	retval = da_monitor_init_wip();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
+
+	return 0;
+}
+
+static void disable_wip(void)
+{
+	rv_wip.enabled = 0;
+
+	rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
+	rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
+	rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
+
+	da_monitor_destroy_wip();
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_wip = {
+	.name = "wip",
+	.description = "auto-generated wip",
+	.enable = enable_wip,
+	.disable = disable_wip,
+	.reset = da_monitor_reset_all_wip,
+	.enabled = 0,
+};
+
+static int register_wip(void)
+{
+	rv_register_monitor(&rv_wip);
+	return 0;
+}
+
+static void unregister_wip(void)
+{
+	rv_unregister_monitor(&rv_wip);
+}
+
+module_init(register_wip);
+module_exit(unregister_wip);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("wip");

2.35.1

The wakeup in preemptive (wip) monitor verifies if the wakeup events always take place with preemption disabled:

                     |
                     |
                     v
                   #==================#
                   H    preemptive    H <+
                   #==================#  |
                     |                   |
                     | preempt_disable   | preempt_enable
                     v                   |
    sched_waking   +------------------+  |
  +--------------- |                  |  |
  |                |  non_preemptive  |  |
  +--------------> |                  | -+
                   +------------------+

The wakeup event always takes place with preemption disabled because of the scheduler synchronization. However, because the preempt_count and its trace event are not atomic with regard to interrupts, some inconsistencies might happen.

The documentation illustrates one of these cases.

---
 Documentation/trace/rv/index.rst       |  1 +
 Documentation/trace/rv/monitor_wip.rst | 55 ++++++++++++++++++++++++++
 include/trace/events/rv.h              | 10 +++++
 kernel/trace/rv/Kconfig                | 13 ++++++
 kernel/trace/rv/Makefile               |  1 +
 kernel/trace/rv/monitors/wip/wip.c     | 51 +++++++-----------------
 tools/verification/models/wip.dot      | 16 ++++++++
 7 files changed, 111 insertions(+), 36 deletions(-)
 create mode 100644 Documentation/trace/rv/monitor_wip.rst
 create mode 100644 tools/verification/models/wip.dot

index db2ae3f90b90..4cb71ed628b8 100644
@@ -10,3 +10,4 @@ Runtime Verification
    deterministic_automata.rst
    da_monitor_synthesis.rst
    da_monitor_instrumentation.rst
+   monitor_wip.rst

index 20a2e09c6416..e972f27d8df3 100644
@@ -56,6 +56,16 @@ DECLARE_EVENT_CLASS(error_da_monitor,
 		__entry->event,
 		__entry->state)
 );
+
+#ifdef CONFIG_RV_MON_WIP
+DEFINE_EVENT(event_da_monitor, event_wip,
+	    TP_PROTO(char *state, char *event, char *next_state, bool final_state),
+	    TP_ARGS(state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor, error_wip,
+	     TP_PROTO(char *state, char *event),
+	     TP_ARGS(state, event));
+#endif /* CONFIG_RV_MON_WIP */
 #endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */
 
 #ifdef CONFIG_DA_MON_EVENTS_ID

index 0d9552b406c6..e50f3346164a 100644
@@ -25,6 +25,19 @@ menuconfig RV
 	  For further information, see:
 	    Documentation/trace/rv/runtime-verification.rst
 
+config RV_MON_WIP
+	depends on RV
+	depends on PREEMPT_TRACER
+	select DA_MON_EVENTS_IMPLICIT
+	bool "wip monitor"
+	help
+	  Enable wip (wakeup in preemptive) sample monitor that illustrates
+	  the usage of per-cpu monitors, and one limitation of the
+	  preempt_disable/enable events.
+
+	  For further information, see:
+	    Documentation/trace/rv/monitor_wip.rst
+
 config RV_REACTORS
 	bool "Runtime verification reactors"
 	default y

index 8944274d9b41..b41109d2750a 100644
@@ -2,3 +2,4 @@
 
 obj-$(CONFIG_RV) += rv.o
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
+obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o

new file mode 100644
index 000000000000..2a53a9700a89
@@ -0,0 +1,16 @@
+digraph state_automaton {
+	{node [shape = circle] "non_preemptive"};
+	{node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
+	{node [shape = doublecircle] "preemptive"};
+	{node [shape = circle] "preemptive"};
+	"__init_preemptive" -> "preemptive";
+	"non_preemptive" [label = "non_preemptive"];
+	"non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
+	"non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
+	"preemptive" [label = "preemptive"];
+	"preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
+	{ rank = min ;
+		"__init_preemptive";
+		"preemptive";
+	}
+}

2.35.1

Per task wakeup while not running (wwnr) monitor.

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.

---
 Documentation/trace/rv/index.rst        |  1 +
 Documentation/trace/rv/monitor_wwnr.rst | 45 +++++++++++++
 include/trace/events/rv.h               | 12 ++++
 kernel/trace/rv/Kconfig                 | 12 ++++
 kernel/trace/rv/Makefile                |  1 +
 kernel/trace/rv/monitors/wwnr/wwnr.c    | 87 +++++++++++++++++++++++++
 kernel/trace/rv/monitors/wwnr/wwnr.h    | 46 +++++++++++++
 tools/verification/models/wwnr.dot      | 16 +++++
 8 files changed, 220 insertions(+)
 create mode 100644 Documentation/trace/rv/monitor_wwnr.rst
 create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c
 create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h
 create mode 100644 tools/verification/models/wwnr.dot

index 4cb71ed628b8..15fa966102c0 100644
@@ -11,3 +11,4 @@ Runtime Verification
    da_monitor_synthesis.rst
    da_monitor_instrumentation.rst
    monitor_wip.rst
+   monitor_wwnr.rst

index e972f27d8df3..56592da9301c 100644
@@ -122,6 +122,18 @@ DECLARE_EVENT_CLASS(error_da_monitor_id,
 		__entry->event,
 		__entry->state)
 );
+
+#ifdef CONFIG_RV_MON_WWNR
+/* id is the pid of the task */
+DEFINE_EVENT(event_da_monitor_id, event_wwnr,
+	     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_wwnr,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+#endif /* CONFIG_RV_MON_WWNR */
+
 #endif /* CONFIG_DA_MON_EVENTS_ID */
 #endif /* _TRACE_RV_H */
 

index e50f3346164a..b259d6e8dc7c 100644
@@ -38,6 +38,18 @@ config RV_MON_WIP
 	  For further information, see:
 	    Documentation/trace/rv/monitor_wip.rst
 
+config RV_MON_WWNR
+	depends on RV
+	select DA_MON_EVENTS_ID
+	bool "wwnr monitor"
+	help
+	  Enable wwnr (wakeup while not running) sample monitor, this is a
+	  sample monitor that illustrates the usage of per-task monitor.
+	  The model is borken on purpose: it serves to test reactors.
+
+	  For further information, see:
+	    Documentation/trace/rv/monitor_wwnr.rst
+
 config RV_REACTORS
 	bool "Runtime verification reactors"
 	default y

index b41109d2750a..af0ff9a46418 100644
@@ -3,3 +3,4 @@
 obj-$(CONFIG_RV) += rv.o
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
+obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o

new file mode 100644
index 000000000000..1b206e83129c
@@ -0,0 +1,16 @@
+digraph state_automaton {
+	{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";
+	}
+}

2.35.1

A reactor that printks the reaction message.

---
 kernel/trace/rv/Kconfig          |  8 ++++++
 kernel/trace/rv/Makefile         |  3 ++-
 kernel/trace/rv/reactor_printk.c | 42 ++++++++++++++++++++++++++++++++
 3 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 kernel/trace/rv/reactor_printk.c

index b259d6e8dc7c..e82d5015e6ab 100644
@@ -60,3 +60,11 @@ config RV_REACTORS
 	  on the model's execution. By default, the monitors have
 	  tracing reactions, printing the monitor output via tracepoints,
 	  but other reactions can be added (on-demand) via this interface.
+
+config RV_REACT_PRINTK
+	bool "Printk reactor"
+	depends on RV_REACTORS
+	default y
+	help
+	  Enables the printk reactor. The printk reactor emits a printk()
+	  message if an exception is found.

index af0ff9a46418..a13c750a35c1 100644
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: GPL-2.0
 
 obj-$(CONFIG_RV) += rv.o
-obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
 obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
+obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
+obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o

2.35.1

Sample reactor that panics the system when an exception is found. This is useful both to capture a vmcore, or to fail-safe a critical system.

---
 kernel/trace/rv/Kconfig         |  8 ++++++
 kernel/trace/rv/Makefile        |  1 +
 kernel/trace/rv/reactor_panic.c | 43 +++++++++++++++++++++++++++++++++
 3 files changed, 52 insertions(+)
 create mode 100644 kernel/trace/rv/reactor_panic.c

index e82d5015e6ab..831779607e84 100644
@@ -68,3 +68,11 @@ config RV_REACT_PRINTK
 	help
 	  Enables the printk reactor. The printk reactor emits a printk()
 	  message if an exception is found.
+
+config RV_REACT_PANIC
+	bool "Panic reactor"
+	depends on RV_REACTORS
+	default y
+	help
+	  Enables the panic reactor. The panic reactor emits a printk()
+	  message if an exception is found and panic()s the system.

index a13c750a35c1..963d14875b45 100644
@@ -5,3 +5,4 @@ obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
 obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
+obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o

2.35.1