Add better documentation of pthread_cond_waits mutex usage

Author: thomasspriggs

regression/cbmc-sequentialization/pthread_cond/checked_signal.c

@@ -24,7 +24,9 @@ void initialise_condition(void)
 }
 
 // Wait for signal. Note that pthreads requires us to lock and unlock the mutex
-// around the call to `pthread_cond_wait`.
+// around the call to `pthread_cond_wait`. Note also that if called
+// pthread_cond_wait function waits then it will leave the mutex unlocked whilst
+// it is waiting.
 void wait(void)
 {
   const int lock_error = pthread_mutex_lock(&signal_mutex);

regression/cbmc-sequentialization/pthread_cond/spurious_wakeup.c

@@ -23,7 +23,9 @@ void initialise_condition(void)
 }
 
 // Wait for signal. Note that pthreads requires us to lock and unlock the mutex
-// around the call to `pthread_cond_wait`.
+// around the call to `pthread_cond_wait`. Note also that if called
+// pthread_cond_wait function waits then it will leave the mutex unlocked whilst
+// it is waiting.
 void wait(void)
 {
   const int lock_error = pthread_mutex_lock(&signal_mutex);