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