Improve explanation for the usage of sched_yield

Because calling `sched_yield` does not guarantee that a different thread
will be switched to.

Author: thomasspriggs

regression/cbmc-sequentialization/pthread_mutex/no_mutex.c

@@ -12,8 +12,8 @@ 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.
+    // The following call to yield is here in order to increase the chance of
+    // thread swaps during concrete execution in order to show unsoundness.
     sched_yield();
     ++shared_count_copy;
     shared_count = shared_count_copy;

regression/cbmc-sequentialization/pthread_mutex/with_mutex.c

@@ -15,8 +15,8 @@ void *worker(void *arguments)
     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.
+    // The following call to yield is here in order to increase the chance of
+    // thread swaps during concrete execution in order to show unsoundness.
     sched_yield();
     ++shared_count_copy;
     shared_count = shared_count_copy;

regression/cbmc-sequentialization/rw_lock/with_lock.c

@@ -19,8 +19,8 @@ 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.
+  // The following call to yield is here in order to increase the chance of
+  // thread swaps during concrete execution in order to show unsoundness.
   sched_yield();
   shared->c = 3;
 }
@@ -29,8 +29,8 @@ 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.
+  // The following call to yield is here in order to increase the chance of
+  // thread swaps during concrete execution in order to show unsoundness.
   sched_yield();
   shared->c = 6;
 }
@@ -81,8 +81,8 @@ void *checker(void *arguments)
     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.
+    // The following call to yield is here in order to increase the chance of
+    // thread swaps during concrete execution in order to show unsoundness.
     sched_yield();
     const bool is_state2 = shared->a == 4 && shared->b == 5 && shared->c == 6;
     assert(is_state1 != is_state2);