Re: [PATCH] rv: Allow epoll in rtapp-sleep monitor
From: Gabriele Monaco
Date: Tue Mar 31 2026 - 09:02:16 EST
On Tue, 2026-03-31 at 12:49 +0200, Nam Cao wrote:
> Since commit 0c43094f8cc9 ("eventpoll: Replace rwlock with spinlock"),
> epoll_wait is real-time-safe syscall for sleeping.
>
> Add epoll_wait to the list of rt-safe sleeping APIs.
>
> Signed-off-by: Nam Cao <namcao@xxxxxxxxxxxxx>
Thanks for the patch, looks reasonable.
I tried re-generating the header (sleep.h) with rvgen based on the new
specification and I'm getting a different order.
Is what you're committing the result of rvgen on your computer?
We probably still have some unpredictable result in the rvgen's output if that's
the case (no big deal then, though it triggers me a bit).
I would still like to run some tests on this, how urgently would you like this
patch through? I was really about to send Steve a PR with the other changes so
this might need to wait for the next merge window.
Thanks,
Gabriele
> ---
> kernel/trace/rv/monitors/sleep/sleep.c | 8 ++
> kernel/trace/rv/monitors/sleep/sleep.h | 98 ++++++++++++-----------
> tools/verification/models/rtapp/sleep.ltl | 1 +
> 3 files changed, 61 insertions(+), 46 deletions(-)
>
> 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
> @@ -49,6 +49,7 @@ static void ltl_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon, bo
> ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
> ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false);
> ltl_atom_set(mon, LTL_FUTEX_WAIT, false);
> + ltl_atom_set(mon, LTL_EPOLL_WAIT, false);
> ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false);
> ltl_atom_set(mon, LTL_BLOCK_ON_RT_MUTEX, false);
> }
> @@ -63,6 +64,7 @@ static void ltl_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon, bo
> ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false);
> ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
> ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false);
> + ltl_atom_set(mon, LTL_EPOLL_WAIT, false);
>
> if (strstarts(task->comm, "migration/"))
> ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, true);
> @@ -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
> }
> }
>
> @@ -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