1. Patchew
  2. linux
  3. View series

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

Nam Cao posted 1 patch 1 day ago 
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(-)
[PATCH] rv: Allow epoll in rtapp-sleep monitor
Posted by Nam Cao 1 day ago 
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@linutronix.de>
---
 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
-- 
2.47.3
Re: [PATCH] rv: Allow epoll in rtapp-sleep monitor
Posted by Gabriele Monaco 19 hours ago 
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
Re: [PATCH] rv: Allow epoll in rtapp-sleep monitor
Posted by Nam Cao 19 hours ago 
Gabriele Monaco <gmonaco@redhat.com> writes:
> 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?

No that's not intentional. It does not affect verification result, but
still should be fixed. I will send v2.

Funnily a colleague just told me earlier today about how good AIs are at
reviewing..

Nam
Re: [PATCH] rv: Allow epoll in rtapp-sleep monitor
Posted by Gabriele Monaco 22 hours ago 
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@linutronix.de>

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
Re: [PATCH] rv: Allow epoll in rtapp-sleep monitor
Posted by Nam Cao 21 hours ago 
Gabriele Monaco <gmonaco@redhat.com> writes:

> 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@linutronix.de>
>
> 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).

Right, fixing this is in my list. The script uses set and set's order is
not deterministic. You get different (but equivalent) results every
time. I should start working on that..

> 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.

The earlier the better, but no one will die because it misses a merge
window.

Nam
Re: [PATCH] rv: Allow epoll in rtapp-sleep monitor
Posted by Gabriele Monaco 21 hours ago 
On Tue, 2026-03-31 at 15:41 +0200, Nam Cao wrote:
> Gabriele Monaco <gmonaco@redhat.com> writes:
> 
> > 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@linutronix.de>
> > 
> > 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).
> 
> Right, fixing this is in my list. The script uses set and set's order is
> not deterministic. You get different (but equivalent) results every
> time. I should start working on that..

Reasonable, no rush. I just noticed this behaviour when trying to write some
selftests for rvgen and didn't manage to make it deterministic with trivial
changes.

> 
> > 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.
> 
> The earlier the better, but no one will die because it misses a merge
> window.

Alright I'll see if I can squeeze it in within this week, if not, it'll have to
wait. For now:

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

Thanks,
Gabriele

Patchew 2.1-devel-ea86937

© 2016 - 2026 Red Hat, Inc.