Skip to content

Commit 04acadc

Browse files
Daniel Bristot de Oliveirarostedt
authored andcommitted
rv: Add runtime reactors 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. 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 <[email protected]> Cc: Guenter Roeck <[email protected]> Cc: Jonathan Corbet <[email protected]> Cc: Ingo Molnar <[email protected]> Cc: Thomas Gleixner <[email protected]> Cc: Peter Zijlstra <[email protected]> Cc: Will Deacon <[email protected]> Cc: Catalin Marinas <[email protected]> Cc: Marco Elver <[email protected]> Cc: Dmitry Vyukov <[email protected]> Cc: "Paul E. McKenney" <[email protected]> Cc: Shuah Khan <[email protected]> Cc: Gabriele Paoloni <[email protected]> Cc: Juri Lelli <[email protected]> Cc: Clark Williams <[email protected]> Cc: Tao Zhou <[email protected]> Cc: Randy Dunlap <[email protected]> Cc: [email protected] Cc: [email protected] Cc: [email protected] Signed-off-by: Daniel Bristot de Oliveira <[email protected]> Signed-off-by: Steven Rostedt (Google) <[email protected]>
1 parent 102227b commit 04acadc

File tree

6 files changed

+581
-0
lines changed

6 files changed

+581
-0
lines changed

include/linux/rv.h

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,13 +24,24 @@
2424
union rv_task_monitor {
2525
};
2626

27+
#ifdef CONFIG_RV_REACTORS
28+
struct rv_reactor {
29+
const char *name;
30+
const char *description;
31+
void (*react)(char *msg);
32+
};
33+
#endif
34+
2735
struct rv_monitor {
2836
const char *name;
2937
const char *description;
3038
bool enabled;
3139
int (*enable)(void);
3240
void (*disable)(void);
3341
void (*reset)(void);
42+
#ifdef CONFIG_RV_REACTORS
43+
void (*react)(char *msg);
44+
#endif
3445
};
3546

3647
bool rv_monitoring_on(void);
@@ -39,5 +50,11 @@ int rv_register_monitor(struct rv_monitor *monitor);
3950
int rv_get_task_monitor_slot(void);
4051
void rv_put_task_monitor_slot(int slot);
4152

53+
#ifdef CONFIG_RV_REACTORS
54+
bool rv_reacting_on(void);
55+
int rv_unregister_reactor(struct rv_reactor *reactor);
56+
int rv_register_reactor(struct rv_reactor *reactor);
57+
#endif /* CONFIG_RV_REACTORS */
58+
4259
#endif /* CONFIG_RV */
4360
#endif /* _LINUX_RV_H */

kernel/trace/rv/Kconfig

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,14 @@ menuconfig RV
1010
theorem proving). RV works by analyzing the trace of the system's
1111
actual execution, comparing it against a formal specification of
1212
the system behavior.
13+
14+
config RV_REACTORS
15+
bool "Runtime verification reactors"
16+
default y
17+
depends on RV
18+
help
19+
Enables the online runtime verification reactors. A runtime
20+
monitor can cause a reaction to the detection of an exception
21+
on the model's execution. By default, the monitors have
22+
tracing reactions, printing the monitor output via tracepoints,
23+
but other reactions can be added (on-demand) via this interface.

kernel/trace/rv/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
# SPDX-License-Identifier: GPL-2.0
22

33
obj-$(CONFIG_RV) += rv.o
4+
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o

kernel/trace/rv/rv.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -353,6 +353,10 @@ static int create_monitor_dir(struct rv_monitor_def *mdef)
353353
goto out_remove_root;
354354
}
355355

356+
retval = reactor_populate_monitor(mdef);
357+
if (retval)
358+
goto out_remove_root;
359+
356360
return 0;
357361

358362
out_remove_root:
@@ -669,6 +673,7 @@ static const struct file_operations monitoring_on_fops = {
669673

670674
static void destroy_monitor_dir(struct rv_monitor_def *mdef)
671675
{
676+
reactor_cleanup_monitor(mdef);
672677
rv_remove(mdef->root_d);
673678
}
674679

@@ -747,6 +752,7 @@ int rv_unregister_monitor(struct rv_monitor *monitor)
747752
int __init rv_init_interface(void)
748753
{
749754
struct dentry *tmp;
755+
int retval;
750756

751757
rv_root.root_dir = rv_create_dir("rv", NULL);
752758
if (!rv_root.root_dir)
@@ -770,6 +776,9 @@ int __init rv_init_interface(void)
770776
&monitoring_on_fops);
771777
if (!tmp)
772778
goto out_err;
779+
retval = init_rv_reactors(rv_root.root_dir);
780+
if (retval)
781+
goto out_err;
773782

774783
turn_monitoring_on();
775784

kernel/trace/rv/rv.h

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,16 +18,51 @@ struct rv_interface {
1818
#define rv_remove tracefs_remove
1919

2020
#define MAX_RV_MONITOR_NAME_SIZE 32
21+
#define MAX_RV_REACTOR_NAME_SIZE 32
2122

2223
extern struct mutex rv_interface_lock;
2324

25+
#ifdef CONFIG_RV_REACTORS
26+
struct rv_reactor_def {
27+
struct list_head list;
28+
struct rv_reactor *reactor;
29+
/* protected by the monitor interface lock */
30+
int counter;
31+
};
32+
#endif
33+
2434
struct rv_monitor_def {
2535
struct list_head list;
2636
struct rv_monitor *monitor;
2737
struct dentry *root_d;
38+
#ifdef CONFIG_RV_REACTORS
39+
struct rv_reactor_def *rdef;
40+
bool reacting;
41+
#endif
2842
bool task_monitor;
2943
};
3044

3145
struct dentry *get_monitors_root(void);
3246
int rv_disable_monitor(struct rv_monitor_def *mdef);
3347
int rv_enable_monitor(struct rv_monitor_def *mdef);
48+
49+
#ifdef CONFIG_RV_REACTORS
50+
int reactor_populate_monitor(struct rv_monitor_def *mdef);
51+
void reactor_cleanup_monitor(struct rv_monitor_def *mdef);
52+
int init_rv_reactors(struct dentry *root_dir);
53+
#else
54+
static inline int reactor_populate_monitor(struct rv_monitor_def *mdef)
55+
{
56+
return 0;
57+
}
58+
59+
static inline void reactor_cleanup_monitor(struct rv_monitor_def *mdef)
60+
{
61+
return;
62+
}
63+
64+
static inline int init_rv_reactors(struct dentry *root_dir)
65+
{
66+
return 0;
67+
}
68+
#endif

0 commit comments

Comments
 (0)