diff options
Diffstat (limited to 'tools/verification')
| -rw-r--r-- | tools/verification/models/rtapp/sleep.ltl | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl index 5923e58d7810..4d78fdd204c0 100644 --- a/tools/verification/models/rtapp/sleep.ltl +++ b/tools/verification/models/rtapp/sleep.ltl @@ -1,6 +1,6 @@ -RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) +RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) -RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD) +RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE) RT_VALID_SLEEP_REASON = FUTEX_WAIT @@ -15,9 +15,6 @@ RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO or WOKEN_BY_HARDIRQ or WOKEN_BY_NMI or ABORT_SLEEP - or KTHREAD_SHOULD_STOP ALLOWLIST = BLOCK_ON_RT_MUTEX or FUTEX_LOCK_PI - or TASK_IS_RCU - or TASK_IS_MIGRATION |