From f2f0c12d0a3ba6946430c467f812b72acc8ad4e0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Nov 2024 10:48:10 +0200 Subject: [PATCH 1/4] Error on must-relocking of non-recursive mutex mayLocks analysis can warn on it, but mutex analysis can be definite about it. --- src/analyses/mutexAnalysis.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9b6aa4f4ca..a608b3b6e3 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -121,14 +121,17 @@ struct let add ctx ((addr, rw): AddrRW.t): D.t = match addr with - | Addr mv -> + | Addr ((v, o) as mv) -> let (s, m) = ctx.local in let s' = MustLocksetRW.add_mval_rw (mv, rw) s in let m' = - if MutexTypeAnalysis.must_be_recursive ctx mv then - MustMultiplicity.increment mv m - else + match ctx.ask (Queries.MutexType (v, Offset.Unit.of_offs o)) with + | `Lifted Recursive -> MustMultiplicity.increment mv m + | `Lifted NonRec -> + if MustLocksetRW.mem_mval mv s then + M.error ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a non-recursive mutex that is already held"; m + | `Bot | `Top -> m in (s', m') | NullPtr -> From dbdefab9825123e08c92b4c36618e7eacb7883d4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 29 Nov 2024 11:21:22 +0200 Subject: [PATCH 2/4] Fix must-double-locking in regression tests --- tests/regression/04-mutex/32-allfuns.c | 4 ++-- tests/regression/09-regions/31-equ_rc.c | 2 +- tests/regression/09-regions/32-equ_nr.c | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/regression/04-mutex/32-allfuns.c b/tests/regression/04-mutex/32-allfuns.c index b59c487c53..e6b88e47ce 100644 --- a/tests/regression/04-mutex/32-allfuns.c +++ b/tests/regression/04-mutex/32-allfuns.c @@ -8,11 +8,11 @@ pthread_mutex_t B_mutex = PTHREAD_MUTEX_INITIALIZER; void t1() { pthread_mutex_lock(&A_mutex); myglobal++; //RACE! - pthread_mutex_lock(&A_mutex); + pthread_mutex_unlock(&A_mutex); } void t2() { pthread_mutex_lock(&B_mutex); myglobal++; //RACE! - pthread_mutex_lock(&B_mutex); + pthread_mutex_unlock(&B_mutex); } diff --git a/tests/regression/09-regions/31-equ_rc.c b/tests/regression/09-regions/31-equ_rc.c index 7cea370c58..2f3aff7f63 100644 --- a/tests/regression/09-regions/31-equ_rc.c +++ b/tests/regression/09-regions/31-equ_rc.c @@ -15,7 +15,7 @@ struct s { void *t_fun(void *arg) { pthread_mutex_lock(&A.mutex); B.datum = 5; // RACE! - pthread_mutex_lock(&A.mutex); + pthread_mutex_unlock(&A.mutex); return NULL; } diff --git a/tests/regression/09-regions/32-equ_nr.c b/tests/regression/09-regions/32-equ_nr.c index d9b909546e..a242448ba8 100644 --- a/tests/regression/09-regions/32-equ_nr.c +++ b/tests/regression/09-regions/32-equ_nr.c @@ -15,7 +15,7 @@ struct s { void *t_fun(void *arg) { pthread_mutex_lock(&A.mutex); A.datum = 5; // NORACE - pthread_mutex_lock(&A.mutex); + pthread_mutex_unlock(&A.mutex); return NULL; } From 218770b8f3f825338db1e10911668151d3317f14 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 29 Nov 2024 11:21:55 +0200 Subject: [PATCH 3/4] Check must-double-locking in 03-practical/21-pfscan_combine_minimal --- tests/regression/03-practical/21-pfscan_combine_minimal.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/03-practical/21-pfscan_combine_minimal.c b/tests/regression/03-practical/21-pfscan_combine_minimal.c index abdef0627b..86cfdabac1 100644 --- a/tests/regression/03-practical/21-pfscan_combine_minimal.c +++ b/tests/regression/03-practical/21-pfscan_combine_minimal.c @@ -18,7 +18,7 @@ int pqueue_init(PQUEUE *qp) void pqueue_close(PQUEUE *qp ) { - pthread_mutex_lock(& qp->mtx); + pthread_mutex_lock(& qp->mtx); // WARN (must double locking) qp->closed = 1; pthread_mutex_unlock(& qp->mtx); return; @@ -26,7 +26,7 @@ void pqueue_close(PQUEUE *qp ) int pqueue_put(PQUEUE *qp) { - pthread_mutex_lock(& qp->mtx); + pthread_mutex_lock(& qp->mtx); // WARN (must double locking) if (qp->closed) { // pfscan actually has a bug and is missing the following unlock at early return // pthread_mutex_unlock(& qp->mtx); From f3dfca7a9ab28fe16ce77bfeac0d55f65058ff4c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 29 Nov 2024 17:25:15 +0200 Subject: [PATCH 4/4] Change must-double-locking in 03-practical/21-pfscan_combine_minimal to TODO On MacOS the mutex type is top because it's zero-initialized global. On MacOS zero-initialized mutex isn't the same as a default mutex (type 0). --- tests/regression/03-practical/21-pfscan_combine_minimal.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/03-practical/21-pfscan_combine_minimal.c b/tests/regression/03-practical/21-pfscan_combine_minimal.c index 86cfdabac1..b8fc7948b2 100644 --- a/tests/regression/03-practical/21-pfscan_combine_minimal.c +++ b/tests/regression/03-practical/21-pfscan_combine_minimal.c @@ -18,7 +18,7 @@ int pqueue_init(PQUEUE *qp) void pqueue_close(PQUEUE *qp ) { - pthread_mutex_lock(& qp->mtx); // WARN (must double locking) + pthread_mutex_lock(& qp->mtx); // TODO (OSX): WARN (must double locking) qp->closed = 1; pthread_mutex_unlock(& qp->mtx); return; @@ -26,7 +26,7 @@ void pqueue_close(PQUEUE *qp ) int pqueue_put(PQUEUE *qp) { - pthread_mutex_lock(& qp->mtx); // WARN (must double locking) + pthread_mutex_lock(& qp->mtx); // TODO (OSX): WARN (must double locking) if (qp->closed) { // pfscan actually has a bug and is missing the following unlock at early return // pthread_mutex_unlock(& qp->mtx);