Skip to content

Commit

Permalink
rv: Add runtime reactors interface
Browse files Browse the repository at this point in the history
A runtime monitor can cause a reaction to the detection of an
exception on the model's execution. By default, the monitors have
tracing reactions, printing the monitor output via tracepoints.
But other reactions can be added (on-demand) via this interface.

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

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

   For example:
     # cat available_reactors
     nop
     panic
     printk

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

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

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

Link: https://lkml.kernel.org/r/1794eb994637457bdeaa6bad0b8263d2f7eece0c.1659052063.git.bristot@kernel.org

Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
Cc: Guenter Roeck <linux@roeck-us.net>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Will Deacon <will@kernel.org>
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Marco Elver <elver@google.com>
Cc: Dmitry Vyukov <dvyukov@google.com>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Shuah Khan <skhan@linuxfoundation.org>
Cc: Gabriele Paoloni <gpaoloni@redhat.com>
Cc: Juri Lelli <juri.lelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: Tao Zhou <tao.zhou@linux.dev>
Cc: Randy Dunlap <rdunlap@infradead.org>
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Cc: linux-trace-devel@vger.kernel.org
Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
  • Loading branch information
Daniel Bristot de Oliveira authored and Steven Rostedt (Google) committed Jul 30, 2022
1 parent 102227b commit 04acadc
Show file tree
Hide file tree
Showing 6 changed files with 581 additions and 0 deletions.
17 changes: 17 additions & 0 deletions include/linux/rv.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,24 @@
union rv_task_monitor {
};

#ifdef CONFIG_RV_REACTORS
struct rv_reactor {
const char *name;
const char *description;
void (*react)(char *msg);
};
#endif

struct rv_monitor {
const char *name;
const char *description;
bool enabled;
int (*enable)(void);
void (*disable)(void);
void (*reset)(void);
#ifdef CONFIG_RV_REACTORS
void (*react)(char *msg);
#endif
};

bool rv_monitoring_on(void);
Expand All @@ -39,5 +50,11 @@ int rv_register_monitor(struct rv_monitor *monitor);
int rv_get_task_monitor_slot(void);
void rv_put_task_monitor_slot(int slot);

#ifdef CONFIG_RV_REACTORS
bool rv_reacting_on(void);
int rv_unregister_reactor(struct rv_reactor *reactor);
int rv_register_reactor(struct rv_reactor *reactor);
#endif /* CONFIG_RV_REACTORS */

#endif /* CONFIG_RV */
#endif /* _LINUX_RV_H */
11 changes: 11 additions & 0 deletions kernel/trace/rv/Kconfig
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,14 @@ menuconfig RV
theorem proving). RV works by analyzing the trace of the system's
actual execution, comparing it against a formal specification of
the system behavior.

config RV_REACTORS
bool "Runtime verification reactors"
default y
depends on RV
help
Enables the online runtime verification reactors. A runtime
monitor can cause a reaction to the detection of an exception
on the model's execution. By default, the monitors have
tracing reactions, printing the monitor output via tracepoints,
but other reactions can be added (on-demand) via this interface.
1 change: 1 addition & 0 deletions kernel/trace/rv/Makefile
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
# SPDX-License-Identifier: GPL-2.0

obj-$(CONFIG_RV) += rv.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
9 changes: 9 additions & 0 deletions kernel/trace/rv/rv.c
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,10 @@ static int create_monitor_dir(struct rv_monitor_def *mdef)
goto out_remove_root;
}

retval = reactor_populate_monitor(mdef);
if (retval)
goto out_remove_root;

return 0;

out_remove_root:
Expand Down Expand Up @@ -669,6 +673,7 @@ static const struct file_operations monitoring_on_fops = {

static void destroy_monitor_dir(struct rv_monitor_def *mdef)
{
reactor_cleanup_monitor(mdef);
rv_remove(mdef->root_d);
}

Expand Down Expand Up @@ -747,6 +752,7 @@ int rv_unregister_monitor(struct rv_monitor *monitor)
int __init rv_init_interface(void)
{
struct dentry *tmp;
int retval;

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

turn_monitoring_on();

Expand Down
35 changes: 35 additions & 0 deletions kernel/trace/rv/rv.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,16 +18,51 @@ struct rv_interface {
#define rv_remove tracefs_remove

#define MAX_RV_MONITOR_NAME_SIZE 32
#define MAX_RV_REACTOR_NAME_SIZE 32

extern struct mutex rv_interface_lock;

#ifdef CONFIG_RV_REACTORS
struct rv_reactor_def {
struct list_head list;
struct rv_reactor *reactor;
/* protected by the monitor interface lock */
int counter;
};
#endif

struct rv_monitor_def {
struct list_head list;
struct rv_monitor *monitor;
struct dentry *root_d;
#ifdef CONFIG_RV_REACTORS
struct rv_reactor_def *rdef;
bool reacting;
#endif
bool task_monitor;
};

struct dentry *get_monitors_root(void);
int rv_disable_monitor(struct rv_monitor_def *mdef);
int rv_enable_monitor(struct rv_monitor_def *mdef);

#ifdef CONFIG_RV_REACTORS
int reactor_populate_monitor(struct rv_monitor_def *mdef);
void reactor_cleanup_monitor(struct rv_monitor_def *mdef);
int init_rv_reactors(struct dentry *root_dir);
#else
static inline int reactor_populate_monitor(struct rv_monitor_def *mdef)
{
return 0;
}

static inline void reactor_cleanup_monitor(struct rv_monitor_def *mdef)
{
return;
}

static inline int init_rv_reactors(struct dentry *root_dir)
{
return 0;
}
#endif
Loading

0 comments on commit 04acadc

Please sign in to comment.