Add test using pthread_rwlock

Author: thomasspriggs

regression/cbmc-sequentialization/rw_lock/race_test.c

@@ -0,0 +1,2 @@
+#define NO_LOCKS
+#include "with_lock.c"

regression/cbmc-sequentialization/rw_lock/race_test.desc

@@ -0,0 +1,12 @@
+FUTURE
+with_lock.c
+--unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound
+--
+Test that concurrent reading and and writing to a shared structure allows its
+state to become inconsistent.

regression/cbmc-sequentialization/rw_lock/with_lock.c

@@ -0,0 +1,138 @@
+#include <assert.h>
+#include <pthread.h>
+#include <sched.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+struct sharedt
+{
+#ifndef NO_LOCKS
+  pthread_rwlock_t lock;
+#endif
+  int a;
+  int b;
+  int c;
+};
+
+void set_state1(struct sharedt *shared)
+{
+  shared->a = 1;
+  shared->b = 2;
+  // The following call to yield causes a thread switch during concrete
+  // execution in order to demonstrate unsoundness without locks.
+  sched_yield();
+  shared->c = 3;
+}
+
+void set_state2(struct sharedt *shared)
+{
+  shared->a = 4;
+  shared->b = 5;
+  // The following call to yield causes a thread switch during concrete
+  // execution in order to demonstrate unsoundness without locks.
+  sched_yield();
+  shared->c = 6;
+}
+
+void *writer1(void *arguments)
+{
+  struct sharedt *shared = (struct sharedt *)arguments;
+  for(int i = 0; i < 1000; ++i)
+  {
+#ifndef NO_LOCKS
+    const int lock_error = pthread_rwlock_wrlock(&(shared->lock));
+    assert(!lock_error);
+#endif
+    set_state1(shared);
+#ifndef NO_LOCKS
+    const int unlock_error = pthread_rwlock_unlock(&(shared->lock));
+    assert(!unlock_error);
+#endif
+  }
+  pthread_exit(NULL);
+}
+
+void *writer2(void *arguments)
+{
+  struct sharedt *shared = (struct sharedt *)arguments;
+  for(int i = 0; i < 1000; ++i)
+  {
+#ifndef NO_LOCKS
+    const int lock_error = pthread_rwlock_wrlock(&(shared->lock));
+    assert(!lock_error);
+#endif
+    set_state2(shared);
+#ifndef NO_LOCKS
+    const int unlock_error = pthread_rwlock_unlock(&(shared->lock));
+    assert(!unlock_error);
+#endif
+  }
+  pthread_exit(NULL);
+}
+
+void *checker(void *arguments)
+{
+  struct sharedt *shared = (struct sharedt *)arguments;
+  for(int i = 0; i < 1000; ++i)
+  {
+#ifndef NO_LOCKS
+    const int lock_error = pthread_rwlock_rdlock(&(shared->lock));
+    assert(!lock_error);
+#endif
+    const bool is_state1 = shared->a == 1 && shared->b == 2 && shared->c == 3;
+    // The following call to yield causes a thread switch during concrete
+    // execution in order to demonstrate unsoundness without locks.
+    sched_yield();
+    const bool is_state2 = shared->a == 4 && shared->b == 5 && shared->c == 6;
+    assert(is_state1 != is_state2);
+#ifndef NO_LOCKS
+    const int unlock_error = pthread_rwlock_unlock(&(shared->lock));
+    assert(!unlock_error);
+#endif
+    printf(is_state1 ? "State1\n" : "State2\n");
+  }
+  pthread_exit(NULL);
+}
+
+int main(void)
+{
+  struct sharedt shared;
+  set_state1(&shared);
+#ifndef NO_LOCKS
+  const pthread_rwlockattr_t *init_attributes = NULL;
+  const int init_error = pthread_rwlock_init(&(shared.lock), init_attributes);
+  assert(!init_error);
+#endif
+
+  const pthread_attr_t *const attributes = NULL;
+  void *const thread_argument = &shared;
+  pthread_t thread_writer1;
+  assert(
+    !pthread_create(&thread_writer1, attributes, &writer1, thread_argument));
+  pthread_t thread_writer2;
+  assert(
+    !pthread_create(&thread_writer2, attributes, &writer2, thread_argument));
+
+  pthread_t thread_checker1;
+  pthread_t thread_checker2;
+  pthread_t thread_checker3;
+  assert(
+    !pthread_create(&thread_checker1, attributes, &checker, thread_argument));
+  assert(
+    !pthread_create(&thread_checker2, attributes, &checker, thread_argument));
+  assert(
+    !pthread_create(&thread_checker3, attributes, &checker, thread_argument));
+
+  assert(!pthread_join(thread_writer1, NULL));
+  assert(!pthread_join(thread_writer2, NULL));
+  assert(!pthread_join(thread_checker1, NULL));
+  assert(!pthread_join(thread_checker2, NULL));
+  assert(!pthread_join(thread_checker3, NULL));
+
+#ifndef NO_LOCKS
+  const int destroy_error = pthread_rwlock_destroy(&(shared.lock));
+  assert(!destroy_error);
+#endif
+  return EXIT_SUCCESS;
+}

regression/cbmc-sequentialization/rw_lock/with_lock.desc

@@ -0,0 +1,12 @@
+FUTURE
+with_lock.c
+--unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound
+--
+Test that an appropriate read write lock keeps the state of a shared structure
+consistent.