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