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 #define RV_MON_GLOBAL 0
14 #define RV_MON_PER_CPU 1
15 #define RV_MON_PER_TASK 2
16 #define RV_MON_PER_OBJ 3
17
18 #ifdef CONFIG_RV
19 #include <linux/array_size.h>
20 #include <linux/bitops.h>
21 #include <linux/list.h>
22 #include <linux/types.h>
23
24 /*
25 * Deterministic automaton per-object variables.
26 */
27 struct da_monitor {
28 bool monitoring;
29 unsigned int curr_state;
30 };
31
32 #ifdef CONFIG_RV_LTL_MONITOR
33
34 /*
35 * In the future, if the number of atomic propositions or the size of Buchi
36 * automaton is larger, we can switch to dynamic allocation. For now, the code
37 * is simpler this way.
38 */
39 #define RV_MAX_LTL_ATOM 32
40 #define RV_MAX_BA_STATES 32
41
42 /**
43 * struct ltl_monitor - A linear temporal logic runtime verification monitor
44 * @states: States in the Buchi automaton. As Buchi automaton is a
45 * non-deterministic state machine, the monitor can be in multiple
46 * states simultaneously. This is a bitmask of all possible states.
47 * If this is zero, that means either:
48 * - The monitor has not started yet (e.g. because not all
49 * atomic propositions are known).
50 * - There is no possible state to be in. In other words, a
51 * violation of the LTL property is detected.
52 * @atoms: The values of atomic propositions.
53 * @unknown_atoms: Atomic propositions which are still unknown.
54 */
55 struct ltl_monitor {
56 DECLARE_BITMAP(states, RV_MAX_BA_STATES);
57 DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
58 DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
59 };
60
rv_ltl_valid_state(struct ltl_monitor * mon)61 static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
62 {
63 for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
64 if (mon->states[i])
65 return true;
66 }
67 return false;
68 }
69
rv_ltl_all_atoms_known(struct ltl_monitor * mon)70 static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
71 {
72 for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) {
73 if (mon->unknown_atoms[i])
74 return false;
75 }
76 return true;
77 }
78
79 #else
80
81 struct ltl_monitor {};
82
83 #endif /* CONFIG_RV_LTL_MONITOR */
84
85 #ifdef CONFIG_RV_HA_MONITOR
86 /*
87 * In the future, hybrid automata may rely on multiple
88 * environment variables, e.g. different clocks started at
89 * different times or running at different speed.
90 * For now we support only 1 variable.
91 */
92 #define MAX_HA_ENV_LEN 1
93
94 /*
95 * Monitors can pick the preferred timer implementation:
96 * No timer: if monitors don't have state invariants.
97 * Timer wheel: lightweight invariants check but far less precise.
98 * Hrtimer: accurate invariants check with higher overhead.
99 */
100 #define HA_TIMER_NONE 0
101 #define HA_TIMER_WHEEL 1
102 #define HA_TIMER_HRTIMER 2
103
104 /*
105 * Hybrid automaton per-object variables.
106 */
107 struct ha_monitor {
108 struct da_monitor da_mon;
109 u64 env_store[MAX_HA_ENV_LEN];
110 union {
111 struct hrtimer hrtimer;
112 struct timer_list timer;
113 };
114 };
115
116 #else
117
118 struct ha_monitor { };
119
120 #endif /* CONFIG_RV_HA_MONITOR */
121
122 #define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS)
123
124 union rv_task_monitor {
125 struct da_monitor da_mon;
126 struct ltl_monitor ltl_mon;
127 struct ha_monitor ha_mon;
128 };
129
130 #ifdef CONFIG_RV_REACTORS
131 struct rv_reactor {
132 const char *name;
133 const char *description;
134 __printf(1, 0) void (*react)(const char *msg, va_list args);
135 struct list_head list;
136 };
137 #endif
138
139 struct rv_monitor {
140 const char *name;
141 const char *description;
142 bool enabled;
143 int (*enable)(void);
144 void (*disable)(void);
145 void (*reset)(void);
146 #ifdef CONFIG_RV_REACTORS
147 struct rv_reactor *reactor;
148 __printf(1, 0) void (*react)(const char *msg, va_list args);
149 #endif
150 struct list_head list;
151 struct rv_monitor *parent;
152 struct dentry *root_d;
153 };
154
155 bool rv_monitoring_on(void);
156 int rv_unregister_monitor(struct rv_monitor *monitor);
157 int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);
158 int rv_get_task_monitor_slot(void);
159 void rv_put_task_monitor_slot(int slot);
160
161 #ifdef CONFIG_RV_REACTORS
162 int rv_unregister_reactor(struct rv_reactor *reactor);
163 int rv_register_reactor(struct rv_reactor *reactor);
164 __printf(2, 3)
165 void rv_react(struct rv_monitor *monitor, const char *msg, ...);
166 #else
167 __printf(2, 3)
rv_react(struct rv_monitor * monitor,const char * msg,...)168 static inline void rv_react(struct rv_monitor *monitor, const char *msg, ...)
169 {
170 }
171 #endif /* CONFIG_RV_REACTORS */
172
173 #endif /* CONFIG_RV */
174 #endif /* _LINUX_RV_H */
175