Linux kernel mirror (for testing)
git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
kernel
os
linux
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 */
27struct 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 */
55struct 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
61static 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
70static 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
81struct 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 */
107struct 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
118struct ha_monitor { };
119
120#endif /* CONFIG_RV_HA_MONITOR */
121
122#define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS)
123
124union 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
131struct 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
139struct 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
155bool rv_monitoring_on(void);
156int rv_unregister_monitor(struct rv_monitor *monitor);
157int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);
158int rv_get_task_monitor_slot(void);
159void rv_put_task_monitor_slot(int slot);
160
161#ifdef CONFIG_RV_REACTORS
162int rv_unregister_reactor(struct rv_reactor *reactor);
163int rv_register_reactor(struct rv_reactor *reactor);
164__printf(2, 3)
165void rv_react(struct rv_monitor *monitor, const char *msg, ...);
166#else
167__printf(2, 3)
168static 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 */