C library: pthread_rwlock_rdlock must allow concurrent readers

regression/cbmc-library/pthread_rwlock_rdlock/main.c

@@ -1,9 +1,12 @@
 #include <assert.h>
-#include <pthread_lib.h>
+#include <pthread.h>
 
-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;
 }

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

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
 }