Greg Kroah-Hartman
598cf27219
Link: https://lore.kernel.org/r/20260217200002.683975158@linuxfoundation.org Tested-by: Florian Fainelli <florian.fainelli@broadcom.com> Tested-by: Takeshi Ogasawara <takeshi.ogasawara@futuring-girl.com> Tested-by: Peter Schneider <pschneider1968@googlemail.com> Tested-by: Jon Hunter <jonathanh@nvidia.com> Tested-by: Salvatore Bonaccorso <carnil@debian.org> Tested-by: Brett A C Sheffield <bacs@librecast.net> Tested-by: Mark Brown <broonie@kernel.org> Tested-by: Luna Jernberg <droidbittin@gmail.com> Tested-by: Ronald Warsow <rwarsow@gmx.de> Tested-by: Justin M. Forbes <jforbes@fedoraproject.org> Tested-by: Ron Economos <re@w6rz.net> Tested-by: Miguel Ojeda <ojeda@kernel.org> Signed-off-by: Greg Kroah-Hartman <gregkh@linuxfoundation.org>
65 lines
1.3 KiB
C
65 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;
|
|
}
|
|
}
|