Re: [PATCH] rv: Allow epoll in rtapp-sleep monitor

[Gabriele Monaco]

On Tue, 2026-03-31 at 12:49 +0200, Nam Cao wrote:
> diff --git a/kernel/trace/rv/monitors/sleep/sleep.c
> b/kernel/trace/rv/monitors/sleep/sleep.c
> index c1347da69e9d..59091863c17c 100644
> --- a/kernel/trace/rv/monitors/sleep/sleep.c
> +++ b/kernel/trace/rv/monitors/sleep/sleep.c
> @@ -162,6 +164,11 @@ static void handle_sys_enter(void *data, struct pt_regs
> *regs, long id)
>  			break;
>  		}
>  		break;
> +#ifdef __NR_epoll_wait
> +	case __NR_epoll_wait:
> +		ltl_atom_set(mon, LTL_EPOLL_WAIT, true);
> +		break;
> +#endif

Sashiko (the AI bot) wonders why this isn't ltl_atom_update() like other things
around here. Is that intentional?

>  	}
>  }
>  
> @@ -174,6 +181,7 @@ static void handle_sys_exit(void *data, struct pt_regs
> *regs, long ret)
>  	ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false);
>  	ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false);
>  	ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
> +	ltl_atom_set(mon, LTL_EPOLL_WAIT, false);
>  	ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, false);
>  }
>  
> diff --git a/kernel/trace/rv/monitors/sleep/sleep.h
> b/kernel/trace/rv/monitors/sleep/sleep.h
> index 2ab46fd218d2..95dc2727c059 100644
> --- a/kernel/trace/rv/monitors/sleep/sleep.h
> +++ b/kernel/trace/rv/monitors/sleep/sleep.h
> @@ -15,6 +15,7 @@ enum ltl_atom {
>  	LTL_ABORT_SLEEP,
>  	LTL_BLOCK_ON_RT_MUTEX,
>  	LTL_CLOCK_NANOSLEEP,
> +	LTL_EPOLL_WAIT,
>  	LTL_FUTEX_LOCK_PI,
>  	LTL_FUTEX_WAIT,
>  	LTL_KERNEL_THREAD,
> @@ -40,6 +41,7 @@ static const char *ltl_atom_str(enum ltl_atom atom)
>  		"ab_sl",
>  		"bl_on_rt_mu",
>  		"cl_na",
> +		"ep_wa",
>  		"fu_lo_pi",
>  		"fu_wa",
>  		"ker_th",
> @@ -75,39 +77,41 @@ 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 task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
> +	bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
> +	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
> +	bool rt = test_bit(LTL_RT, mon->atoms);
> +	bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME,
> 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 kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon-
> >atoms);
> +	bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
>  	bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
> -	bool val9 = futex_wait || val18;
> +	bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
> +	bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
> +	bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
> +	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
> +	bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
> +	bool val42 = task_is_rcu || task_is_migration;
> +	bool val43 = futex_lock_pi || val42;
> +	bool val5 = block_on_rt_mutex || val43;
> +	bool val34 = abort_sleep || kthread_should_stop;
> +	bool val35 = woken_by_nmi || val34;
> +	bool val36 = woken_by_hardirq || val35;
> +	bool val14 = woken_by_equal_or_higher_prio || val36;
> +	bool val13 = !wake;
> +	bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
> +	bool val27 = nanosleep_timer_abstime && val26;
> +	bool val18 = clock_nanosleep && val27;
> +	bool val20 = val18 || epoll_wait;
> +	bool val9 = futex_wait || val20;
>  	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;
>  
> @@ -124,39 +128,41 @@ static void ltl_start(struct task_struct *task, struct
> ltl_monitor *mon)
>  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 task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
> +	bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
> +	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
> +	bool rt = test_bit(LTL_RT, mon->atoms);
> +	bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME,
> 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 kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon-
> >atoms);
> +	bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
>  	bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
> -	bool val9 = futex_wait || val18;
> +	bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
> +	bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
> +	bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
> +	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
> +	bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
> +	bool val42 = task_is_rcu || task_is_migration;
> +	bool val43 = futex_lock_pi || val42;
> +	bool val5 = block_on_rt_mutex || val43;
> +	bool val34 = abort_sleep || kthread_should_stop;
> +	bool val35 = woken_by_nmi || val34;
> +	bool val36 = woken_by_hardirq || val35;
> +	bool val14 = woken_by_equal_or_higher_prio || val36;
> +	bool val13 = !wake;
> +	bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
> +	bool val27 = nanosleep_timer_abstime && val26;
> +	bool val18 = clock_nanosleep && val27;
> +	bool val20 = val18 || epoll_wait;
> +	bool val9 = futex_wait || val20;
>  	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;
>  
> diff --git a/tools/verification/models/rtapp/sleep.ltl
> b/tools/verification/models/rtapp/sleep.ltl
> index 6379bbeb6212..6f26c4810f78 100644
> --- a/tools/verification/models/rtapp/sleep.ltl
> +++ b/tools/verification/models/rtapp/sleep.ltl
> @@ -5,6 +5,7 @@ RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
>  
>  RT_VALID_SLEEP_REASON = FUTEX_WAIT
>                       or RT_FRIENDLY_NANOSLEEP
> +                     or EPOLL_WAIT
>  
>  RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
>                      and NANOSLEEP_TIMER_ABSTIME