1 /* SPDX-License-Identifier: GPL-2.0 */
2
3 /*
4 * C implementation of Buchi automaton, automatically generated by
5 * tools/verification/rvgen from the linear temporal logic specification.
6 * For further information, see kernel documentation:
7 * Documentation/trace/rv/linear_temporal_logic.rst
8 */
9
10 #include <linux/rv.h>
11
12 #define MONITOR_NAME sleep
13
14 enum ltl_atom {
15 LTL_ABORT_SLEEP,
16 LTL_BLOCK_ON_RT_MUTEX,
17 LTL_CLOCK_NANOSLEEP,
18 LTL_FUTEX_LOCK_PI,
19 LTL_FUTEX_WAIT,
20 LTL_KERNEL_THREAD,
21 LTL_KTHREAD_SHOULD_STOP,
22 LTL_NANOSLEEP_CLOCK_MONOTONIC,
23 LTL_NANOSLEEP_CLOCK_TAI,
24 LTL_NANOSLEEP_TIMER_ABSTIME,
25 LTL_RT,
26 LTL_SLEEP,
27 LTL_TASK_IS_MIGRATION,
28 LTL_TASK_IS_RCU,
29 LTL_WAKE,
30 LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
31 LTL_WOKEN_BY_HARDIRQ,
32 LTL_WOKEN_BY_NMI,
33 LTL_NUM_ATOM
34 };
35 static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
36
ltl_atom_str(enum ltl_atom atom)37 static const char *ltl_atom_str(enum ltl_atom atom)
38 {
39 static const char *const names[] = {
40 "ab_sl",
41 "bl_on_rt_mu",
42 "cl_na",
43 "fu_lo_pi",
44 "fu_wa",
45 "ker_th",
46 "kth_sh_st",
47 "na_cl_mo",
48 "na_cl_ta",
49 "na_ti_ab",
50 "rt",
51 "sl",
52 "ta_mi",
53 "ta_rc",
54 "wak",
55 "wo_eq_hi_pr",
56 "wo_ha",
57 "wo_nm",
58 };
59
60 return names[atom];
61 }
62
63 enum ltl_buchi_state {
64 S0,
65 S1,
66 S2,
67 S3,
68 S4,
69 S5,
70 S6,
71 S7,
72 RV_NUM_BA_STATES
73 };
74 static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
75
ltl_start(struct task_struct * task,struct ltl_monitor * mon)76 static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
77 {
78 bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
79 bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
80 bool val40 = task_is_rcu || task_is_migration;
81 bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
82 bool val41 = futex_lock_pi || val40;
83 bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
84 bool val5 = block_on_rt_mutex || val41;
85 bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
86 bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
87 bool val32 = abort_sleep || kthread_should_stop;
88 bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
89 bool val33 = woken_by_nmi || val32;
90 bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
91 bool val34 = woken_by_hardirq || val33;
92 bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
93 mon->atoms);
94 bool val14 = woken_by_equal_or_higher_prio || val34;
95 bool wake = test_bit(LTL_WAKE, mon->atoms);
96 bool val13 = !wake;
97 bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
98 bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
99 bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
100 bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai;
101 bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
102 bool val25 = nanosleep_timer_abstime && val24;
103 bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
104 bool val18 = clock_nanosleep && val25;
105 bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
106 bool val9 = futex_wait || val18;
107 bool val11 = val9 || kernel_thread;
108 bool sleep = test_bit(LTL_SLEEP, mon->atoms);
109 bool val2 = !sleep;
110 bool rt = test_bit(LTL_RT, mon->atoms);
111 bool val1 = !rt;
112 bool val3 = val1 || val2;
113
114 if (val3)
115 __set_bit(S0, mon->states);
116 if (val11 && val13)
117 __set_bit(S1, mon->states);
118 if (val11 && val14)
119 __set_bit(S4, mon->states);
120 if (val5)
121 __set_bit(S5, mon->states);
122 }
123
124 static void
ltl_possible_next_states(struct ltl_monitor * mon,unsigned int state,unsigned long * next)125 ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
126 {
127 bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
128 bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
129 bool val40 = task_is_rcu || task_is_migration;
130 bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
131 bool val41 = futex_lock_pi || val40;
132 bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
133 bool val5 = block_on_rt_mutex || val41;
134 bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
135 bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
136 bool val32 = abort_sleep || kthread_should_stop;
137 bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
138 bool val33 = woken_by_nmi || val32;
139 bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
140 bool val34 = woken_by_hardirq || val33;
141 bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
142 mon->atoms);
143 bool val14 = woken_by_equal_or_higher_prio || val34;
144 bool wake = test_bit(LTL_WAKE, mon->atoms);
145 bool val13 = !wake;
146 bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
147 bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
148 bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
149 bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai;
150 bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
151 bool val25 = nanosleep_timer_abstime && val24;
152 bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
153 bool val18 = clock_nanosleep && val25;
154 bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
155 bool val9 = futex_wait || val18;
156 bool val11 = val9 || kernel_thread;
157 bool sleep = test_bit(LTL_SLEEP, mon->atoms);
158 bool val2 = !sleep;
159 bool rt = test_bit(LTL_RT, mon->atoms);
160 bool val1 = !rt;
161 bool val3 = val1 || val2;
162
163 switch (state) {
164 case S0:
165 if (val3)
166 __set_bit(S0, next);
167 if (val11 && val13)
168 __set_bit(S1, next);
169 if (val11 && val14)
170 __set_bit(S4, next);
171 if (val5)
172 __set_bit(S5, next);
173 break;
174 case S1:
175 if (val11 && val13)
176 __set_bit(S1, next);
177 if (val13 && val3)
178 __set_bit(S2, next);
179 if (val14 && val3)
180 __set_bit(S3, next);
181 if (val11 && val14)
182 __set_bit(S4, next);
183 if (val13 && val5)
184 __set_bit(S6, next);
185 if (val14 && val5)
186 __set_bit(S7, next);
187 break;
188 case S2:
189 if (val11 && val13)
190 __set_bit(S1, next);
191 if (val13 && val3)
192 __set_bit(S2, next);
193 if (val14 && val3)
194 __set_bit(S3, next);
195 if (val11 && val14)
196 __set_bit(S4, next);
197 if (val13 && val5)
198 __set_bit(S6, next);
199 if (val14 && val5)
200 __set_bit(S7, next);
201 break;
202 case S3:
203 if (val3)
204 __set_bit(S0, next);
205 if (val11 && val13)
206 __set_bit(S1, next);
207 if (val11 && val14)
208 __set_bit(S4, next);
209 if (val5)
210 __set_bit(S5, next);
211 break;
212 case S4:
213 if (val3)
214 __set_bit(S0, next);
215 if (val11 && val13)
216 __set_bit(S1, next);
217 if (val11 && val14)
218 __set_bit(S4, next);
219 if (val5)
220 __set_bit(S5, next);
221 break;
222 case S5:
223 if (val3)
224 __set_bit(S0, next);
225 if (val11 && val13)
226 __set_bit(S1, next);
227 if (val11 && val14)
228 __set_bit(S4, next);
229 if (val5)
230 __set_bit(S5, next);
231 break;
232 case S6:
233 if (val11 && val13)
234 __set_bit(S1, next);
235 if (val13 && val3)
236 __set_bit(S2, next);
237 if (val14 && val3)
238 __set_bit(S3, next);
239 if (val11 && val14)
240 __set_bit(S4, next);
241 if (val13 && val5)
242 __set_bit(S6, next);
243 if (val14 && val5)
244 __set_bit(S7, next);
245 break;
246 case S7:
247 if (val3)
248 __set_bit(S0, next);
249 if (val11 && val13)
250 __set_bit(S1, next);
251 if (val11 && val14)
252 __set_bit(S4, next);
253 if (val5)
254 __set_bit(S5, next);
255 break;
256 }
257 }
258