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, Rômulo 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, Rômulo 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).

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

In this RFC I am still not proposing any complex model. Instead, I am presenting only simple monitors that help to illustrate the usage of the automatic code generation and the RV interface. This is important to enable other researchers and developers to start using/extending this method.

It is also worth mentioning that this work has been heavily motivated by the usage of Linux on safety critical systems, mainly by the people involved in the Elisa Project. Indeed, we will be talking about the usage of RV in this field on today's presentation:

A Maintainable and Scalable Kernel Qualification Approach for Automotive Gabriele Paoloni, Intel Corporation & Daniel Bristot de Oliveira, Red Hat

At the Elisa workshop.

The more academic concepts behind this approach have been discussed with some researchers, including:

- Romulo Silva de Oliveira - Universidade Federal de Santa Catarina (BR)
- Tommaso Cucinotta - Scuola Superiore Sant'Anna (IT)
- Srdan Krstic - ETH Zurich (CH)
- Dmitriy Traytel - University of Copenhagen (DK)

Thanks!
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 tracing helper functions
tools/rv: Add dot2c
tools/rv: Add dot2k
rv/monitors: Add the wip monitor skeleton created by dot2k rv/monitors: wip instrumentation and Makefile/Kconfig entries rv/monitors: Add the wwnr monitor skeleton created by dot2k rv/monitors: wwnr instrumentation and Makefile/Kconfig entries rv/reactors: Add the printk reactor
rv/reactors: Add the panic reactor
rv/docs: Add a basic documentation
rv/docs: Add deterministic automata monitor synthesis documentation rv/docs: Add deterministic automata instrumentation documentation

 Documentation/trace/index.rst                 |   1 +
 .../trace/rv/da_monitor_instrumentation.rst   | 230 ++++++
 .../trace/rv/da_monitor_synthesis.rst         | 286 +++++++
 Documentation/trace/rv/index.rst              |   9 +
 .../trace/rv/runtime-verification.rst         | 233 ++++++
 include/linux/rv.h                            |  31 +
 include/rv/automata.h                         |  52 ++
 include/rv/da_monitor.h                       | 336 +++++++++
 include/rv/trace_helpers.h                    |  69 ++
 kernel/trace/Kconfig                          |   2 +
 kernel/trace/Makefile                         |   2 +
 kernel/trace/rv/Kconfig                       |  60 ++
 kernel/trace/rv/Makefile                      |   8 +
 kernel/trace/rv/monitors/wip/model.h          |  38 +
 kernel/trace/rv/monitors/wip/wip.c            | 124 ++++
 kernel/trace/rv/monitors/wip/wip.h            |  64 ++
 kernel/trace/rv/monitors/wwnr/model.h         |  38 +
 kernel/trace/rv/monitors/wwnr/wwnr.c          | 122 +++
 kernel/trace/rv/monitors/wwnr/wwnr.h          |  70 ++
 kernel/trace/rv/reactors/panic.c              |  44 ++
 kernel/trace/rv/reactors/printk.c             |  43 ++
 kernel/trace/rv/rv.c                          | 700 ++++++++++++++++++
 kernel/trace/rv/rv.h                          |  50 ++
 kernel/trace/rv/rv_reactors.c                 | 478 ++++++++++++
 kernel/trace/trace.c                          |   4 +
 kernel/trace/trace.h                          |   2 +
 tools/tracing/rv/dot2/Makefile                |  26 +
 tools/tracing/rv/dot2/automata.py             | 179 +++++
 tools/tracing/rv/dot2/dot2c                   |  30 +
 tools/tracing/rv/dot2/dot2c.py                | 240 ++++++
 tools/tracing/rv/dot2/dot2k                   |  49 ++
 tools/tracing/rv/dot2/dot2k.py                | 184 +++++
 .../rv/dot2/dot2k_templates/main_global.c     |  96 +++
 .../rv/dot2/dot2k_templates/main_global.h     |  64 ++
 .../rv/dot2/dot2k_templates/main_per_cpu.c    |  96 +++
 .../rv/dot2/dot2k_templates/main_per_cpu.h    |  64 ++
 .../rv/dot2/dot2k_templates/main_per_task.c   |  96 +++
 .../rv/dot2/dot2k_templates/main_per_task.h   |  70 ++
 38 files changed, 4290 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/index.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/trace_helpers.h
 create mode 100644 kernel/trace/rv/Kconfig
 create mode 100644 kernel/trace/rv/Makefile
 create mode 100644 kernel/trace/rv/monitors/wip/model.h
 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/model.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/reactors/panic.c
 create mode 100644 kernel/trace/rv/reactors/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/tracing/rv/dot2/Makefile
 create mode 100644 tools/tracing/rv/dot2/automata.py
 create mode 100644 tools/tracing/rv/dot2/dot2c
 create mode 100644 tools/tracing/rv/dot2/dot2c.py
 create mode 100644 tools/tracing/rv/dot2/dot2k
 create mode 100644 tools/tracing/rv/dot2/dot2k.py
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.h
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.h

2.26.2

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, et al. 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:
[root@f32 rv]# 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:
[root@f32 rv]# cat enabled_monitors
[root@f32 rv]# echo wip > enabled_monitors
[root@f32 rv]# echo wwnr >> enabled_monitors
[root@f32 rv]# cat enabled_monitors
wip
wwnr
[root@f32 rv]# echo -wip >> enabled_monitors
[root@f32 rv]# cat enabled_monitors
wwnr
[root@f32 rv]# echo > enabled_monitors
[root@f32 rv]# cat enabled_monitors
[root@f32 rv]#

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, but stop the per-entity monitors of monitoring the events received from the system. It resambles 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 resambles the "events" directory on tracefs.

For example:
[root@f32 rv]# cd monitors/wip/
[root@f32 wip]# ls
desc enable
[root@f32 wip]# cat desc
auto-generated wakeup in preemptive monitor.
[root@f32 wip]# 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       |  21 ++
 kernel/trace/Kconfig     |   2 +
 kernel/trace/Makefile    |   2 +
 kernel/trace/rv/Kconfig  |  13 +
 kernel/trace/rv/Makefile |   3 +
 kernel/trace/rv/rv.c     | 687 +++++++++++++++++++++++++++++++++++++++
 kernel/trace/rv/rv.h     |  31 ++
 kernel/trace/trace.c     |   4 +
 kernel/trace/trace.h     |   2 +
 9 files changed, 765 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..04f94919ebb0
@@ -0,0 +1,21 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Runtime Verification.
+ *
+ * For futher information, see: kernel/trace/rv/rv.c.
+ *
+ * Copyright (C) 2019-2021 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+struct rv_monitor {
+	const char		*name;
+	const char		*description;
+	bool			enabled;
+	int			(*start)(void);
+	void			(*stop)(void);
+	void			(*reset)(void);
+};
+
+extern bool monitoring_on;
+int rv_unregister_monitor(struct rv_monitor *monitor);
+int rv_register_monitor(struct rv_monitor *monitor);

index 7fa82778c3e6..870ecd8a023f 100644
@@ -969,6 +969,8 @@ config HIST_TRIGGERS_DEBUG
 
           If unsure, say N.
 
+source "kernel/trace/rv/Kconfig"
+
 endif # FTRACE
 
 endif # TRACING_SUPPORT

index b28d3e5013cd..70788f15912c 100644
@@ -98,3 +98,5 @@ obj-$(CONFIG_FTRACE_RECORD_RECURSION) += trace_recursion_record.o
 obj-$(CONFIG_TRACEPOINT_BENCHMARK) += trace_benchmark.o
 
 libftrace-y := ftrace.o
+
+obj-$(CONFIG_RV) += rv/

new file mode 100644
index 000000000000..e8e65cfc7959
@@ -0,0 +1,13 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+menuconfig RV
+	bool "Runtime Verification"
+	depends on TRACING
+	default y if DEBUG_KERNEL
+	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..30056469e514
@@ -0,0 +1,31 @@
+#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_create_dir		tracefs_create_dir
+#define rv_create_file		tracefs_create_file
+#define rv_remove		tracefs_remove
+
+#define MAX_RV_MONITOR_NAME_SIZE	100
+
+extern struct mutex interface_lock;
+
+struct rv_monitor_def {
+	struct list_head list;
+	struct rv_monitor *monitor;
+	struct dentry *root_d;
+	bool enabled;
+	bool reacting;
+};
+
+extern bool monitoring_on;
+struct dentry *get_monitors_root(void);
+void reset_all_monitors(void);
+int init_rv_monitors(struct dentry *root_dir);

index a21ef9cd2aae..2d87c6d14167 100644
@@ -9539,6 +9539,10 @@ static __init int tracer_init_tracefs(void)
 
 	update_tracer_options(&global_trace);
 
+#ifdef CONFIG_RV
+	rv_init_interface();
+#endif
+
 	return 0;
 }
 

index cd80d046c7a5..51cb706e3fbe 100644
@@ -1952,4 +1952,6 @@ static inline bool is_good_name(const char *name)
 	return true;
 }
 
+extern int rv_init_interface(void);
+
 #endif /* _LINUX_KERNEL_TRACE_H */

2.26.2

yes, you are right, I will remove it.

Ack!

Thanks!
-- Daniel

Can you send a new updated version. I'd like to review whatever you have as the latest.

Thanks!

-- 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:
[root@f32 rv]# 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:
[root@f32 rv]# cat monitors/wip/reactors [nop]
panic
printk
[root@f32 rv]# echo panic > monitors/wip/reactors [root@f32 rv]# cat monitors/wip/reactors nop
[panic]
printk

---
 include/linux/rv.h            |  10 +
 kernel/trace/rv/Kconfig       |  14 +
 kernel/trace/rv/Makefile      |   1 +
 kernel/trace/rv/rv.c          |  17 +-
 kernel/trace/rv/rv.h          |  19 ++
 kernel/trace/rv/rv_reactors.c | 478 ++++++++++++++++++++++++++++++++++
 6 files changed, 537 insertions(+), 2 deletions(-)
 create mode 100644 kernel/trace/rv/rv_reactors.c

index 04f94919ebb0..1568b48f07a7 100644
@@ -6,6 +6,11 @@
  *
  * Copyright (C) 2019-2021 Daniel Bristot de Oliveira <[email protected]>
  */
+struct rv_reactor {
+	char			*name;
+	char			*description;
+	void			(*react)(char *);
+};
 
 struct rv_monitor {
 	const char		*name;

@@ -14,8 +19,13 @@ struct rv_monitor {
 	int			(*start)(void);
 	void			(*stop)(void);
 	void			(*reset)(void);
+	void			(*react)(char *);
 };
 
 extern bool monitoring_on;
 int rv_unregister_monitor(struct rv_monitor *monitor);
 int rv_register_monitor(struct rv_monitor *monitor);
+
+extern bool reacting_on;
+int rv_unregister_reactor(struct rv_reactor *reactor);
+int rv_register_reactor(struct rv_reactor *reactor);

index e8e65cfc7959..74eb2f216255 100644
@@ -11,3 +11,17 @@ 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.
+
+if RV
+
+config RV_REACTORS
+	bool "Runtime verification reactors"
+	default y if 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.
+
+endif # RV

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 e6e1acfc8666..9c7ea300fab6 100644
@@ -312,8 +312,13 @@ static int create_monitor_dir(struct rv_monitor_def *mdef)
 		retval = -ENOMEM;
 		goto out_remove_root;
 	}
+#ifdef CONFIG_RV_REACTORS
+	retval = reactor_create_monitor_files(mdef);
+	if (retval)
+		goto out_remove_root;
+#endif
 
-	return retval;
+	return 0;
 
 out_remove_root:
 	rv_remove(mdef->root_d);

@@ -621,7 +626,11 @@ int rv_register_monitor(struct rv_monitor *monitor)
 
 	r->monitor = monitor;
 
-	create_monitor_dir(r);
+	retval = create_monitor_dir(r);
+	if (retval) {
+		kfree(r);
+		goto out_unlock;
+	}
 
 	list_add_tail(&r->list, &rv_monitors_list);
 

@@ -681,6 +690,10 @@ int __init rv_init_interface(void)
 	rv_create_file("monitoring_on", 0600, rv_root.root_dir, NULL,
 		       &monitoring_on_fops);
 
+#ifdef CONFIG_RV_REACTORS
+	init_rv_reactors(rv_root.root_dir);
+	reacting_on=true;
+#endif
 	monitoring_on=true;
 
 	return 0;

index 30056469e514..82f64c2b6a50 100644
@@ -14,12 +14,25 @@ struct rv_interface {
 #define rv_remove		tracefs_remove
 
 #define MAX_RV_MONITOR_NAME_SIZE	100
+#define MAX_RV_REACTOR_NAME_SIZE	100
 
 extern struct mutex 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;
+#ifdef CONFIG_RV_REACTORS
+	struct rv_reactor_def *rdef;
+#endif
 	struct dentry *root_d;
 	bool enabled;
 	bool reacting;

@@ -29,3 +42,9 @@ extern bool monitoring_on;
 struct dentry *get_monitors_root(void);
 void reset_all_monitors(void);
 int init_rv_monitors(struct dentry *root_dir);
+
+#ifdef CONFIG_RV_REACTORS
+extern bool reacting_on;
+int reactor_create_monitor_files(struct rv_monitor_def *mdef);
+int init_rv_reactors(struct dentry *root_dir);
+#endif

2.26.2

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 occurence 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 for monitoring.

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

new file mode 100644
index 000000000000..b95941bf78ac
@@ -0,0 +1,52 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Deterministic automata helper functions, to be used with the automata
+ * models in C generated by the dot2k tool.
+ *
+ * The dot2k tool is available at https://gitlab.com/linux-rv-tools/dot2/.
+ *
+ * Copyright (C) 2019-2021 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#define DECLARE_AUTOMATA_HELPERS(name, type)					\
+										\
+static inline void *model_get_model_##name(void)				\
+{										\
+	return (void *) &automaton_##name;					\
+}										\
+										\
+char *model_get_state_name_##name(enum states_##name state)			\
+{										\
+	return automaton_##name.state_names[state];				\
+}										\
+										\
+char *model_get_event_name_##name(enum events_##name event)			\
+{										\
+	return automaton_##name.event_names[event];				\
+}										\
+										\
+static inline type model_get_init_state_##name(void)				\
+{										\
+	return automaton_##name.initial_state;					\
+}										\
+										\
+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))			\
+		return -1;							\
+										\
+	if ((event < 0) || (event > event_max))					\
+		return -1;							\
+										\
+	return automaton_##name.function[curr_state][event];			\
+}										\
+										\
+static inline bool model_is_final_state_##name(enum states_##name state)	\
+{										\
+	if ((state < 0) || (state > state_max))					\
+		return 0;							\
+										\
+	return !!automaton_##name.final_states[state];				\
+}

2.26.2

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>

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 connecting the Formal Reaml to Linux-like code.

This header file goes beyond, extending the code generation to the verification stage, generating the code to the Monitor Instance(s) level using C macros. The trace event code inspires this approach.

The benefits of the usage of macro for monitor synthesis is 3-fold:

- Reduces the code duplication;
- Facilitates the bug fix/improvement;
(but mainly:)
- 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 two different types of monitor instances:

- #define DECLARE_DA_MON_PER_CPU(name, type)
- #define DECLARE_DA_MON_PER_TASK(name, type)

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

In both cases, the name is a string that identifies the monitor, and the type is the data type used by dot2c/k on the representation of the model.

For example, the model "wip" below:

preempt_disable sched_waking
+############+ >------------------> +################+ >------------+
-># preemptive # # non-preemptive # |
+############+ <-----------------< +################+ <------------+
preempt_enable

with two states and three events can be stored in a 'char' type. Considering that the preemption control is a per-cpu behavior, the monitor declaration will be:

  DECLARE_DA_MON_PER_CPU(wip, 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_init_event_$(MONITOR_NAME)($(event from event enum));

The function da_handle_event_$(MONITOR_NAME) is the regular case, while the function da_handle_init_event_$(MONITOR_NAME)() is a special case used to synchronize the system with the model.

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. Hence, the monitor ignores events sent by sent by da_handle_event_$(MONITOR_NAME) until the function da_handle_init_event_$(MONITOR_NAME)() is called.

The function da_handle_init_event_$(MONITOR_NAME)() should be used for the case in which the system generates the event is the one that returns the automata to the initial state.

After receiving a da_handle_init_event_$(MONITOR_NAME)() event, the monitor will know that it is in sync with the system and hence will start processing the next events.

Using the wip model as example, the events "preempt_disable" and "sched_waking" should be sent to to monitor, respectively, via:

        da_handle_event_wip(preempt_disable);
        da_handle_event_wip(sched_waking);

While the event "preempt_enabled" will use:

        da_handle_init_event_wip(preempt_enable);

To notify the monitor that the system will be returning to the initial state, so the system and the monitor should be in sync.

With the monitor synthesis in place, using these headers and dot2k, the developer's work should be limited to the instrumentation of the system, increasing the confidence in the overall approach.

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

new file mode 100644
index 000000000000..6ed95a898d2b
@@ -0,0 +1,336 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Deterministic automata (DA) monitor functions, to be used togheter
+ * with automata models in C generated by the dot2k tool.
+ *
+ * The dot2k tool is available at tools/tracing/rv/
+ *
+ * Copyright (C) 2019-2021 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#include <rv/automata.h>
+#include <rv/trace_helpers.h>
+
+struct da_monitor {
+	char curr_state;
+	bool monitoring;
+	void *model;
+};
+
+#define MAX_PID		 1024000
+
+/*
+ * Generic helpers for all types of deterministic automata monitors.
+ */
+#define DECLARE_DA_MON_GENERIC_HELPERS(name, type)				\
+static char REACT_MSG[1024];							\
+										\
+static inline char								\
+*format_react_msg(type curr_state, type event)					\
+{										\
+	snprintf(REACT_MSG, 1024,						\
+		"rv: monitor %s does not allow event %s on state %s\n",		\
+		MODULE_NAME,							\
+		model_get_event_name_##name(event),				\
+		model_get_state_name_##name(curr_state));			\
+	return REACT_MSG;							\
+}										\
+										\
+static inline void da_monitor_reset_##name(struct da_monitor *da_mon)		\
+{										\
+	da_mon->monitoring = 0;							\
+	da_mon->curr_state = model_get_init_state_##name();			\
+}										\
+										\
+static inline type da_monitor_curr_state_##name(struct da_monitor *da_mon)	\
+{										\
+	return da_mon->curr_state;						\
+}										\
+										\
+static inline void								\
+da_monitor_set_state_##name(struct da_monitor *da_mon, enum states_##name state)\
+{										\
+	da_mon->curr_state = state;						\
+}										\
+static inline void da_monitor_start_##name(struct da_monitor *da_mon)		\
+{										\
+	da_mon->monitoring = 1;							\
+}										\
+										\
+static inline bool da_monitoring_##name(struct da_monitor *da_mon)		\
+{										\
+	return da_mon->monitoring;						\
+}
+
+
+/*
+ * Event handler for implict monitors. Implicity monitor is the one which the
+ * handler does not need to specify which da_monitor to manilupulate. Examples
+ * of implicit monitor are the per_cpu or the global ones.
+ */
+#define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)			\
+static inline void								\
+trace_event_##name(type state, type event, type next_state, bool safe);		\
+static inline void trace_error_##name(type state, type event);			\
+										\
+static inline bool								\
+da_event_##name(struct da_monitor *da_mon, enum events_##name event)		\
+{										\
+	type curr_state = da_monitor_curr_state_##name(da_mon);			\
+	type next_state = model_get_next_state_##name(curr_state, event);	\
+										\
+	if (next_state >= 0) {							\
+		da_monitor_set_state_##name(da_mon, next_state);		\
+										\
+		trace_event_##name(curr_state, event, next_state,		\
+				model_is_final_state_##name(next_state));	\
+										\
+		return true;							\
+	}									\
+										\
+	if (reacting_on && rv_##name.react)					\
+		rv_##name.react(format_react_msg(curr_state, event));		\
+										\
+	trace_error_##name(curr_state, event);					\
+										\
+	return false;								\
+}										\
+
+/*
+ * Event handler for per_task monitors.
+ */
+#define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)			\
+										\
+static inline void								\
+trace_event_##name(pid_t pid, type state, type event,				\
+		   type next_state, bool safe);					\
+static inline void trace_error_##name(pid_t pid, type state, type event);	\
+										\
+static inline type								\
+da_event_##name(struct da_monitor *da_mon, pid_t pid, enum events_##name event)	\
+{										\
+	type curr_state = da_monitor_curr_state_##name(da_mon);			\
+	type next_state = model_get_next_state_##name(curr_state, event);	\
+										\
+	if (next_state >= 0) {							\
+		da_monitor_set_state_##name(da_mon, next_state);		\
+										\
+		trace_event_##name(pid, curr_state, event, next_state,		\
+				   model_is_final_state_##name(next_state));	\
+										\
+		return true;							\
+	}									\
+										\
+	if (reacting_on && rv_##name.react)					\
+		rv_##name.react(format_react_msg(curr_state, event));		\
+										\
+	trace_error_##name(pid, curr_state, event);				\
+										\
+	return false;								\
+}
+
+/*
+ * Functions to define, init and get a per-cpu monitor.
+ *
+ * XXX: Make it dynamic.
+ */
+#define DECLARE_DA_MON_INIT_PER_CPU(name, type)					\
+										\
+DEFINE_PER_CPU(struct da_monitor, da_mon_##name);				\
+										\
+struct da_monitor *da_get_monitor_##name(void)					\
+{										\
+	return this_cpu_ptr(&da_mon_##name);					\
+}										\
+										\
+void da_monitor_reset_all_##name(void)						\
+{										\
+	struct da_monitor *da_mon;						\
+	int cpu;								\
+	for_each_cpu(cpu, cpu_online_mask) {					\
+		da_mon = per_cpu_ptr(&da_mon_##name, cpu);			\
+		da_monitor_reset_##name(da_mon);				\
+	}									\
+}										\
+										\
+static inline void da_monitor_init_##name(void)					\
+{										\
+	struct da_monitor *da_mon;						\
+	int cpu;								\
+	for_each_cpu(cpu, cpu_online_mask) {					\
+		da_mon = per_cpu_ptr(&da_mon_##name, cpu);			\
+		da_mon->curr_state = model_get_init_state_##name();		\
+		da_mon->monitoring = 0;						\
+		da_mon->model = model_get_model_##name();			\
+	}									\
+}										\
+
+
+/*
+ * Functions to define, init and get a per-task monitor.
+ *
+ * XXX: Make it dynamic? make it part of the task structure?
+ */
+#define DECLARE_DA_MON_INIT_PER_TASK(name, type)				\
+										\
+struct da_monitor da_mon_##name[MAX_PID];					\
+										\
+static inline struct da_monitor *da_get_monitor_##name(pid_t pid)		\
+{										\
+	return &da_mon_##name[pid];						\
+}										\
+										\
+void da_monitor_reset_all_##name(void)						\
+{										\
+	struct da_monitor *mon = da_mon_##name;					\
+	int i;									\
+	for (i = 0; i < MAX_PID; i++)						\
+		da_monitor_reset_##name(&mon[i]);				\
+}										\
+										\
+static void da_monitor_init_##name(void)					\
+{										\
+	struct da_monitor *mon = da_mon_##name;					\
+	int i;									\
+										\
+	for (i = 0; i < MAX_PID; i++) {						\
+		mon[i].curr_state = model_get_init_state_##name();		\
+		mon[i].monitoring = 0;						\
+		mon[i].model = model_get_model_##name();			\
+	}									\
+}										\
+
+/*
+ * Handle event for implicit monitor: da_get_monitor_##name() will figure out
+ * the monitor.
+ */
+#define DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)			\
+										\
+static inline void __da_handle_event_##name(struct da_monitor *da_mon,		\
+				     enum events_##name event)			\
+{										\
+	int retval;								\
+										\
+	if (unlikely(!monitoring_on))						\
+		return;								\
+										\
+	if (unlikely(!rv_##name.enabled))					\
+		return;								\
+										\
+	if (unlikely(!da_monitoring_##name(da_mon)))				\
+		return;								\
+										\
+	retval = da_event_##name(da_mon, event);				\
+										\
+	if (!retval)								\
+		da_monitor_reset_##name(da_mon);				\
+}										\
+										\
+static inline void da_handle_event_##name(enum events_##name event)		\
+{										\
+	struct da_monitor *da_mon = da_get_monitor_##name();			\
+	__da_handle_event_##name(da_mon, event);				\
+}										\
+										\
+static inline bool da_handle_init_event_##name(enum events_##name event)	\
+{										\
+	struct da_monitor *da_mon;						\
+										\
+	if (unlikely(!rv_##name.enabled))					\
+		return false;							\
+										\
+	da_mon = da_get_monitor_##name();					\
+										\
+	if (unlikely(!da_monitoring_##name(da_mon))) {				\
+		da_monitor_start_##name(da_mon);				\
+		return false;							\
+	}									\
+										\
+	__da_handle_event_##name(da_mon, event);				\
+										\
+	return true;								\
+}
+
+/*
+ * Handle event for per task.
+ */
+#define DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)			\
+										\
+static inline void								\
+__da_handle_event_##name(struct da_monitor *da_mon, pid_t pid,			\
+			 enum events_##name event)				\
+{										\
+	int retval;								\
+										\
+	if (unlikely(!monitoring_on))						\
+		return;								\
+										\
+	if (unlikely(!rv_##name.enabled))					\
+		return;								\
+										\
+	if (unlikely(!da_monitoring_##name(da_mon)))				\
+		return;								\
+										\
+	retval = da_event_##name(da_mon, pid, event);				\
+										\
+	if (!retval)								\
+		da_monitor_reset_##name(da_mon);				\
+}										\
+										\
+static inline void								\
+da_handle_event_##name(pid_t pid, enum events_##name event)			\
+{										\
+	struct da_monitor *da_mon = da_get_monitor_##name(pid);			\
+	__da_handle_event_##name(da_mon, pid, event);				\
+}										\
+										\
+static inline bool								\
+da_handle_init_event_##name(pid_t pid, enum events_##name event)		\
+{										\
+	struct da_monitor *da_mon;						\
+										\
+	if (unlikely(!rv_##name.enabled))					\
+		return false;							\
+										\
+	da_mon = da_get_monitor_##name(pid);					\
+										\
+	if (unlikely(!da_monitoring_##name(da_mon))) {				\
+		da_monitor_start_##name(da_mon);				\
+		return false;							\
+	}									\
+										\
+	__da_handle_event_##name(da_mon, pid, event);				\
+										\
+	return true;								\
+}
+
+
+/*
+ * Entry point for the per-cpu monitor.
+ */
+#define DECLARE_DA_MON_PER_CPU(name, type)					\
+										\
+DECLARE_AUTOMATA_HELPERS(name, type);						\
+										\
+DECLARE_DA_MON_GENERIC_HELPERS(name, type);					\
+										\
+DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type);				\
+										\
+DECLARE_DA_MON_INIT_PER_CPU(name, type);					\
+										\
+DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type);
+
+/*
+ * Entry point for the per-cpu monitor.
+ */
+#define DECLARE_DA_MON_PER_TASK(name, type)					\
+										\
+DECLARE_AUTOMATA_HELPERS(name, type);						\
+										\
+DECLARE_DA_MON_GENERIC_HELPERS(name, type);					\
+										\
+DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type);				\
+										\
+DECLARE_DA_MON_INIT_PER_TASK(name, type);					\
+										\
+DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type);

2.26.2

Good to know I can use the task struct! This will make my life easier. I did it this way because I started doing the code all "out-of-tree," as modules... but being in kernel gives such possibilities.

I will try to implement your idea! I do not see many concurrent monitors running, and as the list search will be linear to the number of active monitors... it might not even justify any more complex data structure.

Thanks Peter!

-- Daniel

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

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

new file mode 100644
index 000000000000..1a8b6f246d0d
@@ -0,0 +1,69 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Helper functions to facilitate the instrumentation of auto-generated
+ * RV monitors create by dot2k.
+ *
+ * The dot2k tool is available at tools/tracing/rv/dot2/
+ *
+ * Copyright (C) 2019-2021 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#include <linux/ftrace.h>
+
+struct tracepoint_hook_helper {
+	struct tracepoint *tp;
+	void *probe;
+	int registered;
+	char *name;
+};
+
+static inline void thh_compare_name(struct tracepoint *tp, void *priv)
+{
+	struct tracepoint_hook_helper *thh  = priv;
+
+	if (!strcmp(thh->name, tp->name))
+		thh->tp = tp;
+}
+
+static inline bool thh_fill_struct_tracepoint(struct tracepoint_hook_helper *thh)
+{
+	for_each_kernel_tracepoint(thh_compare_name, thh);
+
+	return !!thh->tp;
+}
+
+static inline void thh_unhook_probes(struct tracepoint_hook_helper *thh, int helpers_count)
+{
+	int i;
+
+	for (i = 0; i < helpers_count; i++) {
+		if (!thh[i].registered)
+			continue;
+
+		tracepoint_probe_unregister(thh[i].tp, thh[i].probe, NULL);
+	}
+}
+
+static inline int thh_hook_probes(struct tracepoint_hook_helper *thh, int helpers_count)
+{
+	int retval;
+	int i;
+
+	for (i = 0; i < helpers_count; i++) {
+		retval = thh_fill_struct_tracepoint(&thh[i]);
+		if (!retval)
+			goto out_err;
+
+		retval = tracepoint_probe_register(thh[i].tp, thh[i].probe, NULL);
+
+		if (retval)
+			goto out_err;
+
+		thh[i].registered = 1;
+	}
+	return 0;
+
+out_err:
+	thh_unhook_probes(thh, helpers_count);
+	return -EINVAL;
+}

2.26.2

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/tracing/rv/dot2/Makefile    |  21 +++
 tools/tracing/rv/dot2/automata.py | 179 ++++++++++++++++++++++
 tools/tracing/rv/dot2/dot2c       |  30 ++++
 tools/tracing/rv/dot2/dot2c.py    | 240 ++++++++++++++++++++++++++++++
 4 files changed, 470 insertions(+)
 create mode 100644 tools/tracing/rv/dot2/Makefile
 create mode 100644 tools/tracing/rv/dot2/automata.py
 create mode 100644 tools/tracing/rv/dot2/dot2c
 create mode 100644 tools/tracing/rv/dot2/dot2c.py

new file mode 100644
index 000000000000..9dd59ec8a733
@@ -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 distutils.sysconfig;  print (distutils.sysconfig.get_python_lib())')
+
+.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..be87e7ff2305
@@ -0,0 +1,30 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# dot2m: transform dot files into C structures.
+# For more information, see:
+#   https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# 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.
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+#  Daniel Bristot de Oliveira <[email protected]>
+
+if __name__ == '__main__':
+    from dot2 import dot2c
+    import argparse
+    import ntpath
+    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.26.2

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/tracing/rv/dot2/Makefile                |   5 +
 tools/tracing/rv/dot2/dot2k                   |  49 +++++
 tools/tracing/rv/dot2/dot2k.py                | 184 ++++++++++++++++++
 .../rv/dot2/dot2k_templates/main_global.c     |  96 +++++++++
 .../rv/dot2/dot2k_templates/main_global.h     |  64 ++++++
 .../rv/dot2/dot2k_templates/main_per_cpu.c    |  96 +++++++++
 .../rv/dot2/dot2k_templates/main_per_cpu.h    |  64 ++++++
 .../rv/dot2/dot2k_templates/main_per_task.c   |  96 +++++++++
 .../rv/dot2/dot2k_templates/main_per_task.h   |  70 +++++++
 9 files changed, 724 insertions(+)
 create mode 100644 tools/tracing/rv/dot2/dot2k
 create mode 100644 tools/tracing/rv/dot2/dot2k.py
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.h
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
 create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.h

index 9dd59ec8a733..fcec4bf2bb11 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.26.2

This is the direct output this command line:

  $ dot2k -d ~/wip.dot -t per_cpu

with wip.dot as:
----- %< -----

digraph state_automaton {
	center = true;
	size = "7,11";
	rankdir = LR;
	{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 model is broken because preempt_disable_notrace(). It is broken on purpose to test the reactors.

It does not compile because it lacks the instrumentation, which will be add next.

---
 kernel/trace/rv/monitors/wip/model.h |  38 ++++++++
 kernel/trace/rv/monitors/wip/wip.c   | 124 +++++++++++++++++++++++++++
 kernel/trace/rv/monitors/wip/wip.h   |  64 ++++++++++++++
 3 files changed, 226 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/wip/model.h
 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..5212ba5b1dfb
@@ -0,0 +1,38 @@
+enum states_wip {
+	preemptive = 0,
+	non_preemptive,
+	state_max
+};
+
+enum events_wip {
+	preempt_disable = 0,
+	preempt_enable,
+	sched_waking,
+	event_max
+};
+
+struct automaton_wip {
+	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_wip automaton_wip = {
+	.state_names = {
+		"preemptive",
+		"non_preemptive"
+	},
+	.event_names = {
+		"preempt_disable",
+		"preempt_enable",
+		"sched_waking"
+	},
+	.function = {
+		{ non_preemptive,             -1,             -1 },
+		{             -1,     preemptive, non_preemptive },
+	},
+	.initial_state = preemptive,
+	.final_states = { 1, 0 },
+};
\ No newline at end of file

2.26.2

Adds the instrumentation to the previously created wip monitor, as an example of the developer work. It also adds a Makefile and Kconfig entries.

This is a good example of the manual work that is left for the developer to do.

---
 kernel/trace/rv/Kconfig            |  7 +++++++
 kernel/trace/rv/Makefile           |  1 +
 kernel/trace/rv/monitors/wip/wip.c | 16 ++++++++--------
 kernel/trace/rv/monitors/wip/wip.h |  2 +-
 4 files changed, 17 insertions(+), 9 deletions(-)

index 74eb2f216255..4a1088c5ba68 100644
@@ -14,6 +14,13 @@ menuconfig RV
 
 if RV
 
+config RV_MON_WIP
+	depends on PREEMPTIRQ_TRACEPOINTS
+	tristate "WIP monitor"
+	help
+	  Enable WIP sample monitor, this is a sample monitor that
+	  illustrates the usage of per-cpu monitors.
+
 config RV_REACTORS
 	bool "Runtime verification reactors"
 	default y if RV

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

index 1aec75e683d2..dd35a042e727 100644
@@ -33,36 +33,36 @@ DECLARE_DA_MON_PER_CPU(wip, char);
  *
  */
 
-void handle_preempt_disable(void *data, /* XXX: fill header */)
+void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
 {
 	da_handle_event_wip(preempt_disable);
 }
 
-void handle_preempt_enable(void *data, /* XXX: fill header */)
+void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
 {
-	da_handle_event_wip(preempt_enable);
+	da_handle_init_event_wip(preempt_enable);
 }
 
-void handle_sched_waking(void *data, /* XXX: fill header */)
+void handle_sched_waking(void *data, struct task_struct *task)
 {
 	da_handle_event_wip(sched_waking);
 }
 
-#define NR_TP   3
+#define NR_TP	3
 static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
 	{
 		.probe = handle_preempt_disable,
-		.name = /* XXX: tracepoint name here */,
+		.name = "preempt_disable",
 		.registered = 0
 	},
 	{
 		.probe = handle_preempt_enable,
-		.name = /* XXX: tracepoint name here */,
+		.name = "preempt_enable",
 		.registered = 0
 	},
 	{
 		.probe = handle_sched_waking,
-		.name = /* XXX: tracepoint name here */,
+		.name = "sched_wakeup",
 		.registered = 0
 	},
 };

index 7a751a8896e9..f980b5e85940 100644
@@ -59,6 +59,6 @@ TRACE_EVENT(error_wip,
 
 /* This part ust be outside protection */
 #undef TRACE_INCLUDE_PATH
-#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_PATH ../kernel/trace/rv/monitors/wip/
 #define TRACE_INCLUDE_FILE wip
 #include <trace/define_trace.h>

2.26.2

WIP means "Wakeup In Preemptive." I will add the long name to the first occurrence in patch 08, and to the Kconfig.

Thanks!
-- Daniel

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.

---
 kernel/trace/rv/monitors/wwnr/model.h |  38 ++++++++
 kernel/trace/rv/monitors/wwnr/wwnr.c  | 127 ++++++++++++++++++++++++++
 kernel/trace/rv/monitors/wwnr/wwnr.h  |  70 ++++++++++++++
 3 files changed, 235 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/wwnr/model.h
 create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c
 create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h

new file mode 100644
index 000000000000..7840ffbda98d
@@ -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

2.26.2

Adds the instrumentation to the previously created wwnr monitor, as an example of the developer work. It also adds a Makefile and Kconfig entries.

---
 kernel/trace/rv/Kconfig              |  7 ++++++
 kernel/trace/rv/Makefile             |  1 +
 kernel/trace/rv/monitors/wwnr/wwnr.c | 35 ++++++++++++----------------
 kernel/trace/rv/monitors/wwnr/wwnr.h |  2 +-
 4 files changed, 24 insertions(+), 21 deletions(-)

index 4a1088c5ba68..612b36b97663 100644
@@ -21,6 +21,13 @@ config RV_MON_WIP
 	  Enable WIP sample monitor, this is a sample monitor that
 	  illustrates the usage of per-cpu monitors.
 
+config RV_MON_WWNR
+	tristate "WWNR monitor"
+	help
+	  Enable WWNR sample monitor, this is a sample monitor that
+	  illustrates the usage of per-task monitor. The model is
+	  broken on purpose: it serves to test reactors.
+
 config RV_REACTORS
 	bool "Runtime verification reactors"
 	default y if RV

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

index 91cb3b70a6a7..cb364a02639b 100644
@@ -33,39 +33,34 @@ DECLARE_DA_MON_PER_TASK(wwnr, char);
  *
  */
 
-void handle_switch_in(void *data, /* XXX: fill header */)
+static void handle_switch(void *data, bool preempt, struct task_struct *p, struct task_struct *n)
 {
-	pid_t pid = /* XXX how do I get the pid? */;
-	da_handle_event_wwnr(pid, switch_in);
-}
+	int ppid = p->pid;
+	int npid = n->pid;
 
-void handle_switch_out(void *data, /* XXX: fill header */)
-{
-	pid_t pid = /* XXX how do I get the pid? */;
-	da_handle_event_wwnr(pid, switch_out);
+	if (ppid && ppid < MAX_PID)
+		da_handle_init_event_wwnr(ppid, switch_out);
+
+	if (npid && npid < MAX_PID)
+		da_handle_event_wwnr(npid, switch_in);
 }
 
-void handle_wakeup(void *data, /* XXX: fill header */)
+static void handle_wakeup(void *data, struct task_struct *p)
 {
-	pid_t pid = /* XXX how do I get the pid? */;
-	da_handle_event_wwnr(pid, wakeup);
+	if (p->pid && p->pid < MAX_PID)
+		da_handle_event_wwnr(p->pid, wakeup);
 }
 
-#define NR_TP   3
+#define NR_TP	2
 static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
 	{
-		.probe = handle_switch_in,
-		.name = /* XXX: tracepoint name here */,
-		.registered = 0
-	},
-	{
-		.probe = handle_switch_out,
-		.name = /* XXX: tracepoint name here */,
+		.probe = handle_switch,
+		.name = "sched_switch",
 		.registered = 0
 	},
 	{
 		.probe = handle_wakeup,
-		.name = /* XXX: tracepoint name here */,
+		.name = "sched_wakeup",
 		.registered = 0
 	},
 };

index 4af1827d2f16..ed817952821e 100644
@@ -65,6 +65,6 @@ TRACE_EVENT(error_wwnr,
 
 /* This part ust be outside protection */
 #undef TRACE_INCLUDE_PATH
-#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_PATH ../kernel/trace/rv/monitors/wwnr/
 #define TRACE_INCLUDE_FILE wwnr
 #include <trace/define_trace.h>

2.26.2

yeah, I will do so.

(WWNR stands for "Wakeup while not running")

Thanks!
-- Daniel

Sample reactor that printks the reaction message.

Note: do not use this reactor with rq_lock taken, it will lock the system until printk can handle that.

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

index 612b36b97663..6cbfb0f9cf76 100644
@@ -38,4 +38,12 @@ config RV_REACTORS
 	  tracing reactions, printing the monitor output via tracepoints,
 	  but other reactions can be added (on-demand) via this interface.
 
+config RV_REACT_PRINTK
+	tristate "Printk reactor"
+	depends on RV_REACTORS
+	default y if RV_REACTORS
+	help
+	  Enables the printk reactor. The printk reactor emmits a printk()
+	  message if an exception is found.
+
 endif # RV

index af0ff9a46418..a57cb3c3d410 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) += reactors/printk.o

2.26.2

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/reactors/panic.c | 44 ++++++++++++++++++++++++++++++++
 3 files changed, 53 insertions(+)
 create mode 100644 kernel/trace/rv/reactors/panic.c

index 6cbfb0f9cf76..32de3e7702ec 100644
@@ -46,4 +46,12 @@ config RV_REACT_PRINTK
 	  Enables the printk reactor. The printk reactor emmits a printk()
 	  message if an exception is found.
 
+config RV_REACT_PANIC
+	tristate "Panic reactor"
+	depends on RV_REACTORS
+	default y if RV_REACTORS
+	help
+	  Enables the panic reactor. The panic reactor emmits a printk()
+	  message if an exception is found and panic()s the system.
+
 endif # RV

index a57cb3c3d410..995f199d0348 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) += reactors/printk.o
+obj-$(CONFIG_RV_REACT_PANIC) += reactors/panic.o

2.26.2

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         | 233 ++++++++++++++++++
 kernel/trace/rv/Kconfig                       |   3 +
 4 files changed, 246 insertions(+)
 create mode 100644 Documentation/trace/rv/index.rst
 create mode 100644 Documentation/trace/rv/runtime-verification.rst

index f634b36fd3aa..fd3d26a6c6b8 100644
@@ -28,3 +28,4 @@ Linux Tracing Technologies
    stm
    sys-t
    coresight/index
+   rv/index

new file mode 100644
index 000000000000..92338dceffab
@@ -0,0 +1,9 @@
+===================================
+RV - Runtime Verification Interface
+===================================
+
+.. toctree::
+   :maxdepth: 2
+   :glob:
+
+   *

index 32de3e7702ec..41132a1d481c 100644
@@ -12,6 +12,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
+
 if RV
 
 config RV_MON_WIP

2.26.2

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

---
 .../trace/rv/da_monitor_synthesis.rst         | 286 ++++++++++++++++++
 1 file changed, 286 insertions(+)
 create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst

new file mode 100644
index 000000000000..697eb5a45910
@@ -0,0 +1,286 @@
+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*
+conects to the system via an *instrumentation* layer, that converts the events
+from the *system* to the events of the *specification*.
+
+This document introduces some concepts behind the **Deterministic Automata
+(DA)** monitor synthesis.
+
+DA monitor synthesis in a nutshell
+------------------------------------------------------
+
+The synthesis of automata-based models into the Linux *RV monitor* abstraction
+is automatized by a tool named "dot2k", and the "rv/da_monitor.h" provided
+by the RV interface.
+
+Given a file "wip.dot", representing a per-cpu monitor, with this content::
+
+  digraph state_automaton {
+	center = true;
+	size = "7,11";
+	rankdir = LR;
+	{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";
+	}
+  }
+
+Run the dot2k tool with the model, specifying that it is a "per-cpu"
+model::
+
+  $ dot2k -d ~/wip.dot -t per_cpu
+
+This will create a directory named "wip/" with the following files:
+
+- model.h: the wip in C
+- wip.h: tracepoints that report the execution of the events by the
+  monitor
+- wip.c: the RV monitor
+
+The following line in the "wip.c" file is responsible for the monitor
+synthesis::
+
+  DECLARE_DA_MON_PER_CPU(wip, char);
+
+With that in place, the work left to be done is the *instrumentation* of
+the monitor, which is already initialized by dot2k.
+
+DA: Introduction and representation formats
+---------------------------------------------------------------
+
+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 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*.
+
+One of the most evident benefits for the practical application of the automata
+formalism is its *graphic representation*, represented using vertices (nodes)
+and edges, which is very intuitive for *operating system* practitioners.
+
+For example, given an automata wip, with a regular representation of:
+
+- *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``
+
+
+It can also be represented in a graphic format, without any loss, using this
+format::
+
+                       preempt_enable
+          +---------------------------------+
+          v                                 |
+        #============#  preempt_disable   +------------------+
+    --> H preemptive H -----------------> |  non_preemptive  |
+        #============#                    +------------------+
+                                            ^ sched_waking |
+                                            +--------------+
+
+The Graphviz open-source tool can produce this graphic format using the
+(textual) DOT language as the source code. The DOT format is widely
+used and can be converted to many other formats, including the ASCII art above.
+
+The dot2c tool presented in:
+
+  DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Rômulo
+  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. For instance, using the wip model as input for dot2c results in
+the following C representation::
+
+  enum states {
+	preemptive = 0,
+	non_preemptive,
+	state_max
+  };
+
+  enum events {
+	preempt_disable = 0,
+	preempt_enable,
+	sched_waking,
+	event_max
+  };
+
+  struct automaton {
+	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 aut = {
+	.state_names = {
+		"preemptive",
+		"non_preemptive"
+	},
+	.event_names = {
+		"preempt_disable",
+		"preempt_enable",
+		"sched_waking"
+	},
+	.function = {
+		{ non_preemptive,             -1,             -1 },
+		{             -1,     preemptive, non_preemptive },
+	},
+	.initial_state = preemptive,
+	.final_states = { 1, 0 },
+  };
+
+DA monitor synthesis for Linux
+------------------------------
+
+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>
+
+
+The dot2c tool works connecting the *Reference Model* to the *RV Monitor*
+abstraction by translating the *formal notation* into *code*.
+
+The "rv/da_monitor.h" header goes beyond dot2c, extending the code
+generation to the verification stage, generating the code to the *Monitor
+Instance(s)* level using C macros. The trace event code inspires this
+approach.
+
+The benefits of the usage of macro for monitor synthesis is 3-fold:
+
+- 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 two different types of monitor instances:
+
+- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
+- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
+
+The first declares the functions for deterministic automata monitor with
+per-cpu instances, and the second with per-task instances.
+
+In both cases, the name is a string that identifies the monitor, and the type
+is the data type used by dot2c/k on the representation of the model.
+
+For example, the "wip" model with two states and three events can be
+stored in a "char" type. Considering that the preemption control is a
+per-cpu behavior, the monitor declaration will be::
+
+  DECLARE_DA_MON_PER_CPU(wip, 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_init_event_$(MONITOR_NAME)($(event from event enum));
+
+The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case,
+while the function ``da_handle_init_event_$(MONITOR_NAME)()`` is a special
+case used to synchronize the system with the model.
+
+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*.
+Hence, the monitor ignores events sent by sent by
+``da_handle_event_$(MONITOR_NAME)()`` until the function
+``da_handle_init_event_$(MONITOR_NAME)()`` is called.
+
+The function ``da_handle_init_event_$(MONITOR_NAME)()`` should be used for
+the case in which the system generates the event is the one that returns
+the automata to the initial state.
+
+After receiving a ``da_handle_init_event_$(MONITOR_NAME)()`` event, the
+monitor will know that it is in sync with the system and hence will
+start processing the next events.
+
+Using the wip model as example, the events "preempt_disable" and
+"sched_waking" should be sent to to monitor, respectively, via::
+
+  da_handle_event_wip(preempt_disable);
+  da_handle_event_wip(sched_waking);
+
+While the event "preempt_enabled" will use::
+
+  da_handle_init_event_wip(preempt_enable);
+
+To notify the monitor that the system will be returning to the initial state,
+so the system and the monitor should be in sync.
+
+rv/da_monitor.h
+-------------------------------------------
+
+The "rv/da_monitor.h" is, mostly, a set of C macros that create function
+definitions based on the paremeters passed via ``DECLARE_DA_MON_*``.
+
+In fewer words, the declaration of a monitor generates:
+
+- Helper functions for getting information from the automata model generated
+  by dot2k.
+- Helper functions for the analysis of a deterministic automata model
+- Functions for the initialization of the monitor instances
+- The definition of the structure to store the monitor instances' data
+
+One important aspect is that the monitor does not call external functions
+for the handling of the events sent by the instrumentation, except for
+generating *tracing events* or *reactions*.
+
+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.

2.26.2

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

---
 .../trace/rv/da_monitor_instrumentation.rst   | 230 ++++++++++++++++++
 1 file changed, 230 insertions(+)
 create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst

new file mode 100644
index 000000000000..6c5188f76cba
@@ -0,0 +1,230 @@
+Deterministic Automata Instrumentation
+========================================
+
+This document introduces some concepts behind the **Deterministic Automata
+(DA)** monitor instrumentation.
+
+The synthesis of automata-based models into the Linux *RV monitor* abstraction
+is automatized by a tool named dot2k, and the "rv/da_monitor.h" provided
+by the RV interface.
+
+For example, given a file "wip.dot", representing a per-cpu monitor, with
+this content::
+
+  digraph state_automaton {
+	center = true;
+	size = "7,11";
+	rankdir = LR;
+	{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";
+	}
+  }
+
+That is the "DOT" representation of this automata model::
+
+                       preempt_enable
+          +---------------------------------+
+          v                                 |
+        #============#  preempt_disable   +------------------+
+    --> H preemptive H -----------------> |  non_preemptive  |
+        #============#                    +------------------+
+                                            ^ sched_waking |
+                                            +--------------+
+
+
+Run the dot2k tool with the model, specifying that it is a "per-cpu"
+model::
+
+  $ dot2k -d ~/wip.dot -t per_cpu
+
+This will create a directory named "wip/" with the following files:
+
+- model.h: the wip in C
+- wip.h: tracepoints that report the execution of the events by the
+  monitor
+- wip.c: the RV monitor
+
+The monitor instrumentation should be done entirely in the RV monitor,
+in the example above, in the wip.c file.
+
+The RV monitor instrumentation section
+--------------------------------------
+
+The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
+will include a section dedicated to instrumentation.
+
+In the example of the wip.dot above, 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.
+  *
+  */
+
+ void handle_preempt_disable(void *data, /* XXX: fill header */)
+ {
+	da_handle_event_wip(preempt_disable);
+ }
+
+ void handle_preempt_enable(void *data, /* XXX: fill header */)
+ {
+	da_handle_event_wip(preempt_enable);
+ }
+
+ void handle_sched_waking(void *data, /* XXX: fill header */)
+ {
+	da_handle_event_wip(sched_waking);
+ }
+
+ #define NR_TP   3
+ struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+	{
+		.probe = handle_preempt_disable,
+		.name = /* XXX: tracepoint name here */,
+		.registered = 0
+	},
+	{
+		.probe = handle_preempt_enable,
+		.name = /* XXX: tracepoint name here */,
+		.registered = 0
+	},
+	{
+		.probe = handle_sched_waking,
+		.name = /* XXX: tracepoint name here */,
+		.registered = 0
+	},
+ };
+
+The comment at the top of the section explains the general idea: the
+instrumentation section translates *kernel events* into the *events
+accepted by the model*.
+
+Tracing callback functions
+-----------------------------
+
+The first three functions are skeletons for 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);
+ }
+
+The "preempt_disable" event from the model conects 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 even translates one to one with the automata event,
+and indeed, no other change is needed 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 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 initialization is informed via an special handle function, the
+"da_handle_init_event_$(MONITOR)(event)", in this case::
+
+  da_handle_event_wip(preempt_disable);
+
+So, the callback function will look like::
+
+  void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
+  {
+        da_handle_init_event_wip(preempt_enable);
+  }
+
+Finally, the "handle_sched_waking()" will look like::
+
+  void handle_sched_waking(void *data, struct task_struct *task)
+  {
+        da_handle_event_wip(sched_waking);
+  }
+
+And the explanation is left for the reader as an exercise.
+
+Tracepoint hook helpers
+--------------------------
+
+Still in the previous example, the next code section is the
+"tracepoint_to_hook" definition, which is a structure that aims to help to
+connect a monitor *handler function* with a given "tracepoint". Note that
+this is just a suggestion. Indeed, the *handler functions* can hook to anything
+that is possible to hook in the kernel, not even limited to the
+tracing interface.
+
+For the specific case of wip, the "tracepoints_to_hook" structure was
+defined as::
+
+  #define NR_TP   3
+  struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+        {
+                .probe = handle_preempt_disable,
+                .name = "preempt_disable",
+                .registered = 0
+        },
+        {
+                .probe = handle_preempt_enable,
+                .name = "preempt_enable",
+                .registered = 0
+        },
+        {
+                .probe = handle_sched_waking,
+                .name = "sched_wakeup",
+                .registered = 0
+        },
+  };
+
+And that is the instrumentation required for the wip sample model.
+
+Start and Stop functions
+------------------------
+
+Finally, dot2k automatically creates two special functions::
+
+  start_$MODELNAME()
+  stop_$MODELNAME()
+
+These functions are called when the monitor is enabled and disabled,
+respectivelly.
+They should be used to *hook* and *unhook* the instrumentation to the running
+system. The developer must add to the relative function all that is needed to
+*hook* and *unhook* its monitor to the system.
+
+For the wip case, these functions were named::
+
+ start_wip()
+ stop_wip()
+
+But no change was required because: by default, these functions *hook* and
+*unhook* the tracepoints_to_hook, which was enough for this case.

2.26.2