summaryrefslogtreecommitdiffstats
path: root/tools/verification/models/rtapp
diff options
context:
space:
mode:
authorNuoqi Gui <gnq25@mails.tsinghua.edu.cn>2026-09-04 12:41:55 +0200
committerAlexei Starovoitov <ast@kernel.org>2026-09-04 12:24:25 -0700
commit2b97956af60810cd382b86b9ce9aea421b889861 (patch)
tree7d9b0d8a91f77e63deff23976f68555a4895346a /tools/verification/models/rtapp
downloadlinux-stable-2b97956af60810cd382b86b9ce9aea421b889861.tar.gz
linux-stable-2b97956af60810cd382b86b9ce9aea421b889861.zip
selftests/bpf: Test rhtab kptr cancellation semanticsgrafted
Resizable hash-map updates and deletions must not perform full special-field destruction in their caller context. In particular, a referenced kptr must remain attached to the allocation until the memory allocator destructor can release it safely. Add separate coverage for both affected paths. The update test stores a task kptr, replaces the ordinary value bytes with BPF_EXIST, and verifies that the kptr survived. The delete test removes an element and exchanges its kptr through the still-valid map-value pointer before the allocation is reclaimed. Both cases observe a NULL kptr when rhtab uses bpf_obj_free_fields(). They recover and release the reference after rhtab switches to cancellation semantics. Signed-off-by: Nuoqi Gui <gnq25@mails.tsinghua.edu.cn> [ kkd: Split update and delete coverage and rewrote the commit log ] Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com> Link: https://lore.kernel.org/r/20260904104203.345917-5-memxor@gmail.com Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Diffstat (limited to 'tools/verification/models/rtapp')
-rw-r--r--tools/verification/models/rtapp/pagefault.ltl1
-rw-r--r--tools/verification/models/rtapp/sleep.ltl20
-rw-r--r--tools/verification/models/rtapp/wakeup.ltl5
3 files changed, 26 insertions, 0 deletions
diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl
new file mode 100644
index 000000000..d7ce62102
--- /dev/null
+++ b/tools/verification/models/rtapp/pagefault.ltl
@@ -0,0 +1 @@
+RULE = always (RT imply not PAGEFAULT)
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl
new file mode 100644
index 000000000..4d78fdd20
--- /dev/null
+++ b/tools/verification/models/rtapp/sleep.ltl
@@ -0,0 +1,20 @@
+RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
+
+RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON
+ and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
+
+RT_VALID_SLEEP_REASON = FUTEX_WAIT
+ or RT_FRIENDLY_NANOSLEEP
+ or EPOLL_WAIT
+
+RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
+ and NANOSLEEP_TIMER_ABSTIME
+ and not NANOSLEEP_CLOCK_REALTIME
+
+RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
+ or WOKEN_BY_HARDIRQ
+ or WOKEN_BY_NMI
+ or ABORT_SLEEP
+
+ALLOWLIST = BLOCK_ON_RT_MUTEX
+ or FUTEX_LOCK_PI
diff --git a/tools/verification/models/rtapp/wakeup.ltl b/tools/verification/models/rtapp/wakeup.ltl
new file mode 100644
index 000000000..a5d63ca08
--- /dev/null
+++ b/tools/verification/models/rtapp/wakeup.ltl
@@ -0,0 +1,5 @@
+RULE = always (((RT and USER_THREAD) imply
+ (not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST))
+
+ALLOWLIST = BLOCK_ON_RT_MUTEX
+ or FUTEX_LOCK_PI