Something went wrong. Try again.
Linux kernel mirror (for testing) git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175/* SPDX-License-Identifier: GPL-2.0 *//* * Runtime Verification. * * For futher information, see: kernel/trace/rv/rv.c. */#ifndef _LINUX_RV_H#define _LINUX_RV_H
#define MAX_DA_NAME_LEN 32#define MAX_DA_RETRY_RACING_EVENTS 3
#define RV_MON_GLOBAL 0#define RV_MON_PER_CPU 1#define RV_MON_PER_TASK 2#define RV_MON_PER_OBJ 3
#ifdef CONFIG_RV#include <linux/array_size.h>#include <linux/bitops.h>#include <linux/list.h>#include <linux/types.h>
/* * Deterministic automaton per-object variables. */struct da_monitor { bool monitoring; unsigned int curr_state;};
#ifdef CONFIG_RV_LTL_MONITOR
/* * In the future, if the number of atomic propositions or the size of Buchi * automaton is larger, we can switch to dynamic allocation. For now, the code * is simpler this way. */#define RV_MAX_LTL_ATOM 32#define RV_MAX_BA_STATES 32
/** * struct ltl_monitor - A linear temporal logic runtime verification monitor * @states: States in the Buchi automaton. As Buchi automaton is a * non-deterministic state machine, the monitor can be in multiple * states simultaneously. This is a bitmask of all possible states. * If this is zero, that means either: * - The monitor has not started yet (e.g. because not all * atomic propositions are known). * - There is no possible state to be in. In other words, a * violation of the LTL property is detected. * @atoms: The values of atomic propositions. * @unknown_atoms: Atomic propositions which are still unknown. */struct ltl_monitor { DECLARE_BITMAP(states, RV_MAX_BA_STATES); DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM); DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);};
static inline bool rv_ltl_valid_state(struct ltl_monitor *mon){ for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) { if (mon->states[i]) return true; } return false;}
static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon){ for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) { if (mon->unknown_atoms[i]) return false; } return true;}
#else
struct ltl_monitor {};
#endif /* CONFIG_RV_LTL_MONITOR */
#ifdef CONFIG_RV_HA_MONITOR/* * In the future, hybrid automata may rely on multiple * environment variables, e.g. different clocks started at * different times or running at different speed. * For now we support only 1 variable. */#define MAX_HA_ENV_LEN 1
/* * Monitors can pick the preferred timer implementation: * No timer: if monitors don't have state invariants. * Timer wheel: lightweight invariants check but far less precise. * Hrtimer: accurate invariants check with higher overhead. */#define HA_TIMER_NONE 0#define HA_TIMER_WHEEL 1#define HA_TIMER_HRTIMER 2
/* * Hybrid automaton per-object variables. */struct ha_monitor { struct da_monitor da_mon; u64 env_store[MAX_HA_ENV_LEN]; union { struct hrtimer hrtimer; struct timer_list timer; };};
#else
struct ha_monitor { };
#endif /* CONFIG_RV_HA_MONITOR */
#define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS)
union rv_task_monitor { struct da_monitor da_mon; struct ltl_monitor ltl_mon; struct ha_monitor ha_mon;};
#ifdef CONFIG_RV_REACTORSstruct rv_reactor { const char *name; const char *description; __printf(1, 0) void (*react)(const char *msg, va_list args); struct list_head list;};#endif
struct rv_monitor { const char *name; const char *description; bool enabled; int (*enable)(void); void (*disable)(void); void (*reset)(void);#ifdef CONFIG_RV_REACTORS struct rv_reactor *reactor; __printf(1, 0) void (*react)(const char *msg, va_list args);#endif struct list_head list; struct rv_monitor *parent; struct dentry *root_d;};
bool rv_monitoring_on(void);int rv_unregister_monitor(struct rv_monitor *monitor);int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);int rv_get_task_monitor_slot(void);void rv_put_task_monitor_slot(int slot);
#ifdef CONFIG_RV_REACTORSint rv_unregister_reactor(struct rv_reactor *reactor);int rv_register_reactor(struct rv_reactor *reactor);__printf(2, 3)void rv_react(struct rv_monitor *monitor, const char *msg, ...);#else__printf(2, 3)static inline void rv_react(struct rv_monitor *monitor, const char *msg, ...){}#endif /* CONFIG_RV_REACTORS */
#endif /* CONFIG_RV */#endif /* _LINUX_RV_H */