Add pthreads examples

Author: thomasspriggs

regression/cbmc-sequentialization/pthread_cond/test.c

@@ -0,0 +1,82 @@
+#include <assert.h>
+#include <pthread.h>
+#include <sched.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int shared_global;
+pthread_mutex_t signal_mutex;
+pthread_cond_t condition;
+
+void initialise_condition(void)
+{
+  pthread_mutexattr_t *mutex_attributes = NULL;
+  int pthread_mutex_init_error =
+    pthread_mutex_init(&signal_mutex, mutex_attributes);
+  assert(!pthread_mutex_init_error);
+
+  pthread_condattr_t *condition_attributes = NULL;
+  int condition_init_error =
+    pthread_cond_init(&condition, condition_attributes);
+  assert(!condition_init_error);
+}
+
+// Wait for signal. Note that pthreads requires us to lock and unlock the mutex
+// around the call to `pthread_cond_wait`.
+void wait(void)
+{
+  const int lock_error = pthread_mutex_lock(&signal_mutex);
+  assert(!lock_error);
+  const int wait_error = pthread_cond_wait(&condition, &signal_mutex);
+  assert(!wait_error);
+  const int unlock_error = pthread_mutex_unlock(&signal_mutex);
+  assert(!unlock_error);
+}
+
+void signal(void)
+{
+  const int lock_error = pthread_mutex_lock(&signal_mutex);
+  assert(!lock_error);
+  int signal_error = pthread_cond_signal(&condition);
+  assert(!signal_error);
+  const int unlock_error = pthread_mutex_unlock(&signal_mutex);
+  assert(!unlock_error);
+}
+
+void *worker(void *arguments)
+{
+  shared_global = 42;
+  signal();
+  pthread_exit(NULL);
+}
+
+pthread_t start_worker_thread(void)
+{
+  pthread_t worker_thread;
+  const pthread_attr_t *const attributes = NULL;
+  void *const worker_argument = NULL;
+  const int create_status =
+    pthread_create(&worker_thread, attributes, &worker, worker_argument);
+  assert(create_status == 0);
+  return worker_thread;
+}
+
+void join_thread(const pthread_t thread)
+{
+  const int join_status = pthread_join(thread, NULL);
+  assert(join_status == 0);
+}
+
+int main(void)
+{
+  shared_global = 0;
+  const pthread_t worker_thread1 = start_worker_thread();
+  wait();
+  assert(shared_global == 42);
+  join_thread(worker_thread1);
+
+  pthread_mutex_destroy(&signal_mutex);
+  pthread_cond_destroy(&condition);
+  return EXIT_SUCCESS;
+}

regression/cbmc-sequentialization/pthread_cond/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound
+--
+Test that signals can be used to ensure that the `shared_global` is set before
+the assertion on its value is reached.

regression/cbmc-sequentialization/pthread_join/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+#include <pthread.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+void *worker(void *arguments)
+{
+  int *return_value = malloc(sizeof(int));
+  *return_value = 42;
+  pthread_exit(return_value);
+}
+
+int main(void)
+{
+  pthread_t thread;
+  const pthread_attr_t *const attributes = NULL;
+  void *const worker_argument = NULL;
+  int create_status =
+    pthread_create(&thread, attributes, &worker, worker_argument);
+  assert(create_status == 0);
+  int *worker_return;
+  int join_status = pthread_join(thread, (void **)&worker_return);
+  assert(join_status == 0);
+  printf("Thread return value is %d.\n", *worker_return);
+  assert(*worker_return == 42);
+  free(worker_return);
+  return EXIT_SUCCESS;
+}

regression/cbmc-sequentialization/pthread_join/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound
+--
+Test that the assertion that the worker thread return value acquired by
+pthread_join is the expected hardcoded value cannot be violated.

regression/cbmc-sequentialization/pthread_mutex/no_mutex.c

@@ -0,0 +1,52 @@
+#include <assert.h>
+#include <pthread.h>
+#include <sched.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int shared_count = 0;
+
+void *worker(void *arguments)
+{
+  for(int i = 0; i < 100; ++i)
+  {
+    int shared_count_copy = shared_count;
+    // The following call to yield is here in order to cause a thread swap
+    // during concrete execution in order to demonstrate unsoundness.
+    sched_yield();
+    ++shared_count_copy;
+    shared_count = shared_count_copy;
+  }
+  pthread_exit(NULL);
+}
+
+pthread_t start_worker_thread(void)
+{
+  pthread_t worker_thread;
+  const pthread_attr_t *const attributes = NULL;
+  void *const worker_argument = NULL;
+  const int create_status =
+    pthread_create(&worker_thread, attributes, &worker, worker_argument);
+  assert(create_status == 0);
+  return worker_thread;
+}
+
+void join_thread(const pthread_t thread)
+{
+  const int join_status = pthread_join(thread, NULL);
+  assert(join_status == 0);
+}
+
+int main(void)
+{
+  const pthread_t worker_thread1 = start_worker_thread();
+  const pthread_t worker_thread2 = start_worker_thread();
+  join_thread(worker_thread1);
+  join_thread(worker_thread2);
+
+  // Check if the shared count has been incremented 200 times.
+  printf("The shared count is %d.\n", shared_count);
+  assert(shared_count == 200);
+  return EXIT_SUCCESS;
+}

regression/cbmc-sequentialization/pthread_mutex/no_mutex.desc

@@ -0,0 +1,13 @@
+FUTURE
+no_mutex.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound
+--
+Test that cbmc can detect the unsafe shared global access. This is demonstrated
+by the violation of the final assertion that the final value of the shared count
+is 200.

regression/cbmc-sequentialization/pthread_mutex/with_mutex.c

@@ -0,0 +1,63 @@
+#include <assert.h>
+#include <pthread.h>
+#include <sched.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int shared_count = 0;
+pthread_mutex_t mutex;
+
+void *worker(void *arguments)
+{
+  for(int i = 0; i < 100; ++i)
+  {
+    const int lock_error = pthread_mutex_lock(&mutex);
+    assert(!lock_error);
+    int shared_count_copy = shared_count;
+    // The following call to yield is here in order to cause a thread swap
+    // during concrete execution in order to demonstrate unsoundness.
+    sched_yield();
+    ++shared_count_copy;
+    shared_count = shared_count_copy;
+    const int unlock_error = pthread_mutex_unlock(&mutex);
+    assert(!unlock_error);
+  }
+  pthread_exit(NULL);
+}
+
+pthread_t start_worker_thread(void)
+{
+  pthread_t worker_thread;
+  const pthread_attr_t *const attributes = NULL;
+  void *const worker_argument = NULL;
+  const int create_status =
+    pthread_create(&worker_thread, attributes, &worker, worker_argument);
+  assert(create_status == 0);
+  return worker_thread;
+}
+
+void join_thread(const pthread_t thread)
+{
+  const int join_status = pthread_join(thread, NULL);
+  assert(join_status == 0);
+}
+
+int main(void)
+{
+  pthread_mutexattr_t *mutex_attributes = NULL;
+  int pthread_mutex_init_error = pthread_mutex_init(&mutex, mutex_attributes);
+  assert(!pthread_mutex_init_error);
+
+  const pthread_t worker_thread1 = start_worker_thread();
+  const pthread_t worker_thread2 = start_worker_thread();
+  join_thread(worker_thread1);
+  join_thread(worker_thread2);
+
+  // Check if the shared count has been incremented 200 times.
+  printf("The shared count is %d.\n", shared_count);
+  assert(shared_count == 200);
+
+  pthread_mutex_destroy(&mutex);
+  return EXIT_SUCCESS;
+}

regression/cbmc-sequentialization/pthread_mutex/with_mutex.desc

@@ -0,0 +1,12 @@
+FUTURE
+with_mutex.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound
+--
+Test that adding an appropriate mutex to the `no_mutex.c` example leads to cbmc
+considering the program to be sound.

regression/cbmc-sequentialization/pthread_self_equal/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <pthread.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+pthread_t worker_self_thread;
+
+void *worker(void *arguments)
+{
+  // Check pthread_self() returns a consistent value.
+  const pthread_t self1 = pthread_self();
+  const pthread_t self2 = pthread_self();
+  assert(pthread_equal(self1, self2));
+
+  worker_self_thread = self1;
+  pthread_exit(NULL);
+}
+
+int main(void)
+{
+  pthread_t worker_thread;
+  const pthread_attr_t *const attributes = NULL;
+  void *const worker_argument = NULL;
+  const int create_status =
+    pthread_create(&worker_thread, attributes, &worker, worker_argument);
+  assert(create_status == 0);
+  const int join_status = pthread_join(worker_thread, NULL);
+  assert(join_status == 0);
+
+  // Check main thread self is different from worker thread self.
+  const pthread_t main_thread = pthread_self();
+  assert(!pthread_equal(main_thread, worker_self_thread));
+  return EXIT_SUCCESS;
+}

regression/cbmc-sequentialization/pthread_self_equal/test.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound
+--
+Test sanity of values returned by pthread_self and pthread_equal.