From 36cd4873c78c11cf62e4b9f6338bfd64bd1d3bfa Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 22 Mar 2022 16:59:06 +0200 Subject: [PATCH 1/5] Fix read-write lock access handling (issue #658) --- src/analyses/mutexAnalysis.ml | 27 ++++++++++++++--------- src/cdomains/lockDomain.ml | 22 +++++++++++------- tests/regression/04-mutex/40-rw_lock_rc.c | 2 +- tests/regression/04-mutex/41-pt_rwlock.c | 4 ++-- 4 files changed, 34 insertions(+), 21 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 21bc76686b..3742179cf5 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -155,20 +155,27 @@ struct module A = struct - include D + include Printable.Prod (Mutexes) (Mutexes) (* exclusive locks (normal, writer); non-exclusive locks (reader) *) let name () = "lock" - let may_race ls1 ls2 = - is_empty (join ls1 ls2) (* D is reversed, so join is intersect *) - let should_print ls = not (is_empty ls) + let may_race (ws1, rs1) (ws2, rs2) = + Mutexes.is_empty (Mutexes.inter ws1 ws2) && Mutexes.is_empty (Mutexes.inter ws1 rs2) && Mutexes.is_empty (Mutexes.inter rs1 ws2) + let should_print (ws, rs) = not (Mutexes.is_empty ws) || not (Mutexes.is_empty rs) + + let pretty () (ws, rs) = + let ls = Lockset.meet (Lockset.import_locks ws true) (Lockset.import_locks rs false) in + Lockset.pretty () ls + + include Printable.SimplePretty ( + struct + type nonrec t = t + let pretty = pretty + end + ) end let access ctx e vo w = - if w then - (* when writing: ignore reader locks *) - Lockset.filter snd ctx.local - else - (* when reading: bump reader locks to exclusive as they protect reads *) - Lockset.map (fun (x,_) -> (x,true)) ctx.local + let (writers, readers) = Lockset.ReverseAddrSet.partition snd ctx.local in + (Lockset.export_locks writers, Lockset.export_locks readers) (** Transfer functions: *) diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index cf81c7469e..94ed5a87a4 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -32,17 +32,20 @@ struct (* pair Addr and RW; also change pretty printing*) module Lock = struct - module L = Printable.Prod (Addr) (RW) - include L + include Printable.Prod (Addr) (RW) - let show (a,write) = - let addr_str = Addr.show a in + let pretty () (a, write) = if write then - addr_str + Addr.pretty () a else - "read lock " ^ addr_str - - let pretty () x = text (show x) + Pretty.dprintf "read lock %a" Addr.pretty a + + include Printable.SimplePretty ( + struct + type nonrec t = t + let pretty = pretty + end + ) end (* TODO: use SetDomain.Reverse *) @@ -90,6 +93,9 @@ struct let export_locks ls = let f (x,_) set = Mutexes.add x set in fold f ls (Mutexes.empty ()) + + let import_locks ls write = + Mutexes.fold (fun x acc -> add (x, write) acc) ls (empty ()) end module MayLockset = diff --git a/tests/regression/04-mutex/40-rw_lock_rc.c b/tests/regression/04-mutex/40-rw_lock_rc.c index 72f8a5e206..27c4cf4d8b 100644 --- a/tests/regression/04-mutex/40-rw_lock_rc.c +++ b/tests/regression/04-mutex/40-rw_lock_rc.c @@ -24,7 +24,7 @@ static ssize_t my_read(struct file *file, char __user *buf, size_t count, loff_t static ssize_t my_write(struct file *fp, const char __user *buf, size_t len, loff_t *off) { write_lock(&rwlock1); - data1 = data1==1 ? 0 : 1; //RACE! + data1 = data1==1 ? 0 : 1; //NORACE write_unlock(&rwlock1); write_lock(&rwlock2); diff --git a/tests/regression/04-mutex/41-pt_rwlock.c b/tests/regression/04-mutex/41-pt_rwlock.c index a116234697..af80ddadee 100644 --- a/tests/regression/04-mutex/41-pt_rwlock.c +++ b/tests/regression/04-mutex/41-pt_rwlock.c @@ -9,7 +9,7 @@ static pthread_rwlock_t rwlock = PTHREAD_RWLOCK_INITIALIZER; void *t_fun(void *arg) { pthread_rwlock_wrlock(&rwlock); data1++; // NORACE - printf("%d",data2); // RACE + printf("%d",data2); // NORACE pthread_rwlock_unlock(&rwlock); return NULL; } @@ -20,7 +20,7 @@ int main(void) { pthread_rwlock_rdlock(&rwlock); printf("%d",data1); // NORACE - data2++; // RACE + data2++; // NORACE pthread_rwlock_unlock(&rwlock); pthread_join (id, NULL); From 0f3cea963d95bf5739a2d0d2f4c5f18720f7d041 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 22 Mar 2022 16:59:20 +0200 Subject: [PATCH 2/5] Ignore pthread_rwlock_t accesses --- src/domains/access.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/domains/access.ml b/src/domains/access.ml index 5102e6076d..2d98846603 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -10,7 +10,7 @@ module M = Messages let is_ignorable_type (t: typ): bool = match t with - | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "spinlock_t"; _ }, _) -> true + | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "spinlock_t"; _ }, _) -> true | TComp ({ cname = "lock_class_key"; _ }, _) -> true | TInt (IInt, attr) when hasAttribute "mutex" attr -> true | t when hasAttribute "atomic" (typeAttrs t) -> true (* C11 _Atomic *) From 54dc4187bf72867eedf919615b916f6190664a68 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 22 Mar 2022 17:17:04 +0200 Subject: [PATCH 3/5] Change exitfuns to have unique thread IDs --- src/analyses/threadId.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index aa0947e62b..658e0a3975 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -34,7 +34,7 @@ struct let name () = "threadid" let startstate v = (ThreadLifted.bot (), TD.bot ()) - let exitstate v = (`Lifted (Thread.threadinit v ~multiple:true), TD.bot ()) + let exitstate v = (`Lifted (Thread.threadinit v ~multiple:false), TD.bot ()) let morphstate v _ = let tid = Thread.threadinit v ~multiple:false in From c97adbd068648f58d0a474accf5d719b72dd6437 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 22 Mar 2022 17:29:50 +0200 Subject: [PATCH 4/5] Simplify mutex analysis access back to single set Instead may_race looks for mutually exclusive lock pair directly. This avoids constructing many intermediate sets. --- src/analyses/mutexAnalysis.ml | 30 +++++++++++++----------------- src/cdomains/lockDomain.ml | 3 --- 2 files changed, 13 insertions(+), 20 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 3742179cf5..5126e70a71 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -155,27 +155,23 @@ struct module A = struct - include Printable.Prod (Mutexes) (Mutexes) (* exclusive locks (normal, writer); non-exclusive locks (reader) *) + include D let name () = "lock" - let may_race (ws1, rs1) (ws2, rs2) = - Mutexes.is_empty (Mutexes.inter ws1 ws2) && Mutexes.is_empty (Mutexes.inter ws1 rs2) && Mutexes.is_empty (Mutexes.inter rs1 ws2) - let should_print (ws, rs) = not (Mutexes.is_empty ws) || not (Mutexes.is_empty rs) - - let pretty () (ws, rs) = - let ls = Lockset.meet (Lockset.import_locks ws true) (Lockset.import_locks rs false) in - Lockset.pretty () ls - - include Printable.SimplePretty ( - struct - type nonrec t = t - let pretty = pretty - end - ) + let may_race ls1 ls2 = + (* not mutually exclusive *) + not @@ D.ReverseAddrSet.exists (fun ((m1, w1) as l1) -> + if w1 then + (* write lock is exclusive with write lock or read lock *) + D.ReverseAddrSet.mem l1 ls2 || D.ReverseAddrSet.mem (m1, false) ls2 + else + (* read lock is exclusive with just write lock *) + D.ReverseAddrSet.mem (m1, true) ls2 + ) ls1 + let should_print ls = not (is_empty ls) end let access ctx e vo w = - let (writers, readers) = Lockset.ReverseAddrSet.partition snd ctx.local in - (Lockset.export_locks writers, Lockset.export_locks readers) + ctx.local (** Transfer functions: *) diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index 94ed5a87a4..1fa5e375c5 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -93,9 +93,6 @@ struct let export_locks ls = let f (x,_) set = Mutexes.add x set in fold f ls (Mutexes.empty ()) - - let import_locks ls write = - Mutexes.fold (fun x acc -> add (x, write) acc) ls (empty ()) end module MayLockset = From 2d7fa308807e0c0ed2f7990556449c9d8b8f1d39 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 22 Mar 2022 17:47:28 +0200 Subject: [PATCH 5/5] Add mem & exists to LockDomain.Lockset --- src/analyses/mutexAnalysis.ml | 6 +++--- src/cdomains/lockDomain.ml | 2 ++ 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 5126e70a71..bf24fa2f44 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -159,13 +159,13 @@ struct let name () = "lock" let may_race ls1 ls2 = (* not mutually exclusive *) - not @@ D.ReverseAddrSet.exists (fun ((m1, w1) as l1) -> + not @@ D.exists (fun ((m1, w1) as l1) -> if w1 then (* write lock is exclusive with write lock or read lock *) - D.ReverseAddrSet.mem l1 ls2 || D.ReverseAddrSet.mem (m1, false) ls2 + D.mem l1 ls2 || D.mem (m1, false) ls2 else (* read lock is exclusive with just write lock *) - D.ReverseAddrSet.mem (m1, true) ls2 + D.mem (m1, true) ls2 ) ls1 let should_print ls = not (is_empty ls) end diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index 1fa5e375c5..d37a31ec57 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -89,6 +89,8 @@ struct let filter = ReverseAddrSet.filter let fold = ReverseAddrSet.fold let singleton = ReverseAddrSet.singleton + let mem = ReverseAddrSet.mem + let exists = ReverseAddrSet.exists let export_locks ls = let f (x,_) set = Mutexes.add x set in