Merge branch 'for-linus' of git://git.infradead.org/users/eparis/notify
[pandora-kernel.git] / scripts / coccinelle / locks / double_lock.cocci
1 /// Find double locks.  False positives may occur when some paths cannot
2 /// occur at execution, due to the values of variables, and when there is
3 /// an intervening function call that releases the lock.
4 ///
5 // Confidence: Moderate
6 // Copyright: (C) 2010 Nicolas Palix, DIKU.  GPLv2.
7 // Copyright: (C) 2010 Julia Lawall, DIKU.  GPLv2.
8 // Copyright: (C) 2010 Gilles Muller, INRIA/LiP6.  GPLv2.
9 // URL: http://coccinelle.lip6.fr/
10 // Comments:
11 // Options: -no_includes -include_headers
12
13 virtual org
14 virtual report
15
16 @locked@
17 position p1;
18 expression E1;
19 position p;
20 @@
21
22 (
23 mutex_lock@p1
24 |
25 mutex_trylock@p1
26 |
27 spin_lock@p1
28 |
29 spin_trylock@p1
30 |
31 read_lock@p1
32 |
33 read_trylock@p1
34 |
35 write_lock@p1
36 |
37 write_trylock@p1
38 ) (E1@p,...);
39
40 @balanced@
41 position p1 != locked.p1;
42 position locked.p;
43 identifier lock,unlock;
44 expression x <= locked.E1;
45 expression E,locked.E1;
46 expression E2;
47 @@
48
49 if (E) {
50  <+... when != E1
51  lock(E1@p,...)
52  ...+>
53 }
54 ... when != E1
55     when != \(x = E2\|&x\)
56     when forall
57 if (E) {
58  <+... when != E1
59  unlock@p1(E1,...)
60  ...+>
61 }
62
63 @r depends on !balanced exists@
64 expression x <= locked.E1;
65 expression locked.E1;
66 expression E2;
67 identifier lock;
68 position locked.p,p1,p2;
69 @@
70
71 lock@p1 (E1@p,...);
72 ... when != E1
73     when != \(x = E2\|&x\)
74 lock@p2 (E1,...);
75
76 @script:python depends on org@
77 p1 << r.p1;
78 p2 << r.p2;
79 lock << r.lock;
80 @@
81
82 cocci.print_main(lock,p1)
83 cocci.print_secs("second lock",p2)
84
85 @script:python depends on report@
86 p1 << r.p1;
87 p2 << r.p2;
88 lock << r.lock;
89 @@
90
91 msg = "second lock on line %s" % (p2[0].line)
92 coccilib.report.print_report(p1[0],msg)