From 13c431dac467c466ed8f897072713f0fc23a35d2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 28 Oct 2026 08:42:35 +0000 Subject: [PATCH] C library: pthread_rwlock_rdlock must allow concurrent readers pthread_rwlock_rdlock used __CPROVER_assume(!lock), which blocks while any lock is held, including a read lock. Thus a second reader blocked, and all executions in which two threads hold a read lock at the same time were excluded. POSIX.1-2017 pthread_rwlock_rdlock(): "A thread may hold multiple concurrent read locks on rwlock". Only block while a writer holds the lock (bit 2), and set the reader bit (bit 1). The previously KNOWNBUG regression test is now CORE. Reported by Jeroen Robben (https://reports.robben.io/methodology/). Fixes #9316 Co-authored-by: Kiro --- regression/cbmc-library/pthread_rwlock_rdlock/main.c | 11 +++++++---- .../cbmc-library/pthread_rwlock_rdlock/test.desc | 8 ++++---- src/ansi-c/library/pthread_lib.c | 6 ++++-- 3 files changed, 15 insertions(+), 10 deletions(-) diff --git a/regression/cbmc-library/pthread_rwlock_rdlock/main.c b/regression/cbmc-library/pthread_rwlock_rdlock/main.c index 25647e44d783..d160fdc3ee9c 100644 --- a/regression/cbmc-library/pthread_rwlock_rdlock/main.c +++ b/regression/cbmc-library/pthread_rwlock_rdlock/main.c @@ -1,9 +1,12 @@ #include -#include +#include -int main() +// POSIX.1-2017: a thread may hold multiple concurrent read locks. +int main(void) { - pthread_rwlock_rdlock(); - assert(0); + pthread_rwlock_t l = PTHREAD_RWLOCK_INITIALIZER; + int r1 = pthread_rwlock_rdlock(&l); + int r2 = pthread_rwlock_rdlock(&l); + assert(0); // reachable: both rdlocks succeed return 0; } diff --git a/regression/cbmc-library/pthread_rwlock_rdlock/test.desc b/regression/cbmc-library/pthread_rwlock_rdlock/test.desc index 7ace9bfa3cbe..1f75d776f1e9 100644 --- a/regression/cbmc-library/pthread_rwlock_rdlock/test.desc +++ b/regression/cbmc-library/pthread_rwlock_rdlock/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG unix +CORE unix main.c ---pointer-check --bounds-check -^EXIT=0$ + +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 3b408b27f34b..00b2ceb3a4cb 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -466,8 +466,10 @@ int pthread_rwlock_rdlock(pthread_rwlock_t *lock) __CPROVER_atomic_begin(); __CPROVER_assert(*((signed char *)lock)!=-1, "lock not initialised or destroyed"); - __CPROVER_assume(!*((signed char *)lock)); - *((signed char *)lock)=1; + // POSIX.1-2017: a thread may hold multiple concurrent read locks; + // only a writer (bit 1) blocks a reader. + __CPROVER_assume(!(*((signed char *)lock) & 2)); + (*(signed char *)lock) |= 1; __CPROVER_atomic_end(); return 0; // we never fail }