mirror of https://lore.kernel.org/lkml/
 help / color / mirror / Atom feed
From: Julia Lawall <julia.lawall@inria.fr>
To: Sang-Heon Jeon <ekffu200098@gmail.com>
Cc: Nicolas Palix <nicolas.palix@imag.fr>,
	cocci@inria.fr,  linux-kernel@vger.kernel.org
Subject: Re: [PATCH v2] coccinelle: mini_lock: improve performance when searching loops
Date: Thu, 6 Aug 2026 23:14:13 +0200 (CEST)	[thread overview]
Message-ID: <ee2d8872-4b8f-8ea0-282-51a3e5591ffa@inria.fr> (raw)
In-Reply-To: <20260727135249.1634580-1-ekffu200098@gmail.com>



On Mon, 27 Jul 2026, Sang-Heon Jeon wrote:

> 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.

Thanks for the fixes.  Applied.

julia

>
> Signed-off-by: Sang-Heon Jeon <ekffu200098@gmail.com>
> ---
> Changes from v1 [1]
> - remove unnecessary depends keyword as Julia suggested
> - add exists keyword to 'looped' rule
>
> [1] https://lore.kernel.org/all/20260725113303.691676-2-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..c65241c895ff 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 exists@
> +position err_candidate.rc;
>  position r;
>  @@
>
> -for(...;...;...) { <+... return@r ...; ...+> }
> +for(...;...;...) { <+... return@rc@r ...; ...+> }
>
>  @err exists@
>  expression E1;
> --
> 2.43.0
>
>

      reply	other threads:[~2026-08-06 21:14 UTC|newest]

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2026-07-27 13:52 Sang-Heon Jeon
2026-08-06 21:14 ` Julia Lawall [this message]

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=ee2d8872-4b8f-8ea0-282-51a3e5591ffa@inria.fr \
    --to=julia.lawall@inria.fr \
    --cc=cocci@inria.fr \
    --cc=ekffu200098@gmail.com \
    --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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox

all inboxes | Powered by JetHome®