1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
/* 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 wakeup
enum ltl_atom {
LTL_BLOCK_ON_RT_MUTEX,
LTL_FUTEX_LOCK_PI,
LTL_RT,
LTL_USER_THREAD,
LTL_WOKEN_BY_LOWER_PRIO,
LTL_WOKEN_BY_SOFTIRQ,
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[] = {
"bl_on_rt_mu",
"fu_lo_pi",
"rt",
"us_th",
"wo_lo_pr",
"wo_so",
};
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 woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms);
bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms);
bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool val9 = block_on_rt_mutex || futex_lock_pi;
bool val6 = !woken_by_softirq;
bool val5 = !woken_by_lower_prio;
bool val8 = val5 && val6;
bool val10 = val8 || val9;
bool val3 = !user_thread;
bool val2 = !rt;
bool val4 = val2 || val3;
bool val11 = val4 || val10;
if (val11)
__set_bit(S0, mon->states);
}
static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
bool woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms);
bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms);
bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool val9 = block_on_rt_mutex || futex_lock_pi;
bool val6 = !woken_by_softirq;
bool val5 = !woken_by_lower_prio;
bool val8 = val5 && val6;
bool val10 = val8 || val9;
bool val3 = !user_thread;
bool val2 = !rt;
bool val4 = val2 || val3;
bool val11 = val4 || val10;
switch (state) {
case S0:
if (val11)
__set_bit(S0, next);
break;
}
}
|
