threadingSystemBusy = false; // Must be an atomic assignment. systemCall_enableInterrupts(); // Turn pre-emptive switching back on on this core. // Mesa style: // The woken threads are not given any priority. } class Mutex { protected volatile bool held = false; private volatile ThreadQueue blockingThreads; // Thread-unsafe queue of blocked threads. Elements are (Thread*). public method acquire() { // Internal spin-lock while other threads on any core are accessing this object's // "held" and "threadQueue", or "readyQueue". while (testAndSet(threadingSystemBusy)) {} // N.B.: "threadingSystemBusy" is now true. // System call to disable interrupts on this core so that threadSleep() doesn't get interrupted by // the thread-switching timer on this core which would call contextSwitchISR(). // Done outside threadSleep() for more efficiency so that this thread will be sleeped // right after going on the lock queue. systemCall_disableInterrupts(); assert !blockingThreads.contains(currentThread); if (held) { // Put "currentThread" on this lock's queue so that it will be // considered "sleeping" on this lock. // Note that "currentThread" still needs to be handled by threadSleep(). readyQueue.remove(currentThread); blockingThreads.enqueue(currentThread); threadSleep(); // Now we are woken up, which must be because "held" became false. assert !held; assert !blockingThreads.contains(currentThread); } held = true; threadingSystemBusy = false; // Must be an atomic assignment. systemCall_enableInterrupts(); // Turn pre-emptive switching back on on this core. } public method release() { // Internal spin-lock while other threads on any core are accessing this object's // "held" and "threadQueue", or "readyQueue". while (testAndSet(threadingSystemBusy)) {} // N.B.: "threadingSystemBusy" is now true. // System call to disable interrupts on this core for efficiency. systemCall_disableInterrupts(); assert held; // (Release should only be performed while the lock is held.) held = false; if (!blockingThreads.isEmpty()) { Thread* unblockedThread = blockingThreads.dequeue(); readyQueue.enqueue(unblockedThread); } threadingSystemBusy = false; // Must be an atomic assignment. systemCall_enableInterrupts(); // Turn pre-emptive switching back on on this core. } } struct ConditionVariable { volatile ThreadQueue waitingThreads; } Semaphore As an example, consider a thread-safe class that implements a semaphore. There are methods to increment (V) and to decrement (P) a private integer s. However, the integer must never be decremented below 0; thus a thread that tries to decrement must wait until the integer is positive. We use a condition variable sIsPositive with an associated assertion of . monitor class Semaphore { private int s := 0 invariant s >= 0 private Condition sIsPositive /* associated with s > 0 */ public method P() { while