[go: up one dir, main page]
1/* SPDX-License-Identifier: GPL-2.0 */
2/*
3 * Runtime Verification.
4 *
5 * For futher information, see: kernel/trace/rv/rv.c.
6 */
7#ifndef _LINUX_RV_H
8#define _LINUX_RV_H
9
10#define MAX_DA_NAME_LEN 32
11#define MAX_DA_RETRY_RACING_EVENTS 3
12
13#ifdef CONFIG_RV
14#include <linux/array_size.h>
15#include <linux/bitops.h>
16#include <linux/list.h>
17#include <linux/types.h>
18
19/*
20 * Deterministic automaton per-object variables.
21 */
22struct da_monitor {
23 bool monitoring;
24 unsigned int curr_state;
25};
26
27#ifdef CONFIG_RV_LTL_MONITOR
28
29/*
30 * In the future, if the number of atomic propositions or the size of Buchi
31 * automaton is larger, we can switch to dynamic allocation. For now, the code
32 * is simpler this way.
33 */
34#define RV_MAX_LTL_ATOM 32
35#define RV_MAX_BA_STATES 32
36
37/**
38 * struct ltl_monitor - A linear temporal logic runtime verification monitor
39 * @states: States in the Buchi automaton. As Buchi automaton is a
40 * non-deterministic state machine, the monitor can be in multiple
41 * states simultaneously. This is a bitmask of all possible states.
42 * If this is zero, that means either:
43 * - The monitor has not started yet (e.g. because not all
44 * atomic propositions are known).
45 * - There is no possible state to be in. In other words, a
46 * violation of the LTL property is detected.
47 * @atoms: The values of atomic propositions.
48 * @unknown_atoms: Atomic propositions which are still unknown.
49 */
50struct ltl_monitor {
51 DECLARE_BITMAP(states, RV_MAX_BA_STATES);
52 DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
53 DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
54};
55
56static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
57{
58 for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
59 if (mon->states[i])
60 return true;
61 }
62 return false;
63}
64
65static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
66{
67 for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) {
68 if (mon->unknown_atoms[i])
69 return false;
70 }
71 return true;
72}
73
74#else
75
76struct ltl_monitor {};
77
78#endif /* CONFIG_RV_LTL_MONITOR */
79
80#define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS)
81
82union rv_task_monitor {
83 struct da_monitor da_mon;
84 struct ltl_monitor ltl_mon;
85};
86
87#ifdef CONFIG_RV_REACTORS
88struct rv_reactor {
89 const char *name;
90 const char *description;
91 __printf(1, 0) void (*react)(const char *msg, va_list args);
92 struct list_head list;
93};
94#endif
95
96struct rv_monitor {
97 const char *name;
98 const char *description;
99 bool enabled;
100 int (*enable)(void);
101 void (*disable)(void);
102 void (*reset)(void);
103#ifdef CONFIG_RV_REACTORS
104 struct rv_reactor *reactor;
105 __printf(1, 0) void (*react)(const char *msg, va_list args);
106#endif
107 struct list_head list;
108 struct rv_monitor *parent;
109 struct dentry *root_d;
110};
111
112bool rv_monitoring_on(void);
113int rv_unregister_monitor(struct rv_monitor *monitor);
114int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);
115int rv_get_task_monitor_slot(void);
116void rv_put_task_monitor_slot(int slot);
117
118#ifdef CONFIG_RV_REACTORS
119int rv_unregister_reactor(struct rv_reactor *reactor);
120int rv_register_reactor(struct rv_reactor *reactor);
121__printf(2, 3)
122void rv_react(struct rv_monitor *monitor, const char *msg, ...);
123#else
124__printf(2, 3)
125static inline void rv_react(struct rv_monitor *monitor, const char *msg, ...)
126{
127}
128#endif /* CONFIG_RV_REACTORS */
129
130#endif /* CONFIG_RV */
131#endif /* _LINUX_RV_H */
132

source code of linux/include/linux/rv.h