s = 0: wait sIsPositive assert s > 0 s := s - 1 } public method V() { s := s + 1 assert s > 0 signal sIsPositive } } Implemented showing all synchronization (removing the assumption of a thread-safe class and showing the mutex): class Semaphore { private volatile int s := 0 invariant s >= 0 private ConditionVariable sIsPositive /* associated with s > 0 */ private Mutex myLock /* Lock on "s" */ public method P() { myLock.acquire() while s = 0: wait(myLock, sIsPositive) assert s > 0 s := s - 1 myLock.release() } public method V() { myLock.acquire() s := s + 1 assert s > 0 signal sIsPositive myLock.release() } } Monitor implemented using semaphores Conversely, locks and condition variables can also be derived from semaphores, thus making monitors and semaphores reducible to one another: The implementation given here is incorrect. If a thread calls wait() after broadcast() has been called, an originally thread may be stuck indefinitely, since broadcast() increments the semaphore only enough times for threads already waiting. public method wait(Mutex m, ConditionVariable c) { assert m.held; c.internalMutex.acquire(); c.numWaiters++; m.release(); // Can go before/after the neighboring lines. c.internalMutex.release(); // Another thread could signal here, but that's OK because of how // semaphores count. If c.sem's number becomes 1, we'll have no // waiting time. c.sem.acquire(); // Block on the CV. // Woken m.acquire(); // Re-acquire the mutex. } public method signal(ConditionVariable c) { c.internalMutex.acquire(); if (c.numWaiters > 0) { c.numWaiters--; c.sem.release(); // (Doesn't need to be protected by c.internalMutex.) } c.internalMutex.release(); } public method broadcast(ConditionVariable c) { c.internalMutex.acquire(); while (c.numWaiters > 0) { c.numWaiters--; c.sem.release(); // (Doesn't need to be protected by c.internalMutex.) } c.internalMutex.release(); } class Mutex { protected boolean held = false; // For assertions only, to make sure sem's number never goes > 1. protected Semaphore sem = Semaphore(1); // The number shall always be at most 1. // Not held <--> 1; held <--> 0. public method acquire() { sem.acquire(); assert !held; held = true; } public method release() { assert held; // Make sure we never acquire sem above 1. That would be bad. held = false; sem.release(); } } class ConditionVariable { protected int numWaiters = 0; // Roughly tracks the number of waiters blocked in sem. // (The semaphore's internal state is necessarily private.) protected Semaphore sem = Semaphore(0); // Provides the wait