The Runtime Verification (RV) interface

kernel/trace/rv/rv.c new file +16 -0

+/*
+ * interface for enabling/disabling a monitor.
+ */
+static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf,
+					 size_t count, loff_t *ppos)
+{
+	struct rv_monitor_def *mdef = filp->private_data;
+	int retval;
+	bool val;
+
+	retval = kstrtobool_from_user(user_buf, count, &val);
+	if (retval)
+		return retval;
+
+	retval = count;
+

kernel/trace/rv/rv.c new file +6 -0

+static void *enabled_monitors_start(struct seq_file *m, loff_t *pos)
+{
+	struct rv_monitor_def *m_def;
+	loff_t l;
+
+	mutex_lock(&rv_interface_lock);

kernel/trace/rv/rv.c new file +44 -0

+		return -EINVAL;
+
+	memset(buff, 0, sizeof(buff));
+
+	retval = simple_write_to_buffer(buff, sizeof(buff) - 1, ppos, user_buf, count);
+	if (!retval)
+		return -EFAULT;
+
+	ptr = strim(buff);
+
+	if (ptr[0] == '!') {
+		enable = false;
+		ptr++;
+	}
+
+	len = strlen(ptr);
+	if (!len)
+		return count;
+
+	mutex_lock(&rv_interface_lock);
+
+	retval = -EINVAL;
+
+	list_for_each_entry(mdef, &rv_monitors_list, list) {
+		if (strcmp(ptr, mdef->monitor->name) != 0)
+			continue;
+
+		/*
+		 * Monitor found!
+		 */
+		if (enable)
+			retval = enable_monitor(mdef);
+		else
+			retval = disable_monitor(mdef);
+
+		if (!retval)
+			retval = count;
+
+		break;
+	}
+
+	mutex_unlock(&rv_interface_lock);
+	return retval;
+}

On Wed, Jul 13, 2022 at 11:17:17PM +0200, Daniel Bristot de Oliveira <[email protected]> wrote:

[...]

kernel/trace/rv/rv.c line 194

Quoted 5 lines

kernel/trace/rv/rv.c new file +5 -0

+void put_task_monitor_slot(int slot)
+{
+	lockdep_assert_held(&rv_interface_lock);
+
+	if (slot < 0 || slot > RV_PER_TASK_MONITORS) {

slot is the array index that should be 0 here. The up bound is not bigger than 0 because the element of array now is RV_PER_TASK_MONITORS.

So up bound check is 'slot > RV_PER_TASK_MONITORS-1'.

[...]

Quoted 20 lines

kernel/trace/rv/rv.c new file +20 -0

+/*
+ * interface for enabling/disabling a monitor.
+ */
+static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf,
+					 size_t count, loff_t *ppos)
+{
+	struct rv_monitor_def *mdef = filp->private_data;
+	int retval;
+	bool val;
+
+	retval = kstrtobool_from_user(user_buf, count, &val);
+	if (retval)
+		return retval;
+
+	retval = count;
+
+	mutex_lock(&rv_interface_lock);
+
+	if (val)
+		retval = enable_monitor(mdef);

kernel/trace/rv/rv.c line 283

Quoted 6 lines

kernel/trace/rv/rv.c new file +6 -0

+	else
+		retval = disable_monitor(mdef);
+
+	mutex_unlock(&rv_interface_lock);
+
+	return retval ? retval : count;

Feel that this can be written return retval ? : count;

[...]

Quoted 6 lines

kernel/trace/rv/rv.c new file +6 -0

+static void *enabled_monitors_start(struct seq_file *m, loff_t *pos)
+{
+	struct rv_monitor_def *m_def;
+	loff_t l;
+
+	mutex_lock(&rv_interface_lock);

kernel/trace/rv/rv.c line 420

Quoted 10 lines

kernel/trace/rv/rv.c new file +10 -0

+
+	if (list_empty(&rv_monitors_list))
+		return NULL;
+
+	m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list);
+
+	for (l = 0; l <= *pos; ) {
+		m_def = enabled_monitors_next(m, m_def, &l);
+		if (!m_def)
+			break;

Is this check is inversed. enabled_monitors_start() will stop at first enabled monitor, then enabled_monitors_next() do loop to next. Check like the above, enabled_monitors_start() will loop to the last monitor. But I doubt myself I do not mention/see it. Sorry for these.

the check is:

if (m_def)

     break;

[...]

Quoted 8 lines

kernel/trace/rv/rv.c new file +8 -0

+static ssize_t
+enabled_monitors_write(struct file *filp, const char __user *user_buf,
+		      size_t count, loff_t *ppos)
+{
+	char buff[MAX_RV_MONITOR_NAME_SIZE + 2];
+	struct rv_monitor_def *mdef;
+	int retval = -EINVAL;
+	bool enable = true;

kernel/trace/rv/rv.c line 488

Quoted 4 lines

kernel/trace/rv/rv.c new file +4 -0

+	char *ptr = buff;
+	int len;
+
+	if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE + 2)

@count would not include '\0'. That the max val of @count is MAX_RV_MONITOR_NAME_SIZE+1. So the up bound check of @count is count > MAX_RV_MONITOR_NAME_SIZE + 1.

Quoted 14 lines · Tao Zhou

On Wed, Jul 13, 2022 at 11:17:17PM +0200, Daniel Bristot de Oliveira <[email protected]> wrote:

[...]

kernel/trace/rv/rv.c line 194

Quoted 5 lines

kernel/trace/rv/rv.c new file +5 -0

+void put_task_monitor_slot(int slot)
+{
+	lockdep_assert_held(&rv_interface_lock);
+
+	if (slot < 0 || slot > RV_PER_TASK_MONITORS) {

slot is the array index that should be 0 here. The up bound is not bigger than 0 because the element of array now is RV_PER_TASK_MONITORS.

Quoted 1 line

So up bound check is 'slot > RV_PER_TASK_MONITORS-1'.

fixed! (slot >= RV...)

Quoted 22 lines

[...]

Quoted 20 lines

kernel/trace/rv/rv.c new file +20 -0

+/*
+ * interface for enabling/disabling a monitor.
+ */
+static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf,
+					 size_t count, loff_t *ppos)
+{
+	struct rv_monitor_def *mdef = filp->private_data;
+	int retval;
+	bool val;
+
+	retval = kstrtobool_from_user(user_buf, count, &val);
+	if (retval)
+		return retval;
+
+	retval = count;
+
+	mutex_lock(&rv_interface_lock);
+
+	if (val)
+		retval = enable_monitor(mdef);

Quoted 8 lines

kernel/trace/rv/rv.c line 283

Quoted 6 lines

kernel/trace/rv/rv.c new file +6 -0

+	else
+		retval = disable_monitor(mdef);
+
+	mutex_unlock(&rv_interface_lock);
+
+	return retval ? retval : count;

Feel that this can be written return retval ? : count;

why not...

Quoted 26 lines

[...]

Quoted 6 lines

kernel/trace/rv/rv.c new file +6 -0

+static void *enabled_monitors_start(struct seq_file *m, loff_t *pos)
+{
+	struct rv_monitor_def *m_def;
+	loff_t l;
+
+	mutex_lock(&rv_interface_lock);

kernel/trace/rv/rv.c line 420

Quoted 10 lines

kernel/trace/rv/rv.c new file +10 -0

+
+	if (list_empty(&rv_monitors_list))
+		return NULL;
+
+	m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list);
+
+	for (l = 0; l <= *pos; ) {
+		m_def = enabled_monitors_next(m, m_def, &l);
+		if (!m_def)
+			break;

Is this check is inversed. enabled_monitors_start() will stop at first enabled monitor, then enabled_monitors_next() do loop to next. Check like the above, enabled_monitors_start() will loop to the last monitor. But I doubt myself I do not mention/see it. Sorry for these.

the check is:

Quoted 4 lines

if (m_def)

     break;

[...]

see kernel/trace/trace_events.c:s_start...

Quoted 8 lines

Quoted 8 lines

kernel/trace/rv/rv.c new file +8 -0

+static ssize_t
+enabled_monitors_write(struct file *filp, const char __user *user_buf,
+		      size_t count, loff_t *ppos)
+{
+	char buff[MAX_RV_MONITOR_NAME_SIZE + 2];
+	struct rv_monitor_def *mdef;
+	int retval = -EINVAL;
+	bool enable = true;

Quoted 8 lines

kernel/trace/rv/rv.c line 488

Quoted 4 lines

kernel/trace/rv/rv.c new file +4 -0

+	char *ptr = buff;
+	int len;
+
+	if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE + 2)

@count would not include '\0'. That the max val of @count is MAX_RV_MONITOR_NAME_SIZE+1. So the up bound check of @count is count > MAX_RV_MONITOR_NAME_SIZE + 1.

Fixed for v6...

-- Daniel

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

Cc Wim Van Sebroeck <[email protected]>

Cc Guenter Roeck <[email protected]>

Cc Jonathan Corbet <[email protected]>

Cc Steven Rostedt <[email protected]>

Cc Ingo Molnar <[email protected]>

Cc Thomas Gleixner <[email protected]>

Cc Peter Zijlstra <[email protected]>

Cc Will Deacon <[email protected]>

Cc Catalin Marinas <[email protected]>

Cc Marco Elver <[email protected]>

Cc Dmitry Vyukov <[email protected]>

Cc "Paul E. McKenney" <[email protected]>

Cc Shuah Khan <[email protected]>

Cc Gabriele Paoloni <[email protected]>

Cc Juri Lelli <[email protected]>

Cc Clark Williams <[email protected]>

Cc Tao Zhou <[email protected]>

Cc Randy Dunlap <[email protected]>

Cc [email protected]

Cc [email protected]

Cc [email protected]

Signed-off-by Daniel Bristot de Oliveira <[email protected]>

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

new file mode 100644
index 000000000000..27f48fec5a51

kernel/trace/rv/rv_reactors.c new file +167 -0

@@ -0,0 +1,488 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
+ *
+ * Runtime reactor interface.
+ *
+ * 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.
+ *
+ * == Registering reactors ==
+ *
+ * The struct rv_reactor defines a callback function to be executed
+ * in case of a model exception happens. The callback function
+ * receives a message to be (optionally) printed before executing
+ * the reaction.
+ *
+ * A RV reactor is registered via:
+ *   int rv_register_reactor(struct rv_reactor *reactor)
+ * And unregistered via:
+ *   int rv_unregister_reactor(struct rv_reactor *reactor)
+ *
+ * These functions are exported to modules, enabling reactors to be
+ * dynamically loaded.
+ *
+ * == User interface ==
+ *
+ * The user interface resembles the kernel tracing interface and
+ * presents these files:
+ *
+ *  "available_reactors"
+ *    - List 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 an 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/slab.h>
+
+#include "rv.h"
+
+bool __read_mostly reacting_on;
+
+/*
+ * Interface for the reactor register.
+ */
+LIST_HEAD(rv_reactors_list);
+
+static struct rv_reactor_def *get_reactor_rdef_by_name(char *name)
+{
+	struct rv_reactor_def *r;
+
+	list_for_each_entry(r, &rv_reactors_list, list) {
+		if (strcmp(name, r->reactor->name) == 0)
+			return r;
+	}
+	return NULL;
+}
+
+/*
+ * Available reactors seq functions.
+ */
+static int reactors_show(struct seq_file *m, void *p)
+{
+	struct rv_reactor_def *rea_def = p;
+
+	seq_printf(m, "%s\n", rea_def->reactor->name);
+	return 0;
+}
+
+static void reactors_stop(struct seq_file *m, void *p)
+{
+	mutex_unlock(&rv_interface_lock);
+}
+
+static void *reactors_start(struct seq_file *m, loff_t *pos)
+{
+	mutex_lock(&rv_interface_lock);
+	return seq_list_start(&rv_reactors_list, *pos);
+}
+
+static void *reactors_next(struct seq_file *m, void *p, loff_t *pos)
+{
+	return seq_list_next(p, &rv_reactors_list, pos);
+}
+
+/*
+ * available reactors seq definition.
+ */
+static const struct seq_operations available_reactors_seq_ops = {
+	.start	= reactors_start,
+	.next	= reactors_next,
+	.stop	= reactors_stop,
+	.show	= reactors_show
+};
+
+/*
+ * available_reactors interface.
+ */
+static int available_reactors_open(struct inode *inode, struct file *file)
+{
+	return seq_open(file, &available_reactors_seq_ops);
+};
+
+static const struct file_operations available_reactors_ops = {
+	.open    = available_reactors_open,
+	.read    = seq_read,
+	.llseek  = seq_lseek,
+	.release = seq_release
+};
+
+/*
+ * Monitor reactor file.
+ */
+static int monitor_reactor_show(struct seq_file *m, void *p)
+{
+	struct rv_monitor_def *mdef = m->private;
+	struct rv_reactor_def *rdef = p;
+
+	if (mdef->rdef == rdef)
+		seq_printf(m, "[%s]\n", rdef->reactor->name);
+	else
+		seq_printf(m, "%s\n", rdef->reactor->name);
+	return 0;
+}
+
+/*
+ * available reactors seq definition.
+ */
+static const struct seq_operations monitor_reactors_seq_ops = {
+	.start	= reactors_start,
+	.next	= reactors_next,
+	.stop	= reactors_stop,
+	.show	= monitor_reactor_show
+};
+
+static ssize_t
+monitor_reactors_write(struct file *file, const char __user *user_buf,
+		      size_t count, loff_t *ppos)
+{
+	char buff[MAX_RV_REACTOR_NAME_SIZE + 2];

kernel/trace/rv/rv_reactors.c new file +245 -0

+
+	ptr = strim(buff);
+
+	len = strlen(ptr);
+	if (!len)
+		return count;
+
+	/*
+	 * See monitor_reactors_open()
+	 */
+	seq_f = file->private_data;
+	mdef = seq_f->private;
+
+	mutex_lock(&rv_interface_lock);
+
+	retval = -EINVAL;
+
+	/*
+	 * nop special case: disable reacting.
+	 */
+	if (strcmp(ptr, "nop") == 0) {
+
+		enabled = mdef->monitor->enabled;
+		if (enabled)
+			mdef->monitor->stop();
+
+		mdef->rdef = get_reactor_rdef_by_name("nop");
+		mdef->reacting = false;
+		mdef->monitor->react = NULL;
+
+		if (enabled) {
+			mdef->monitor->start();
+			mdef->monitor->enabled = 1;
+		}
+
+		retval = count;
+		goto unlock;
+	}
+
+	list_for_each_entry(rdef, &rv_reactors_list, list) {
+		if (strcmp(ptr, rdef->reactor->name) != 0)
+			continue;
+
+		/*
+		 * found!
+		 */
+		enabled = mdef->monitor->enabled;
+		if (enabled)
+			mdef->monitor->stop();
+
+		mdef->rdef = rdef;
+		mdef->reacting = true;
+		mdef->monitor->react = rdef->reactor->react;
+
+		if (enabled) {
+			mdef->monitor->start();
+			mdef->monitor->enabled = 1;
+		}
+
+		retval = count;
+		break;
+	}
+
+unlock:
+	mutex_unlock(&rv_interface_lock);
+
+	return retval;
+}
+
+/*
+ * available_reactors interface.
+ */
+static int monitor_reactors_open(struct inode *inode, struct file *file)
+{
+	/*
+	 * create file "private" info is stored in the inode->i_private
+	 */
+	struct rv_monitor_def *mdef = inode->i_private;
+	struct seq_file *seq_f;
+	int ret;
+
+	ret = seq_open(file, &monitor_reactors_seq_ops);
+	if (ret < 0)
+		return ret;
+
+	/*
+	 * seq_open stores the seq_file on the file->private data.
+	 */
+	seq_f = file->private_data;
+
+	/*
+	 * Copy the create file "private" data to the seq_file
+	 * private data.
+	 */
+	seq_f->private = mdef;
+
+	return 0;
+};
+
+static const struct file_operations monitor_reactors_ops = {
+	.open    = monitor_reactors_open,
+	.read    = seq_read,
+	.llseek  = seq_lseek,
+	.release = seq_release,
+	.write = monitor_reactors_write
+};
+
+static int __rv_register_reactor(struct rv_reactor *reactor)
+{
+	struct rv_reactor_def *r;
+
+	list_for_each_entry(r, &rv_reactors_list, list) {
+		if (strcmp(reactor->name, r->reactor->name) == 0) {
+			pr_info("Reactor %s is already registered\n",
+				reactor->name);
+			return -EINVAL;
+		}
+	}
+
+	r = kzalloc(sizeof(struct rv_reactor_def), GFP_KERNEL);
+	if (!r)
+		return -ENOMEM;
+
+	r->reactor = reactor;
+	r->counter = 0;
+
+	list_add_tail(&r->list, &rv_reactors_list);
+
+	return 0;
+}
+
+/**
+ * rv_register_reactor - register a rv reactor.
+ * @reactor:    The rv_reactor to be registered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_register_reactor(struct rv_reactor *reactor)
+{
+	int retval = 0;
+
+	if (strlen(reactor->name) >= MAX_RV_REACTOR_NAME_SIZE) {
+		pr_info("Reactor %s has a name longer than %d\n",
+			reactor->name, MAX_RV_MONITOR_NAME_SIZE);
+		return -EINVAL;
+	}
+
+	mutex_lock(&rv_interface_lock);
+	retval = __rv_register_reactor(reactor);
+	mutex_unlock(&rv_interface_lock);
+	return retval;
+}
+
+/**
+ * rv_unregister_reactor - unregister a rv reactor.
+ * @reactor:    The rv_reactor to be unregistered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_unregister_reactor(struct rv_reactor *reactor)
+{
+	struct rv_reactor_def *ptr, *next;
+
+	mutex_lock(&rv_interface_lock);
+
+	list_for_each_entry_safe(ptr, next, &rv_reactors_list, list) {
+		if (strcmp(reactor->name, ptr->reactor->name) == 0) {
+
+			if (!ptr->counter) {
+				list_del(&ptr->list);
+			} else {
+				printk(KERN_WARNING
+				       "rv: the rv_reactor %s is in use by %d monitor(s)\n",
+				       ptr->reactor->name, ptr->counter);
+				printk(KERN_WARNING "rv: the rv_reactor %s cannot be removed\n",
+				       ptr->reactor->name);
+				return -EBUSY;
+			}
+
+		}
+	}
+
+	mutex_unlock(&rv_interface_lock);
+	return 0;
+}
+
+/*
+ * reacting_on interface.
+ */
+static ssize_t reacting_on_read_data(struct file *filp,
+				     char __user *user_buf,
+				     size_t count, loff_t *ppos)
+{
+	char *buff;
+
+	mutex_lock(&rv_interface_lock);
+	buff = reacting_on ? "1\n" : "0\n";
+	mutex_unlock(&rv_interface_lock);
+
+	return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff)+1);
+}
+
+static void turn_reacting_off(void)
+{
+	reacting_on = false;
+}
+
+static void turn_reacting_on(void)
+{
+	reacting_on = true;
+}
+
+static ssize_t
+reacting_on_write_data(struct file *filp, const char __user *user_buf,
+		       size_t count, loff_t *ppos)
+{
+	int retval;
+	bool val;
+
+	retval = kstrtobool_from_user(user_buf, count, &val);
+	if (retval)
+		return retval;
+
+	mutex_lock(&rv_interface_lock);
+
+	if (val)
+		turn_reacting_on();
+	else
+		turn_reacting_off();
+
+	mutex_unlock(&rv_interface_lock);
+
+	return count;
+}
+
+static const struct file_operations reacting_on_fops = {
+	.open   = simple_open,
+	.llseek = no_llseek,
+	.write  = reacting_on_write_data,
+	.read   = reacting_on_read_data,
+};
+
+int reactor_create_monitor_files(struct rv_monitor_def *mdef)
+{
+	struct dentry *tmp;

kernel/trace/rv/rv_reactors.c new file +49 -0

+
+	return 0;
+}
+
+/*
+ * None reactor register
+ */
+static void rv_nop_reaction(char *msg)
+{
+}
+
+struct rv_reactor rv_nop = {
+	.name = "nop",
+	.description = "no-operation reactor: do nothing.",
+	.react = rv_nop_reaction
+};
+
+/*
+ * This section collects the rv/ root dir files and folders.
+ */
+int init_rv_reactors(struct dentry *root_dir)
+{
+	struct dentry *available, *reacting;
+	int retval;
+
+	available = rv_create_file("available_reactors", RV_MODE_READ, root_dir, NULL,
+				   &available_reactors_ops);
+	if (!available)
+		goto out_err;
+
+	reacting = rv_create_file("reacting_on", RV_MODE_WRITE, root_dir, NULL, &reacting_on_fops);
+	if (!reacting)
+		goto rm_available;
+
+	retval = __rv_register_reactor(&rv_nop);
+	if (retval)
+		goto rm_reacting;
+
+	reacting_on = 1;
+
+	return 0;
+
+rm_reacting:
+	rv_remove(reacting);
+rm_available:
+	rv_remove(available);
+out_err:
+	return -ENOMEM;
+}

Signature · 1 line

2.35.1

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.

Cc Wim Van Sebroeck <[email protected]>

Cc Guenter Roeck <[email protected]>

Cc Jonathan Corbet <[email protected]>

Cc Steven Rostedt <[email protected]>

Cc Ingo Molnar <[email protected]>

Cc Thomas Gleixner <[email protected]>

Cc Peter Zijlstra <[email protected]>

Cc Will Deacon <[email protected]>

Cc Catalin Marinas <[email protected]>

Cc Marco Elver <[email protected]>

Cc Dmitry Vyukov <[email protected]>

Cc "Paul E. McKenney" <[email protected]>

Cc Shuah Khan <[email protected]>

Cc Gabriele Paoloni <[email protected]>

Cc Juri Lelli <[email protected]>

Cc Clark Williams <[email protected]>

Cc Tao Zhou <[email protected]>

Cc Randy Dunlap <[email protected]>

Cc [email protected]

Cc [email protected]

Cc [email protected]

Signed-off-by Daniel Bristot de Oliveira <[email protected]>

---
 include/linux/rv.h        |   2 +
 include/rv/da_monitor.h   | 521 ++++++++++++++++++++++++++++++++++++++
 include/rv/rv.h           |   9 +
 include/trace/events/rv.h | 120 +++++++++
 kernel/fork.c             |  14 +
 kernel/trace/rv/Kconfig   |  14 +
 kernel/trace/rv/rv.c      |   5 +
 7 files changed, 685 insertions(+)
 create mode 100644 include/rv/da_monitor.h
 create mode 100644 include/trace/events/rv.h

include/linux/rv.h +2 -0

index 88d28d207f3a..bdefdff12a1f 100644
@@ -7,6 +7,8 @@
 #ifndef _LINUX_RV_H
 #define _LINUX_RV_H
 
+#define MAX_DA_NAME_LEN         24
+
 struct rv_reactor {
 	char			*name;
 	char			*description;

include/rv/da_monitor.h new file +245 -0

new file mode 100644
index 000000000000..d21045e6c5fc
@@ -0,0 +1,521 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
+ *
+ * Deterministic automata (DA) monitor functions, to be used together
+ * with automata models in C generated by the dot2k tool.
+ *
+ * The dot2k tool is available at tools/verification/dot2k/
+ */
+
+#include <rv/automata.h>
+#include <linux/rv.h>
+
+/*
+ * 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",	\
+		 #name,								\
+		 model_get_event_name_##name(event),				\
+		 model_get_state_name_##name(curr_state));			\
+	return REACT_MSG;							\
+}										\
+										\
+static void cond_react(char *msg)						\
+{										\
+	if (rv_##name.react)							\
+		rv_##name.react(msg);						\
+}										\
+										\
+/*										\
+ * da_monitor_reset_##name - reset a monitor and setting it to init state	\
+ */										\
+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();			\
+}										\
+										\
+/*										\
+ * da_monitor_curr_state_##name - return the current state			\
+ */										\
+static inline type da_monitor_curr_state_##name(struct da_monitor *da_mon)	\
+{										\
+	return da_mon->curr_state;						\
+}										\
+										\
+/*										\
+ * da_monitor_set_state_##name - set the new current state			\
+ */										\
+static inline void								\
+da_monitor_set_state_##name(struct da_monitor *da_mon, enum states_##name state)\
+{										\
+	da_mon->curr_state = state;						\
+}										\
+										\
+/*										\
+ * da_monitor_start_##name - start monitoring					\
+ *										\
+ * The monitor will ignore all events until monitoring is set to true. This	\
+ * function needs to be called to tell the monitor to start monitoring.		\
+ */										\
+static inline void da_monitor_start_##name(struct da_monitor *da_mon)		\
+{										\
+	da_mon->monitoring = 1;							\
+}										\
+										\
+/*										\
+ * da_monitoring_##name - returns true if the monitor is processing events	\
+ */										\
+static inline bool da_monitoring_##name(struct da_monitor *da_mon)		\
+{										\
+	return da_mon->monitoring;						\
+}
+
+
+/*
+ * Event handler for implicit monitors. Implicit monitor is the one which the
+ * handler does not need to specify which da_monitor to manipulate. Examples
+ * of implicit monitor are the per_cpu or the global ones.
+ */
+#define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)			\
+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 != INVALID_STATE) {					\
+		da_monitor_set_state_##name(da_mon, next_state);		\
+										\
+		trace_event_##name(model_get_state_name_##name(curr_state),	\
+				model_get_event_name_##name(event),		\
+				model_get_state_name_##name(next_state),	\
+				model_is_final_state_##name(next_state));	\
+										\
+		return true;							\
+	}									\
+										\
+	if (reacting_on)							\
+		cond_react(format_react_msg(curr_state, event));		\
+										\
+	trace_error_##name(model_get_state_name_##name(curr_state),		\
+			   model_get_event_name_##name(event));			\
+										\
+	return false;								\
+}										\
+
+/*
+ * Event handler for per_task monitors.
+ */
+#define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)			\
+static inline type								\
+da_event_##name(struct da_monitor *da_mon, struct task_struct *tsk,		\
+		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 != INVALID_STATE) {					\
+		da_monitor_set_state_##name(da_mon, next_state);		\
+										\
+		trace_event_##name(tsk->pid,					\
+				   model_get_state_name_##name(curr_state),	\
+				   model_get_event_name_##name(event),		\
+				   model_get_state_name_##name(next_state),	\
+				   model_is_final_state_##name(next_state));	\
+										\
+		return true;							\
+	}									\
+										\
+	if (reacting_on)							\
+		cond_react(format_react_msg(curr_state, event));		\
+										\
+	trace_error_##name(tsk->pid,						\
+			   model_get_state_name_##name(curr_state),		\
+			   model_get_event_name_##name(event));			\
+										\
+	return false;								\
+}
+
+/*
+ * Functions to define, init and get a global monitor.
+ */
+#define DECLARE_DA_MON_INIT_GLOBAL(name, type)					\
+										\
+/*										\
+ * global monitor (a single variable)						\
+ */										\
+static struct da_monitor da_mon_##name;						\
+										\
+/*										\
+ * da_get_monitor_##name - return the global monitor address			\
+ */										\
+static struct da_monitor *da_get_monitor_##name(void)				\
+{										\
+	return &da_mon_##name;							\
+}										\
+										\
+/*										\
+ * da_monitor_reset_all_##name - reset the single monitor			\
+ */										\
+static void da_monitor_reset_all_##name(void)					\
+{										\
+	da_monitor_reset_##name(&da_mon_##name);				\
+}										\
+										\
+/*										\
+ * da_monitor_init_##name - initialize a monitor				\
+ */										\
+static inline int da_monitor_init_##name(void)					\
+{										\
+	struct da_monitor *da_mon = &da_mon_##name;				\
+	da_mon->curr_state = model_get_init_state_##name();			\
+	da_mon->monitoring = 0;							\
+	return 0;								\
+}										\
+										\
+/*										\
+ * da_monitor_destroy_##name - destroy the monitor				\
+ */										\
+static inline void da_monitor_destroy_##name(void)				\
+{										\
+	return;									\
+}
+
+/*
+ * Functions to define, init and get a per-cpu monitor.
+ */
+#define DECLARE_DA_MON_INIT_PER_CPU(name, type)					\
+										\
+/*										\
+ * per-cpu monitor variables							\
+ */										\
+DEFINE_PER_CPU(struct da_monitor, da_mon_##name);				\
+										\
+/*										\
+ * da_get_monitor_##name - return current CPU monitor address			\
+ */										\
+static struct da_monitor *da_get_monitor_##name(void)				\
+{										\
+	return this_cpu_ptr(&da_mon_##name);					\
+}										\
+										\
+/*										\
+ * da_monitor_reset_all_##name - reset all CPUs' monitor			\
+ */										\
+static 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);				\
+	}									\
+}										\
+										\
+/*										\
+ * da_monitor_init_##name - initialize all CPUs' monitor			\
+ */										\
+static inline int 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;						\
+	}									\
+	return 0;								\
+}										\
+										\
+/*										\
+ * da_monitor_destroy_##name - destroy the monitor				\
+ */										\
+static inline void da_monitor_destroy_##name(void)				\
+{										\
+	return;									\
+}
+

Quoted 1 line

+static int task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT; \

In patch1, RV_PER_TASK_MONITOR_INIT is defined as:

#define RV_PER_TASK_MONITORS 1
#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS)

RV_PER_TASK_MONITOR_INIT is 1 now, seems not the index of the first only element in vector. Now no map here, one task has one monitor though if I am not wrong.
So task_mon_slot_##name must be defined to the index of first element. Modify the macro definition of RV_PER_TASK_MONITOR_INIT to the index of first element in vector.

#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS) - 1

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

Cc Wim Van Sebroeck <[email protected]>

Cc Guenter Roeck <[email protected]>

Cc Jonathan Corbet <[email protected]>

Cc Steven Rostedt <[email protected]>

Cc Ingo Molnar <[email protected]>

Cc Thomas Gleixner <[email protected]>

Cc Peter Zijlstra <[email protected]>

Cc Will Deacon <[email protected]>

Cc Catalin Marinas <[email protected]>

Cc Marco Elver <[email protected]>

Cc Dmitry Vyukov <[email protected]>

Cc "Paul E. McKenney" <[email protected]>

Cc Shuah Khan <[email protected]>

Cc Gabriele Paoloni <[email protected]>

Cc Juri Lelli <[email protected]>

Cc Clark Williams <[email protected]>

Cc Tao Zhou <[email protected]>

Cc Randy Dunlap <[email protected]>

Cc [email protected]

Cc [email protected]

Cc [email protected]

Signed-off-by Daniel Bristot de Oliveira <[email protected]>

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

+ runtime-verification.rst

Documentation/trace/rv/runtime-verification.rst new file +24 -0

+The user interface
+==================
+
+The user interface resembles the tracing interface (on purpose). It is
+currently at "/sys/kernel/tracing/rv/".
+
+The following files/folders are currently available:
+
+**available_monitors**
+
+- Reading list the available monitors, one per line
+
+For example::
+
+   # cat available_monitors
+   wip
+   wwnr
+
+**available_reactors**
+
+- Reading shows the available reactors, one per line.
+
+For example::
+

+- Truncating the file disables all enabled monitors

Documentation/trace/rv/runtime-verification.rst new file +26 -0

+
+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 it is possible to enable more than one monitor concurrently.
+
+
+**monitoring_on**
+
+This is an on/off general switcher for monitoring. It resembles the
+"tracing_on" switcher in the trace interface.
+
+- Writing "0" stops the monitoring
+- Writing "1" continues the monitoring

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

Cc Wim Van Sebroeck <[email protected]>

Cc Guenter Roeck <[email protected]>

Cc Jonathan Corbet <[email protected]>

Cc Steven Rostedt <[email protected]>

Cc Ingo Molnar <[email protected]>

Cc Thomas Gleixner <[email protected]>

Cc Peter Zijlstra <[email protected]>

Cc Will Deacon <[email protected]>

Cc Catalin Marinas <[email protected]>

Cc Marco Elver <[email protected]>

Cc Dmitry Vyukov <[email protected]>

Cc "Paul E. McKenney" <[email protected]>

Cc Shuah Khan <[email protected]>

Cc Gabriele Paoloni <[email protected]>

Cc Juri Lelli <[email protected]>

Cc Clark Williams <[email protected]>

Cc Tao Zhou <[email protected]>

Cc Randy Dunlap <[email protected]>

Cc [email protected]

Cc [email protected]

Cc [email protected]

Signed-off-by Daniel Bristot de Oliveira <[email protected]>

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

Documentation/trace/rv/da_monitor_instrumentation.rst new file +84 -0

new file mode 100644
index 000000000000..7b83d6c7dbed
@@ -0,0 +1,169 @@
+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 start_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.