1*6fdaab4eSNam Cao /* SPDX-License-Identifier: GPL-2.0 */ 2*6fdaab4eSNam Cao 3*6fdaab4eSNam Cao /* 4*6fdaab4eSNam Cao * C implementation of Buchi automaton, automatically generated by 5*6fdaab4eSNam Cao * tools/verification/rvgen from the linear temporal logic specification. 6*6fdaab4eSNam Cao * For further information, see kernel documentation: 7*6fdaab4eSNam Cao * Documentation/trace/rv/linear_temporal_logic.rst 8*6fdaab4eSNam Cao */ 9*6fdaab4eSNam Cao 10*6fdaab4eSNam Cao #include <linux/rv.h> 11*6fdaab4eSNam Cao 12*6fdaab4eSNam Cao #define MONITOR_NAME wakeup 13*6fdaab4eSNam Cao 14*6fdaab4eSNam Cao enum ltl_atom { 15*6fdaab4eSNam Cao LTL_BLOCK_ON_RT_MUTEX, 16*6fdaab4eSNam Cao LTL_FUTEX_LOCK_PI, 17*6fdaab4eSNam Cao LTL_RT, 18*6fdaab4eSNam Cao LTL_USER_THREAD, 19*6fdaab4eSNam Cao LTL_WOKEN_BY_LOWER_PRIO, 20*6fdaab4eSNam Cao LTL_WOKEN_BY_SOFTIRQ, 21*6fdaab4eSNam Cao LTL_NUM_ATOM 22*6fdaab4eSNam Cao }; 23*6fdaab4eSNam Cao static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); 24*6fdaab4eSNam Cao 25*6fdaab4eSNam Cao static const char *ltl_atom_str(enum ltl_atom atom) 26*6fdaab4eSNam Cao { 27*6fdaab4eSNam Cao static const char *const names[] = { 28*6fdaab4eSNam Cao "bl_on_rt_mu", 29*6fdaab4eSNam Cao "fu_lo_pi", 30*6fdaab4eSNam Cao "rt", 31*6fdaab4eSNam Cao "us_th", 32*6fdaab4eSNam Cao "wo_lo_pr", 33*6fdaab4eSNam Cao "wo_so", 34*6fdaab4eSNam Cao }; 35*6fdaab4eSNam Cao 36*6fdaab4eSNam Cao return names[atom]; 37*6fdaab4eSNam Cao } 38*6fdaab4eSNam Cao 39*6fdaab4eSNam Cao enum ltl_buchi_state { 40*6fdaab4eSNam Cao S0, 41*6fdaab4eSNam Cao RV_NUM_BA_STATES 42*6fdaab4eSNam Cao }; 43*6fdaab4eSNam Cao static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); 44*6fdaab4eSNam Cao 45*6fdaab4eSNam Cao static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) 46*6fdaab4eSNam Cao { 47*6fdaab4eSNam Cao bool woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms); 48*6fdaab4eSNam Cao bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms); 49*6fdaab4eSNam Cao bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms); 50*6fdaab4eSNam Cao bool rt = test_bit(LTL_RT, mon->atoms); 51*6fdaab4eSNam Cao bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms); 52*6fdaab4eSNam Cao bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms); 53*6fdaab4eSNam Cao bool val9 = block_on_rt_mutex || futex_lock_pi; 54*6fdaab4eSNam Cao bool val6 = !woken_by_softirq; 55*6fdaab4eSNam Cao bool val5 = !woken_by_lower_prio; 56*6fdaab4eSNam Cao bool val8 = val5 && val6; 57*6fdaab4eSNam Cao bool val10 = val8 || val9; 58*6fdaab4eSNam Cao bool val3 = !user_thread; 59*6fdaab4eSNam Cao bool val2 = !rt; 60*6fdaab4eSNam Cao bool val4 = val2 || val3; 61*6fdaab4eSNam Cao bool val11 = val4 || val10; 62*6fdaab4eSNam Cao 63*6fdaab4eSNam Cao if (val11) 64*6fdaab4eSNam Cao __set_bit(S0, mon->states); 65*6fdaab4eSNam Cao } 66*6fdaab4eSNam Cao 67*6fdaab4eSNam Cao static void 68*6fdaab4eSNam Cao ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) 69*6fdaab4eSNam Cao { 70*6fdaab4eSNam Cao bool woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms); 71*6fdaab4eSNam Cao bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms); 72*6fdaab4eSNam Cao bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms); 73*6fdaab4eSNam Cao bool rt = test_bit(LTL_RT, mon->atoms); 74*6fdaab4eSNam Cao bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms); 75*6fdaab4eSNam Cao bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms); 76*6fdaab4eSNam Cao bool val9 = block_on_rt_mutex || futex_lock_pi; 77*6fdaab4eSNam Cao bool val6 = !woken_by_softirq; 78*6fdaab4eSNam Cao bool val5 = !woken_by_lower_prio; 79*6fdaab4eSNam Cao bool val8 = val5 && val6; 80*6fdaab4eSNam Cao bool val10 = val8 || val9; 81*6fdaab4eSNam Cao bool val3 = !user_thread; 82*6fdaab4eSNam Cao bool val2 = !rt; 83*6fdaab4eSNam Cao bool val4 = val2 || val3; 84*6fdaab4eSNam Cao bool val11 = val4 || val10; 85*6fdaab4eSNam Cao 86*6fdaab4eSNam Cao switch (state) { 87*6fdaab4eSNam Cao case S0: 88*6fdaab4eSNam Cao if (val11) 89*6fdaab4eSNam Cao __set_bit(S0, next); 90*6fdaab4eSNam Cao break; 91*6fdaab4eSNam Cao } 92*6fdaab4eSNam Cao } 93