rv: Allow epoll in rtapp-sleep monitor

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>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/20260401130828.3115428-1-namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

diff --git a/kernel/trace/rv/monitors/sleep/sleep.c b/kernel/trace/rv/monitors/sleep/sleep.c
index c1347da69e9decb0b9ce7e10677a212db7494f2d..8dfe5ec13e19297b1806203c7277362495d45c14 100644 (file)
--- 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_update(current, 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 2ab46fd218d232ca6084ad9bb7bacc923dd0dca7..95dc2727c059770c1dd5cbccf99b0c1a8be17e6e 100644 (file)
--- 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 6379bbeb62124b3e7e384c84419112d56889c937..6f26c4810f783ce1bf8dfb4c81609d4aeca83141 100644 (file)
--- 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