include/linux/rv.h

Source file repositories/reference/linux-study-clean/include/linux/rv.h

File Facts

System
Linux kernel
Corpus path
include/linux/rv.h
Extension
.h
Size
4339 bytes
Lines
175
Domain
Core OS
Bucket
Core Kernel Interface
Inferred role
Core OS: implementation source
Status
source implementation candidate

Why This File Exists

Core operating-system implementation surface: boot, tasks, memory, VFS, syscall-facing interfaces, synchronization, credentials, and isolation.

Dependency Surface

Detected Declarations

Annotated Snippet

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

Annotation

Implementation Notes