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 <[email protected]> --- 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
