cocci.inria.fr archive mirror
 help / color / mirror / Atom feed
From: Sumera Priyadarsini <sylphrenadin@gmail.com>
To: Julia.Lawall@lip6.fr
Cc: linux-kernel@vger.kernel.org, michal.lkml@markovi.net,
	nicolas.palix@imag.fr, cocci@systeme.lip6.fr,
	Gilles.Muller@lip6.fr
Subject: [Cocci] [PATCH] coccinelle: locks: Add balancedlock.cocci script
Date: Fri, 6 Nov 2020 17:15:12 +0530	[thread overview]
Message-ID: <20201106114512.fl22zzewvnimfxnb@adolin> (raw)

When acquiring locks under certain conditions, they must be released
under the same conditions as well. However, sometimes, there may be
missing unlocks which may lead to a potential deadlock.

Add this script to detect such code segments and avoid potential
deadlock situations.

Signed-off-by: Sumera Priyadarsini <sylphrenadin@gmail.com>
---
 scripts/coccinelle/locks/balancedlock.cocci | 162 ++++++++++++++++++++
 1 file changed, 162 insertions(+)
 create mode 100644 scripts/coccinelle/locks/balancedlock.cocci

diff --git a/scripts/coccinelle/locks/balancedlock.cocci b/scripts/coccinelle/locks/balancedlock.cocci
new file mode 100644
index 000000000000..fe7bc2dfeb29
--- /dev/null
+++ b/scripts/coccinelle/locks/balancedlock.cocci
@@ -0,0 +1,162 @@
+/// Sometimes, locks that are acquired under certain conditions may have missing unlocks
+/// leading to a potential deadlock situation. This patch detects such cases.
+//# False positives may be generated due to locks released within a nested
+//# function call or a goto block.
+///
+// Confidence: Moderate
+// Copyright: (C) 2020 Julia Lawall INRIA/LIP6
+
+virtual context
+virtual org
+virtual report
+
+
+@prelocked@
+expression E;
+position p;
+@@
+
+(
+mutex_lock(E@p);
+|
+read_lock(E@p);
+|
+write_lock(E@p);
+|
+spin_lock(E@p);
+|
+spin_lock_bh(E@p);
+|
+spin_lock_irqsave(E@p, ...);
+|
+read_lock_irqsave(E@p, ...);
+|
+write_lock_irqsave(E@p, ...);
+|
+raw_spin_lock(E@p);
+|
+raw_spin_lock_irq(E@p);
+|
+raw_spin_lock_bh(E@p);
+|
+local_lock(E@p);
+|
+local_lock_irq(E@p);
+|
+local_lock_irqsave(E@p, ...);
+|
+read_lock_irq(E@p);
+|
+read_lock_bh(E@p);
+|
+write_lock_bh(E@p);
+)
+
+@balanced@
+position prelocked.p;
+position pif;
+expression e,prelocked.E;
+statement S1,S2;
+identifier lock;
+identifier unlock={mutex_unlock,
+                   spin_unlock,
+                   spin_unlock_bh,
+                   spin_unlock_irqrestore,
+                   read_unlock_irqrestore,
+                   write_unlock_irqrestore,
+                   raw_spin_unlock,
+                   raw_spin_unlock_irq,
+                   raw_spin_unlock_bh,
+                   local_unlock,
+                   local_unlock_irq,
+                   local_unlock_irqrestore,
+                   read_unlock_irq,
+                   read_unlock_bh,
+                   write_unlock_bh
+                   };
+@@
+
+if (e) {
+ ... when any
+lock(E@p, ...)
+ ... when != E
+     when any
+} else S1
+... when != E
+    when any
+if@pif (e) {
+ ... when != E
+     when any
+ unlock(E, ...);
+ ... when any
+} else S2
+...  when != E
+     when any
+
+// ----------------------------------------------------------------------------
+
+@balanced2 depends on context || org || report@
+identifier lock, unlock = {mutex_unlock,
+                           spin_unlock,
+                           spin_unlock_bh,
+                           spin_unlock_irqrestore,
+                           read_unlock_irqrestore,
+                           write_unlock_irqrestore,
+                           raw_spin_unlock,
+                           raw_spin_unlock_irq,
+                           raw_spin_unlock_bh,
+                           local_unlock,
+                           local_unlock_irq,
+                           local_unlock_irqrestore,
+                           read_unlock_irq,
+                           read_unlock_bh,
+                           write_unlock_bh
+                           };
+expression E, f, x;
+statement S1, S2, S3, S4;
+position prelocked.p, balanced.pif;
+position j0, j1, j2, j3;
+@@
+
+* lock@j0(E@p, ...);
+... when != E;
+    when != if@pif (...) S1 else S2
+    when any
+x@j1 = f(...);
+* if (<+...x...+>)
+{
+  ... when != E;
+      when forall
+      when != if@pif (...) S3 else S4
+*  return@j2 ...;
+}
+... when any
+* unlock@j3(E, ...);
+
+// ----------------------------------------------------------------------------
+
+@script:python balanced2_org depends on org@
+j0 << balanced2.j0;
+j1 << balanced2.j1;
+j2 << balanced2.j2;
+j3 << balanced2.j3;
+@@
+
+msg = "This code segment might have an unbalanced lock."
+coccilib.org.print_todo(j0[0], msg)
+coccilib.org.print_link(j1[0], "")
+coccilib.org.print_link(j2[0], "")
+coccilib.org.print_link(j3[0], "")
+
+// ----------------------------------------------------------------------------
+
+@script:python balanced2_report depends on report@
+j0 << balanced2.j0;
+j1 << balanced2.j1;
+j2 << balanced2.j2;
+j3 << balanced2.j3;
+@@
+
+msg = "This code segment might have an unbalanced lock around lines %s,%s,%s." % (j1[0].line,j2[0].line,j3[0].line)
+coccilib.report.print_report(j0[0], msg)
+
-- 
2.25.1

_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

                 reply	other threads:[~2020-11-06 11:45 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

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=20201106114512.fl22zzewvnimfxnb@adolin \
    --to=sylphrenadin@gmail.com \
    --cc=Gilles.Muller@lip6.fr \
    --cc=Julia.Lawall@lip6.fr \
    --cc=cocci@systeme.lip6.fr \
    --cc=linux-kernel@vger.kernel.org \
    --cc=michal.lkml@markovi.net \
    --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;
as well as URLs for NNTP newsgroup(s).