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 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 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 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