Add comment why MutexUnlock makes unrealistically strong assumptions.

goblint · Aug 4, 2022 · 11891d4 · 11891d4
1 parent d75d664
commit 11891d4
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/spin/pthread.base.pml b/spin/pthread.base.pml
@@ -196,6 +196,9 @@ inline __MutexLock(thread_id, x) {
   }
 }
 
+// This makes a strong assumption! If other threads are waiting for the mutex, they get it before we can attempt to
+// relock the mutex.
+// This is not really what happens for pthreads!
 inline MutexUnlock(x) {
   atomic {
     if