mirror of
https://github.com/torvalds/linux.git
synced 2025-11-02 09:40:27 +02:00
9162620eb6
Userspace real-time applications may have design flaws that they raise page faults in real-time threads, and thus have unexpected latencies. Add an linear temporal logic monitor to detect this scenario. Cc: John Ogness <john.ogness@linutronix.de> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/78fea8a2de6d058241d3c6502c1a92910772b0ed.1752088709.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
64 lines
1.3 KiB
C
64 lines
1.3 KiB
C
/* SPDX-License-Identifier: GPL-2.0 */
|
|
|
|
/*
|
|
* C implementation of Buchi automaton, automatically generated by
|
|
* tools/verification/rvgen from the linear temporal logic specification.
|
|
* For further information, see kernel documentation:
|
|
* Documentation/trace/rv/linear_temporal_logic.rst
|
|
*/
|
|
|
|
#include <linux/rv.h>
|
|
|
|
#define MONITOR_NAME pagefault
|
|
|
|
enum ltl_atom {
|
|
LTL_PAGEFAULT,
|
|
LTL_RT,
|
|
LTL_NUM_ATOM
|
|
};
|
|
static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
|
|
|
|
static const char *ltl_atom_str(enum ltl_atom atom)
|
|
{
|
|
static const char *const names[] = {
|
|
"pa",
|
|
"rt",
|
|
};
|
|
|
|
return names[atom];
|
|
}
|
|
|
|
enum ltl_buchi_state {
|
|
S0,
|
|
RV_NUM_BA_STATES
|
|
};
|
|
static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
|
|
|
|
static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
|
|
{
|
|
bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
|
|
bool val3 = !pagefault;
|
|
bool rt = test_bit(LTL_RT, mon->atoms);
|
|
bool val1 = !rt;
|
|
bool val4 = val1 || val3;
|
|
|
|
if (val4)
|
|
__set_bit(S0, mon->states);
|
|
}
|
|
|
|
static void
|
|
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
|
|
{
|
|
bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
|
|
bool val3 = !pagefault;
|
|
bool rt = test_bit(LTL_RT, mon->atoms);
|
|
bool val1 = !rt;
|
|
bool val4 = val1 || val3;
|
|
|
|
switch (state) {
|
|
case S0:
|
|
if (val4)
|
|
__set_bit(S0, next);
|
|
break;
|
|
}
|
|
}
|