| /* SPDX-License-Identifier: GPL-2.0 */ |
| |
| /* |
| * C implementation of Buchi automaton, automatically generated by |
| * tools/verification/rvgen from the linear temporal logic specification. |
| * For further information, see kernel documentation: |
| * Documentation/trace/rv/linear_temporal_logic.rst |
| */ |
| |
| #include <linux/rv.h> |
| |
| #define MONITOR_NAME sleep |
| |
| enum ltl_atom { |
| LTL_ABORT_SLEEP, |
| LTL_BLOCK_ON_RT_MUTEX, |
| LTL_CLOCK_NANOSLEEP, |
| LTL_FUTEX_LOCK_PI, |
| LTL_FUTEX_WAIT, |
| LTL_KERNEL_THREAD, |
| LTL_KTHREAD_SHOULD_STOP, |
| LTL_NANOSLEEP_CLOCK_MONOTONIC, |
| LTL_NANOSLEEP_CLOCK_TAI, |
| LTL_NANOSLEEP_TIMER_ABSTIME, |
| LTL_RT, |
| LTL_SLEEP, |
| LTL_TASK_IS_MIGRATION, |
| LTL_TASK_IS_RCU, |
| LTL_WAKE, |
| LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, |
| LTL_WOKEN_BY_HARDIRQ, |
| LTL_WOKEN_BY_NMI, |
| LTL_NUM_ATOM |
| }; |
| static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); |
| |
| static const char *ltl_atom_str(enum ltl_atom atom) |
| { |
| static const char *const names[] = { |
| "ab_sl", |
| "bl_on_rt_mu", |
| "cl_na", |
| "fu_lo_pi", |
| "fu_wa", |
| "ker_th", |
| "kth_sh_st", |
| "na_cl_mo", |
| "na_cl_ta", |
| "na_ti_ab", |
| "rt", |
| "sl", |
| "ta_mi", |
| "ta_rc", |
| "wak", |
| "wo_eq_hi_pr", |
| "wo_ha", |
| "wo_nm", |
| }; |
| |
| return names[atom]; |
| } |
| |
| enum ltl_buchi_state { |
| S0, |
| S1, |
| S2, |
| S3, |
| S4, |
| S5, |
| S6, |
| S7, |
| RV_NUM_BA_STATES |
| }; |
| static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); |
| |
| static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) |
| { |
| bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms); |
| bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms); |
| bool val40 = task_is_rcu || task_is_migration; |
| bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms); |
| bool val41 = futex_lock_pi || val40; |
| bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms); |
| bool val5 = block_on_rt_mutex || val41; |
| bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms); |
| bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms); |
| bool val32 = abort_sleep || kthread_should_stop; |
| bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms); |
| bool val33 = woken_by_nmi || val32; |
| bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms); |
| bool val34 = woken_by_hardirq || val33; |
| bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, |
| mon->atoms); |
| bool val14 = woken_by_equal_or_higher_prio || val34; |
| bool wake = test_bit(LTL_WAKE, mon->atoms); |
| bool val13 = !wake; |
| bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms); |
| bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms); |
| bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms); |
| bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai; |
| bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms); |
| bool val25 = nanosleep_timer_abstime && val24; |
| bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms); |
| bool val18 = clock_nanosleep && val25; |
| bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms); |
| bool val9 = futex_wait || val18; |
| bool val11 = val9 || kernel_thread; |
| bool sleep = test_bit(LTL_SLEEP, mon->atoms); |
| bool val2 = !sleep; |
| bool rt = test_bit(LTL_RT, mon->atoms); |
| bool val1 = !rt; |
| bool val3 = val1 || val2; |
| |
| if (val3) |
| __set_bit(S0, mon->states); |
| if (val11 && val13) |
| __set_bit(S1, mon->states); |
| if (val11 && val14) |
| __set_bit(S4, mon->states); |
| if (val5) |
| __set_bit(S5, mon->states); |
| } |
| |
| static void |
| ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) |
| { |
| bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms); |
| bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms); |
| bool val40 = task_is_rcu || task_is_migration; |
| bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms); |
| bool val41 = futex_lock_pi || val40; |
| bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms); |
| bool val5 = block_on_rt_mutex || val41; |
| bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms); |
| bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms); |
| bool val32 = abort_sleep || kthread_should_stop; |
| bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms); |
| bool val33 = woken_by_nmi || val32; |
| bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms); |
| bool val34 = woken_by_hardirq || val33; |
| bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, |
| mon->atoms); |
| bool val14 = woken_by_equal_or_higher_prio || val34; |
| bool wake = test_bit(LTL_WAKE, mon->atoms); |
| bool val13 = !wake; |
| bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms); |
| bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms); |
| bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms); |
| bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai; |
| bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms); |
| bool val25 = nanosleep_timer_abstime && val24; |
| bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms); |
| bool val18 = clock_nanosleep && val25; |
| bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms); |
| bool val9 = futex_wait || val18; |
| bool val11 = val9 || kernel_thread; |
| bool sleep = test_bit(LTL_SLEEP, mon->atoms); |
| bool val2 = !sleep; |
| bool rt = test_bit(LTL_RT, mon->atoms); |
| bool val1 = !rt; |
| bool val3 = val1 || val2; |
| |
| switch (state) { |
| case S0: |
| if (val3) |
| __set_bit(S0, next); |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val5) |
| __set_bit(S5, next); |
| break; |
| case S1: |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val13 && val3) |
| __set_bit(S2, next); |
| if (val14 && val3) |
| __set_bit(S3, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val13 && val5) |
| __set_bit(S6, next); |
| if (val14 && val5) |
| __set_bit(S7, next); |
| break; |
| case S2: |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val13 && val3) |
| __set_bit(S2, next); |
| if (val14 && val3) |
| __set_bit(S3, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val13 && val5) |
| __set_bit(S6, next); |
| if (val14 && val5) |
| __set_bit(S7, next); |
| break; |
| case S3: |
| if (val3) |
| __set_bit(S0, next); |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val5) |
| __set_bit(S5, next); |
| break; |
| case S4: |
| if (val3) |
| __set_bit(S0, next); |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val5) |
| __set_bit(S5, next); |
| break; |
| case S5: |
| if (val3) |
| __set_bit(S0, next); |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val5) |
| __set_bit(S5, next); |
| break; |
| case S6: |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val13 && val3) |
| __set_bit(S2, next); |
| if (val14 && val3) |
| __set_bit(S3, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val13 && val5) |
| __set_bit(S6, next); |
| if (val14 && val5) |
| __set_bit(S7, next); |
| break; |
| case S7: |
| if (val3) |
| __set_bit(S0, next); |
| if (val11 && val13) |
| __set_bit(S1, next); |
| if (val11 && val14) |
| __set_bit(S4, next); |
| if (val5) |
| __set_bit(S5, next); |
| break; |
| } |
| } |
