| 1 |
|
| 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 |
|
| 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 |
|
| 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
|
| 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
|
| 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)
|
| 168 | static inline void rv_react(struct rv_monitor *monitor, const char *msg, ...)
|
| 169 | {
|
| 170 | }
|
| 171 | #endif
|
| 172 |
|
| 173 | #endif
|
| 174 | #endif
|