sleep.h

  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
 14enum 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};
 35static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
 36
 37static 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
 63enum 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};
 74static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
 75
 76static 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
124static void
125ltl_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}