From: Sang-Heon Jeon <ekffu200098@gmail.com>
To: Julia Lawall <Julia.Lawall@inria.fr>,
Nicolas Palix <nicolas.palix@imag.fr>
Cc: cocci@inria.fr, linux-kernel@vger.kernel.org
Subject: [cocci] [PATCH 1/3] coccinelle: mini_lock: improve performance when searching loops
Date: Sat, 25 Jul 2026 20:32:39 +0900 [thread overview]
Message-ID: <20260725113303.691676-2-ekffu200098@gmail.com> (raw)
In-Reply-To: <20260725113303.691676-1-ekffu200098@gmail.com>
The 'looped' rule collects the returns inside a for loop to
prevent 'err' from reporting them. It searches every for loop in
the file, and on files with large loop bodies the search explodes.
For example, kernel/bpf/verifier.c runs for over 200 seconds,
almost entirely in 'looped' according to --profile. Since the
kernel .cocciconfig sets a 200 second timeout, coccicheck silently
skips the file.
To avoid this, collect the candidate returns first, so that
'looped' checks only those positions. 'err' then excludes what
'looped' found.
Every return that 'err' can report is also a candidate, so the
same returns are excluded as before and the output does not change.
A report-mode run over every .c file in the tree produces identical
output.
So verifier.c now finishes well within the timeout, in a few
seconds.
Signed-off-by: Sang-Heon Jeon <ekffu200098@gmail.com>
---
scripts/coccinelle/locks/mini_lock.cocci | 24 ++++++++++++++++++++++--
1 file changed, 22 insertions(+), 2 deletions(-)
diff --git a/scripts/coccinelle/locks/mini_lock.cocci b/scripts/coccinelle/locks/mini_lock.cocci
index 71065d8a5d54..54e06cced63b 100644
--- a/scripts/coccinelle/locks/mini_lock.cocci
+++ b/scripts/coccinelle/locks/mini_lock.cocci
@@ -53,11 +53,31 @@ spin_lock_irq@p1
spin_lock_irqsave@p1
) (E1@p,...);
-@looped@
+@err_candidate exists@
+expression E1;
+position prelocked.p;
+position up != prelocked.p1;
+position rc;
+identifier lock,unlock;
+@@
+
+lock(E1@p,...);
+... when != E1
+ when any
+if (...) {
+ ... when != E1
+ return@rc ...;
+}
+... when != E1
+ when any
+unlock@up(E1,...);
+
+@looped depends on err_candidate@
+position err_candidate.rc;
position r;
@@
-for(...;...;...) { <+... return@r ...; ...+> }
+for(...;...;...) { <+... return@rc@r ...; ...+> }
@err exists@
expression E1;
--
2.43.0
WARNING: multiple messages have this Message-ID (diff)
From: Sang-Heon Jeon <ekffu200098@gmail.com>
To: Julia Lawall <Julia.Lawall@inria.fr>,
Nicolas Palix <nicolas.palix@imag.fr>
Cc: cocci@inria.fr, linux-kernel@vger.kernel.org
Subject: [PATCH 1/3] coccinelle: mini_lock: improve performance when searching loops
Date: Sat, 25 Jul 2026 20:32:39 +0900 [thread overview]
Message-ID: <20260725113303.691676-2-ekffu200098@gmail.com> (raw)
In-Reply-To: <20260725113303.691676-1-ekffu200098@gmail.com>
The 'looped' rule collects the returns inside a for loop to
prevent 'err' from reporting them. It searches every for loop in
the file, and on files with large loop bodies the search explodes.
For example, kernel/bpf/verifier.c runs for over 200 seconds,
almost entirely in 'looped' according to --profile. Since the
kernel .cocciconfig sets a 200 second timeout, coccicheck silently
skips the file.
To avoid this, collect the candidate returns first, so that
'looped' checks only those positions. 'err' then excludes what
'looped' found.
Every return that 'err' can report is also a candidate, so the
same returns are excluded as before and the output does not change.
A report-mode run over every .c file in the tree produces identical
output.
So verifier.c now finishes well within the timeout, in a few
seconds.
Signed-off-by: Sang-Heon Jeon <ekffu200098@gmail.com>
---
scripts/coccinelle/locks/mini_lock.cocci | 24 ++++++++++++++++++++++--
1 file changed, 22 insertions(+), 2 deletions(-)
diff --git a/scripts/coccinelle/locks/mini_lock.cocci b/scripts/coccinelle/locks/mini_lock.cocci
index 71065d8a5d54..54e06cced63b 100644
--- a/scripts/coccinelle/locks/mini_lock.cocci
+++ b/scripts/coccinelle/locks/mini_lock.cocci
@@ -53,11 +53,31 @@ spin_lock_irq@p1
spin_lock_irqsave@p1
) (E1@p,...);
-@looped@
+@err_candidate exists@
+expression E1;
+position prelocked.p;
+position up != prelocked.p1;
+position rc;
+identifier lock,unlock;
+@@
+
+lock(E1@p,...);
+... when != E1
+ when any
+if (...) {
+ ... when != E1
+ return@rc ...;
+}
+... when != E1
+ when any
+unlock@up(E1,...);
+
+@looped depends on err_candidate@
+position err_candidate.rc;
position r;
@@
-for(...;...;...) { <+... return@r ...; ...+> }
+for(...;...;...) { <+... return@rc@r ...; ...+> }
@err exists@
expression E1;
--
2.43.0
next prev parent reply other threads:[~2026-07-25 11:44 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-07-25 11:32 [cocci] [PATCH 0/3] coccinelle: improve performance of mini_lock, double_lock and minmax Sang-Heon Jeon
2026-07-25 11:32 ` Sang-Heon Jeon
2026-07-25 11:32 ` Sang-Heon Jeon [this message]
2026-07-25 11:32 ` [PATCH 1/3] coccinelle: mini_lock: improve performance when searching loops Sang-Heon Jeon
2026-07-25 11:32 ` [cocci] [PATCH 2/3] coccinelle: double_lock: improve performance when no double lock exists Sang-Heon Jeon
2026-07-25 11:32 ` Sang-Heon Jeon
2026-07-25 11:32 ` [cocci] [PATCH 3/3] coccinelle: misc: minmax: improve performance when no candidate exists Sang-Heon Jeon
2026-07-25 11:32 ` Sang-Heon Jeon
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20260725113303.691676-2-ekffu200098@gmail.com \
--to=ekffu200098@gmail.com \
--cc=Julia.Lawall@inria.fr \
--cc=cocci@inria.fr \
--cc=linux-kernel@vger.kernel.org \
--cc=nicolas.palix@imag.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.