Refine modelling of pthread_join to avoid deadlock on invalid

thread id

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4311 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc-concurrency/pthread_join2/main.c

@@ -0,0 +1,98 @@
+#include <pthread.h>
+#include <assert.h>
+
+// ========= Chord library =========
+
+// This struct is not thread-safe itself!
+//
+// A chord is like a chain of threads `f, g, ...` where `f`
+// must terminate before `g` can start to run, and so forth.
+struct chord_t
+{
+  // last thread in chain
+  pthread_t thread;
+};
+
+// Public function pointer
+typedef void *(*start_routine)(void *);
+
+// Internal
+struct chord_args_t
+{
+  // last thread in chain
+  pthread_t thread;
+
+  // function pointer for new thread
+  start_routine f;
+
+  // argument to f
+  void *f_arg;
+};
+
+// Internal start routine for a thread in a chord
+static void* chord_start_routine(void *ptr)
+{
+  struct chord_args_t *args = (struct chord_args_t *) ptr; 
+
+  // ignore errors
+  pthread_join(args->thread, NULL);
+  return args->f(args->f_arg);
+}
+
+// This function is not thread-safe itself!
+//
+// Create a new thread for `f` where `f(arg)` starts to run as
+// soon as the currently running `self->thread` has terminated.
+//
+// \post: self->thread is the newly created thread for `f`
+int chord_run(struct chord_t *self, start_routine f, void *arg)
+{
+  struct chord_args_t args;
+  args.thread = self->thread;
+  args.f = f;
+  args.f_arg = arg;
+
+  return pthread_create(&(self->thread), NULL, chord_start_routine, (void *) &args);
+}
+
+// ========= Symbolic test =========
+
+char test_global;
+
+void* test_write_a( void *arg)
+{
+  test_global = 'A';
+  return NULL;
+}
+
+void* test_write_b(void *arg)
+{
+  test_global = 'B';
+  return NULL;
+}
+
+int main(void)
+{
+#ifdef _ENABLE_CHORD_
+  struct chord_t chord;
+  chord_run(&chord, test_write_a, NULL);
+  chord_run(&chord, test_write_b, NULL);
+#else
+  pthread_t a_thread, b_thread;
+  pthread_create(&a_thread, NULL, test_write_a, NULL);
+  pthread_create(&b_thread, NULL, test_write_b, NULL);
+#endif
+
+  char x = test_global;
+  char y = test_global;
+
+  // Verification condition:
+  //
+  //  If global variable equals 'B', then it cannot change.
+  //
+  // It is expected that this implication
+  // fails if _ENABLE_CHORD_ is undefined.
+  assert(x != 'B' || y == 'B');
+
+  return 0;
+}

regression/cbmc-concurrency/pthread_join2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/ansi-c/ansi_c_internal_additions.cpp

@@ -115,6 +115,7 @@ void ansi_c_internal_additions(std::string &code)
     "void __CPROVER_atomic_begin();\n"
     "void __CPROVER_atomic_end();\n"
     "void __CPROVER_fence(const char *kind, ...);\n"
+    "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
     "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
     "unsigned long __CPROVER_next_thread_id=0;\n"
 

src/ansi-c/library/cprover.h

@@ -31,6 +31,7 @@ void __CPROVER_atomic_begin();
 void __CPROVER_atomic_end();
 void __CPROVER_fence(const char *kind, ...);
 #if 0
+__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;
 __CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 unsigned long __CPROVER_next_thread_id=0;
 

src/ansi-c/library/pthread_lib.c

@@ -136,11 +136,20 @@ inline void pthread_exit(void *value_ptr)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#include <errno.h>
+#define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
 extern __CPROVER_bool __CPROVER_threads_exited[];
+extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
+extern unsigned long __CPROVER_next_thread_id;
 
 inline int pthread_join(pthread_t thread, void **value_ptr)
 {
   __CPROVER_HIDE:;
+  if((unsigned long)thread>__CPROVER_next_thread_id) return ESRCH;
+  if((unsigned long)thread==__CPROVER_thread_id) return EDEADLK;
   if(value_ptr!=0) (void)**(char**)value_ptr;
   __CPROVER_assume(__CPROVER_threads_exited[(unsigned long)thread]);
   return 0;