From patchwork Thu Jun 16 08:44:43 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883550 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 788A3C43334 for ; Thu, 16 Jun 2022 08:45:25 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231386AbiFPIpY (ORCPT ); Thu, 16 Jun 2022 04:45:24 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34220 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229436AbiFPIpW (ORCPT ); Thu, 16 Jun 2022 04:45:22 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id A24C35D1B3; Thu, 16 Jun 2022 01:45:20 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 1A96C61D7B; Thu, 16 Jun 2022 08:45:20 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id C9BD4C341C0; Thu, 16 Jun 2022 08:45:14 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369119; bh=7rF47gmADnP3lrfwS6uOhVYx6Pwu32doN7Yn8DdVMdA=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=OkQ5FAkwruk0MvCv9hLQ1a3jTs3kYydnjo+r8+2J4Op2G0WkrPYiP4IAixZRwj00b E1C2j0b1AWi6DRvL0mwEPWEwjJ8F3m71NVukLiwsorcfXAiiVdX2WYrq+3KmtHxFCa Z/Ig0T9o9W/Tu8vtNoB/52GBlI0RY8cfGz6tLymPdoFPd7G7zNpVorlGXzFr5UEjkh F4z50MDe0PS+wRMQg6GHmBce3mAhBmszHAApzaUfM3pcAx1vxbrmqHhPvX0/kdWK/A sf9w0+If2+Z3XqI/EJ8IUCmDy/cse3JzwblX+DZS0nMFKGDSD2es9Q0DuWm4SlxRLx MjRVvUDspwPMg== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 01/20] rv: Add Runtime Verification (RV) interface Date: Thu, 16 Jun 2022 10:44:43 +0200 Message-Id: <60548902dbccaa7ba420e40e46835693e27f643f.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org 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. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- include/linux/rv.h | 23 ++ include/linux/sched.h | 11 + include/rv/rv.h | 23 ++ kernel/fork.c | 14 + kernel/trace/Kconfig | 2 + kernel/trace/Makefile | 2 + kernel/trace/rv/Kconfig | 12 + kernel/trace/rv/Makefile | 3 + kernel/trace/rv/rv.c | 738 +++++++++++++++++++++++++++++++++++++++ kernel/trace/rv/rv.h | 34 ++ kernel/trace/trace.c | 4 + kernel/trace/trace.h | 2 + 12 files changed, 868 insertions(+) create mode 100644 include/linux/rv.h create mode 100644 include/rv/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 diff --git a/include/linux/rv.h b/include/linux/rv.h new file mode 100644 index 000000000000..205e65f57637 --- /dev/null +++ b/include/linux/rv.h @@ -0,0 +1,23 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Runtime Verification. + * + * For futher information, see: kernel/trace/rv/rv.c. + * + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira + */ +#ifndef _LINUX_RV_H +#define _LINUX_RV_H +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); +#endif /* _LINUX_RV_H */ diff --git a/include/linux/sched.h b/include/linux/sched.h index c46f3a63b758..b037f364efdc 100644 --- a/include/linux/sched.h +++ b/include/linux/sched.h @@ -35,6 +35,7 @@ #include #include #include +#include /* task_struct member predeclarations (sorted alphabetically): */ struct audit_context; @@ -1500,6 +1501,16 @@ struct task_struct { struct callback_head l1d_flush_kill; #endif +#ifdef CONFIG_RV + /* + * Per-task RV monitor. Nowadays fixed in RV_PER_TASK_MONITORS. + * If we find justification for more monitors, we can think + * about adding more or developing a dynamic method. So far, + * none of these are justified. + */ + union rv_task_monitor rv[RV_PER_TASK_MONITORS]; +#endif + /* * New fields for task_struct should be added above here, so that * they are included in the randomized portion of task_struct. diff --git a/include/rv/rv.h b/include/rv/rv.h new file mode 100644 index 000000000000..27a108881d35 --- /dev/null +++ b/include/rv/rv.h @@ -0,0 +1,23 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +#ifndef _RV_RV_H +#define _RV_RV_H + +/* + * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS. + * If we find justification for more monitors, we can think about + * adding more or developing a dynamic method. So far, none of + * these are justified. + */ +#define RV_PER_TASK_MONITORS 1 +#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS) + +/* + * Futher monitor types are expected, so make this a union. + */ +union rv_task_monitor { +}; + +int get_task_monitor_slot(void); +void put_task_monitor_slot(int slot); +#endif /* _RV_RV_H */ diff --git a/kernel/fork.c b/kernel/fork.c index 9d44f2d46c69..5e40e58ef83d 100644 --- a/kernel/fork.c +++ b/kernel/fork.c @@ -1964,6 +1964,18 @@ static void copy_oom_score_adj(u64 clone_flags, struct task_struct *tsk) mutex_unlock(&oom_adj_mutex); } +#ifdef CONFIG_RV +static void rv_task_fork(struct task_struct *p) +{ + int i; + + for (i = 0; i < RV_PER_TASK_MONITORS; i++) + ; +} +#else +#define rv_task_fork(p) do {} while (0) +#endif + /* * This creates a new process as a copy of the old one, * but does not actually start it yet. @@ -2399,6 +2411,8 @@ static __latent_entropy struct task_struct *copy_process( */ copy_seccomp(p); + rv_task_fork(p); + rseq_fork(p, clone_flags); /* Don't start children in a dying pid namespace */ diff --git a/kernel/trace/Kconfig b/kernel/trace/Kconfig index debbbb083286..b415690748bf 100644 --- a/kernel/trace/Kconfig +++ b/kernel/trace/Kconfig @@ -1105,4 +1105,6 @@ config HIST_TRIGGERS_DEBUG If unsure, say N. +source "kernel/trace/rv/Kconfig" + endif # FTRACE diff --git a/kernel/trace/Makefile b/kernel/trace/Makefile index 0d261774d6f3..b2670fff6e94 100644 --- a/kernel/trace/Makefile +++ b/kernel/trace/Makefile @@ -108,3 +108,5 @@ obj-$(CONFIG_RETHOOK) += rethook.o obj-$(CONFIG_TRACEPOINT_BENCHMARK) += trace_benchmark.o libftrace-y := ftrace.o + +obj-$(CONFIG_RV) += rv/ diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig new file mode 100644 index 000000000000..6d127cdb00dd --- /dev/null +++ b/kernel/trace/rv/Kconfig @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +menuconfig RV + bool "Runtime Verification" + depends on TRACING + help + Enable the kernel runtime verification infrastructure. RV is a + lightweight (yet rigorous) method that complements classical + exhaustive verification techniques (such as model checking and + theorem proving). RV works by analyzing the trace of the system's + actual execution, comparing it against a formal specification of + the system behavior. diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile new file mode 100644 index 000000000000..fd995379df67 --- /dev/null +++ b/kernel/trace/rv/Makefile @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: GPL-2.0 + +obj-$(CONFIG_RV) += rv.o diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c new file mode 100644 index 000000000000..43af7b13187e --- /dev/null +++ b/kernel/trace/rv/rv.c @@ -0,0 +1,738 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * This is the online Runtime Verification (RV) interface. + * + * 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. + * + * == Runtime monitor interface == + * + * A monitor is the central part of the runtime verification of a system. + * + * The monitor stands in between the formal specification of the desired + * (or undesired) behavior, and the trace of the actual system. + * + * In Linux terms, the runtime verification monitors are encapsulated + * inside the "RV monitor" abstraction. A RV monitor includes a reference + * model of the system, a set of instances of the monitor (per-cpu monitor, + * per-task monitor, and so on), and the helper functions that glue the + * monitor to the system via trace. Generally, a monitor includes some form + * of trace output as a reaction for event parsing and exceptions, + * as depicted bellow: + * + * Linux +----- RV Monitor ----------------------------------+ Formal + * Realm | | Realm + * +-------------------+ +----------------+ +-----------------+ + * | Linux kernel | | Monitor | | Reference | + * | Tracing | -> | Instance(s) | <- | Model | + * | (instrumentation) | | (verification) | | (specification) | + * +-------------------+ +----------------+ +-----------------+ + * | | | + * | V | + * | +----------+ | + * | | Reaction | | + * | +--+--+--+-+ | + * | | | | | + * | | | +-> trace output ? | + * +------------------------|--|----------------------+ + * | +----> panic ? + * +-------> + * + * This file implements the interface for loading RV monitors, and + * to control the verification session. + * + * == Registering monitors == + * + * The struct rv_monitor defines a set of callback functions to control + * a verification session. For instance, when a given monitor is enabled, + * the "start" callback function is called to hook the instrumentation + * functions to the kernel trace events. The "stop" function is called + * when disabling the verification session. + * + * A RV monitor is registered via: + * int rv_register_monitor(struct rv_monitor *monitor); + * And unregistered via: + * int rv_unregister_monitor(struct rv_monitor *monitor); + * + * These functions are exported to modules, enabling verification monitors + * to be dynamically loaded. + * + * == User interface == + * + * The user interface resembles kernel tracing interface. 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 + * + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira + */ + +#include +#include +#include +#include +#include + +#include "rv.h" + +DEFINE_MUTEX(rv_interface_lock); +struct rv_interface rv_root; + +struct dentry *get_monitors_root(void) +{ + return rv_root.monitors_dir; +} + +/* + * Monitoring on global switcher! + */ +bool __read_mostly monitoring_on; + +/* + * Interface for the monitor register. + */ +LIST_HEAD(rv_monitors_list); + +static int task_monitor_count; +static bool task_monitor_slots[RV_PER_TASK_MONITORS]; + +int get_task_monitor_slot(void) +{ + int i; + + lockdep_assert_held(&rv_interface_lock); + + if (task_monitor_count == RV_PER_TASK_MONITORS) + return -EBUSY; + + task_monitor_count++; + + for (i = 0; i < RV_PER_TASK_MONITORS; i++) { + if (task_monitor_slots[i] == false) { + task_monitor_slots[i] = true; + return i; + } + } + + WARN_ONCE(1, "RV task_monitor_cout and slots are out of sync\n"); + + return -EINVAL; +} + +void put_task_monitor_slot(int slot) +{ + lockdep_assert_held(&rv_interface_lock); + + if (slot < 0 || slot > RV_PER_TASK_MONITORS) { + WARN_ONCE(1, "RV releasing an invlid slot!: %d\n", slot); + return; + } + + WARN_ONCE(!task_monitor_slots[slot], "RV releasing unsused task_monitor_slots: %d\n", + slot); + + task_monitor_count--; + task_monitor_slots[slot] = false; +} + +/* + * This section collects the monitor/ files and folders. + */ +static ssize_t monitor_enable_read_data(struct file *filp, + char __user *user_buf, + size_t count, loff_t *ppos) +{ + struct rv_monitor_def *mdef = filp->private_data; + char buff[4]; + + memset(buff, 0, sizeof(buff)); + + mutex_lock(&rv_interface_lock); + sprintf(buff, "%x\n", mdef->monitor->enabled); + mutex_unlock(&rv_interface_lock); + + return simple_read_from_buffer(user_buf, count, ppos, + buff, strlen(buff)+1); +} + +/* + * Disable a given runtime monitor. + */ +static int disable_monitor(struct rv_monitor_def *mdef) +{ + if (mdef->monitor->enabled) { + mdef->monitor->enabled = 0; + mdef->monitor->stop(); + } + + mdef->enabled = 0; + return 0; +} + +/* + * Enable a given monitor. + */ +static int enable_monitor(struct rv_monitor_def *mdef) +{ + int retval; + + /* + * Reset all internal monitors before starting. + */ + mdef->monitor->reset(); + if (!mdef->monitor->enabled) { + retval = mdef->monitor->start(); + if (retval) + return retval; + } + + mdef->monitor->enabled = 1; + mdef->enabled = 1; + + return 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; + u64 val; + + retval = kstrtoull_from_user(user_buf, count, 10, &val); + if (retval) + return retval; + + retval = count; + + mutex_lock(&rv_interface_lock); + + switch (val) { + case 0: + retval = disable_monitor(mdef); + break; + case 1: + retval = enable_monitor(mdef); + break; + default: + retval = -EINVAL; + } + + mutex_unlock(&rv_interface_lock); + + return retval; +} + +static const struct file_operations interface_enable_fops = { + .open = simple_open, + .llseek = no_llseek, + .write = monitor_enable_write_data, + .read = monitor_enable_read_data, +}; + +/* + * Interface to read the enable/disable status of a monitor. + */ +static ssize_t +monitor_desc_read_data(struct file *filp, char __user *user_buf, + size_t count, loff_t *ppos) +{ + struct rv_monitor_def *mdef = filp->private_data; + char buf[MAX_RV_MONITOR_NAME_SIZE]; + + memset(buf, 0, sizeof(buf)); + + mutex_lock(&rv_interface_lock); + sprintf(buf, "%s\n", mdef->monitor->description); + mutex_unlock(&rv_interface_lock); + + return simple_read_from_buffer(user_buf, count, ppos, + buf, strlen(buf)+1); +} + +static const struct file_operations interface_desc_fops = { + .open = simple_open, + .llseek = no_llseek, + .read = monitor_desc_read_data, +}; + +/* + * During the registration of a monitor, this function creates + * the monitor dir, where the specific options of the monitor + * is exposed. + */ +static int create_monitor_dir(struct rv_monitor_def *mdef) +{ + struct dentry *root = get_monitors_root(); + struct dentry *tmp; + const char *name = mdef->monitor->name; + int retval = 0; + + mdef->root_d = rv_create_dir(name, root); + + if (!mdef->root_d) + return -ENOMEM; + + tmp = rv_create_file("enable", 0600, + mdef->root_d, mdef, + &interface_enable_fops); + if (!tmp) { + retval = -ENOMEM; + goto out_remove_root; + } + + tmp = rv_create_file("desc", 0400, + mdef->root_d, mdef, + &interface_desc_fops); + if (!tmp) { + retval = -ENOMEM; + goto out_remove_root; + } + + return retval; + +out_remove_root: + rv_remove(mdef->root_d); + return retval; +} + +/* + * Available/Enable monitor shared seq functions. + */ +static int monitors_show(struct seq_file *m, void *p) +{ + struct rv_monitor_def *mon_def = p; + + seq_printf(m, "%s\n", mon_def->monitor->name); + return 0; +} + +/* + * Used by the seq file operations at the end of a read + * operation. + */ +static void monitors_stop(struct seq_file *m, void *p) +{ + mutex_unlock(&rv_interface_lock); +} + +/* + * Available monitor seq functions: + */ +static void *available_monitors_start(struct seq_file *m, loff_t *pos) +{ + mutex_lock(&rv_interface_lock); + return seq_list_start(&rv_monitors_list, *pos); +} + +static void *available_monitors_next(struct seq_file *m, void *p, loff_t *pos) +{ + return seq_list_next(p, &rv_monitors_list, pos); +} + +/* + * Enable monitor seq functions: + */ + +static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos) +{ + struct rv_monitor_def *m_def = p; + + (*pos)++; + + list_for_each_entry_continue(m_def, &rv_monitors_list, list) { + if (m_def->monitor->enabled) + return m_def; + } + + return NULL; +} + +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); + 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; + } + + return m_def; +} + +/* + * available/enabled monitors seq definition. + */ +static const struct seq_operations available_monitors_seq_ops = { + .start = available_monitors_start, + .next = available_monitors_next, + .stop = monitors_stop, + .show = monitors_show +}; + +static const struct seq_operations enabled_monitors_seq_ops = { + .start = enabled_monitors_start, + .next = enabled_monitors_next, + .stop = monitors_stop, + .show = monitors_show +}; + +/* + * available_monitors interface. + */ +static int available_monitors_open(struct inode *inode, struct file *file) +{ + return seq_open(file, &available_monitors_seq_ops); +}; + +static const struct file_operations available_monitors_ops = { + .open = available_monitors_open, + .read = seq_read, + .llseek = seq_lseek, + .release = seq_release +}; + +/* + * enabled_monitors interface + */ +static void disable_all_monitors(void) +{ + struct rv_monitor_def *mdef; + + list_for_each_entry(mdef, &rv_monitors_list, list) + disable_monitor(mdef); +} + +static int enabled_monitors_open(struct inode *inode, struct file *file) +{ + if ((file->f_mode & FMODE_WRITE) && (file->f_flags & O_TRUNC)) + disable_all_monitors(); + + return seq_open(file, &enabled_monitors_seq_ops); +}; + +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+1]; + struct rv_monitor_def *mdef; + int retval = -EINVAL; + bool enable = true; + char *ptr = buff; + int len; + + if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE+1) + return -EINVAL; + + memset(buff, 0, sizeof(buff)); + + retval = simple_write_to_buffer(buff, sizeof(buff)-1, ppos, user_buf, + count); + if (!retval) + return -EFAULT; + + if (buff[0] == '!') { + enable = false; + ptr++; + } + + len = strlen(ptr); + if (!len) + return count; + /* + * remove \n + */ + ptr[len-1] = '\0'; + + mutex_lock(&rv_interface_lock); + + retval = -EINVAL; + + list_for_each_entry(mdef, &rv_monitors_list, list) { + if (strcmp(ptr, mdef->monitor->name) == 0) { + /* + * Monitor found! + */ + if (enable) + retval = enable_monitor(mdef); + else + retval = disable_monitor(mdef); + + if (retval) + goto out; + + /* + * Success! + */ + retval = count; + break; + } + } + +out: + mutex_unlock(&rv_interface_lock); + return retval; +} + +static const struct file_operations enabled_monitors_ops = { + .open = enabled_monitors_open, + .read = seq_read, + .write = enabled_monitors_write, + .llseek = seq_lseek, + .release = seq_release, +}; + +/* + * monitoring_on general switcher + */ +static ssize_t monitoring_on_read_data(struct file *filp, + char __user *user_buf, + size_t count, loff_t *ppos) +{ + char buff[4]; + + memset(buff, 0, sizeof(buff)); + + mutex_lock(&rv_interface_lock); + sprintf(buff, "%d\n", monitoring_on); + mutex_unlock(&rv_interface_lock); + + return simple_read_from_buffer(user_buf, count, ppos, + buff, strlen(buff)+1); +} + +static void turn_monitoring_off(void) +{ + monitoring_on = false; +} + +static void turn_monitoring_on(void) +{ + reset_all_monitors(); + monitoring_on = true; +} + +static ssize_t monitoring_on_write_data(struct file *filp, + const char __user *user_buf, + size_t count, loff_t *ppos) +{ + int retval; + u64 val; + + retval = kstrtoull_from_user(user_buf, count, 10, &val); + if (retval) + return retval; + + retval = count; + + mutex_lock(&rv_interface_lock); + + switch (val) { + case 0: + turn_monitoring_off(); + break; + case 1: + turn_monitoring_on(); + break; + default: + retval = -EINVAL; + } + + mutex_unlock(&rv_interface_lock); + + return retval; +} + +static const struct file_operations monitoring_on_fops = { + .open = simple_open, + .llseek = no_llseek, + .write = monitoring_on_write_data, + .read = monitoring_on_read_data, +}; + +/* + * Monitor API. + */ +static void destroy_monitor_dir(struct rv_monitor_def *mdef) +{ + rv_remove(mdef->root_d); +} + +/** + * rv_register_monitor - register a rv monitor. + * @monitor: The rv_monitor to be registered. + * + * Returns 0 if successful, error otherwise. + */ +int rv_register_monitor(struct rv_monitor *monitor) +{ + struct rv_monitor_def *r; + int retval = 0; + + if (strlen(monitor->name) >= MAX_RV_MONITOR_NAME_SIZE) { + pr_info("Monitor %s has a name longer than %d\n", + monitor->name, MAX_RV_MONITOR_NAME_SIZE); + return -1; + } + + mutex_lock(&rv_interface_lock); + + list_for_each_entry(r, &rv_monitors_list, list) { + if (strcmp(monitor->name, r->monitor->name) == 0) { + pr_info("Monitor %s is already registered\n", + monitor->name); + retval = -1; + goto out_unlock; + } + } + + r = kzalloc(sizeof(struct rv_monitor_def), GFP_KERNEL); + if (!r) { + retval = -ENOMEM; + goto out_unlock; + } + + r->monitor = monitor; + + create_monitor_dir(r); + + list_add_tail(&r->list, &rv_monitors_list); + +out_unlock: + mutex_unlock(&rv_interface_lock); + return retval; +} + +/** + * rv_unregister_monitor - unregister a rv monitor. + * @monitor: The rv_monitor to be unregistered. + * + * Returns 0 if successful, error otherwise. + */ +int rv_unregister_monitor(struct rv_monitor *monitor) +{ + struct rv_monitor_def *ptr, *next; + + mutex_lock(&rv_interface_lock); + + list_for_each_entry_safe(ptr, next, &rv_monitors_list, list) { + if (strcmp(monitor->name, ptr->monitor->name) == 0) { + list_del(&ptr->list); + destroy_monitor_dir(ptr); + } + } + + mutex_unlock(&rv_interface_lock); + return 0; +} + +void reset_all_monitors(void) +{ + struct rv_monitor_def *mdef; + + /* + * Reset all monitors before re-enabling monitoring. + */ + list_for_each_entry(mdef, &rv_monitors_list, list) { + if (mdef->monitor->enabled) + mdef->monitor->reset(); + } + +} + +int __init rv_init_interface(void) +{ + rv_root.root_dir = rv_create_dir("rv", NULL); + rv_root.monitors_dir = rv_create_dir("monitors", rv_root.root_dir); + + rv_create_file("available_monitors", 0400, rv_root.root_dir, NULL, + &available_monitors_ops); + rv_create_file("enabled_monitors", 0600, rv_root.root_dir, NULL, + &enabled_monitors_ops); + rv_create_file("monitoring_on", 0600, rv_root.root_dir, NULL, + &monitoring_on_fops); + + monitoring_on = true; + + return 0; +} diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h new file mode 100644 index 000000000000..0796867a7b1e --- /dev/null +++ b/kernel/trace/rv/rv.h @@ -0,0 +1,34 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +#include + +struct rv_interface { + struct dentry *root_dir; + struct dentry *monitors_dir; +}; + +#include "../trace.h" +#include +#include + +#define rv_create_dir tracefs_create_dir +#define rv_create_file tracefs_create_file +#define rv_remove tracefs_remove + +#define MAX_RV_MONITOR_NAME_SIZE 32 + +extern struct mutex rv_interface_lock; + +struct rv_monitor_def { + struct list_head list; + struct rv_monitor *monitor; + struct dentry *root_d; + bool enabled; + bool task_monitor; +}; + +extern bool monitoring_on; +struct dentry *get_monitors_root(void); +void reset_all_monitors(void); +int init_rv_monitors(struct dentry *root_dir); +int get_task_monitor_slot(void); +void put_task_monitor_slot(int slot); diff --git a/kernel/trace/trace.c b/kernel/trace/trace.c index 2c95992e2c71..60e357c3120b 100644 --- a/kernel/trace/trace.c +++ b/kernel/trace/trace.c @@ -9774,6 +9774,10 @@ static __init int tracer_init_tracefs(void) tracer_init_tracefs_work_func(NULL); } +#ifdef CONFIG_RV + rv_init_interface(); +#endif + return 0; } diff --git a/kernel/trace/trace.h b/kernel/trace/trace.h index ff816fb41e48..becc03c0a45e 100644 --- a/kernel/trace/trace.h +++ b/kernel/trace/trace.h @@ -2005,4 +2005,6 @@ struct trace_min_max_param { extern const struct file_operations trace_min_max_fops; +extern int rv_init_interface(void); + #endif /* _LINUX_KERNEL_TRACE_H */ From patchwork Thu Jun 16 08:44:44 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883551 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 5774AC43334 for ; Thu, 16 Jun 2022 08:45:29 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359738AbiFPIp2 (ORCPT ); Thu, 16 Jun 2022 04:45:28 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34284 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359726AbiFPIp0 (ORCPT ); Thu, 16 Jun 2022 04:45:26 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 120E85D641; Thu, 16 Jun 2022 01:45:25 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 9340361D7B; Thu, 16 Jun 2022 08:45:24 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id B999CC341C5; Thu, 16 Jun 2022 08:45:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369124; bh=5tR+ioR72vpql7is2gwJ+hptQLed7y7xYTKhidAvHsI=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=amfwvka9a451GiXHyafk+zLs9L+9Te8mVlEPw1Zbr1R5H4MMMi6gj49ecUcVNucSU v9IVkPYVajwKYj+Y4Y6w2O5TzJ/HMU9Qn1FQpYha7f9iMLUz4nzyvUVVZ4255BKynf w65I+AO6iWtvHcnfJfVcOPmKB1A47Cmt24lYsgFBR0R4U9Hkni9DB2kzmMm0n5SwFc 3xRMafqWtw7vT1Y7Yd9TwmAUbq1Xr2xPOAazf8etAETUMRSfS6ky+mkio4WoiVzk3j 1dmvzR2DvL1u9ZZAJMRQw1ikAZEd8C0FXLhxwjhMDnjg+9EANZEqKUeIBet6A6qdjY otchBmcrV9GXw== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 02/20] rv: Add runtime reactors interface Date: Thu, 16 Jun 2022 10:44:44 +0200 Message-Id: <83874ccd86a34f6f2a4e6a8ca1fbe474685d6ba9.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org 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 Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- include/linux/rv.h | 13 + kernel/trace/rv/Kconfig | 14 + kernel/trace/rv/Makefile | 1 + kernel/trace/rv/rv.c | 18 +- kernel/trace/rv/rv.h | 20 ++ kernel/trace/rv/rv_reactors.c | 476 ++++++++++++++++++++++++++++++++++ 6 files changed, 540 insertions(+), 2 deletions(-) create mode 100644 kernel/trace/rv/rv_reactors.c diff --git a/include/linux/rv.h b/include/linux/rv.h index 205e65f57637..1e48c6bb74bf 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -8,6 +8,13 @@ */ #ifndef _LINUX_RV_H #define _LINUX_RV_H + +struct rv_reactor { + char *name; + char *description; + void (*react)(char *msg); +}; + struct rv_monitor { const char *name; const char *description; @@ -15,9 +22,15 @@ struct rv_monitor { int (*start)(void); void (*stop)(void); void (*reset)(void); + void (*react)(char *msg); + }; 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); #endif /* _LINUX_RV_H */ diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 6d127cdb00dd..560408fec0c8 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -10,3 +10,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 diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index fd995379df67..8944274d9b41 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -1,3 +1,4 @@ # SPDX-License-Identifier: GPL-2.0 obj-$(CONFIG_RV) += rv.o +obj-$(CONFIG_RV_REACTORS) += rv_reactors.o diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c index 43af7b13187e..7576d492a974 100644 --- a/kernel/trace/rv/rv.c +++ b/kernel/trace/rv/rv.c @@ -362,8 +362,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); @@ -674,7 +679,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); @@ -732,6 +741,11 @@ 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; diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h index 0796867a7b1e..6d43f52d72a9 100644 --- a/kernel/trace/rv/rv.h +++ b/kernel/trace/rv/rv.h @@ -15,14 +15,28 @@ struct rv_interface { #define rv_remove tracefs_remove #define MAX_RV_MONITOR_NAME_SIZE 32 +#define MAX_RV_REACTOR_NAME_SIZE 32 extern struct mutex rv_interface_lock; +#ifdef CONFIG_RV_REACTORS +struct rv_reactor_def { + struct list_head list; + struct rv_reactor *reactor; + /* protected by the monitor interface lock */ + int counter; +}; +#endif + struct rv_monitor_def { struct list_head list; struct rv_monitor *monitor; +#ifdef CONFIG_RV_REACTORS + struct rv_reactor_def *rdef; +#endif struct dentry *root_d; bool enabled; + bool reacting; bool task_monitor; }; @@ -32,3 +46,9 @@ void reset_all_monitors(void); int init_rv_monitors(struct dentry *root_dir); int get_task_monitor_slot(void); void put_task_monitor_slot(int slot); + +#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 diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c new file mode 100644 index 000000000000..bfe54d6996cc --- /dev/null +++ b/kernel/trace/rv/rv_reactors.c @@ -0,0 +1,476 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * 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: + * [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 defaul one is the nop (no operation) + * reactor. + * - Writing the name of an 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 + * + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira + */ + +#include + +#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+1]; + struct rv_monitor_def *mdef; + struct rv_reactor_def *rdef; + struct seq_file *seq_f; + int retval = -EINVAL; + char *ptr = buff; + int len; + + if (count < 1 || count > MAX_RV_REACTOR_NAME_SIZE+1) + return -EINVAL; + + memset(buff, 0, sizeof(buff)); + + retval = simple_write_to_buffer(buff, sizeof(buff)-1, ppos, user_buf, + count); + if (!retval) + return -EFAULT; + + len = strlen(ptr); + if (!len) + return count; + /* + * remove the \n + */ + ptr[len-1] = '\0'; + + /* + * 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) { + + if (mdef->monitor->enabled) + mdef->monitor->stop(); + + mdef->rdef = get_reactor_rdef_by_name("nop"); + mdef->reacting = false; + mdef->monitor->react = NULL; + + if (mdef->monitor->enabled) + mdef->monitor->start(); + + retval = count; + goto unlock; + } + + list_for_each_entry(rdef, &rv_reactors_list, list) { + if (strcmp(ptr, rdef->reactor->name) == 0) { + /* + * found! + */ + if (mdef->monitor->enabled) + mdef->monitor->stop(); + + mdef->rdef = rdef; + mdef->reacting = true; + mdef->monitor->react = rdef->reactor->react; + + if (mdef->monitor->enabled) + mdef->monitor->start(); + + 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[4]; + + memset(buff, 0, sizeof(buff)); + + mutex_lock(&rv_interface_lock); + sprintf(buff, "%d\n", reacting_on); + 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; + u64 val; + + retval = kstrtoull_from_user(user_buf, count, 10, &val); + if (retval) + return retval; + + retval = count; + + mutex_lock(&rv_interface_lock); + + switch (val) { + case 0: + turn_reacting_off(); + break; + case 1: + turn_reacting_on(); + break; + default: + retval = -EINVAL; + } + + mutex_unlock(&rv_interface_lock); + + return retval; +} + +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; + + tmp = rv_create_file("reactors", 0400, mdef->root_d, mdef, + &monitor_reactors_ops); + if (!tmp) + return -ENOMEM; + + /* + * Configure as the rv_nop reactor. + */ + mdef->rdef = get_reactor_rdef_by_name("nop"); + mdef->reacting = false; + + 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) +{ + rv_create_file("available_reactors", 0400, root_dir, NULL, + &available_reactors_ops); + rv_create_file("reacting_on", 0600, root_dir, NULL, &reacting_on_fops); + + __rv_register_reactor(&rv_nop); + + return 0; +} From patchwork Thu Jun 16 08:44:45 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883552 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 56742CCA47A for ; Thu, 16 Jun 2022 08:45:44 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359667AbiFPIpl (ORCPT ); Thu, 16 Jun 2022 04:45:41 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34384 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359726AbiFPIpa (ORCPT ); Thu, 16 Jun 2022 04:45:30 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id CD5C45D641; Thu, 16 Jun 2022 01:45:29 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 6959461D76; Thu, 16 Jun 2022 08:45:29 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 80F91C341C7; Thu, 16 Jun 2022 08:45:24 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369128; bh=n2qM9u0TQLUSVjUppzMp6Ophh/bAVGpgXwPtBN683xM=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=m2ZDSr+8gUOdjz63JyRCih5+vxxkTP+l4iEhhX6dd3WdtNYGmGNlc2Qy1Ohcwcn1P rQKsSUo5DzS0rwusvLT5ycpF+uQBTdcInV3CtxCFzFestLjT+sCG2ZogkOJNTdiyqa vmSjz/wVYxLISNI2GsoNXwX0phnzNhm6jfks5yTwPe/ArAddtHrLdMK5ZUMT7hPuWx SA54dSdA82gN3fIDEJa7nP5eLPnIcnSAyT3OIeWdMFjvC6laHt3Pfqs164kz8CUA8K wa8vTRBtqgwflX0bzNawDy71NH++0uD7HMPJoDcP1f/2QXGTQ85nP6cvuZ3ups3A1Y QsT+1BizoHHyQ== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 03/20] rv/include: Add helper functions for deterministic automata Date: Thu, 16 Jun 2022 10:44:45 +0200 Message-Id: <2b5b14c821ee4b069f68571e7f78fbc2ee4e9626.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Formally, a deterministic automaton, denoted by G, is defined as a quintuple: G = { X, E, f, x_0, X_m } where: - X is the set of states; - E is the finite set of events; - x_0 is the initial state; - X_m (subset of X) is the set of marked states. - f : X x E -> X $ is the transition function. It defines the state transition in the occurrence of a event from E in the state X. In the special case of deterministic automata, the occurrence of the event in E in a state in X has a deterministic next state from X. An automaton can also be represented using a graphical format of vertices (nodes) and edges. The open-source tool Graphviz can produce this graphic format using the (textual) DOT language as the source code. The dot2c tool presented in this paper: DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo Silva. Efficient formal verification for the Linux kernel. In: International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. p. 315-332. Translates a deterministic automaton in the DOT format into a C source code representation that to be used for monitoring. This header file implements helper functions to facilitate the usage of the C output from dot2c for monitoring. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- include/rv/automata.h | 49 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 include/rv/automata.h diff --git a/include/rv/automata.h b/include/rv/automata.h new file mode 100644 index 000000000000..0c0aa54bd820 --- /dev/null +++ b/include/rv/automata.h @@ -0,0 +1,49 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Deterministic automata helper functions, to be used with the automata + * models in C generated by the dot2k tool. + * + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira + */ + +#define DECLARE_AUTOMATA_HELPERS(name, type) \ + \ +static inline void *model_get_model_##name(void) \ +{ \ + return (void *) &automaton_##name; \ +} \ + \ +static char *model_get_state_name_##name(enum states_##name state) \ +{ \ + return automaton_##name.state_names[state]; \ +} \ + \ +static 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_##name)) \ + return -1; \ + \ + if ((event < 0) || (event > event_max_##name)) \ + 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_##name)) \ + return 0; \ + \ + return !!automaton_##name.final_states[state]; \ +} From patchwork Thu Jun 16 08:44:46 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883553 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 45AC6CCA47A for ; Thu, 16 Jun 2022 08:45:59 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359456AbiFPIp6 (ORCPT ); Thu, 16 Jun 2022 04:45:58 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34614 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359749AbiFPIpp (ORCPT ); Thu, 16 Jun 2022 04:45:45 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [IPv6:2604:1380:4601:e00::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 870E85DBE1; Thu, 16 Jun 2022 01:45:36 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 085A4B822A7; Thu, 16 Jun 2022 08:45:35 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 4531DC3411B; Thu, 16 Jun 2022 08:45:29 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369133; bh=7EwQgG3CqDtitxLOEmc3mRF06KIygTE+Vzh09/ZfK9A=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=aoar6oJ5NE5/FdMeWce2iZlgTiyaLssk6RSJBl/gRClZl6JFU3lXtfCUYeejZteoQ r4ZlvqFvtBdVnwviei/Q8JV8g4EKg1Z6luD3srIbhd8OaXu2CQNitkBSpVVbhZT+Zm YBT6MGMZl/gZ03KPaRzDN+MDOgSWLSG2+AwER6ODhz49sVh+jueVk7JcdTMSt6/RX6 9DxyOG8/+UEK5yTek9yArCMnIjkoc+uZolAdWL7sgH5Kje31Mpm+b+5sAEoyp1l/JG w7NISg5vvbp6ifr361d9xbmeJaszojmLJJxFbQM/ovRwrjFArie1QaZEj36P4pjZPx iCSDhI5CsmH0w== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 04/20] rv/include: Add deterministic automata monitor definition via C macros Date: Thu, 16 Jun 2022 10:44:46 +0200 Message-Id: X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org 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 ? +-------> 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 three different types of monitor instances: - #define DECLARE_DA_MON_GLOBAL(name, type) - #define DECLARE_DA_MON_PER_CPU(name, type) - #define DECLARE_DA_MON_PER_TASK(name, type) The first declares the functions for a global deterministic automata monitor, the second with per-cpu instances, and the third with per-task instances. In all 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 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. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- include/linux/rv.h | 2 + include/rv/da_monitor.h | 419 ++++++++++++++++++++++++++++++++++++++ include/rv/rv.h | 9 + include/trace/events/rv.h | 120 +++++++++++ kernel/fork.c | 2 +- kernel/trace/rv/Kconfig | 14 ++ kernel/trace/rv/rv.c | 5 + 7 files changed, 570 insertions(+), 1 deletion(-) create mode 100644 include/rv/da_monitor.h create mode 100644 include/trace/events/rv.h diff --git a/include/linux/rv.h b/include/linux/rv.h index 1e48c6bb74bf..af2081671219 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -9,6 +9,8 @@ #ifndef _LINUX_RV_H #define _LINUX_RV_H +#define MAX_DA_NAME_LEN 24 + struct rv_reactor { char *name; char *description; diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h new file mode 100644 index 000000000000..043660429659 --- /dev/null +++ b/include/rv/da_monitor.h @@ -0,0 +1,419 @@ +/* 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-2022 Daniel Bristot de Oliveira + */ + +#include +#include + +/* + * 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 void cond_react(char *msg) \ +{ \ + if (rv_##name.react) \ + rv_##name.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 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(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 >= 0) { \ + 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) \ + \ +static struct da_monitor da_mon_##name; \ + \ +static struct da_monitor *da_get_monitor_##name(void) \ +{ \ + return &da_mon_##name; \ +} \ + \ +static void da_monitor_reset_all_##name(void) \ +{ \ + da_monitor_reset_##name(da_mon_##name); \ +} \ + \ +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; \ +} \ + \ +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) \ + \ +DEFINE_PER_CPU(struct da_monitor, da_mon_##name); \ + \ +static struct da_monitor *da_get_monitor_##name(void) \ +{ \ + return this_cpu_ptr(&da_mon_##name); \ +} \ + \ +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); \ + } \ +} \ + \ +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; \ +} \ + \ +static inline void da_monitor_destroy_##name(void) \ +{ \ + return; \ +} + +/* + * Functions to define, init and get a per-task monitor. + */ +#define DECLARE_DA_MON_INIT_PER_TASK(name, type) \ + \ +static int task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT; \ + \ +static inline struct da_monitor *da_get_monitor_##name(struct task_struct *tsk) \ +{ \ + return &tsk->rv[task_mon_slot_##name].da_mon; \ +} \ + \ +static void da_monitor_reset_all_##name(void) \ +{ \ + struct task_struct *g, *p; \ + \ + read_lock(&tasklist_lock); \ + for_each_process_thread(g, p) \ + da_monitor_reset_##name(da_get_monitor_##name(p)); \ + read_unlock(&tasklist_lock); \ +} \ + \ +static int da_monitor_init_##name(void) \ +{ \ + struct da_monitor *da_mon; \ + struct task_struct *g, *p; \ + int retval; \ + \ + retval = get_task_monitor_slot(); \ + if (retval < 0) \ + return retval; \ + \ + task_mon_slot_##name = retval; \ + \ + read_lock(&tasklist_lock); \ + for_each_process_thread(g, p) { \ + da_mon = da_get_monitor_##name(p); \ + da_mon->curr_state = model_get_init_state_##name(); \ + da_mon->monitoring = 0; \ + } \ + read_unlock(&tasklist_lock); \ + \ + return 0; \ +} \ + \ +static inline void da_monitor_destroy_##name(void) \ +{ \ + if (task_mon_slot_##name == RV_PER_TASK_MONITOR_INIT) { \ + WARN_ONCE(1, "Disabling a disabled monitor: " #name); \ + return; \ + } \ + put_task_monitor_slot(task_mon_slot_##name); \ + return; \ +} + +/* + * 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; \ +} \ + \ +static inline bool da_handle_init_run_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); \ + \ + __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, struct task_struct *tsk, \ + 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, tsk, event); \ + \ + if (!retval) \ + da_monitor_reset_##name(da_mon); \ +} \ + \ +static inline void \ +da_handle_event_##name(struct task_struct *tsk, enum events_##name event) \ +{ \ + struct da_monitor *da_mon = da_get_monitor_##name(tsk); \ + __da_handle_event_##name(da_mon, tsk, event); \ +} \ + \ +static inline bool \ +da_handle_init_event_##name(struct task_struct *tsk, enum events_##name event) \ +{ \ + struct da_monitor *da_mon; \ + \ + if (unlikely(!rv_##name.enabled)) \ + return false; \ + \ + da_mon = da_get_monitor_##name(tsk); \ + \ + if (unlikely(!da_monitoring_##name(da_mon))) { \ + da_monitor_start_##name(da_mon); \ + return false; \ + } \ + \ + __da_handle_event_##name(da_mon, tsk, event); \ + \ + return true; \ +} + +/* + * Entry point for the global monitor. + */ +#define DECLARE_DA_MON_GLOBAL(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_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-task 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); diff --git a/include/rv/rv.h b/include/rv/rv.h index 27a108881d35..b0658cdc53d9 100644 --- a/include/rv/rv.h +++ b/include/rv/rv.h @@ -3,6 +3,14 @@ #ifndef _RV_RV_H #define _RV_RV_H +/* + * Deterministic automaton per-object variables. + */ +struct da_monitor { + bool monitoring; + int curr_state; +}; + /* * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS. * If we find justification for more monitors, we can think about @@ -16,6 +24,7 @@ * Futher monitor types are expected, so make this a union. */ union rv_task_monitor { + struct da_monitor da_mon; }; int get_task_monitor_slot(void); diff --git a/include/trace/events/rv.h b/include/trace/events/rv.h new file mode 100644 index 000000000000..9f40f2a49f84 --- /dev/null +++ b/include/trace/events/rv.h @@ -0,0 +1,120 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +#undef TRACE_SYSTEM +#define TRACE_SYSTEM rv + +#if !defined(_TRACE_RV_H) || defined(TRACE_HEADER_MULTI_READ) +#define _TRACE_RV_H + +#include +#include + +#ifdef CONFIG_DA_MON_EVENTS_IMPLICIT +DECLARE_EVENT_CLASS(event_da_monitor, + + TP_PROTO(char *state, char *event, char *next_state, bool safe), + + TP_ARGS(state, event, next_state, safe), + + TP_STRUCT__entry( + __array( char, state, MAX_DA_NAME_LEN ) + __array( char, event, MAX_DA_NAME_LEN ) + __array( char, next_state, MAX_DA_NAME_LEN ) + __field( bool, safe ) + ), + + TP_fast_assign( + memcpy(__entry->state, state, MAX_DA_NAME_LEN); + memcpy(__entry->event, event, MAX_DA_NAME_LEN); + memcpy(__entry->next_state, next_state, MAX_DA_NAME_LEN); + __entry->safe = safe; + ), + + TP_printk("%s x %s -> %s %s", + __entry->state, + __entry->event, + __entry->next_state, + __entry->safe ? "(safe)" : "") +); + +DECLARE_EVENT_CLASS(error_da_monitor, + + TP_PROTO(char *state, char *event), + + TP_ARGS(state, event), + + TP_STRUCT__entry( + __array( char, state, MAX_DA_NAME_LEN ) + __array( char, event, MAX_DA_NAME_LEN ) + ), + + TP_fast_assign( + memcpy(__entry->state, state, MAX_DA_NAME_LEN); + memcpy(__entry->event, event, MAX_DA_NAME_LEN); + ), + + TP_printk("event %s not expected in the state %s", + __entry->event, + __entry->state) +); +#endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */ + +#ifdef CONFIG_DA_MON_EVENTS_ID +DECLARE_EVENT_CLASS(event_da_monitor_id, + + TP_PROTO(int id, char *state, char *event, char *next_state, bool safe), + + TP_ARGS(id, state, event, next_state, safe), + + TP_STRUCT__entry( + __field( int, id ) + __array( char, state, MAX_DA_NAME_LEN ) + __array( char, event, MAX_DA_NAME_LEN ) + __array( char, next_state, MAX_DA_NAME_LEN ) + __field( bool, safe ) + ), + + TP_fast_assign( + memcpy(__entry->state, state, MAX_DA_NAME_LEN); + memcpy(__entry->event, event, MAX_DA_NAME_LEN); + memcpy(__entry->next_state, next_state, MAX_DA_NAME_LEN); + __entry->id = id; + __entry->safe = safe; + ), + + TP_printk("%d: %s x %s -> %s %s", + __entry->id, + __entry->state, + __entry->event, + __entry->next_state, + __entry->safe ? "(safe)" : "") +); + +DECLARE_EVENT_CLASS(error_da_monitor_id, + + TP_PROTO(int id, char *state, char *event), + + TP_ARGS(id, state, event), + + TP_STRUCT__entry( + __field( int, id ) + __array( char, state, MAX_DA_NAME_LEN ) + __array( char, event, MAX_DA_NAME_LEN ) + ), + + TP_fast_assign( + memcpy(__entry->state, state, MAX_DA_NAME_LEN); + memcpy(__entry->event, event, MAX_DA_NAME_LEN); + __entry->id = id; + ), + + TP_printk("%d: event %s not expected in the state %s", + __entry->id, + __entry->event, + __entry->state) +); +#endif /* CONFIG_DA_MON_EVENTS_ID */ +#endif /* _TRACE_RV_H */ + +/* This part ust be outside protection */ +#undef TRACE_INCLUDE_PATH +#include diff --git a/kernel/fork.c b/kernel/fork.c index 5e40e58ef83d..6f1f82ccd5f2 100644 --- a/kernel/fork.c +++ b/kernel/fork.c @@ -1970,7 +1970,7 @@ static void rv_task_fork(struct task_struct *p) int i; for (i = 0; i < RV_PER_TASK_MONITORS; i++) - ; + p->rv[i].da_mon.monitoring = false; } #else #define rv_task_fork(p) do {} while (0) diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 560408fec0c8..1eafb5adcfcb 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -1,5 +1,19 @@ # SPDX-License-Identifier: GPL-2.0-only # +config DA_MON_EVENTS + default n + bool + +config DA_MON_EVENTS_IMPLICIT + select DA_MON_EVENTS + default n + bool + +config DA_MON_EVENTS_ID + select DA_MON_EVENTS + default n + bool + menuconfig RV bool "Runtime Verification" depends on TRACING diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c index 7576d492a974..51a610227341 100644 --- a/kernel/trace/rv/rv.c +++ b/kernel/trace/rv/rv.c @@ -143,6 +143,11 @@ #include #include +#ifdef CONFIG_DA_MON_EVENTS +#define CREATE_TRACE_POINTS +#include +#endif + #include "rv.h" DEFINE_MUTEX(rv_interface_lock); From patchwork Thu Jun 16 08:44:47 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883554 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 6CF79C43334 for ; Thu, 16 Jun 2022 08:46:02 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359810AbiFPIqA (ORCPT ); Thu, 16 Jun 2022 04:46:00 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34566 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359735AbiFPIp5 (ORCPT ); Thu, 16 Jun 2022 04:45:57 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 5BE665DBE7; Thu, 16 Jun 2022 01:45:41 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id C7AA2B822A9; Thu, 16 Jun 2022 08:45:39 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 09536C385A2; Thu, 16 Jun 2022 08:45:33 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369138; bh=vh8GCJZdFY4jPSPg5VmzbjDbx7oE/fXp3z/xiXgywUc=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=n1lkWXHzI+t0mDgoSWSWheuGl+Yhhd0wPSb0bVE2UysyybbErUSot7z9E6GuG8RAn V+IsRMk1iaRoVsYR/szBarWkL/Jw8ftsevck0e6FM5p8SGxkFNjYVYRU5GuMWipgcJ tJVFgctbyrPyI6QZ1uT5cR8YaccrBPy1x5wGTFHztlpTIwlSnXmA/w+e5MVhO4Sgin qL6wzVaBls6N5AwchaONOy4479TCsqLBqOsAXhOY/cSSYRhC8QVK44a3/7QHhB9kPU 3z/gepmHDxOH8OtqIJnWFyXL289cn06T/HNXcgEOo2Oqc/Oxg0igioh3ykIR4KHun+ +hkokUInw+jZw== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 05/20] rv/include: Add instrumentation helper functions Date: Thu, 16 Jun 2022 10:44:47 +0200 Message-Id: <858a1130aa4b3add27ca2cdc6a5490de5b06befa.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Instrumentation helper functions to facilitate the instrumentation of auto-generated RV monitors create by dot2k. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- include/rv/instrumentation.h | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 include/rv/instrumentation.h diff --git a/include/rv/instrumentation.h b/include/rv/instrumentation.h new file mode 100644 index 000000000000..88dd33f10827 --- /dev/null +++ b/include/rv/instrumentation.h @@ -0,0 +1,23 @@ +/* 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-2022 Daniel Bristot de Oliveira + */ + +#include + +#define rv_attach_trace_probe(monitor, tp, rv_handler) \ + do { \ + check_trace_callback_type_##tp(rv_handler); \ + WARN_ONCE(register_trace_##tp(rv_handler, NULL), \ + "fail attaching " #monitor " " #tp "handler"); \ + } while (0) + +#define rv_detach_trace_probe(monitor, tp, rv_handler) \ + do { \ + unregister_trace_##tp(rv_handler, NULL); \ + } while (0) From patchwork Thu Jun 16 08:44:48 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883555 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 50365C43334 for ; Thu, 16 Jun 2022 08:46:04 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359767AbiFPIqC (ORCPT ); Thu, 16 Jun 2022 04:46:02 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34618 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359766AbiFPIp6 (ORCPT ); Thu, 16 Jun 2022 04:45:58 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 9A7465DBF1; Thu, 16 Jun 2022 01:45:44 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 928A161D58; Thu, 16 Jun 2022 08:45:43 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id C06F1C3411F; Thu, 16 Jun 2022 08:45:38 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369143; bh=rP28sJePyrZSun7tv9P2hpI1QdYZIeV8UXSwoUZbzus=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=TQkTv6r0bfqIG2OiiPEqOaa8g/UEg6zAlnRmEJOIvJegqVE4UZgmmUN3rNb4WsrEO pIbPu+M2YLTLFEuLcoeTX9hxgjgZ5LeMem6f17XUgLbkVQuiP8T8QWp2kFJjwLyIR4 0AUn2LF88tNo9bC5P2BYnEfDzTkBNj00M1oXAe9MEY5Reyba4a2X4cwQdOl0Yn+Ydr uQVh4m5D1+iTudX2B0lc0ETSJvNHXRmsLQVPRSHiL+kR2YeVbJBjfgdm9RXDdEI2Pn UHMHMSD7LP8z5DGyt20pjfp5q7HIuSqtlCwCeMX54uB/TUh/Xg9KFQb8d4Z/ZKn78e 3tRQd4Bf7yDzw== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 06/20] tools/rv: Add dot2c Date: Thu, 16 Jun 2022 10:44:48 +0200 Message-Id: <5b1e664b0c33f4da0430922718adc71a5d58d86c.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org 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 Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- tools/verification/dot2/Makefile | 21 +++ tools/verification/dot2/automata.py | 179 ++++++++++++++++++++ tools/verification/dot2/dot2c | 30 ++++ tools/verification/dot2/dot2c.py | 244 ++++++++++++++++++++++++++++ 4 files changed, 474 insertions(+) create mode 100644 tools/verification/dot2/Makefile create mode 100644 tools/verification/dot2/automata.py create mode 100644 tools/verification/dot2/dot2c create mode 100644 tools/verification/dot2/dot2c.py diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile new file mode 100644 index 000000000000..235d182f6b2c --- /dev/null +++ b/tools/verification/dot2/Makefile @@ -0,0 +1,21 @@ +INSTALL=install + +prefix ?= /usr +bindir ?= $(prefix)/bin +mandir ?= $(prefix)/share/man +miscdir ?= $(prefix)/share/dot2 +srcdir ?= $(prefix)/src + +PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') + +.PHONY: all +all: + +.PHONY: clean +clean: + +.PHONY: install +install: + $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py + $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py + $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/automata.py new file mode 100644 index 000000000000..171ad4497983 --- /dev/null +++ b/tools/verification/dot2/automata.py @@ -0,0 +1,179 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# automata object: parse a dot file into a python object +# 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 + +import ntpath + +class Automata: + """Automata class: Reads a dot file and part it as an automata. + + Attributes: + dot_file: A dot file with an state_automaton definition. + """ + + def __init__(self, file_path): + self.__dot_path=file_path + self.name=self.__get_model_name() + self.__dot_lines = self.__open_dot() + self.states, self.initial_state, self.final_states = self.__get_state_variables() + self.events = self.__get_event_variables() + self.function = self.__create_matrix() + + def __get_model_name(self): + basename=ntpath.basename(self.__dot_path) + if basename.endswith(".dot") == False: + print("not a dot file") + raise Exception("not a dot file: %s" % self.__dot_path) + + model_name=basename[0:-4] + if model_name.__len__() == 0: + raise Exception("not a dot file: %s" % self.__dot_path) + + return model_name + + def __open_dot(self): + cursor = 0 + dot_lines = [] + try: + dot_file = open(self.__dot_path) + except: + raise Exception("Cannot open the file: %s" % self.__dot_path) + + dot_lines = dot_file.read().splitlines() + dot_file.close() + + # checking the first line: + line = dot_lines[cursor].split() + + if (line[0] != "digraph") and (line[1] != "state_automaton"): + raise Exception("Not a valid .dot format: %s" % self.__dot_path) + else: + cursor = cursor + 1 + return dot_lines + + def __get_cursor_begin_states(self): + cursor = 0 + while self.__dot_lines[cursor].split()[0] != "{node": + cursor += 1 + return cursor + + def __get_cursor_begin_events(self): + cursor = 0 + while self.__dot_lines[cursor].split()[0] != "{node": + cursor += 1 + while self.__dot_lines[cursor].split()[0] == "{node": + cursor += 1 + # skip initial state transition + cursor += 1 + return cursor + + def __get_state_variables(self): + # wait for node declaration + states = [] + final_states=[] + + has_final_states = False + cursor = self.__get_cursor_begin_states() + + # process nodes + while self.__dot_lines[cursor].split()[0] == "{node": + line = self.__dot_lines[cursor].split() + raw_state = line[-1] + + # "enabled_fired"}; -> enabled_fired + state = raw_state.replace('"', '').replace('};', '').replace(',','_') + if state[0:7] == "__init_": + initial_state = state[7:] + else: + states.append(state) + if self.__dot_lines[cursor].__contains__("doublecircle") == True: + final_states.append(state) + has_final_states = True + + if self.__dot_lines[cursor].__contains__("ellipse") == True: + final_states.append(state) + has_final_states = True + + cursor = cursor + 1 + + states = sorted(set(states)) + states.remove(initial_state) + + # Insert the initial state at the bein og the states + states.insert(0, initial_state) + + if has_final_states == False: + final_states.append(initial_state) + + return states, initial_state, final_states + + def __get_event_variables(self): + # here we are at the begin of transitions, take a note, we will return later. + cursor = self.__get_cursor_begin_events() + + events = [] + while self.__dot_lines[cursor][1] == '"': + # transitions have the format: + # "all_fired" -> "both_fired" [ label = "disable_irq" ]; + # ------------ event is here ------------^^^^^ + if self.__dot_lines[cursor].split()[1] == "->": + line = self.__dot_lines[cursor].split() + event = line[-2].replace('"','') + + # when a transition has more than one lables, they are like this + # "local_irq_enable\nhw_local_irq_enable_n" + # so split them. + + event = event.replace("\\n", " ") + for i in event.split(): + events.append(i) + cursor = cursor + 1 + + return sorted(set(events)) + + def __create_matrix(self): + # transform the array into a dictionary + events = self.events + states = self.states + events_dict = {} + states_dict = {} + nr_event = 0 + for event in events: + events_dict[event] = nr_event + nr_event += 1 + + nr_state = 0 + for state in states: + states_dict[state] = nr_state + nr_state = nr_state + 1 + + # declare the matrix.... + matrix = [['-1' for x in range(nr_event)] for y in range(nr_state)] + + # and we are back! Let's fill the matrix + cursor = self.__get_cursor_begin_events() + + while self.__dot_lines[cursor][1] == '"': + if self.__dot_lines[cursor].split()[1] == "->": + line = self.__dot_lines[cursor].split() + origin_state = line[0].replace('"','').replace(',','_') + dest_state = line[2].replace('"','').replace(',','_') + possible_events = line[-2].replace('"','').replace("\\n", " ") + for event in possible_events.split(): + matrix[states_dict[origin_state]][events_dict[event]] = dest_state + cursor = cursor + 1 + + return matrix diff --git a/tools/verification/dot2/dot2c b/tools/verification/dot2/dot2c new file mode 100644 index 000000000000..0165f203dedc --- /dev/null +++ b/tools/verification/dot2/dot2c @@ -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 + +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() diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot2c.py new file mode 100644 index 000000000000..07f040ebf882 --- /dev/null +++ b/tools/verification/dot2/dot2c.py @@ -0,0 +1,244 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# dot2c: 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-2022 Red Hat, Inc. +# +# Author: +# Daniel Bristot de Oliveira + +from dot2.automata import Automata + +class Dot2c(Automata): + enum_suffix="" + enum_states_def="states" + enum_events_def="events" + struct_automaton_def="automaton" + var_automaton_def="aut" + + def __init__(self, file_path): + super().__init__(file_path) + self.line_length=80 + + def __buff_to_string(self, buff): + string="" + + for line in buff: + string=string + line + "\n" + + # cut off the last \n + return string[:-1] + + def __get_enum_states_content(self): + buff=[] + buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix)) + for state in self.states: + if state != self.initial_state: + buff.append("\t%s%s," % (state, self.enum_suffix)) + buff.append("\tstate_max%s" % (self.enum_suffix)) + + return buff + + def get_enum_states_string(self): + buff=self.__get_enum_states_content() + return self.__buff_to_string(buff) + + def format_states_enum(self): + buff=[] + buff.append("enum %s {" % self.enum_states_def) + buff.append(self.get_enum_states_string()) + buff.append("};\n") + + return buff + + def __get_enum_events_content(self): + buff=[] + first=True + for event in self.events: + if first: + buff.append("\t%s%s = 0," % (event, self.enum_suffix)) + first=False + else: + buff.append("\t%s%s," % (event, self.enum_suffix)) + buff.append("\tevent_max%s" % self.enum_suffix) + + return buff + + def get_enum_events_string(self): + buff=self.__get_enum_events_content() + return self.__buff_to_string(buff) + + def format_events_enum(self): + buff=[] + buff.append("enum %s {" % self.enum_events_def) + buff.append(self.get_enum_events_string()) + buff.append("};\n") + + return buff + + def get_minimun_type(self): + min_type="char" + + if self.states.__len__() > 255: + min_type="short" + + if self.states.__len__() > 65535: + min_type="int" + + return min_type + + def format_automaton_definition(self): + min_type = self.get_minimun_type() + buff=[] + buff.append("struct %s {" % self.struct_automaton_def) + buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix)) + buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix)) + buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix)) + buff.append("\t%s initial_state;" % min_type) + buff.append("\tchar final_states[state_max%s];" % (self.enum_suffix)) + buff.append("};\n") + return buff + + def format_aut_init_header(self): + buff=[] + buff.append("struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def)) + return buff + + def __get_string_vector_per_line_content(self, buff): + first=True + string="" + for entry in buff: + if first: + string = string + "\t\t\"" + entry + first=False; + else: + string = string + "\",\n\t\t\"" + entry + string = string + "\"" + + return string + + def get_aut_init_events_string(self): + return self.__get_string_vector_per_line_content(self.events) + + def get_aut_init_states_string(self): + return self.__get_string_vector_per_line_content(self.states) + + def format_aut_init_events_string(self): + buff=[] + buff.append("\t.event_names = {") + buff.append(self.get_aut_init_events_string()) + buff.append("\t},") + return buff + + def format_aut_init_states_string(self): + buff=[] + buff.append("\t.state_names = {") + buff.append(self.get_aut_init_states_string()) + buff.append("\t},") + + return buff + + def __get_max_strlen_of_states(self): + return max(self.states, key=len).__len__() + + def __get_state_string_length(self): + maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__() + return "%" + str(maxlen) + "s" + + def get_aut_init_function(self): + nr_states=self.states.__len__() + nr_events=self.events.__len__() + buff=[] + + strformat = self.__get_state_string_length() + + for x in range(nr_states): + line="\t\t{ " + for y in range(nr_events): + next_state = self.function[x][y] + if next_state != '-1': + next_state = self.function[x][y] + self.enum_suffix + + if y != nr_events-1: + line = line + strformat % next_state + ", " + else: + line = line + strformat % next_state + " }," + buff.append(line) + + return self.__buff_to_string(buff) + + def format_aut_init_function(self): + buff=[] + buff.append("\t.function = {") + buff.append(self.get_aut_init_function()) + buff.append("\t},") + + return buff + + def get_aut_init_initial_state(self): + return self.initial_state + + def format_aut_init_initial_state(self): + buff=[] + initial_state=self.get_aut_init_initial_state() + buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",") + + return buff + + def get_aut_init_final_states(self): + line="" + first=True + for state in self.states: + if first == False: + line = line + ', ' + else: + first = False + + if self.final_states.__contains__(state): + line = line + '1' + else: + line = line + '0' + return line + + def format_aut_init_final_states(self): + buff=[] + buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states()) + + return buff + + def __get_automaton_initialization_footer_string(self): + footer="};\n" + return footer + + def format_aut_init_footer(self): + buff=[] + buff.append(self.__get_automaton_initialization_footer_string()) + + return buff + + def format_model(self): + buff=[] + buff += self.format_states_enum() + buff += self.format_events_enum() + buff += self.format_automaton_definition() + buff += self.format_aut_init_header() + buff += self.format_aut_init_states_string() + buff += self.format_aut_init_events_string() + buff += self.format_aut_init_function() + buff += self.format_aut_init_initial_state() + buff += self.format_aut_init_final_states() + buff += self.format_aut_init_footer() + + return buff + + def print_model_classic(self): + buff=self.format_model() + print(self.__buff_to_string(buff)) From patchwork Thu Jun 16 08:44:49 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883556 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 28A57CCA47F for ; Thu, 16 Jun 2022 08:46:05 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359813AbiFPIqE (ORCPT ); Thu, 16 Jun 2022 04:46:04 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34606 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359782AbiFPIp6 (ORCPT ); Thu, 16 Jun 2022 04:45:58 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 1AA0C5DBDD; Thu, 16 Jun 2022 01:45:48 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 5A77661D78; Thu, 16 Jun 2022 08:45:48 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 7EFEAC341C0; Thu, 16 Jun 2022 08:45:43 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369147; bh=B88M7ZEwl68n7THj+esBYgDD9SubditJErT6VVWUfQo=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=VkX9227Bir4FoX04g6kzBhmp5jdkGgrgX6rjFTe8ZTYMldzqtQ68Eul3/syEMTteq WEoy4bSXDAgGWNN/GZTb2IfzC3oByQnFKrSwNsaexdAxpdI328UgdPhl2QQASYkbb5 4Zm/9QE0oKJh83wEZa2aq5SNAy/hrSO91Jf3tHasOs8BLK+34fNbRKoEVGLnlxYrvE ETpNxXow+6JLZjD67Cz9Wj7BKEixmaazQLej7lxQ32boNS7wgNFn/SifmuqOVRbNP2 OIIAOFpEzybFWY438p3fkzZ9I3eqpx2NP+HaAOBC3MbJlGqO7RAox/QWI1b1rDDM7e Fsv9bFGNP1siw== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 07/20] tools/rv: Add dot2k Date: Thu, 16 Jun 2022 10:44:49 +0200 Message-Id: X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org 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 Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- tools/verification/dot2/Makefile | 5 + tools/verification/dot2/dot2k | 50 +++++ tools/verification/dot2/dot2k.py | 177 ++++++++++++++++++ .../dot2/dot2k_templates/main_global.c | 94 ++++++++++ .../dot2/dot2k_templates/main_per_cpu.c | 94 ++++++++++ .../dot2/dot2k_templates/main_per_task.c | 94 ++++++++++ 6 files changed, 514 insertions(+) create mode 100644 tools/verification/dot2/dot2k create mode 100644 tools/verification/dot2/dot2k.py create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile index 235d182f6b2c..021beb07a521 100644 --- a/tools/verification/dot2/Makefile +++ b/tools/verification/dot2/Makefile @@ -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)/ diff --git a/tools/verification/dot2/dot2k b/tools/verification/dot2/dot2k new file mode 100644 index 000000000000..6a35297e812e --- /dev/null +++ b/tools/verification/dot2/dot2k @@ -0,0 +1,50 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For more information, see: +# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/ +# +# Copyright 2018-2020 Red Hat, Inc. +# +# Author: +# Daniel Bristot de Oliveira + +if __name__ == '__main__': + from dot2.dot2k import dot2k + import argparse + import ntpath + import os + import platform + import sys + import sys + import argparse + + parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor') + parser.add_argument('-d', "--dot", dest="dot_file", required=True) + parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True) + parser.add_argument('-n', "--model_name", dest="model_name", required=False) + parser.add_argument("-D", "--description", dest="description", required=False) + params = parser.parse_args() + + print("Opening and parsing the dot file %s" % params.dot_file) + try: + monitor=dot2k(params.dot_file, params.monitor_type) + except Exception as e: + print('Error: '+ str(e)) + print("Sorry : :-(") + sys.exit(1) + + # easier than using argparse action. + if params.model_name != None: + print(params.model_name) + + print("Writing the monitor into the directory %s" % monitor.name) + monitor.print_files() + print("Almost done, checklist") + print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name)) + print(" - Edit include/trace/events/rv.h to add the tracepoint entry") + print(" - Move it to the kernel's monitor directory") + print(" - Edit kernel/trace/rv/Makefile") + print(" - Edit kernel/trace/rv/Kconfig") diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2k.py new file mode 100644 index 000000000000..230ad530b50c --- /dev/null +++ b/tools/verification/dot2/dot2k.py @@ -0,0 +1,177 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For more information, see: +# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/ +# +# Copyright 2018-2020 Red Hat, Inc. +# +# Author: +# Daniel Bristot de Oliveira + +from dot2.dot2c import Dot2c +import platform +import os + +class dot2k(Dot2c): + monitor_types={ "global" : 1, "per_cpu" : 2, "per_task" : 3 } + monitor_templates_dir="dot2k/rv_templates/" + monitor_type="per_cpu" + + def __init__(self, file_path, MonitorType): + super().__init__(file_path) + + self.monitor_type=self.monitor_types.get(MonitorType) + if self.monitor_type == None: + raise Exception("Unknown monitor type: %s" % MonitorType) + + self.monitor_type=MonitorType + self.__fill_rv_templates_dir() + self.main_c = self.__open_file(self.monitor_templates_dir + "main_" + MonitorType + ".c") + self.enum_suffix = "_%s" % self.name + + def __fill_rv_templates_dir(self): + + if os.path.exists(self.monitor_templates_dir) == True: + return + + if platform.system() != "Linux": + raise Exception("I can only run on Linux.") + + kernel_path="/lib/modules/%s/build/tools/rv/%s" % (platform.release(), self.monitor_templates_dir) + + if os.path.exists(kernel_path) == True: + self.monitor_templates_dir=kernel_path + return + + if os.path.exists("/usr/share/dot2/dot2k_templates/") == True: + self.monitor_templates_dir="/usr/share/dot2/dot2k_templates/" + return + + raise Exception("Could not find the template directory, do you have the kernel source installed?") + + + def __open_file(self, path): + try: + fd = open(path) + except OSError: + raise Exception("Cannot open the file: %s" % path) + + content = fd.read() + + return content + + def __buff_to_string(self, buff): + string="" + + for line in buff: + string=string + line + "\n" + + # cut off the last \n + return string[:-1] + + def fill_monitor_h(self): + monitor_h = self.monitor_h + + min_type=self.get_minimun_type() + + monitor_h = monitor_h.replace("MIN_TYPE", min_type) + + return monitor_h + + def fill_tracepoint_handlers_skel(self): + buff=[] + for event in self.events: + buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) + buff.append("{") + if self.monitor_type == "per_task": + buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;"); + buff.append("\tda_handle_event_%s(p, %s%s);" % (self.name, event, self.enum_suffix)); + else: + buff.append("\tda_handle_event_%s(%s%s);" % (self.name, event, self.enum_suffix)); + buff.append("}") + buff.append("") + return self.__buff_to_string(buff) + + def fill_tracepoint_attach_probe(self): + buff=[] + for event in self.events: + buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return self.__buff_to_string(buff) + + def fill_tracepoint_detach_helper(self): + buff=[] + for event in self.events: + buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return self.__buff_to_string(buff) + + def fill_main_c(self): + main_c = self.main_c + min_type=self.get_minimun_type() + nr_events=self.events.__len__() + tracepoint_handlers=self.fill_tracepoint_handlers_skel() + tracepoint_attach=self.fill_tracepoint_attach_probe() + tracepoint_detach=self.fill_tracepoint_detach_helper() + + main_c = main_c.replace("MIN_TYPE", min_type) + main_c = main_c.replace("MODEL_NAME", self.name) + main_c = main_c.replace("NR_EVENTS", str(nr_events)) + main_c = main_c.replace("TRACEPOINT_HANDLERS_SKEL", tracepoint_handlers) + main_c = main_c.replace("TRACEPOINT_ATTACH", tracepoint_attach) + main_c = main_c.replace("TRACEPOINT_DETACH", tracepoint_detach) + + return main_c + + def fill_model_h(self): + # + # Adjust the definition names + # + self.enum_states_def="states_%s" % self.name + self.enum_events_def="events_%s" % self.name + self.struct_automaton_def="automaton_%s" % self.name + self.var_automaton_def="automaton_%s" % self.name + + buff=self.format_model() + + return self.__buff_to_string(buff) + + def __create_directory(self): + try: + os.mkdir(self.name) + except FileExistsError: + return + except: + print("Fail creating the output dir: %s" % self.name) + + def __create_file(self, file_name, content): + path="%s/%s" % (self.name, file_name) + try: + file = open(path, 'w') + except FileExistsError: + return + except: + print("Fail creating file: %s" % path) + + file.write(content) + + file.close() + + def __get_main_name(self): + path="%s/%s" % (self.name, "main.c") + if os.path.exists(path) == False: + return "main.c" + return "__main.c" + + def print_files(self): + main_c=self.fill_main_c() + model_h=self.fill_model_h() + + self.__create_directory() + + path="%s.c" % self.name + self.__create_file(path, main_c) + + path="%s.h" % self.name + self.__create_file(path, model_h) diff --git a/tools/verification/dot2/dot2k_templates/main_global.c b/tools/verification/dot2/dot2k_templates/main_global.c new file mode 100644 index 000000000000..913dc68d782d --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/main_global.c @@ -0,0 +1,94 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "MODEL_NAME" + +/* + * XXX: include required tracepoint headers, e.g., + * #include + */ +#include + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "MODEL_NAME.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +struct rv_monitor rv_MODEL_NAME; +DECLARE_DA_MON_GLOBAL(MODEL_NAME, MIN_TYPE); + +/* + * 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. + * + */ +TRACEPOINT_HANDLERS_SKEL +static int start_MODEL_NAME(void) +{ + int retval; + + retval = da_monitor_init_MODEL_NAME(); + if (retval) + return retval; + +TRACEPOINT_ATTACH + + return 0; +} + +static void stop_MODEL_NAME(void) +{ + rv_MODEL_NAME.enabled = 0; + +TRACEPOINT_DETACH + + da_monitor_destroy_MODEL_NAME(); +} + +/* + * This is the monitor register section. + */ +struct rv_monitor rv_MODEL_NAME = { + .name = "MODEL_NAME", + .description = "auto-generated MODEL_NAME", + .start = start_MODEL_NAME, + .stop = stop_MODEL_NAME, + .reset = da_monitor_reset_all_MODEL_NAME, + .enabled = 0, +}; + +int register_MODEL_NAME(void) +{ + rv_register_monitor(&rv_MODEL_NAME); + return 0; +} + +void unregister_MODEL_NAME(void) +{ + if (rv_MODEL_NAME.enabled) + stop_MODEL_NAME(); + + rv_unregister_monitor(&rv_MODEL_NAME); +} + +module_init(register_MODEL_NAME); +module_exit(unregister_MODEL_NAME); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("MODEL_NAME"); diff --git a/tools/verification/dot2/dot2k_templates/main_per_cpu.c b/tools/verification/dot2/dot2k_templates/main_per_cpu.c new file mode 100644 index 000000000000..95eac96d8951 --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/main_per_cpu.c @@ -0,0 +1,94 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "MODEL_NAME" + +/* + * XXX: include required tracepoint headers, e.g., + * #include + */ +#include + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "MODEL_NAME.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +struct rv_monitor rv_MODEL_NAME; +DECLARE_DA_MON_PER_CPU(MODEL_NAME, MIN_TYPE); + +/* + * 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. + * + */ +TRACEPOINT_HANDLERS_SKEL +static int start_MODEL_NAME(void) +{ + int retval; + + retval = da_monitor_init_MODEL_NAME(); + if (retval) + return retval; + +TRACEPOINT_ATTACH + + return 0; +} + +static void stop_MODEL_NAME(void) +{ + rv_MODEL_NAME.enabled = 0; + +TRACEPOINT_DETACH + + da_monitor_destroy_MODEL_NAME(); +} + +/* + * This is the monitor register section. + */ +struct rv_monitor rv_MODEL_NAME = { + .name = "MODEL_NAME", + .description = "auto-generated MODEL_NAME", + .start = start_MODEL_NAME, + .stop = stop_MODEL_NAME, + .reset = da_monitor_reset_all_MODEL_NAME, + .enabled = 0, +}; + +int register_MODEL_NAME(void) +{ + rv_register_monitor(&rv_MODEL_NAME); + return 0; +} + +void unregister_MODEL_NAME(void) +{ + if (rv_MODEL_NAME.enabled) + stop_MODEL_NAME(); + + rv_unregister_monitor(&rv_MODEL_NAME); +} + +module_init(register_MODEL_NAME); +module_exit(unregister_MODEL_NAME); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("MODEL_NAME"); diff --git a/tools/verification/dot2/dot2k_templates/main_per_task.c b/tools/verification/dot2/dot2k_templates/main_per_task.c new file mode 100644 index 000000000000..8bafb8c8a0a4 --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/main_per_task.c @@ -0,0 +1,94 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "MODEL_NAME" + +/* + * XXX: include required tracepoint headers, e.g., + * #include + */ +#include + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "MODEL_NAME.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +struct rv_monitor rv_MODEL_NAME; +DECLARE_DA_MON_PER_TASK(MODEL_NAME, MIN_TYPE); + +/* + * 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. + * + */ +TRACEPOINT_HANDLERS_SKEL +static int start_MODEL_NAME(void) +{ + int retval; + + retval = da_monitor_init_MODEL_NAME(); + if (retval) + return retval; + +TRACEPOINT_ATTACH + + return 0; +} + +static void stop_MODEL_NAME(void) +{ + rv_MODEL_NAME.enabled = 0; + +TRACEPOINT_DETACH + + da_monitor_destroy_MODEL_NAME(); +} + +/* + * This is the monitor register section. + */ +struct rv_monitor rv_MODEL_NAME = { + .name = "MODEL_NAME", + .description = "auto-generated MODEL_NAME", + .start = start_MODEL_NAME, + .stop = stop_MODEL_NAME, + .reset = da_monitor_reset_all_MODEL_NAME, + .enabled = 0, +}; + +int register_MODEL_NAME(void) +{ + rv_register_monitor(&rv_MODEL_NAME); + return 0; +} + +void unregister_MODEL_NAME(void) +{ + if (rv_MODEL_NAME.enabled) + stop_MODEL_NAME(); + + rv_unregister_monitor(&rv_MODEL_NAME); +} + +module_init(register_MODEL_NAME); +module_exit(unregister_MODEL_NAME); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("MODEL_NAME"); From patchwork Thu Jun 16 08:44:50 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883557 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id DB041C43334 for ; Thu, 16 Jun 2022 08:46:20 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359769AbiFPIqQ (ORCPT ); Thu, 16 Jun 2022 04:46:16 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34610 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359805AbiFPIqA (ORCPT ); Thu, 16 Jun 2022 04:46:00 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 4E3315DBCD; Thu, 16 Jun 2022 01:45:55 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id D67F2B81E20; Thu, 16 Jun 2022 08:45:53 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 3F995C3411F; Thu, 16 Jun 2022 08:45:48 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369152; bh=ZJ0brquACtNcXCIAgCRgNB+aJ/fU2CSwf1pEP1xdS3c=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=rmpY9+pOtMmQn4Yy+VrFIeWB31DRRL5kf9pHv2pn3dg9ADHcEztUGaTGnuSDtJ6FK OmGgKEoJYtkHsedir14+rjJXSGEE4KnNz8BPq7sSioUaiR2y8rcdK4v5sJxdtFle0e jQ+8CBDW5LNum7z8NWYzn7INcYejQJGJC8Y7CqVWINIQye2LQf6qlf/1CSMbaY7oDi /BNuZp2SAHQALxiY3qpXxM0+RcrsqEKps5uDPQgcPREYnMNYZS3p8QJnprDlfTA8jw 4MOnuKBznzsFdKwX3X8Xe0suHsarKBdbUNesxloU8EcJex0Dmkgfqk6FfjjXYEVRGg iYEtuB5wBfVAQ== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 08/20] rv/monitor: Add the wip monitor skeleton created by dot2k Date: Thu, 16 Jun 2022 10:44:50 +0200 Message-Id: <6559fb9064f683fda469849549c72607c0f2ae5b.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org 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. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- kernel/trace/rv/monitors/wip/wip.c | 112 +++++++++++++++++++++++++++++ kernel/trace/rv/monitors/wip/wip.h | 38 ++++++++++ 2 files changed, 150 insertions(+) create mode 100644 kernel/trace/rv/monitors/wip/wip.c create mode 100644 kernel/trace/rv/monitors/wip/wip.h diff --git a/kernel/trace/rv/monitors/wip/wip.c b/kernel/trace/rv/monitors/wip/wip.c new file mode 100644 index 000000000000..08950e09b823 --- /dev/null +++ b/kernel/trace/rv/monitors/wip/wip.c @@ -0,0 +1,112 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "wip" + +/* + * XXX: include required tracepoint headers, e.g., + * #include + */ +#include + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "wip.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +struct rv_monitor rv_wip; +DECLARE_DA_MON_PER_CPU(wip, char); + +/* + * This is the instrumentation part of the monitor. + * + * This is the section where manual work is required. Here the kernel events + * are translated into model's event. + * + */ +static void handle_preempt_disable(void *data, /* XXX: fill header */) +{ + da_handle_event_wip(preempt_disable_wip); +} + +static void handle_preempt_enable(void *data, /* XXX: fill header */) +{ + da_handle_event_wip(preempt_enable_wip); +} + +static void handle_sched_waking(void *data, /* XXX: fill header */) +{ + da_handle_event_wip(sched_waking_wip); +} + +static int 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; +} + +static void stop_wip(void) +{ + rv_wip.enabled = 0; + + rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable); + rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable); + rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking); + + da_monitor_destroy_wip(); +} + +/* + * This is the monitor register section. + */ +struct rv_monitor rv_wip = { + .name = "wip", + .description = "auto-generated wip", + .start = start_wip, + .stop = stop_wip, + .reset = da_monitor_reset_all_wip, + .enabled = 0, +}; + +int register_wip(void) +{ + rv_register_monitor(&rv_wip); + return 0; +} + +void unregister_wip(void) +{ + if (rv_wip.enabled) + stop_wip(); + + rv_unregister_monitor(&rv_wip); +} + +module_init(register_wip); +module_exit(unregister_wip); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("wip"); diff --git a/kernel/trace/rv/monitors/wip/wip.h b/kernel/trace/rv/monitors/wip/wip.h new file mode 100644 index 000000000000..3055ea331706 --- /dev/null +++ b/kernel/trace/rv/monitors/wip/wip.h @@ -0,0 +1,38 @@ +enum states_wip { + preemptive_wip = 0, + non_preemptive_wip, + state_max_wip +}; + +enum events_wip { + preempt_disable_wip = 0, + preempt_enable_wip, + sched_waking_wip, + event_max_wip +}; + +struct automaton_wip { + char *state_names[state_max_wip]; + char *event_names[event_max_wip]; + char function[state_max_wip][event_max_wip]; + char initial_state; + char final_states[state_max_wip]; +}; + +struct automaton_wip automaton_wip = { + .state_names = { + "preemptive", + "non_preemptive" + }, + .event_names = { + "preempt_disable", + "preempt_enable", + "sched_waking" + }, + .function = { + { non_preemptive_wip, -1, -1 }, + { -1, preemptive_wip, non_preemptive_wip }, + }, + .initial_state = preemptive_wip, + .final_states = { 1, 0 }, +}; From patchwork Thu Jun 16 08:44:51 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883558 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 28CF5CCA47D for ; Thu, 16 Jun 2022 08:46:22 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359783AbiFPIqS (ORCPT ); Thu, 16 Jun 2022 04:46:18 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35130 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359808AbiFPIqA (ORCPT ); Thu, 16 Jun 2022 04:46:00 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 942F75DBD4; Thu, 16 Jun 2022 01:45:58 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id CF2D161D78; Thu, 16 Jun 2022 08:45:57 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id F2A16C34114; Thu, 16 Jun 2022 08:45:52 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369157; bh=qa1UKmJJVTSGhHfJiyJQ35RQtbOYfyr8tjVSosqFRI8=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=MNTXaE51gCqcnturGqLHl03q4uwui54XPP1ZRunXdI588fO5i9Km1cpq8PlONqyBv qAhgRJG8uwnNgQkpPaaMjbxKeeUB8qkGCKrXzAPbm2JDfXMjL1APBs89Uj2GdJrrPp flfxYjyk+viWPo7MBMc5U8pcHei5obaMryY59Yv+fGwQJQtkkQuFJu5vLRw06ENRbU KtqkfMzHjM6VsHf852HzaIv+Gj3uhXXHIbzDeYThwA7EhlPyvClaVHiVRVVee/dPvP Z6ftb6nesFl/wVSAo53Ij5Whf1KmlkhSd6OILkEVChrl8eAZER+Kvf9JHTdJTAhkhg y3hgbdvWWTGng== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 09/20] rv/monitor: wip instrumentation and Makefile/Kconfig entries Date: Thu, 16 Jun 2022 10:44:51 +0200 Message-Id: <9c05a95927c18bebcf0eb79bef15ec59667bc08c.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Adds the instrumentation to the previously created wip monitor, as an example of the developer work. It also adds a Makefile, Kconfig and tracepoint entries. This is a good example of the manual work that is left for the developer to do. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira Reported-by: kernel test robot --- include/trace/events/rv.h | 10 ++++++++++ kernel/trace/rv/Kconfig | 7 +++++++ kernel/trace/rv/Makefile | 1 + kernel/trace/rv/monitors/wip/wip.c | 30 ++++++++++++++---------------- 4 files changed, 32 insertions(+), 16 deletions(-) diff --git a/include/trace/events/rv.h b/include/trace/events/rv.h index 9f40f2a49f84..4e0dabffcf29 100644 --- a/include/trace/events/rv.h +++ b/include/trace/events/rv.h @@ -56,6 +56,16 @@ DECLARE_EVENT_CLASS(error_da_monitor, __entry->event, __entry->state) ); + +#ifdef CONFIG_RV_MON_WIP +DEFINE_EVENT(event_da_monitor, event_wip, + TP_PROTO(char *state, char *event, char *next_state, bool safe), + TP_ARGS(state, event, next_state, safe)); + +DEFINE_EVENT(error_da_monitor, error_wip, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_WIP */ #endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */ #ifdef CONFIG_DA_MON_EVENTS_ID diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 1eafb5adcfcb..e9246b0bec9d 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -26,6 +26,13 @@ menuconfig RV the system behavior. if RV +config RV_MON_WIP + depends on PREEMPTIRQ_TRACEPOINTS + select DA_MON_EVENTS_IMPLICIT + bool "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" diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index 8944274d9b41..b41109d2750a 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -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 diff --git a/kernel/trace/rv/monitors/wip/wip.c b/kernel/trace/rv/monitors/wip/wip.c index 08950e09b823..123827db0a03 100644 --- a/kernel/trace/rv/monitors/wip/wip.c +++ b/kernel/trace/rv/monitors/wip/wip.c @@ -10,11 +10,9 @@ #define MODULE_NAME "wip" -/* - * XXX: include required tracepoint headers, e.g., - * #include - */ #include +#include +#include /* * This is the self-generated part of the monitor. Generally, there is no need @@ -37,17 +35,17 @@ DECLARE_DA_MON_PER_CPU(wip, char); * are translated into model's event. * */ -static void handle_preempt_disable(void *data, /* XXX: fill header */) +static void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip) { da_handle_event_wip(preempt_disable_wip); } -static void handle_preempt_enable(void *data, /* XXX: fill header */) +static void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip) { - da_handle_event_wip(preempt_enable_wip); + da_handle_init_event_wip(preempt_enable_wip); } -static void handle_sched_waking(void *data, /* XXX: fill header */) +static void handle_sched_waking(void *data, struct task_struct *task) { da_handle_event_wip(sched_waking_wip); } @@ -60,9 +58,9 @@ static int start_wip(void) 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); + rv_attach_trace_probe("wip", preempt_disable, handle_preempt_disable); + rv_attach_trace_probe("wip", preempt_enable, handle_preempt_enable); + rv_attach_trace_probe("wip", sched_waking, handle_sched_waking); return 0; } @@ -71,9 +69,9 @@ static void stop_wip(void) { rv_wip.enabled = 0; - rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable); - rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable); - rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking); + rv_detach_trace_probe("wip", preempt_disable, handle_preempt_disable); + rv_detach_trace_probe("wip", preempt_enable, handle_preempt_enable); + rv_detach_trace_probe("wip", sched_waking, handle_sched_waking); da_monitor_destroy_wip(); } @@ -108,5 +106,5 @@ module_init(register_wip); module_exit(unregister_wip); MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); -MODULE_DESCRIPTION("wip"); +MODULE_AUTHOR("Daniel Bristot de Oliveira "); +MODULE_DESCRIPTION("wip: wakeup in preemptive - per-cpu sample monitor."); From patchwork Thu Jun 16 08:44:52 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883559 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 4C102C43334 for ; Thu, 16 Jun 2022 08:46:54 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359672AbiFPIqx (ORCPT ); Thu, 16 Jun 2022 04:46:53 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35280 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359817AbiFPIqH (ORCPT ); Thu, 16 Jun 2022 04:46:07 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [IPv6:2604:1380:4601:e00::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id C89525DBCF; Thu, 16 Jun 2022 01:46:04 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 54CC4B81E20; Thu, 16 Jun 2022 08:46:03 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id B4031C341C0; Thu, 16 Jun 2022 08:45:57 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369162; bh=QJ0oWYDc7OPYMH2YBsjWV6GFlgp05pic3QCtSoNMg0Q=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=TA4JNrII/Pxpf01tIQdJIhstCWVXVR2JAXyErTSf1rpdgdwniKmxVfad/mMY1NucH 0da+h9p2JRmZoK9gb9a1GlcVDoZQM3ycM4I+IW/vyyfBbbcJQ/GLwSVKkEeuItTuTw f8yyEgBC+DF8sQM0H18rNNuDIxh16JINOVXhkZqdn/Jk5cZ6ft5VQhwd1gppZigLwd dNwrcsK5KK8/MtN9R8XTDJE9YnPIFBcglAFHZCLC9Alzt/+bqvT51e9WLn2bm1kNek LEwkShhbDtcqjc7tQU+bSfSXroUlCNfddZvWbLspj+Uml9Ktd1HuuUcbDPPt+7R9oE p6A6vWCI27/ww== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 10/20] rv/monitor: Add the wwnr monitor skeleton created by dot2k Date: Thu, 16 Jun 2022 10:44:52 +0200 Message-Id: <7d1b2238aa5c805501ae3dc80b213d06f6588cb3.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Per task wakeup while not running (wwnr) monitor, generated by dot2k with this command line: $ dot2k -d wwnr.dot -t per_task The model is: ----- %< ----- digraph state_automaton { center = true; size = "7,11"; {node [shape = plaintext, style=invis, label=""] "__init_not_running"}; {node [shape = ellipse] "not_running"}; {node [shape = plaintext] "not_running"}; {node [shape = plaintext] "running"}; "__init_not_running" -> "not_running"; "not_running" [label = "not_running", color = green3]; "not_running" -> "not_running" [ label = "wakeup" ]; "not_running" -> "running" [ label = "switch_in" ]; "running" [label = "running"]; "running" -> "not_running" [ label = "switch_out" ]; { rank = min ; "__init_not_running"; "not_running"; } } ----- >% ----- This model is broken, the reason is that a task can be running in the processor without being set as RUNNABLE. Think about a task about to sleep: 1: set_current_state(TASK_UNINTERRUPTIBLE); 2: schedule(); And then imagine an IRQ happening in between the lines one and two, waking the task up. BOOM, the wakeup will happen while the task is running. Q: Why do we need this model, so? A: To test the reactors. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- kernel/trace/rv/monitors/wwnr/wwnr.c | 115 +++++++++++++++++++++++++++ kernel/trace/rv/monitors/wwnr/wwnr.h | 38 +++++++++ 2 files changed, 153 insertions(+) create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h diff --git a/kernel/trace/rv/monitors/wwnr/wwnr.c b/kernel/trace/rv/monitors/wwnr/wwnr.c new file mode 100644 index 000000000000..8ba01f0f0df8 --- /dev/null +++ b/kernel/trace/rv/monitors/wwnr/wwnr.c @@ -0,0 +1,115 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "wwnr" + +/* + * XXX: include required tracepoint headers, e.g., + * #include + */ +#include + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "wwnr.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +struct rv_monitor rv_wwnr; +DECLARE_DA_MON_PER_TASK(wwnr, char); + +/* + * This is the instrumentation part of the monitor. + * + * This is the section where manual work is required. Here the kernel events + * are translated into model's event. + * + */ +static void handle_switch_in(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event_wwnr(p, switch_in_wwnr); +} + +static void handle_switch_out(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event_wwnr(p, switch_out_wwnr); +} + +static void handle_wakeup(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event_wwnr(p, wakeup_wwnr); +} + +static int start_wwnr(void) +{ + int retval; + + retval = da_monitor_init_wwnr(); + if (retval) + return retval; + + rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in); + rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out); + rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup); + + return 0; +} + +static void stop_wwnr(void) +{ + rv_wwnr.enabled = 0; + + rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in); + rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out); + rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup); + + da_monitor_destroy_wwnr(); +} + +/* + * This is the monitor register section. + */ +struct rv_monitor rv_wwnr = { + .name = "wwnr", + .description = "auto-generated wwnr", + .start = start_wwnr, + .stop = stop_wwnr, + .reset = da_monitor_reset_all_wwnr, + .enabled = 0, +}; + +int register_wwnr(void) +{ + rv_register_monitor(&rv_wwnr); + return 0; +} + +void unregister_wwnr(void) +{ + if (rv_wwnr.enabled) + stop_wwnr(); + + rv_unregister_monitor(&rv_wwnr); +} + +module_init(register_wwnr); +module_exit(unregister_wwnr); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("wwnr"); diff --git a/kernel/trace/rv/monitors/wwnr/wwnr.h b/kernel/trace/rv/monitors/wwnr/wwnr.h new file mode 100644 index 000000000000..f3dc160642bf --- /dev/null +++ b/kernel/trace/rv/monitors/wwnr/wwnr.h @@ -0,0 +1,38 @@ +enum states_wwnr { + not_running_wwnr = 0, + running_wwnr, + state_max_wwnr +}; + +enum events_wwnr { + switch_in_wwnr = 0, + switch_out_wwnr, + wakeup_wwnr, + event_max_wwnr +}; + +struct automaton_wwnr { + char *state_names[state_max_wwnr]; + char *event_names[event_max_wwnr]; + char function[state_max_wwnr][event_max_wwnr]; + char initial_state; + char final_states[state_max_wwnr]; +}; + +struct automaton_wwnr automaton_wwnr = { + .state_names = { + "not_running", + "running" + }, + .event_names = { + "switch_in", + "switch_out", + "wakeup" + }, + .function = { + { running_wwnr, -1, not_running_wwnr }, + { -1, not_running_wwnr, -1 }, + }, + .initial_state = not_running_wwnr, + .final_states = { 1, 0 }, +}; From patchwork Thu Jun 16 08:44:53 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883560 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 2AA64CCA47D for ; Thu, 16 Jun 2022 08:46:55 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1376276AbiFPIqy (ORCPT ); Thu, 16 Jun 2022 04:46:54 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34788 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359719AbiFPIqM (ORCPT ); Thu, 16 Jun 2022 04:46:12 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 6900E5DBE3; Thu, 16 Jun 2022 01:46:09 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 142C6B822A7; Thu, 16 Jun 2022 08:46:08 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 72F85C36AE3; Thu, 16 Jun 2022 08:46:02 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369166; bh=q2Nr0Do4T+VNYLHE7CNjZGMYVNS+vUVZnmunR/+50Bw=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=gJVathLlY3OD6ZpvCxIhusEa0wKl7DfZl2hmahA85dBfvkwSZMRr848G5H3M/D3I4 WYLpEnGcX9vbipHbR6zdmVE7tckIrY1MqK8Zb2BMfZ29RDwK8C4izI5Dn7Q0LXFzih etj5tlof1DhAz74Jcw43VJwu19gSSc6ph8UbQPwyBVZSTJQKpg5bJqmhnSy+pt98GK y/zyUYcbgEIt/FyWVIUgpDzJJfoVwBio2itHw2AimTVWGGawPr6rGnbGgDeW9fythz WeIKDZC1Lq/iLIRisM2vovWbP1v8fNBRc7IgE11nlBUjHU6utqR+AWXoX9Ryc1uxUH vLduASJbhVUuA== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 11/20] rv/monitor: wwnr instrumentation and Makefile/Kconfig entries Date: Thu, 16 Jun 2022 10:44:53 +0200 Message-Id: <944694879f67c0e635815ac57154be477a1b9108.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Adds the instrumentation to the previously created wwnr monitor, as an example of the developer work. It also adds a Makefile, Kconfig and tracepoint entries. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira Reported-by: kernel test robot --- include/trace/events/rv.h | 12 +++++++++ kernel/trace/rv/Kconfig | 8 ++++++ kernel/trace/rv/Makefile | 1 + kernel/trace/rv/monitors/wwnr/wwnr.c | 38 ++++++++++++---------------- 4 files changed, 37 insertions(+), 22 deletions(-) diff --git a/include/trace/events/rv.h b/include/trace/events/rv.h index 4e0dabffcf29..00f11a8dac3b 100644 --- a/include/trace/events/rv.h +++ b/include/trace/events/rv.h @@ -122,6 +122,18 @@ DECLARE_EVENT_CLASS(error_da_monitor_id, __entry->event, __entry->state) ); + +#ifdef CONFIG_RV_MON_WWNR +/* id is the pid of the task */ +DEFINE_EVENT(event_da_monitor_id, event_wwnr, + TP_PROTO(int id, char *state, char *event, char *next_state, bool safe), + TP_ARGS(id, state, event, next_state, safe)); + +DEFINE_EVENT(error_da_monitor_id, error_wwnr, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); +#endif /* CONFIG_RV_MON_WWNR */ + #endif /* CONFIG_DA_MON_EVENTS_ID */ #endif /* _TRACE_RV_H */ diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index e9246b0bec9d..fba2ace2a22b 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -34,6 +34,14 @@ 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 + select DA_MON_EVENTS_ID + bool "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 diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index b41109d2750a..af0ff9a46418 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -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 diff --git a/kernel/trace/rv/monitors/wwnr/wwnr.c b/kernel/trace/rv/monitors/wwnr/wwnr.c index 8ba01f0f0df8..3fe1ad9125d3 100644 --- a/kernel/trace/rv/monitors/wwnr/wwnr.c +++ b/kernel/trace/rv/monitors/wwnr/wwnr.c @@ -10,11 +10,8 @@ #define MODULE_NAME "wwnr" -/* - * XXX: include required tracepoint headers, e.g., - * #include - */ #include +#include /* * This is the self-generated part of the monitor. Generally, there is no need @@ -37,21 +34,20 @@ DECLARE_DA_MON_PER_TASK(wwnr, char); * are translated into model's event. * */ -static 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, unsigned int prev_state) { - struct task_struct *p = /* XXX: how do I get p? */; - da_handle_event_wwnr(p, switch_in_wwnr); -} + /* start monitoring only after the first suspension */ + if (prev_state == TASK_INTERRUPTIBLE) + da_handle_init_event_wwnr(p, switch_out_wwnr); + else + da_handle_event_wwnr(p, switch_out_wwnr); -static void handle_switch_out(void *data, /* XXX: fill header */) -{ - struct task_struct *p = /* XXX: how do I get p? */; - da_handle_event_wwnr(p, switch_out_wwnr); + da_handle_event_wwnr(n, switch_in_wwnr); } -static void handle_wakeup(void *data, /* XXX: fill header */) +static void handle_wakeup(void *data, struct task_struct *p) { - struct task_struct *p = /* XXX: how do I get p? */; da_handle_event_wwnr(p, wakeup_wwnr); } @@ -63,9 +59,8 @@ static int start_wwnr(void) if (retval) return retval; - rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in); - rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out); - rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup); + rv_attach_trace_probe("wwnr", sched_switch, handle_switch); + rv_attach_trace_probe("wwnr", sched_wakeup, handle_wakeup); return 0; } @@ -74,9 +69,8 @@ static void stop_wwnr(void) { rv_wwnr.enabled = 0; - rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in); - rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out); - rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup); + rv_detach_trace_probe("wwnr", sched_switch, handle_switch); + rv_detach_trace_probe("wwnr", sched_wakeup, handle_wakeup); da_monitor_destroy_wwnr(); } @@ -111,5 +105,5 @@ module_init(register_wwnr); module_exit(unregister_wwnr); MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); -MODULE_DESCRIPTION("wwnr"); +MODULE_AUTHOR("Daniel Bristot de Oliveira "); +MODULE_DESCRIPTION("wwnr: wakeup while not running monitor."); From patchwork Thu Jun 16 08:44:54 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883562 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id AC182C433EF for ; Thu, 16 Jun 2022 08:47:02 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359761AbiFPIq7 (ORCPT ); Thu, 16 Jun 2022 04:46:59 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35410 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359763AbiFPIqP (ORCPT ); Thu, 16 Jun 2022 04:46:15 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 669B55DBF2; Thu, 16 Jun 2022 01:46:12 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 0AB3F61D58; Thu, 16 Jun 2022 08:46:12 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 30AA5C34114; Thu, 16 Jun 2022 08:46:07 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369171; bh=grmOOJEABOUWSLsmON0N5vfx4AsyJeKk/lzSYDXQuAc=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=DTY3ENwZTwWJjVFmf3d8cZapqdgKg04KqBmzF7ZSEizxdHvP6TVJb6ZfFcqm/L0J9 SJy7P8n1/fj09JBIS/zn1oEWF4WP4P1geag7MfWfWChIriJzUf+O7Z1qBm8gBUn/jm mLJ8rvkEAbnXNf68FvaapWWYxCmWE/Mr7LBiLn0uK7w7FLp4uTyBflfE3ArR9Nmo8n oEFeYeU6QBYXGLD76hHai2iGUPSPOlIf/4aBGYItuyyxk2ke4j2Ogq1VfYGX9Px7CD Oc/pnKkvws43h0JqfyHkxjS9mV7ldrrJbIlnxnxwaAo21H41RcKaB3WyOKIv0Gim2i wCvzBKrggFEiQ== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 12/20] rv/reactor: Add the printk reactor Date: Thu, 16 Jun 2022 10:44:54 +0200 Message-Id: <338533d97b25ccedb862691d866cfcc8e0b69cb3.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Sample reactor that printks the reaction message. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- kernel/trace/rv/Kconfig | 8 ++++++ kernel/trace/rv/Makefile | 3 ++- kernel/trace/rv/reactor_printk.c | 43 ++++++++++++++++++++++++++++++++ 3 files changed, 53 insertions(+), 1 deletion(-) create mode 100644 kernel/trace/rv/reactor_printk.c diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index fba2ace2a22b..be8e3dab0a52 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -52,4 +52,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 + bool "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 diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index af0ff9a46418..a13c750a35c1 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -1,6 +1,7 @@ # SPDX-License-Identifier: GPL-2.0 obj-$(CONFIG_RV) += rv.o -obj-$(CONFIG_RV_REACTORS) += rv_reactors.o obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o +obj-$(CONFIG_RV_REACTORS) += rv_reactors.o +obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o diff --git a/kernel/trace/rv/reactor_printk.c b/kernel/trace/rv/reactor_printk.c new file mode 100644 index 000000000000..6a7bbf3fc03f --- /dev/null +++ b/kernel/trace/rv/reactor_printk.c @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * Printk RV reactor: + * Prints the exception msg to the kernel message log. + * + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira + * + */ +#include +#include +#include +#include +#include +#include + +static void rv_printk_reaction(char *msg) +{ + printk_deferred(msg); +} + +struct rv_reactor rv_printk = { + .name = "printk", + .description = "prints the exception msg to the kernel message log", + .react = rv_printk_reaction +}; + +int register_react_printk(void) +{ + rv_register_reactor(&rv_printk); + return 0; +} + +void unregister_react_printk(void) +{ + rv_unregister_reactor(&rv_printk); +} + +module_init(register_react_printk); +module_exit(unregister_react_printk); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Daniel Bristot de Oliveira"); +MODULE_DESCRIPTION("printk rv reactor: printk if an exception is hit"); From patchwork Thu Jun 16 08:44:55 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883561 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id E5952C433EF for ; Thu, 16 Jun 2022 08:47:00 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359812AbiFPIq6 (ORCPT ); Thu, 16 Jun 2022 04:46:58 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35516 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359806AbiFPIqV (ORCPT ); Thu, 16 Jun 2022 04:46:21 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id EE5B25DBDA; Thu, 16 Jun 2022 01:46:18 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 961E0B822AA; Thu, 16 Jun 2022 08:46:17 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id E5140C341C6; Thu, 16 Jun 2022 08:46:11 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369176; bh=/xZOtWjGXYTz/J2Aiul1V0Ty93/KmzjcS55M0yhNTrk=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=doipYHKQb4BVV959SwfH4xhLIiAmUC5P4OunW4L2kNxA9OtOLSCnkPlNZOgrlGMsi isfWf0Pnq+kQvZSDgukxH4KI/r4JZcDYxWmwl43YLk6lO7mGBuBEymZy2Wo+yly2c/ fqD9AnlWYXxGkOfVNpX7EgnsxN1l2gh1B85LDPSAENAoPVkjgciHotNZhnqsDEfciq PSz9lcfbd1j7zHhU+QyZw/8H5qhdNX2DdxB/6Qf3AFrD9X+F9/VWx+CEsPLan7FDqK aX3qP9BLjHe5yBIucBu3a/cNVEGXFtx8FpFzMTlQQCIK8SIBCu7n2e5XnDN3p8XTmt TpuXFnt10mvig== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 13/20] rv/reactor: Add the panic reactor Date: Thu, 16 Jun 2022 10:44:55 +0200 Message-Id: <67e522ab57e64eee313af508a8c70f3cce33e525.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org 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. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira Reported-by: kernel test robot --- kernel/trace/rv/Kconfig | 8 ++++++ kernel/trace/rv/Makefile | 1 + kernel/trace/rv/reactor_panic.c | 44 +++++++++++++++++++++++++++++++++ 3 files changed, 53 insertions(+) create mode 100644 kernel/trace/rv/reactor_panic.c diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index be8e3dab0a52..91a17b13a080 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -60,4 +60,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 + bool "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 diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index a13c750a35c1..963d14875b45 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -5,3 +5,4 @@ obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o obj-$(CONFIG_RV_REACTORS) += rv_reactors.o obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o +obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o diff --git a/kernel/trace/rv/reactor_panic.c b/kernel/trace/rv/reactor_panic.c new file mode 100644 index 000000000000..9d8d78a337a3 --- /dev/null +++ b/kernel/trace/rv/reactor_panic.c @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * Panic RV reactor: + * Prints the exception msg to the kernel message log and panic(). + * + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira + * + */ + +#include +#include +#include +#include +#include +#include + +static void rv_panic_reaction(char *msg) +{ + panic(msg); +} + +struct rv_reactor rv_panic = { + .name = "panic", + .description = "panic the system if an exception is found.", + .react = rv_panic_reaction +}; + +int register_react_panic(void) +{ + rv_register_reactor(&rv_panic); + return 0; +} + +void unregister_react_panic(void) +{ + rv_unregister_reactor(&rv_panic); +} + +module_init(register_react_panic); +module_exit(unregister_react_panic); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Daniel Bristot de Oliveira"); +MODULE_DESCRIPTION("panic rv reactor: panic if an exception is found"); From patchwork Thu Jun 16 08:44:56 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883563 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id CEC11CCA47F for ; Thu, 16 Jun 2022 08:47:02 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1376315AbiFPIrB (ORCPT ); Thu, 16 Jun 2022 04:47:01 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35660 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359828AbiFPIq0 (ORCPT ); Thu, 16 Jun 2022 04:46:26 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 06DA45DBFB; Thu, 16 Jun 2022 01:46:21 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 7FD6961D7D; Thu, 16 Jun 2022 08:46:21 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id A4E1FC3411F; Thu, 16 Jun 2022 08:46:16 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369180; bh=AsbZF+dPE9MyAO08LOdMaZboB3eGu/DKKj0s/59Krgo=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=hHiRWJN37UzYBjcNs6TwwYPT/qa5l40fPvCS/LdGYZO/lkTwMchctWTZ9zxnnWG2O rGFz4BdT+dUqIXYYZcSRpnJUfqnd8Tx7OgGHzD8Z9QI7L2WOLQkyuh0LyiGvCD1Z37 OuBMrNiPcKQfHpumivsIsBuKH9XcmLg16WAGQ0m9TqF0Jy8oK6OVSdg0TuHLLd/Qq3 6apCEb/i6gODLkTobNqiRgU7+l0hMO7caoVgBkujwxW24Buk9scenf5NYS9isNkHmN By4U7IJ7vM168PrImP1c/M8PIM1W15MhxWFzW3SHu5vW92NbDcxj7AlHpj04wTrGDa 1oau/oxhAz/PQ== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 14/20] Documentation/rv: Add a basic documentation Date: Thu, 16 Jun 2022 10:44:56 +0200 Message-Id: <575554f7bebc0278dd3dfad056d4438c2fbab7b3.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Add the runtime-verification.rst document, explaining the basics of RV and how to use the interface. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- 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 diff --git a/Documentation/trace/index.rst b/Documentation/trace/index.rst index f9b7bcb5a630..2d73e8697523 100644 --- a/Documentation/trace/index.rst +++ b/Documentation/trace/index.rst @@ -32,3 +32,4 @@ Linux Tracing Technologies sys-t coresight/index user_events + rv/index diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst new file mode 100644 index 000000000000..92338dceffab --- /dev/null +++ b/Documentation/trace/rv/index.rst @@ -0,0 +1,9 @@ +=================================== +RV - Runtime Verification Interface +=================================== + +.. toctree:: + :maxdepth: 2 + :glob: + + * diff --git a/Documentation/trace/rv/runtime-verification.rst b/Documentation/trace/rv/runtime-verification.rst new file mode 100644 index 000000000000..f51cf69b10d3 --- /dev/null +++ b/Documentation/trace/rv/runtime-verification.rst @@ -0,0 +1,233 @@ +==================== +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 main advantage is that RV can give precise information on the runtime +behavior of the monitored system, without the pitfalls of developing models +that require a re-implementation of the entire system in a modeling language. +Moreover, given an efficient monitoring method, it is possible execute an +*online* verification of a system, enabling the *reaction* for unexpected +events, avoiding, for example, the propagation of a failure on safety-critical +systems. + +Runtime Monitors and Reactors +============================= + +A monitor is the central part of the runtime verification of a system. The +monitor stands in between the formal specification of the desired (or +undesired) behavior, and the trace of the actual system. + +In Linux terms, the runtime verification monitors are encapsulated inside the +*RV monitor* abstraction. A *RV monitor* includes a reference model of the +system, a set of instances of the monitor (per-cpu monitor, per-task monitor, +and so on), and the helper functions that glue the monitor to the system via +trace, as depicted bellow:: + + Linux +---- RV Monitor ----------------------------------+ Formal + Realm | | Realm + +-------------------+ +----------------+ +-----------------+ + | Linux kernel | | Monitor | | Reference | + | Tracing | -> | Instance(s) | <- | Model | + | (instrumentation) | | (verification) | | (specification) | + +-------------------+ +----------------+ +-----------------+ + | | | + | V | + | +----------+ | + | | Reaction | | + | +--+--+--+-+ | + | | | | | + | | | +-> trace output ? | + +------------------------|--|----------------------+ + | +----> panic ? + +-------> + +In addition to the verification and monitoring of the system, a monitor can +react to an unexpected event. The forms of reaction can vary from logging the +event occurrence to the enforcement of the correct behavior to the extreme +action of taking a system down to avoid the propagation of a failure. + +In Linux terms, a *reactor* is an reaction method available for *RV monitors*. +By default, all monitors should provide a trace output of their actions, +which is already a reaction. In addition, other reactions will be available +so the user can enable them as needed. + +For further information about the principles of runtime verification and +RV applied to Linux: + + BARTOCCI, Ezio, et al. *Introduction to runtime verification.* In: Lectures on + Runtime Verification. Springer, Cham, 2018. p. 1-33. + + FALCONE, Ylies, et al. *A taxonomy for classifying runtime verification tools.* + In: International Conference on Runtime Verification. Springer, Cham, 2018. p. + 241-262. + + DE OLIVEIRA, Daniel Bristot, et al. *Automata-based formal analysis and + verification of the real-time Linux kernel.* Ph.D. Thesis, 2020. + +Online RV monitors +================== + +Monitors can be classified as *offline* and *online* monitors. *Offline* +monitor process the traces generated by a system after the events, generally by +reading the trace execution from a permanent storage system. *Online* monitors +process the trace during the execution of the system. Online monitors are said +to be *synchronous* if the processing of an event is attached to the system +execution, blocking the system during the event monitoring. On the other hand, +an *asynchronous* monitor has its execution detached from the system. Each type +of monitor has a set of advantages. For example, *offline* monitors can be +executed on different machines but require operations to save the log to a +file. In contrast, *synchronous online* method can react at the exact moment +a violation occurs. + +Another important aspect regarding monitors is the overhead associated with the +event analysis. If the system generates events at a frequency higher than the +monitor's ability to process them in the same system, only the *offline* +methods are viable. On the other hand, if the tracing of the events incurs +on higher overhead than the simple handling of an event by a monitor, then a +*synchronous online* monitors will incur on lower overhead. + +Indeed, the research presented in: + + 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. + +Shows that for Deterministic Automata models, the synchronous processing of +events in-kernel causes lower overhead than saving the same events to the trace +buffer, not even considering collecting the trace for user-space analysis. +This motivated the development of an in-kernel interface for online monitors. + +For further information about modeling of Linux kernel behavior using automata, +please read: + + DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread + synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems + Architecture, 2020, 107: 101729. + +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:: + + [root@f32 rv]# cat available_monitors + wip + wwnr + +**available_reactors** + +- Reading shows the available reactors, one per line. + +For example:: + + [root@f32 rv]# cat available_reactors + nop + panic + printk + +**enabled_monitors**: + +- Reading 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 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 +- Reading returns the current status of the monitoring + +Note that it does not disable enabled monitors but stop the per-entity +monitors monitoring the events received from the system. + +**reacting_on** + +- Writing "0" prevents reactions for happening +- Writing "1" enable reactions +- Reading returns the current status of the monitoring + +**monitors/** + +Each monitor will have its own directory inside "monitors/". There the +monitor-specific files will be presented. The "monitors/" directory resembles +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 + +**monitors/$MONITOR/desc** + +- Reading shows a description of the monitor *$MONITOR* + +**monitors/$MONITOR/enable** + +- Writing "0" disables the *$MONITOR* +- Writing "1" enables the *$MONITOR* +- Reading return the current status of the *$MONITOR* + +**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 diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 91a17b13a080..21f03fb3101a 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -25,6 +25,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 depends on PREEMPTIRQ_TRACEPOINTS From patchwork Thu Jun 16 08:44:57 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883564 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 1DDD4C43334 for ; Thu, 16 Jun 2022 08:47:17 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359860AbiFPIrP (ORCPT ); Thu, 16 Jun 2022 04:47:15 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:36532 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359780AbiFPIqx (ORCPT ); Thu, 16 Jun 2022 04:46:53 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id DB8EC5DD22; Thu, 16 Jun 2022 01:46:26 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 3F2F061D7D; Thu, 16 Jun 2022 08:46:26 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 64FFDC341C6; Thu, 16 Jun 2022 08:46:21 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369185; bh=RSXtvmUy632JYyL5m1ybJouoonN6y/iJYBvbYk3+LnM=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=UEgxxw1azqcobv9yT9GCnL2tbEEwTQaKkbkQWrR/e1i8p07amaj1zwe55Qzp9zPD9 32c9sexgZwRiXGjsc0vTAsT9eyS8+ctjyUoD71JKHCJbFl81D1Zkv6M4tqStkZJRcN eaqjfN3dH3MGL8PVHtMxn84t5qWPp3l6GAPrN4WhPIf2yxfIxepk2GmKM4WEm1av2/ vAsL3TVitGYnbbzcILJSW9utXZ8ItmwNXsp7sjJxY91BoTMlY0wU+7gA2MI/ZYzTN5 pTl5cZhnqXe7feMyxzrWV/nbwofAmU2tzFwdxpLDh9ZyMJ/OVQ0Vb0L4dvxuhefuRi TyyJPxZi0ThCQ== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 15/20] Documentation/rv: Add deterministic automata monitor synthesis documentation Date: Thu, 16 Jun 2022 10:44:57 +0200 Message-Id: <65c0f41a30850002cac84f143616f932d147251d.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Add the da_monitor_synthesis.rst introduces some concepts behind the Deterministic Automata (DA) monitor synthesis and interface. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- .../trace/rv/da_monitor_synthesis.rst | 284 ++++++++++++++++++ 1 file changed, 284 insertions(+) create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst b/Documentation/trace/rv/da_monitor_synthesis.rst new file mode 100644 index 000000000000..1e1c857d7bbd --- /dev/null +++ b/Documentation/trace/rv/da_monitor_synthesis.rst @@ -0,0 +1,284 @@ +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 automated 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: + +- wip.h: the wip in C +- 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, 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. For instance, using the wip model as input for dot2c results in +the following C representation:: + + enum states_wip { + preemptive_wip = 0, + non_preemptive_wip, + state_max_wip + }; + + enum events_wip { + preempt_disable_wip = 0, + preempt_enable_wip, + sched_waking_wip, + event_max_wip + }; + + struct automaton_wip { + char *state_names[state_max_wip]; + char *event_names[event_max_wip]; + char function[state_max_wip][event_max_wip]; + char initial_state; + char final_states[state_max_wip]; + }; + + struct automaton_wip automaton_wip = { + .state_names = { + "preemptive", + "non_preemptive" + }, + .event_names = { + "preempt_disable", + "preempt_enable", + "sched_waking" + }, + .function = { + { non_preemptive_wip, -1, -1 }, + { -1, preemptive_wip, non_preemptive_wip }, + }, + .initial_state = preemptive_wip, + .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 ? + +-------> + + +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 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. From patchwork Thu Jun 16 08:44:58 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883565 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id DC68DC43334 for ; Thu, 16 Jun 2022 08:47:21 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1376263AbiFPIrS (ORCPT ); Thu, 16 Jun 2022 04:47:18 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:36558 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1376264AbiFPIqx (ORCPT ); Thu, 16 Jun 2022 04:46:53 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 2F9595DD39; Thu, 16 Jun 2022 01:46:31 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id ECA5461D74; Thu, 16 Jun 2022 08:46:30 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 24486C385A2; Thu, 16 Jun 2022 08:46:25 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369190; bh=r3LQRxsB4zvMJAbVYAKgMVYZMxuBkCguR2Xd1O6Gqto=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=ZQpUvZVMbha3cDI+oZladehpZNwnxt/I10aiGs74dcvV7UO3yi9Uty8Oqa4mnGeNS 52KIYOkQ8WjNXY3FwMYqU+RP0f1PzANjDe7pJTn/J/aqCEAcBUU7qBj+xUsA6Lc69J uJ5U8Eu38vYK6aR0X0cLFHl3noTa82euSfsWBofFWWAOW0t/pFfhIEzrlqnw3YIxVG MIZCzoKO+jJ9UGe4XjCnTy+si8pNFzZU91MuoBdUcksM4MWrCqum8mbghUCy7mpE/3 YQxhti9YnXzZXWNBJUlCk8mO6GusqoQD8K87KNDJw3TnZU0lwrN2t6knndqsI9AksG dJT6YTpoOOyMw== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 16/20] Documentation/rv: Add deterministic automata instrumentation documentation Date: Thu, 16 Jun 2022 10:44:58 +0200 Message-Id: <30171062e035a5cf0e64cfa9cbb8e56376ec5101.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Add the da_monitor_instrumentation.rst. It describes the basics of RV monitor instrumentation. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- .../trace/rv/da_monitor_instrumentation.rst | 223 ++++++++++++++++++ 1 file changed, 223 insertions(+) create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst diff --git a/Documentation/trace/rv/da_monitor_instrumentation.rst b/Documentation/trace/rv/da_monitor_instrumentation.rst new file mode 100644 index 000000000000..994110050d93 --- /dev/null +++ b/Documentation/trace/rv/da_monitor_instrumentation.rst @@ -0,0 +1,223 @@ +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 automated 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. + * + */ + 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 *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_wip); + } + +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_wip); + +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_wip); + } + +Finally, the "handle_sched_waking()" will look like:: + + void handle_sched_waking(void *data, struct task_struct *task) + { + da_handle_event_wip(sched_waking_wip); + } + +And the explanation is left for the reader as an exercise. + +Start and Stop functions +------------------------ + +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 *attach* and *detach* the instrumentation to the running +system. The developer must add to the relative function all that is needed to +*attach* and *detach* its monitor to the system. + +For the wip case, these functions were named:: + + start_wip() + stop_wip() + +But no change was required because: by default, these functions *attach* and +*detach* the tracepoints_to_attach, which was enough for this case. + +Instrumentation helpers +-------------------------- + +To complete the instrumentation, the *handler functions* need to be attached to a +kernel event, at the monitoring start phase. + +The RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()" +is used to connect the wip model events to the relative kernel event. dot2k automatically +adds "rv_attach_trace_probe()" function call for each model event in the start phase, as +a suggestion. + +For example, from the wip sample model:: + + 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 probes then need to be detached at the stop phase. From patchwork Thu Jun 16 08:44:59 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883566 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id F039EC433EF for ; Thu, 16 Jun 2022 08:47:44 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359770AbiFPIrn (ORCPT ); Thu, 16 Jun 2022 04:47:43 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35512 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359733AbiFPIqz (ORCPT ); Thu, 16 Jun 2022 04:46:55 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id EFC775DE56; Thu, 16 Jun 2022 01:46:37 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 7B887B822A8; Thu, 16 Jun 2022 08:46:36 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id D8925C385A9; Thu, 16 Jun 2022 08:46:30 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369195; bh=xp5szzRsyHzfmBZJ6GrNJ30mR5ggLppYgYmYnc1wD+A=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=GEsg2uwRt7idQloAWTHYa1DLQYPO5PFJzm3k54Wb2ezoYvOVKC+tXVb5ceBrYBuvO jjnnGpEYiQeRI1bZ2na1IK/JpYKScoTwNeDd+gKbvEtx3tEMojknmJkMXr3E7uIhcA /J8beHNYE8a49M1vRn2BuLyyy0oUDguPk7YJ5rq+RsncWJYMw2goccjS/jQiQO/aCp 3eaYALwZ57Z0v6yVCDQPrPEQfdxQRwfneP3rBedjJaqKahWKUh40B7RpOc3LO7TAxj yEZYbxEUtvakQToeRC/SBq0wrXX2Tr0wFMUxCVwz73J91IZxWQXKpr/MCpo6kJxpTi 45E4vAdjIMUEw== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 17/20] watchdog/dev: Add tracepoints Date: Thu, 16 Jun 2022 10:44:59 +0200 Message-Id: X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Add a set of tracepoints, enabling the observability of the watchdog device interactions with user-space. The events are: watchdog:watchdog_open watchdog:watchdog_close watchdog:watchdog_start watchdog:watchdog_stop watchdog:watchdog_set_timeout watchdog:watchdog_ping watchdog:watchdog_nowayout watchdog:watchdog_set_keep_alive watchdog:watchdog_keep_alive watchdog:watchdog_set_pretimeout watchdog:watchdog_pretimeout Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- drivers/watchdog/watchdog_dev.c | 43 ++++++++++- drivers/watchdog/watchdog_pretimeout.c | 2 + include/linux/watchdog.h | 7 +- include/trace/events/watchdog.h | 101 +++++++++++++++++++++++++ 4 files changed, 143 insertions(+), 10 deletions(-) create mode 100644 include/trace/events/watchdog.h diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c index 54903f3c851e..2f28dc5ab763 100644 --- a/drivers/watchdog/watchdog_dev.c +++ b/drivers/watchdog/watchdog_dev.c @@ -44,6 +44,9 @@ #include /* For watchdog specific items */ #include /* For copy_to_user/put_user/... */ +#define CREATE_TRACE_POINTS +#include + #include "watchdog_core.h" #include "watchdog_pretimeout.h" @@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd) if (watchdog_need_worker(wdd)) { ktime_t t = watchdog_next_keepalive(wdd); - if (t > 0) + if (t > 0) { hrtimer_start(&wd_data->timer, t, HRTIMER_MODE_REL_HARD); + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t)); + } } else { hrtimer_cancel(&wd_data->timer); } @@ -141,7 +146,7 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd) static int __watchdog_ping(struct watchdog_device *wdd) { struct watchdog_core_data *wd_data = wdd->wd_data; - ktime_t earliest_keepalive, now; + ktime_t earliest_keepalive, now, next_keepalive; int err; earliest_keepalive = ktime_add(wd_data->last_hw_keepalive, @@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd) now = ktime_get(); if (ktime_after(earliest_keepalive, now)) { - hrtimer_start(&wd_data->timer, - ktime_sub(earliest_keepalive, now), + next_keepalive = ktime_sub(earliest_keepalive, now); + hrtimer_start(&wd_data->timer, next_keepalive, HRTIMER_MODE_REL_HARD); + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(next_keepalive)); return 0; } wd_data->last_hw_keepalive = now; + trace_watchdog_ping(wdd); if (wdd->ops->ping) err = wdd->ops->ping(wdd); /* ping the watchdog */ else @@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work) wd_data = container_of(work, struct watchdog_core_data, work); mutex_lock(&wd_data->lock); + trace_watchdog_keep_alive(wd_data->wdd); if (watchdog_worker_should_ping(wd_data)) __watchdog_ping(wd_data->wdd); mutex_unlock(&wd_data->lock); @@ -250,6 +258,8 @@ static int watchdog_start(struct watchdog_device *wdd) set_bit(_WDOG_KEEPALIVE, &wd_data->status); + trace_watchdog_start(wdd); + started_at = ktime_get(); if (watchdog_hw_running(wdd) && wdd->ops->ping) { err = __watchdog_ping(wdd); @@ -294,6 +304,7 @@ static int watchdog_stop(struct watchdog_device *wdd) return -EBUSY; } + trace_watchdog_stop(wdd); if (wdd->ops->stop) { clear_bit(WDOG_HW_RUNNING, &wdd->status); err = wdd->ops->stop(wdd); @@ -367,6 +378,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd, if (watchdog_timeout_invalid(wdd, timeout)) return -EINVAL; + trace_watchdog_set_timeout(wdd, timeout); if (wdd->ops->set_timeout) { err = wdd->ops->set_timeout(wdd, timeout); } else { @@ -399,6 +411,8 @@ static int watchdog_set_pretimeout(struct watchdog_device *wdd, if (watchdog_pretimeout_invalid(wdd, timeout)) return -EINVAL; + trace_watchdog_set_pretimeout(wdd, timeout); + if (wdd->ops->set_pretimeout && (wdd->info->options & WDIOF_PRETIMEOUT)) err = wdd->ops->set_pretimeout(wdd, timeout); else @@ -430,6 +444,23 @@ static int watchdog_get_timeleft(struct watchdog_device *wdd, return 0; } +/** + * watchdog_set_nowayout - set nowaout bit + * @wdd: The watchdog device to set nowayoutbit + * @nowayout A boolean on/off switcher + * + * If nowayout boolean is true, the nowayout option is set. No action is + * taken if nowayout is false. + */ +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout) +{ + if (nowayout) { + set_bit(WDOG_NO_WAY_OUT, &wdd->status); + trace_watchdog_nowayout(wdd); + } +} +EXPORT_SYMBOL(watchdog_set_nowayout); + #ifdef CONFIG_WATCHDOG_SYSFS static ssize_t nowayout_show(struct device *dev, struct device_attribute *attr, char *buf) @@ -861,6 +892,8 @@ static int watchdog_open(struct inode *inode, struct file *file) goto out_clear; } + trace_watchdog_open(wdd); + err = watchdog_start(wdd); if (err < 0) goto out_mod; @@ -883,6 +916,7 @@ static int watchdog_open(struct inode *inode, struct file *file) return stream_open(inode, file); out_mod: + trace_watchdog_close(wdd); module_put(wd_data->wdd->ops->owner); out_clear: clear_bit(_WDOG_DEV_OPEN, &wd_data->status); @@ -944,6 +978,7 @@ static int watchdog_release(struct inode *inode, struct file *file) /* make sure that /dev/watchdog can be re-opened */ clear_bit(_WDOG_DEV_OPEN, &wd_data->status); + trace_watchdog_close(wdd); done: running = wdd && watchdog_hw_running(wdd); mutex_unlock(&wd_data->lock); diff --git a/drivers/watchdog/watchdog_pretimeout.c b/drivers/watchdog/watchdog_pretimeout.c index 376a495ab80c..58c391ed2205 100644 --- a/drivers/watchdog/watchdog_pretimeout.c +++ b/drivers/watchdog/watchdog_pretimeout.c @@ -8,6 +8,7 @@ #include #include #include +#include #include "watchdog_core.h" #include "watchdog_pretimeout.h" @@ -107,6 +108,7 @@ void watchdog_notify_pretimeout(struct watchdog_device *wdd) return; } + trace_watchdog_pretimeout(wdd); wdd->gov->pretimeout(wdd); spin_unlock_irqrestore(&pretimeout_lock, flags); } diff --git a/include/linux/watchdog.h b/include/linux/watchdog.h index 99660197a36c..11d93407e492 100644 --- a/include/linux/watchdog.h +++ b/include/linux/watchdog.h @@ -139,12 +139,7 @@ static inline bool watchdog_hw_running(struct watchdog_device *wdd) return test_bit(WDOG_HW_RUNNING, &wdd->status); } -/* Use the following function to set the nowayout feature */ -static inline void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout) -{ - if (nowayout) - set_bit(WDOG_NO_WAY_OUT, &wdd->status); -} +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout); /* Use the following function to stop the watchdog on reboot */ static inline void watchdog_stop_on_reboot(struct watchdog_device *wdd) diff --git a/include/trace/events/watchdog.h b/include/trace/events/watchdog.h new file mode 100644 index 000000000000..145cd6cfaa02 --- /dev/null +++ b/include/trace/events/watchdog.h @@ -0,0 +1,101 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +#undef TRACE_SYSTEM +#define TRACE_SYSTEM watchdog + +#if !defined(_TRACE_WATCHDOG_H) || defined(TRACE_HEADER_MULTI_READ) +#define _TRACE_WATCHDOG_H + +#include + +/* + * These are all events whose sole argument is the watchdog id. + */ +DECLARE_EVENT_CLASS(dev_operations_template, + + TP_PROTO(struct watchdog_device *wdd), + + TP_ARGS(wdd), + + TP_STRUCT__entry( + __field(__u32, id) + ), + + TP_fast_assign( + __entry->id = wdd->id; + ), + + TP_printk("id=%d", + __entry->id) +); + +DEFINE_EVENT(dev_operations_template, watchdog_open, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +DEFINE_EVENT(dev_operations_template, watchdog_close, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +DEFINE_EVENT(dev_operations_template, watchdog_start, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +DEFINE_EVENT(dev_operations_template, watchdog_stop, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +DEFINE_EVENT(dev_operations_template, watchdog_ping, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +DEFINE_EVENT(dev_operations_template, watchdog_nowayout, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +DEFINE_EVENT(dev_operations_template, watchdog_keep_alive, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +DEFINE_EVENT(dev_operations_template, watchdog_pretimeout, + TP_PROTO(struct watchdog_device *wdd), + TP_ARGS(wdd)); + +/* + * These are all events with a device ID and a given timeout. + */ +DECLARE_EVENT_CLASS(watchdog_timeout_template, + + TP_PROTO(struct watchdog_device *wdd, u64 timeout), + + TP_ARGS(wdd, timeout), + + TP_STRUCT__entry( + __field(__u32, id) + __field(__u64, timeout) + ), + + TP_fast_assign( + __entry->id = wdd->id; + __entry->timeout = timeout; + ), + + TP_printk("id=%d timeout=%llus", + __entry->id, __entry->timeout) +); + +DEFINE_EVENT(watchdog_timeout_template, watchdog_set_timeout, + TP_PROTO(struct watchdog_device *wdd, u64 timeout), + TP_ARGS(wdd, timeout)); + +DEFINE_EVENT(watchdog_timeout_template, watchdog_set_pretimeout, + TP_PROTO(struct watchdog_device *wdd, u64 timeout), + TP_ARGS(wdd, timeout)); + +DEFINE_EVENT(watchdog_timeout_template, watchdog_set_keep_alive, + TP_PROTO(struct watchdog_device *wdd, u64 timeout), + TP_ARGS(wdd, timeout)); + +#endif /* _TRACE_WATCHDOG_H */ + +/* This part must be outside protection */ +#include From patchwork Thu Jun 16 08:45:00 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883567 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id A69EDC43334 for ; Thu, 16 Jun 2022 08:47:49 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1376276AbiFPIrs (ORCPT ); Thu, 16 Jun 2022 04:47:48 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35272 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1376322AbiFPIrB (ORCPT ); Thu, 16 Jun 2022 04:47:01 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 247B95DE76; Thu, 16 Jun 2022 01:46:41 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 7777361D98; Thu, 16 Jun 2022 08:46:40 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 9AF2BC385A5; Thu, 16 Jun 2022 08:46:35 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369199; bh=rp8p1in6XSjjIlPwwGB/IGry0t0yANStwOH4/NCPCDo=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=pbySOll6TmqwMkFntyeSC8x46dH4x6gdNN6wbzr5oDqlfw0sULtu8nf/VLZxspWCr OzePsT8wvbtEETPG+FxaTFMs3oU2FRk4rgSVRjGsQ14avuq2iIwcpZ5J9y964DFn4u 4Xn7I047eE+5laGCB919zyLxMn6/z9zZsw4Pj6Tt+BqKDSY2MoSF2yjAiMidp2q8Wz onKY7WCg9iBdrxGUQKGfVMlVuJC+WJPUAyVb3Mvm2sJ2Zxmibs8S8ip7Re5U/nJTf8 JjRknpOwgUN2RzWvguDQnDaFzPDQ9VpaDk0lTPNRercXt0YkkNcWplnY52+1HJqrnd kHNc2jSQ8C9LA== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 18/20] rv/monitor: Add safe watchdog monitor Date: Thu, 16 Jun 2022 10:45:00 +0200 Message-Id: <6366fdc89d65b8d9b14ccd1e42fa0d793fbe9f73.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org The watchdog is an essential building block for the usage of Linux in safety-critical systems because it allows the system to be monitored from an external element - the watchdog hardware, acting as a safety-monitor. A user-space application controls the watchdog device via the watchdog interface. This application, hereafter safety_app, enables the watchdog and periodically pets the watchdog upon correct completion of the safety related processing. If the safety_app, for any reason, stops pinging the watchdog, the watchdog hardware can set the system in a fail-safe state. For example, shutting the system down. Given the importance of the safety_app / watchdog hardware couple, the interaction between these software pieces also needs some sort of monitoring. In other words, "who monitors the monitor?" The safe watchdog (safe_wtd) RV monitor monitors the interaction between the safety_app and the watchdog device, enforcing the correct sequence of events that leads the system to a safe state. Furthermore, the safety_app can monitor the RV monitor by collecting the events generated by the RV monitor itself via tracing interface. In this way, closing the monitoring loop with the safety_app. To reach a safe state, the safe_wtd RV monitor requires the safety_app to: - Open the watchdog device - Start the watchdog - Set a timeout - ping at least once The RV monitor also avoids some undesired actions. For example, to have other threads to touch the watchdog. The monitor also has a set of options, enabled via kernel command line/module options. They are: - watchdog_id: the device id to monitor (default 0). - dont_stop: once enabled, do not allow the RV monitor to be stopped (default off); - safe_timeout: define a maximum safe value that an user-space application can set as the watchdog timeout (default unlimited). - check_timeout: After every ping, check if the time left in the watchdog is less than or equal to the last timeout set for the watchdog. It only works for watchdog devices that provide the get_timeleft() function (default off). For further information, please refer to: Documentation/trace/rv/watchdog-monitor.rst The monitor specification was developed together with Gabriele Paoloni, in the context of the Linux Foundation Elisa Project. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- include/trace/events/rv.h | 11 + kernel/trace/rv/Kconfig | 10 + kernel/trace/rv/Makefile | 1 + kernel/trace/rv/monitors/safe_wtd/safe_wtd.c | 300 +++++++++++++++++++ kernel/trace/rv/monitors/safe_wtd/safe_wtd.h | 84 ++++++ 5 files changed, 406 insertions(+) create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.c create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h diff --git a/include/trace/events/rv.h b/include/trace/events/rv.h index 00f11a8dac3b..895eb3435ed7 100644 --- a/include/trace/events/rv.h +++ b/include/trace/events/rv.h @@ -66,6 +66,17 @@ DEFINE_EVENT(error_da_monitor, error_wip, TP_PROTO(char *state, char *event), TP_ARGS(state, event)); #endif /* CONFIG_RV_MON_WIP */ + +#ifdef CONFIG_RV_MON_SAFE_WTD +DEFINE_EVENT(event_da_monitor, event_safe_wtd, + TP_PROTO(char *state, char *event, char *next_state, bool safe), + TP_ARGS(state, event, next_state, safe)); + +DEFINE_EVENT(error_da_monitor, error_safe_wtd, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_SAFE_WTD */ + #endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */ #ifdef CONFIG_DA_MON_EVENTS_ID diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 21f03fb3101a..b14ae63e792b 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -45,6 +45,16 @@ config RV_MON_WWNR illustrates the usage of per-task monitor. The model is broken on purpose: it serves to test reactors. +config RV_MON_SAFE_WTD + select DA_MON_EVENTS_IMPLICIT + bool "Safety watchdog" + help + Enable safe_wtd, this monitor observes the interaction + between a user-space safety monitor and a watchdog device. + + For futher information see: + Documentation/trace/rv/safety-monitor.rst + config RV_REACTORS bool "Runtime verification reactors" default y if RV diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index 963d14875b45..904db96c7eae 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -3,6 +3,7 @@ obj-$(CONFIG_RV) += rv.o obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o +obj-$(CONFIG_RV_MON_SAFE_WTD) += monitors/safe_wtd/safe_wtd.o obj-$(CONFIG_RV_REACTORS) += rv_reactors.o obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o diff --git a/kernel/trace/rv/monitors/safe_wtd/safe_wtd.c b/kernel/trace/rv/monitors/safe_wtd/safe_wtd.c new file mode 100644 index 000000000000..9856e0770d0d --- /dev/null +++ b/kernel/trace/rv/monitors/safe_wtd/safe_wtd.c @@ -0,0 +1,300 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +#include +#include + +#define MODULE_NAME "safe_wtd" + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "safe_wtd.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +struct rv_monitor rv_safe_wtd; +DECLARE_DA_MON_GLOBAL(safe_wtd, char); + +/* + * custom: safe_timeout is the maximum value a watchdog monitor + * can set. This value is registered here to duplicate the information. + * In this way, a miss-behaving monitor can be detected. + */ +static int safe_timeout = ~0; +module_param(safe_timeout, int, 0444); + +/* + * custom: if check_timeout is set, the monitor will check if the time left + * in the watchdog is less than or equals to the last safe timeout set by + * user-space. This check is done after each ping. In this way, if any + * code by-passed the watchdog dev interface setting a higher (so unsafe) + * timeout, this monitor will catch the side effect and react. + */ +static int last_timeout_set = 0; +static int check_timeout = 0; +module_param(check_timeout, int, 0444); + +/* + * custom: if dont_stop is set the monitor will react if stopped. + */ +static int dont_stop = 0; +module_param(dont_stop, int, 0444); + +/* + * custom: there are some states that are kept after the watchdog is closed. + * For example, the nowayout state. + * + * Thus, the RV monitor needs to keep track of these states after a start/stop + * of the RV monitor itself, and should not reset after each restart - keeping the + * know state until the system shutdown. + * + * If for an unknown reason an RV monitor would like to reset the RV monitor at each + * RV monitor start, set it to one. + */ +static int reset_on_restart = 0; +module_param(reset_on_restart, int, 0444); + +/* + * open_pid takes note of the first thread that opened the watchdog. + * + * Any other thread that generates an event will cause an "other_threads" + * event in the monitor. + */ +static int open_pid = 0; + +/* + * watchdog_id: the watchdog to monitor + */ +static int watchdog_id = 0; +module_param(watchdog_id, int, 0444); + +static void handle_nowayout(void *data, struct watchdog_device *wdd) +{ + if (wdd->id != watchdog_id) + return; + + da_handle_init_run_event_safe_wtd(nowayout_safe_wtd); +} + +static void handle_close(void *data, struct watchdog_device *wdd) +{ + if (wdd->id != watchdog_id) + return; + + if (open_pid && current->pid != open_pid) { + da_handle_init_run_event_safe_wtd(other_threads_safe_wtd); + } else { + da_handle_event_safe_wtd(close_safe_wtd); + open_pid = 0; + } +} + +static void handle_open(void *data, struct watchdog_device *wdd) +{ + if (wdd->id != watchdog_id) + return; + + if (open_pid && current->pid != open_pid) { + da_handle_init_run_event_safe_wtd(other_threads_safe_wtd); + } else { + da_handle_init_run_event_safe_wtd(open_safe_wtd); + open_pid = current->pid; + } +} + +static void blocked_events(void *data, struct watchdog_device *wdd) +{ + if (wdd->id != watchdog_id) + return; + + if (open_pid && current->pid != open_pid) { + da_handle_init_run_event_safe_wtd(other_threads_safe_wtd); + return; + } + da_handle_event_safe_wtd(other_threads_safe_wtd); +} + +static void blocked_events_timeout(void *data, struct watchdog_device *wdd, u64 timeout) +{ + blocked_events(data, wdd); +} + +static void handle_ping(void *data, struct watchdog_device *wdd) +{ + char msg[128]; + unsigned int timeout; + + if (wdd->id != watchdog_id) + return; + + if (open_pid && current->pid != open_pid) { + da_handle_init_run_event_safe_wtd(other_threads_safe_wtd); + return; + } + + da_handle_event_safe_wtd(ping_safe_wtd); + + if (!check_timeout) + return; + + if (wdd->ops->get_timeleft) { + timeout = wdd->ops->get_timeleft(wdd); + if (timeout > last_timeout_set) { + snprintf(msg, 128, + "watchdog timeout is %u > than previously set (%d)\n", + timeout, last_timeout_set); + cond_react(msg); + } + } else { + snprintf(msg, 128, "error getting timeout: option not supported\n"); + cond_react(msg); + } +} + +static void handle_set_safe_timeout(void *data, struct watchdog_device *wdd, u64 timeout) +{ + char msg[128]; + + if (wdd->id != watchdog_id) + return; + + if (open_pid && current->pid != open_pid) { + da_handle_init_run_event_safe_wtd(other_threads_safe_wtd); + return; + } + + da_handle_event_safe_wtd(set_safe_timeout_safe_wtd); + + if (timeout > safe_timeout) { + snprintf(msg, 128, "set safety timeout is too high: %d", (int) timeout); + cond_react(msg); + } + + if (check_timeout) + last_timeout_set = timeout; +} + +static void handle_start(void *data, struct watchdog_device *wdd) +{ + if (wdd->id != watchdog_id) + return; + + if (open_pid && current->pid != open_pid) { + da_handle_init_run_event_safe_wtd(other_threads_safe_wtd); + return; + } + + da_handle_event_safe_wtd(start_safe_wtd); +} + +static void handle_stop(void *data, struct watchdog_device *wdd) +{ + if (wdd->id != watchdog_id) + return; + + if (open_pid && current->pid != open_pid) { + da_handle_init_run_event_safe_wtd(other_threads_safe_wtd); + return; + } + + da_handle_event_safe_wtd(stop_safe_wtd); +} + +static int mon_started = 0; + +static int start_safe_wtd_monitor(void) +{ + int retval; + + if (!mon_started || reset_on_restart) { + retval = da_monitor_init_safe_wtd(); + if (retval) + return retval; + + mon_started = 1; + } + + rv_attach_trace_probe("safe_wtd", watchdog_close, handle_close); + rv_attach_trace_probe("safe_wtd", watchdog_nowayout, handle_nowayout); + rv_attach_trace_probe("safe_wtd", watchdog_open, handle_open); + rv_attach_trace_probe("safe_wtd", watchdog_ping, handle_ping); + rv_attach_trace_probe("safe_wtd", watchdog_set_timeout, handle_set_safe_timeout); + rv_attach_trace_probe("safe_wtd", watchdog_start, handle_start); + rv_attach_trace_probe("safe_wtd", watchdog_stop, handle_stop); + rv_attach_trace_probe("safe_wtd", watchdog_set_keep_alive, blocked_events_timeout); + rv_attach_trace_probe("safe_wtd", watchdog_keep_alive, blocked_events); + rv_attach_trace_probe("safe_wtd", watchdog_set_pretimeout, blocked_events_timeout); + rv_attach_trace_probe("safe_wtd", watchdog_pretimeout, blocked_events); + + return 0; +} + +static void stop_safe_wtd_monitor(void) +{ + if (dont_stop) + cond_react("dont_stop safe_wtd is set."); + + rv_safe_wtd.enabled = 0; + + rv_detach_trace_probe("safe_wtd", watchdog_close, handle_close); + rv_detach_trace_probe("safe_wtd", watchdog_nowayout, handle_nowayout); + rv_detach_trace_probe("safe_wtd", watchdog_open, handle_open); + rv_detach_trace_probe("safe_wtd", watchdog_ping, handle_ping); + rv_detach_trace_probe("safe_wtd", watchdog_set_timeout, handle_set_safe_timeout); + rv_detach_trace_probe("safe_wtd", watchdog_start, handle_start); + rv_detach_trace_probe("safe_wtd", watchdog_stop, handle_stop); + rv_detach_trace_probe("safe_wtd", watchdog_set_keep_alive, blocked_events_timeout); + rv_detach_trace_probe("safe_wtd", watchdog_keep_alive, blocked_events); + rv_detach_trace_probe("safe_wtd", watchdog_set_pretimeout, blocked_events_timeout); + rv_detach_trace_probe("safe_wtd", watchdog_pretimeout, blocked_events); + + da_monitor_destroy_safe_wtd(); +} + +/* + * This is the monitor register section. + */ +struct rv_monitor rv_safe_wtd = { + .name = "safe_wtd", + .description = "A watchdog monitor guarding a safety monitor actions", + .start = start_safe_wtd_monitor, + .stop = stop_safe_wtd_monitor, + .reset = da_monitor_reset_all_safe_wtd, + .enabled = 0, +}; + +int register_safe_wtd(void) +{ + rv_register_monitor(&rv_safe_wtd); + return 0; +} + +void unregister_safe_wtd(void) +{ + if (rv_safe_wtd.enabled) + stop_safe_wtd_monitor(); + + rv_unregister_monitor(&rv_safe_wtd); +} + +module_init(register_safe_wtd); +module_exit(unregister_safe_wtd); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Daniel Bristot de Oliveira "); +MODULE_DESCRIPTION("Safe watchdog RV monitor"); diff --git a/kernel/trace/rv/monitors/safe_wtd/safe_wtd.h b/kernel/trace/rv/monitors/safe_wtd/safe_wtd.h new file mode 100644 index 000000000000..835c9d0979f6 --- /dev/null +++ b/kernel/trace/rv/monitors/safe_wtd/safe_wtd.h @@ -0,0 +1,84 @@ +enum states_safe_wtd { + init_safe_wtd = 0, + closed_running_safe_wtd, + closed_running_nwo_safe_wtd, + nwo_safe_wtd, + opened_safe_wtd, + opened_nwo_safe_wtd, + reopened_safe_wtd, + safe_safe_wtd, + safe_nwo_safe_wtd, + set_safe_wtd, + set_nwo_safe_wtd, + started_safe_wtd, + started_nwo_safe_wtd, + stoped_safe_wtd, + state_max_safe_wtd +}; + +enum events_safe_wtd { + close_safe_wtd = 0, + nowayout_safe_wtd, + open_safe_wtd, + other_threads_safe_wtd, + ping_safe_wtd, + set_safe_timeout_safe_wtd, + start_safe_wtd, + stop_safe_wtd, + event_max_safe_wtd +}; + +struct automaton_safe_wtd { + char *state_names[state_max_safe_wtd]; + char *event_names[event_max_safe_wtd]; + char function[state_max_safe_wtd][event_max_safe_wtd]; + char initial_state; + char final_states[state_max_safe_wtd]; +}; + +struct automaton_safe_wtd automaton_safe_wtd = { + .state_names = { + "init", + "closed_running", + "closed_running_nwo", + "nwo", + "opened", + "opened_nwo", + "reopened", + "safe", + "safe_nwo", + "set", + "set_nwo", + "started", + "started_nwo", + "stoped" + }, + .event_names = { + "close", + "nowayout", + "open", + "other_threads", + "ping", + "set_safe_timeout", + "start", + "stop" + }, + .function = { + { -1, nwo_safe_wtd, opened_safe_wtd, init_safe_wtd, -1, -1, -1, -1 }, + { -1, closed_running_nwo_safe_wtd, reopened_safe_wtd, closed_running_safe_wtd, -1, -1, -1, -1 }, + { -1, closed_running_nwo_safe_wtd, started_nwo_safe_wtd, closed_running_nwo_safe_wtd, -1, -1, -1, -1 }, + { -1, nwo_safe_wtd, opened_nwo_safe_wtd, nwo_safe_wtd, -1, -1, -1, -1 }, + { init_safe_wtd, -1, -1, -1, -1, -1, started_safe_wtd, -1 }, + { nwo_safe_wtd, -1, -1, -1, -1, -1, started_nwo_safe_wtd, -1 }, + { closed_running_safe_wtd, -1, -1, -1, -1, set_safe_wtd, -1, opened_safe_wtd }, + { closed_running_safe_wtd, -1, -1, -1, safe_safe_wtd, -1, -1, stoped_safe_wtd }, + { closed_running_nwo_safe_wtd, -1, -1, -1, safe_nwo_safe_wtd, -1, -1, -1 }, + { -1, -1, -1, -1, safe_safe_wtd, -1, -1, -1 }, + { -1, -1, -1, -1, safe_nwo_safe_wtd, -1, -1, -1 }, + { closed_running_safe_wtd, -1, -1, -1, -1, set_safe_wtd, -1, stoped_safe_wtd }, + { closed_running_nwo_safe_wtd, -1, -1, -1, -1, set_nwo_safe_wtd, -1, -1 }, + { init_safe_wtd, -1, -1, -1, -1, -1, -1, -1 }, + }, + .initial_state = init_safe_wtd, + .final_states = { 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 }, +}; From patchwork Thu Jun 16 08:45:01 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883568 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 0FBA0C433EF for ; Thu, 16 Jun 2022 08:48:07 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359777AbiFPIsG (ORCPT ); Thu, 16 Jun 2022 04:48:06 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35518 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1376340AbiFPIrn (ORCPT ); Thu, 16 Jun 2022 04:47:43 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [IPv6:2604:1380:4601:e00::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 7A5F05DBC3; Thu, 16 Jun 2022 01:46:47 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id F380AB822A8; Thu, 16 Jun 2022 08:46:45 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 5C79FC34114; Thu, 16 Jun 2022 08:46:40 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369204; bh=gBQRWBS65y6AvIyCwVqPSalZ1C7O6+dSSnUu2L6tC1E=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=ZnPKHDm+hw0xeu3XjfXSFkk3nBbOw9zwMNEI5QYfS/YfXuEr07Oh9+Ng3UBULq8LH 8fF0cBc1U/iBvFiJdWpI3QBGyzIH2mp6LjnH/jovSW4gNcIi8glxTm5y/BKlYVHjiw o/joIBUeGM9qpE9/Rr1Zn3lcDQBMl1hzy9b8CNWgJwL/EtVacBYqjyMptONl7Tz0fT X5gnWkdwuUNVnsHZqawBvhaenF7wSokk6ickmOiCr170mzCuBTtYIv/JNQhzd/8WpX d8zeMvGq9VRR0LLeM8ZuJeUOMLzdM90jDLzKb/Qgn3CR5/8W8BKfFzGbh9DP3Pw2JE iM7pBvT8px/yA== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 19/20] rv/safety_app: Add a safety_app sample Date: Thu, 16 Jun 2022 10:45:01 +0200 Message-Id: X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org This is the sample code of a safety application that uses the watchdog as a safety monitor and the RV monitors to monitor this interaction/get feedback from kernel about the watchdog states. This tool first creates a trace instance to follow the RV events and then enables RV monitor. After that, the tool configures the watchdog and starts running the main loop. The main loop runs a use-case-specific function, like checking the system. If the system is running as expected, it pings the watchdog. After pinging the watchdog, the tool then collects trace information to see if the RV monitor received the expected events and is in a safe/safe_nwo state. For further information, run safety_app --help The safety-app specification was developed together with Gabriele Paoloni, in the context of the Linux Foundation Elisa Project. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- tools/verification/safety_app/Makefile | 51 ++ tools/verification/safety_app/safety_app.c | 614 +++++++++++++++++++++ 2 files changed, 665 insertions(+) create mode 100644 tools/verification/safety_app/Makefile create mode 100644 tools/verification/safety_app/safety_app.c diff --git a/tools/verification/safety_app/Makefile b/tools/verification/safety_app/Makefile new file mode 100644 index 000000000000..002531022e45 --- /dev/null +++ b/tools/verification/safety_app/Makefile @@ -0,0 +1,51 @@ +NAME := safety_app +VERSION := 0.1 + +# From libtracefs: +# Makefiles suck: This macro sets a default value of $(2) for the +# variable named by $(1), unless the variable has been set by +# environment or command line. This is necessary for CC and AR +# because make sets default values, so the simpler ?= approach +# won't work as expected. +define allow-override + $(if $(or $(findstring environment,$(origin $(1))),\ + $(findstring command line,$(origin $(1)))),,\ + $(eval $(1) = $(2))) +endef + +# Allow setting CC and AR, or setting CROSS_COMPILE as a prefix. +$(call allow-override,CC,$(CROSS_COMPILE)gcc) +$(call allow-override,AR,$(CROSS_COMPILE)ar) +$(call allow-override,STRIP,$(CROSS_COMPILE)strip) +$(call allow-override,PKG_CONFIG,pkg-config) +$(call allow-override,LD_SO_CONF_PATH,/etc/ld.so.conf.d/) +$(call allow-override,LDCONFIG,ldconfig) + +INSTALL = install +FOPTS := -flto=auto -ffat-lto-objects -fexceptions -fstack-protector-strong \ + -fasynchronous-unwind-tables -fstack-clash-protection +WOPTS := -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -Wno-maybe-uninitialized + +TRACEFS_HEADERS := $$($(PKG_CONFIG) --cflags libtracefs) + +CFLAGS := -O -g -DVERSION=\"$(VERSION)\" $(FOPTS) $(WOPTS) $(TRACEFS_HEADERS) +LDFLAGS := -ggdb +LIBS := $$($(PKG_CONFIG) --libs libtracefs) +FILES := Makefile +BINDIR := /usr/bin + +OBJ := $(NAME).o + +.PHONY: all +all: $(OBJ) + $(CC) -o $(NAME) $(LDFLAGS) $(OBJ) $(LIBS) + +.PHONY: install +install: + $(INSTALL) -d -m 755 $(DESTDIR)$(BINDIR) + $(INSTALL) $(NAME) -m 755 $(DESTDIR)$(BINDIR) + $(STRIP) $(DESTDIR)$(BINDIR)/$(NAME) + +.PHONY: clean +clean: + @rm -rf *~ $(OBJ) $(NAME) diff --git a/tools/verification/safety_app/safety_app.c b/tools/verification/safety_app/safety_app.c new file mode 100644 index 000000000000..143ebe17dfc9 --- /dev/null +++ b/tools/verification/safety_app/safety_app.c @@ -0,0 +1,614 @@ +// SPDX-License-Identifier: LGPL-2.1 +/* + * This is the starting point for a safety monitor. + * + * The safety_check() function is where you need to add your own code. + * + * Copyright: Red Hat, Inc. Daniel Bristot de Oliveira + */ +#define _GNU_SOURCE +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#define MAX_PATH 1024 + +static int config_watchdog_id; +static char config_watchdog_path[MAX_PATH]; +static int config_nowayout; +static char config_nowayout_path[MAX_PATH]; +static long long config_timeout = 10; +static long config_cycles; +static long config_monitor_period = 1; +static char *config_rv_monitor = "safe_wtd"; +static char *config_rv_reactor = "panic"; +static int config_stop_monitor = 0; +static int config_restart_monitor = 0; + +/* + * print_msg - print a message to stdout + */ +void print_msg(const char *fmt, ...) +{ + char message[1024]; + va_list ap; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stdout, "%s", message); + fflush(NULL); +} + +/* + * ================================================================== + * The code section bellow is responsible for enabling the RV monitor. + * ================================================================== + */ + +/* + * __disable_rv_monitor - disables the RV monitor + * + * Unconditionally disables the RV monitor and set the reactor to nop. + */ +static void __disable_rv_monitor(char *monitor) +{ + char path[MAX_PATH]; + int retval; + + snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor); + retval = tracefs_instance_file_write(NULL, path, "0\n"); + if (retval < 0) { + perror("Error disabling the RV monitor"); + return; + } + + snprintf(path, MAX_PATH, "rv/monitors/%s/reactors", monitor); + retval = tracefs_instance_file_write(NULL, path, "nop\n"); + if (retval < 0) { + perror("Error disabling the RV reactor"); + return; + } +} + +/* + * disable_rv_monitor - conditionally disables the RV monitor + */ +static void disable_rv_monitor(char *monitor) +{ + if (!config_stop_monitor) + return; + + __disable_rv_monitor(monitor); +} + +/* + * enable_rv_monitor - sets the 'reactor' and enable RV 'monitor' + */ +static int enable_rv_monitor(char *monitor, char *reactor) +{ + char buffer[MAX_PATH]; + char path[MAX_PATH]; + int size = 2; + int retval; + char *on; + + snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor); + on = tracefs_instance_file_read(NULL, path, &size); + if (on && on[0] == '1') { + if (!config_restart_monitor) + return 0; + __disable_rv_monitor(monitor); + } + + snprintf(path, MAX_PATH, "rv/monitors/%s/reactors", monitor); + snprintf(buffer, MAX_PATH, "%s\n", reactor); + retval = tracefs_instance_file_write(NULL, path, buffer); + if (retval < 0) { + perror("Error enabling the RV reactor"); + return -1; + } + + snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor); + retval = tracefs_instance_file_write(NULL, path, "1\n"); + if (retval < 0) { + perror("Error enabling the RV monitor"); + return -1; + } + + return 0; +} + +/* + * ================================================================== + * The code section bellow is responsible for parsing the RV monitor output. + * ================================================================== + */ +struct trace_instance { + struct tracefs_instance *inst; + struct tep_handle *tep; + struct trace_seq *seq; +}; + +int ping_counter = 0; +int last_state_running = 0; + +/* + * handle_safe_wtd_rv_event - parse events from the safe_wtd RV monitor + */ +static int +handle_safe_wtd_rv_event(struct trace_seq *s, struct tep_record *record, + struct tep_event *event, void *context) +{ + char *event_name; + char *state; + int len; + + event_name = tep_get_field_raw(s, event, "event", record, &len, 1); + if (event_name && !strcmp(event_name, "ping")) + ping_counter++; + + state = tep_get_field_raw(s, event, "next_state", record, &len, 0); + if (state && !strncmp(state, "safe", 4)) + last_state_running = 1; + else + last_state_running = 0; + + return 0; +} + +/* + * collect_registered_events - call the existing callback function for the event + * + * If an event has a registered callback function, call it. + * Otherwise, ignore the event. + */ +static int +collect_registered_events(struct tep_event *event, struct tep_record *record, + int cpu, void *context) +{ + struct trace_instance *trace = context; + struct trace_seq *s = trace->seq; + + if (!event->handler) + return 0; + + event->handler(s, record, event, context); + + return 0; +} + +/* + * check_rv_events - parse trace events and check for the desired states + * + * Return 0 if success, 1 otherwise. + */ +static int check_rv_events(struct trace_instance *trace) +{ + int prev_ping_counter = ping_counter; + int retval; + int pings; + + retval = tracefs_iterate_raw_events(trace->tep, trace->inst, NULL, 0, + collect_registered_events, trace); + if (retval < 0) { + print_msg("Error iterating on events\n"); + return 1; + } + + pings = ping_counter - prev_ping_counter; + print_msg("RV read %d ping(s) and is %s the watchdog\n", pings, + last_state_running ? "running" : "not running"); + + /* + * If there is exactly one ping and the last state is running, + * it is safe. + */ + if (pings == 1 && last_state_running) { + /* reset the variable */ + last_state_running = 0; + return 0; + } else { + return 1; + } +} + +/* + * trace_instance_destroy - destroy and free a trace instance + */ +static void trace_instance_destroy(struct trace_instance *trace) +{ + if (!trace) + return; + + if (trace->inst) { + tracefs_instance_destroy(trace->inst); + tracefs_instance_free(trace->inst); + } + + if (trace->seq) + free(trace->seq); + + if (trace->tep) + tep_free(trace->tep); + + free(trace); +} + +/* + * trace_instance_init - create a trace instance to read monitor's event + * + * It is more than the tracefs instance, as it contains other + * things required for the tracing, such as the local events and + * a seq file. + */ +static struct trace_instance *trace_instance_init(void) +{ + struct trace_instance *trace; + + trace = calloc(1, sizeof(*trace)); + if (!trace) + return NULL; + + trace->seq = calloc(1, sizeof(*trace->seq)); + if (!trace->seq) + goto destroy_instance; + + trace_seq_init(trace->seq); + + trace->inst = tracefs_instance_create("safety_app"); + if (!trace->inst) + goto destroy_instance; + + trace->tep = tracefs_local_events(NULL); + if (!trace->tep) + goto destroy_instance; + + /* + * register for both monitors, it is free. + */ + tep_register_event_handler(trace->tep, -1, "rv", "event_safe_wtd", + handle_safe_wtd_rv_event, trace); + tracefs_event_enable(trace->inst, "rv", "event_safe_wtd"); + + return trace; + +destroy_instance: + trace_instance_destroy(trace); + return NULL; +} + +/* + * ================================================================== + * The code section bellow are helper functions to use a watchdog device. + * ================================================================== + */ + +/* + * set_nowayout - set the watchdog's nowayout option + */ +static int set_nowayout(char *nowayout_path) +{ + int nowayout_fd; + int retval; + + print_msg("nowayout\n"); + + nowayout_fd = open(nowayout_path, O_WRONLY); + if (nowayout_path < 0) { + perror("Error opening nowayout fd"); + return -1; + } + + retval = write(nowayout_fd, "1", 1); + if (retval != 1) { + perror("Error setting nowayout"); + close(nowayout_fd); + return -1; + } + + close(nowayout_fd); + return 0; +} + +/* + * open_watchdog - open watchdog at the watchdog_path + */ +static int open_watchdog(char *watchdog_path) +{ + int watchdog_fd; + + print_msg("open %s\n", watchdog_path); + + watchdog_fd = open(watchdog_path, O_WRONLY); + if (watchdog_fd < 0) { + perror("Error opening watchdog"); + return -1; + } + + return watchdog_fd; +} + +/* + * set_timeout - set the timeout in seconds for the previously opened watchdog_fd + */ +static int set_timeout(int watchdog_fd, int timeout) +{ + int retval; + + print_msg("set_timeout %d\n", timeout); + + retval = ioctl(watchdog_fd, WDIOC_SETTIMEOUT, &timeout); + if (retval) { + perror("Error set_timeout"); + return -1; + } + + return 0; +} + +/* + * ping - ping (or pet) the watchdog + */ +static int ping(int watchdog_fd) +{ + int retval; + + print_msg("ping\n"); + + retval = write(watchdog_fd, "1", 1); + if (retval != 1) { + perror("Error resseting watchdog"); + return -1; + } + + return 0; +} + +/* + * stop - try to the watchdog + * + * Writing "V" to the watchdog is a special case. Unless nowayout is set, + * it will stop the watchdog device. + */ +static void stop(int watchdog_fd) +{ + int retval; + + print_msg("stop\n"); + + retval = write(watchdog_fd, "V", 1); + if (retval != 1) + perror("Error disabling the watchdog"); +} + +/* + * usage - print usage message + */ +static void usage(char *usage, int exitval) +{ + int i; + + static const char * const msg[] = { + " usage: safety_app [-i id] [-t timeout in seconds ] [-n nowayout_path] \\", + " [-c cycles] [-p period] [-N] \\", + " [-N] [-r reactor] [-s] [-R] \\", + " [-h] \\", + "", + "Watchdog options", + " -i/--id: watchdog id", + " -t/--timeout: watchdog timeout", + " -n/--nowayout: set nowayout", + "", + "Safety monitor options", + " -c/--cycles: run cycle nr ping, 0 means forever (default)", + " -p/--period: monitor loop period", + "", + "RV monitor options", + " -r/--reactor set the reactor (panic is automatically set if no other reactor is passed)", + " -s/--stop-mon stop the rv monitor at the end of the execution", + " -R/--restart-mon restart the monitor if already started", + "", + "Generic options", + " -h/--help: print help message", + NULL, + }; + + if (usage) + fprintf(stderr, "%s\n", usage); + + fprintf(stderr, "sample safety monitor (version %s)\n", VERSION); + + for (i = 0; msg[i]; i++) + fprintf(stderr, "%s\n", msg[i]); + exit(exitval); +} + +static long long get_long_from_str(char *start) +{ + long value; + char *end; + + errno = 0; + value = strtoll(start, &end, 10); + if (errno || start == end) { + fprintf(stderr, "Invalid value '%s'", start); + return -1; + } + + return value; +} + +static int parse_args(int argc, char **argv) +{ + int c; + + while (1) { + static struct option long_options[] = { + {"help", no_argument, 0, 'h'}, + {"id", required_argument, 0, 'i'}, + {"timeout", required_argument, 0, 't'}, + {"nowayout", optional_argument, 0, 'n'}, + {"cycles", required_argument, 0, 'c'}, + {"period", required_argument, 0, 'p'}, + {"reactor", required_argument, 0, 'r'}, + {"stop-mon", no_argument, 0, 's'}, + {"restart-mon", no_argument, 0, 'R'}, + {0, 0, 0, 0} + }; + + /* getopt_long stores the option index here. */ + int option_index = 0; + + c = getopt_long(argc, argv, "hi:t:n::c:p:r:sR", + long_options, &option_index); + + /* Detect the end of the options. */ + if (c == -1) + break; + + switch (c) { + case 'i': + config_watchdog_id = get_long_from_str(optarg); + break; + case 't': + config_timeout = get_long_from_str(optarg); + break; + case 'n': + config_nowayout = 1; + if (optarg) + strncpy(config_nowayout_path, optarg, MAX_PATH); + break; + case 'c': + config_cycles = get_long_from_str(optarg); + break; + case 'p': + config_monitor_period = get_long_from_str(optarg); + break; + case 'r': + config_rv_reactor = optarg; + break; + case 's': + config_stop_monitor = 1; + break; + case 'R': + config_restart_monitor = 1; + break; + case 'h': + usage("Help message", 0); + break; + default: + usage("Invalid option", 1); + } + } + + if (!strlen(config_nowayout_path)) { + snprintf(config_nowayout_path, MAX_PATH, + "/sys/devices/virtual/watchdog/watchdog%i/nowayout", + config_watchdog_id); + } + + if (config_monitor_period > config_timeout) + usage("Monitor period higher than the watchdog timeout.\n", 1); + + snprintf(config_watchdog_path, MAX_PATH, "/dev/watchdog%d", config_watchdog_id); + + return 0; +} + +/* + * safety_check - check if the system is working properly + * + * This is the function where the system check will be actually done. + * It will be periodically called by the safety_app. If it returns + * true, the watchdog will be pinged and the system will continue running. + * If this function returns false, the safety_app will not ping the + * watchdog and will exit with an error. + */ +static int safety_check(void) +{ + /* + * Add your code here. + * + * Return 0 to make the safety monitor to skip the watchdog ping and + * exit with error, or just kill the system yourself. + */ + return 1; +} + +int main(int argc, char *argv[]) +{ + struct trace_instance *trace; + int exit_val = 1; + int watchdog_fd; + long cycles = 0; + int retval; + + parse_args(argc, argv); + + trace = trace_instance_init(); + + retval = enable_rv_monitor(config_rv_monitor, config_rv_reactor); + if (retval) { + perror("Cannot proceed without the RV monitor"); + goto out_destroy_trace; + } + + if (config_nowayout) + set_nowayout(config_nowayout_path); + + watchdog_fd = open_watchdog(config_watchdog_path); + if (watchdog_fd < 0) { + perror("Error opening watchdog"); + exit(1); + } + + if (config_timeout) { + retval = set_timeout(watchdog_fd, config_timeout); + if (retval) + goto out_close_watchdog; + } + + retval = check_rv_events(trace); + if (retval) { + print_msg("RV monitor returned a failure, it is not safe to continue\n"); + goto out_close_watchdog; + } + + do { + retval = safety_check(); + if (!retval) + goto out_close_watchdog; + + retval = ping(watchdog_fd); + if (retval) + goto out_close_watchdog; + + retval = check_rv_events(trace); + if (retval) { + print_msg("RV monitor returned a failure, it is not safe to continue\n"); + goto out_close_watchdog; + } + + sleep(config_monitor_period); + } while (!config_cycles || ++cycles < config_cycles); + + stop(watchdog_fd); + + exit_val = 0; + +out_close_watchdog: + close(watchdog_fd); + disable_rv_monitor(config_rv_monitor); +out_destroy_trace: + trace_instance_destroy(trace); + return exit_val; +} From patchwork Thu Jun 16 08:45:02 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Daniel Bristot de Oliveira X-Patchwork-Id: 12883569 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 27B97CCA47A for ; Thu, 16 Jun 2022 08:48:09 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1376361AbiFPIsI (ORCPT ); Thu, 16 Jun 2022 04:48:08 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:36352 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359805AbiFPIrq (ORCPT ); Thu, 16 Jun 2022 04:47:46 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 472C15E75A; Thu, 16 Jun 2022 01:46:52 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id C56B0B822B0; Thu, 16 Jun 2022 08:46:50 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 1E2BAC341CB; Thu, 16 Jun 2022 08:46:44 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369209; bh=bdDAcR0HjZJFIwntvamKxxbeGIgFlMkgAgwD/aNZMUg=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=qhE2Z1kxHHmMoI0ytsNbGs77YMejHNJmaQtWeg8xugywbbBIzbfHqyFiQNPBhtObH abEEZl3AQ2thYv6cQkW0TnUD9D8Jr/uTalMn2P8Gl8ceipda9naJk48Ed9028lDNqU iWjp77uNu8NI6zIsKMsE7/8FfcbGv1LKF0pLv7m4ZFWsrXaaO09pLt3bt3y8zOPPqK 9mzngcI00N/QEJwYaK/4EdcOANSGxrb+NW4AI/8m2xHnpv7uF8Ocw7ZiarCe+44AsC ceu24HWEe6HuDE+298zLQCqd6rrZKqHzOoKFm91cxf9it/pTCjG/Bwtx7U+2cJ+grt iGQwmqDrdDokA== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 20/20] Documentation/rv: Add watchdog-monitor documentation Date: Thu, 16 Jun 2022 10:45:02 +0200 Message-Id: <129a431c1a12610fa7b44f76ce73aa8058f55bc6.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-trace-devel@vger.kernel.org Adds documentation about the safe_wtd and safe_wtd_nwo RV monitors, and their usage via a safety application. Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++++++++++++++++ 1 file changed, 250 insertions(+) create mode 100644 Documentation/trace/rv/watchdog-monitor.rst diff --git a/Documentation/trace/rv/watchdog-monitor.rst b/Documentation/trace/rv/watchdog-monitor.rst new file mode 100644 index 000000000000..2b142fb31572 --- /dev/null +++ b/Documentation/trace/rv/watchdog-monitor.rst @@ -0,0 +1,250 @@ +Watchdog monitor +---------------- + +The watchdog is an essential building block for the usage of Linux in +safety-critical systems because it allows the system to be monitored from +an external element - the watchdog hardware, acting as a safety-monitor. + +A user-space application controls the watchdog device via the watchdog +interface. This application, hereafter safety_app, enables the watchdog +and periodically pets the watchdog upon correct completion of the safety +related processing. + +If the safety_app, for any reason, stops pinging the watchdog, +the watchdog hardware can set the system in a fail-safe state. For +example, shutting the system down. + +Given the importance of the safety_app / watchdog hardware couple, +the interaction between these software pieces also needs some +sort of monitoring. In other words, "who monitors the monitor?" + +The safe watchdog (safe_wtd) RV monitor monitors the interaction between +the safety_app and the watchdog device, enforcing the correct sequence of +events that leads the system to a safe state. + +Furthermore, the safety_app can monitor the RV monitor by collecting the +events generated by the RV monitor itself via tracing interface. In this way, +closing the monitoring loop with the safety_app. + +A diagram of the components and their interactions is:: + + user-space: + +--------------------------------+ + | safety_app |-----------+ + +--------------------------------+ | + | ^ | + | Configure | Enable and | + | | check data | + ===================+====================+=============== | + kernel-space: | | | + v v | + +----------+ instr. +-------------+ | + | watchdog | ----------->| RV Monitor |----+ | + | device | +-------------+ | | + +----------+ | | + | | | + | | | + ================+====================================== | | + hardware: | | | + v | +-> Bring the system + +--------------------+ +----> to a safe state, + | watchdog hardware |---------------------------> e.g., halt. + +--------------------+ + +Sample safety_app +----------------- + +The user-space safety_app sample code in ``tools/verification/safety_app/`` +serves to illustrate the usage of the RV monitors for this use-case, as +well as the starting point to the development of a user-specific safety_app. + +Watchdog events +--------------- + +The RV monitor observes the watchdog by using instrumentation to +process the events generated by the interaction between the +safety_app and the watchdog device layer in kernel. + +The monitored events are: + + - watchdog:watchdog_open: open the watchdog device; + - watchdog:watchdog_close: close the watchdog device; + - watchdog:watchdog_start: start the watchdog; + - watchdog:watchdog_stop: stop the watchdog; + - watchdog:watchdog_set_timeout: set the watchdog timeout; + - watchdog:watchdog_ping: reprogram the watchdog with the previously set + timeout; + - watchdog:watchdog_nowayout: prevents the watchdog from stopping; + - watchdog:watchdog_set_keep_alive: set an intermediary ping to overcome + the limitation of a hardware watchdog maximum timeout being shorter than + the timeout set by the user-space tool; + - watchdog:watchdog_keep_alive: the execution of the function that runs the + intermediary keep alive ping; + +RV monitor events +----------------- + +The RV monitor monitors the relevant events as an outside observer, +interpreting all the components (the hardware; the watchdog device +interface; and the safety monitor) as an integrated component. + +The events selected for the monitor are: + + - other_threads: an event generated by any thread other than the + one that set nowayout or open the watchdog the last time. + - open: a thread opens the watchdog to manipulate it; + - close: a thread closes the watchdog; + - start: starts the watchdog countdown; + - stop: stops the watchdog; + - set_safe_timeout: configures the watchdog with a given timeout; + - ping: resets the watchdog countdown with the previously configured timeout; + - nowayout: prevents the watchdog to be stopped until the system's shutdown; + - sched_keep_alive: schedules a kernel worker to ping the watchdog if the + timeout is longer than the watchdog hardware can handle. + - keep_alive: executes the previously scheduled watchdog ping; + +Noting that the events that does not appear in the automata models are +considered blocked events, and their execution will always cause the +RV monitor to react to an unexpected event. + +RV monitor specification +------------------------ + +The monitor's goal is to assess a set of specifications that conducts the +system to a safe state. + +These specifications are: + + - 1: Once open, only one process manipulates the watchdog; + - 2: Following 1, the keep-alive mechanisms will not be used; + - 3: If required, nowayout will be set before opening the watchdog; + - 4: A safe timeout must be set; + - 5: At least one ping must be made before entering the safe/safe_nwo states + - 6: The RV monitor does not react if the watchdog is closed without stopping. + But the hardware watchdog is expected to react. + +Deterministic automata monitors +------------------------------- + +Following the specifications, a deterministic automata monitor +was developed. The monitor is modeled as Deterministic Automata model. + +The deterministic automata model for safe_wtd is:: + + #==================================# other_threads + H H ----------------+ + -----------> H init H | + H H <---------------+ + #==================================# + | | ^ + | | | close + | | +----------------------------------------------------+ + | | | + | | open | + | +------------------------------------------------------+ | + | | | + | nowayout | | + v | | + nowayout +-------------------+ | | + other_threads | | nowayout | | + +---------------- | nwo |<-------------------------------------+ | | + | | | | | | + +---------------> | | <+ | | | + +-------------------+ | | | | + | | | | | + | open | close | | | + v | | | | + +-------------------+ | | | | + | opened_nwo | -+ | | | + +-------------------+ | | | + | | | | + | start | | | + v | | | + +-------------------+ | | | + +---------------> | started_nwo | -+ | | | + | +-------------------+ | | | | + | | | | | | + | open | set_safe_timeout | | | | + | v | | | | + | +-------------------+ | | | | + | | set_nwo | | | | | + | +-------------------+ | | | | + | | | | | | + | +-------------+ | ping | | | | + | | | | | | | | + | | ping v v | | | | + | | +-------------------+ | | | | + | +-----------| safe_nwo | | | | | + | +-------------------+ | | | | + | | | | | | + | | close | close | | | + | v v | | | + | +----------------------------------+ nowayout | | | + | | | other_threads | | | + | | closed_running_nwo | ----------------+ | | | + | | | | | | | + +---------------- | | <---------------+ | | | + +----------------------------------+ | | | + | nowayout ^ | | | + +-----------------------------+ | | | + | | | + | | | + +-------------------+ +--------+ | | | + | | | |------+---+ | + | started | start | opened | | | + +---------------- | | <-------- | |>-----+-------+ + | +-------------------+ +--------+ | ^ + | | | | + | | set_safe_timeout +-------------+-------+ + | v | | + | +-------------------+ | | + | | | | | + | | set | | | + +----------+---------------> | | | | + | | +-------------------+ | | + | | | | | + | | | ping | | + | | v | | + | | +-------------------+ ping | | + | | | | -------+ | | + | | +---- | safe | | | | + | | | | | <------+ | | + | | | +-------------------+ | | + | | | | | | + | | stop | | stop | | + | | | v | | + | | | +-------------------+ close | | + | +-----------+---> | stopped |-------------+ | + | | +-------------------+ | + | +---+ | + | | close | + | v | + | other_threads +----------------------------------------+ | + | +--------------> | | | + | | | closed_running | | + | +--------------- | |--------------+ + | +----------------------------------------+ + | | ^ + | open | | close + | v | + | set_safe_timeout +-------------------+ + +-------------------------> | reopened | + +-------------------+ + +It is important to note that the events sched_keep_alive and keep_alive +are not allowed in the monitor (they are said to be blocked events). +The execution of any blocked events leads the RV monitor to react. + +Additional options +------------------ + +The RV monitor also has a set of options enabled via kernel command +line/module options. They are: + + - watchdog_id: the device id to monitor (default 0); + - dont_stop: once enabled, do not allow the RV monitor to be stopped (default off); + - safe_timeout: define a maximum safe value that a user-space application can + set as the watchdog timeout (default unlimited); + - check_timeout: After every ping, check if the time left in the watchdog is less + than or equal to the last timeout set for the watchdog. It only works for watchdog + devices that provide the get_timeleft() function (default off);