1 /* SPDX-License-Identifier: GPL-2.0 */ 1 /* SPDX-License-Identifier: GPL-2.0 */
2 /* 2 /*
3 * Runtime Verification. 3 * Runtime Verification.
4 * 4 *
5 * For futher information, see: kernel/trace/r 5 * For futher information, see: kernel/trace/rv/rv.c.
6 */ 6 */
7 #ifndef _LINUX_RV_H 7 #ifndef _LINUX_RV_H
8 #define _LINUX_RV_H 8 #define _LINUX_RV_H
9 9
10 #define MAX_DA_NAME_LEN 24 10 #define MAX_DA_NAME_LEN 24
11 11
12 #ifdef CONFIG_RV 12 #ifdef CONFIG_RV
13 /* 13 /*
14 * Deterministic automaton per-object variable 14 * Deterministic automaton per-object variables.
15 */ 15 */
16 struct da_monitor { 16 struct da_monitor {
17 bool monitoring; 17 bool monitoring;
18 unsigned int curr_state; 18 unsigned int curr_state;
19 }; 19 };
20 20
21 /* 21 /*
22 * Per-task RV monitors count. Nowadays fixed 22 * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS.
23 * If we find justification for more monitors, 23 * If we find justification for more monitors, we can think about
24 * adding more or developing a dynamic method. 24 * adding more or developing a dynamic method. So far, none of
25 * these are justified. 25 * these are justified.
26 */ 26 */
27 #define RV_PER_TASK_MONITORS 1 27 #define RV_PER_TASK_MONITORS 1
28 #define RV_PER_TASK_MONITOR_INIT (RV_PE 28 #define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS)
29 29
30 /* 30 /*
31 * Futher monitor types are expected, so make 31 * Futher monitor types are expected, so make this a union.
32 */ 32 */
33 union rv_task_monitor { 33 union rv_task_monitor {
34 struct da_monitor da_mon; 34 struct da_monitor da_mon;
35 }; 35 };
36 36
37 #ifdef CONFIG_RV_REACTORS 37 #ifdef CONFIG_RV_REACTORS
38 struct rv_reactor { 38 struct rv_reactor {
39 const char *name; 39 const char *name;
40 const char *description; 40 const char *description;
41 void (*react)(char 41 void (*react)(char *msg);
42 }; 42 };
43 #endif 43 #endif
44 44
45 struct rv_monitor { 45 struct rv_monitor {
46 const char *name; 46 const char *name;
47 const char *description; 47 const char *description;
48 bool enabled; 48 bool enabled;
49 int (*enable)(void 49 int (*enable)(void);
50 void (*disable)(voi 50 void (*disable)(void);
51 void (*reset)(void) 51 void (*reset)(void);
52 #ifdef CONFIG_RV_REACTORS 52 #ifdef CONFIG_RV_REACTORS
53 void (*react)(char 53 void (*react)(char *msg);
54 #endif 54 #endif
55 }; 55 };
56 56
57 bool rv_monitoring_on(void); 57 bool rv_monitoring_on(void);
58 int rv_unregister_monitor(struct rv_monitor *m 58 int rv_unregister_monitor(struct rv_monitor *monitor);
59 int rv_register_monitor(struct rv_monitor *mon 59 int rv_register_monitor(struct rv_monitor *monitor);
60 int rv_get_task_monitor_slot(void); 60 int rv_get_task_monitor_slot(void);
61 void rv_put_task_monitor_slot(int slot); 61 void rv_put_task_monitor_slot(int slot);
62 62
63 #ifdef CONFIG_RV_REACTORS 63 #ifdef CONFIG_RV_REACTORS
64 bool rv_reacting_on(void); 64 bool rv_reacting_on(void);
65 int rv_unregister_reactor(struct rv_reactor *r 65 int rv_unregister_reactor(struct rv_reactor *reactor);
66 int rv_register_reactor(struct rv_reactor *rea 66 int rv_register_reactor(struct rv_reactor *reactor);
67 #endif /* CONFIG_RV_REACTORS */ 67 #endif /* CONFIG_RV_REACTORS */
68 68
69 #endif /* CONFIG_RV */ 69 #endif /* CONFIG_RV */
70 #endif /* _LINUX_RV_H */ 70 #endif /* _LINUX_RV_H */
71 71
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.