Mesa vs Hoare Semantics: The Two Paradigms

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

HOARE SEMANTICS: signal(cv)
 
Precondition: S holds the monitor lock
              W is in cv.waitQueue
 
1. W is removed from cv.waitQueue
2. ATOMIC: Monitor lock transfers from S to W
   (No gap where lock is free)
3. S enters urgentQueue (special priority queue)
4. W resumes from wait(), holding the lock
5. (Later) When W exits monitor or waits:
   - If urgentQueue not empty: S resumes from signal()
   - Else: Next entry queue thread gets lock
 
Key Invariant:
  If predicate P is true when signal(cv) executes,
  then P is true when W resumes from wait(cv).
 
Required structures:
  - waitQueue per condition variable
  - urgentQueue per monitor
  - Priority: urgentQueue > entryQueue

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

MESA SEMANTICS: signal(cv)
 
Precondition: S holds the monitor lock
              W is in cv.waitQueue
 
1. W is removed from cv.waitQueue
2. W is moved to entryQueue (or general ready queue)
3. S continues executing, still holding the lock
4. (Later) S exits monitor normally, releasing lock
5. (Eventually) W acquires lock and resumes from wait()
   - But other threads may acquire lock before W does
 
Key Invariant:
  NONE regarding predicate preservation!
  The predicate that was true at signal time
  may be false when W resumes.
 
Required structures:
  - waitQueue per condition variable
  - entryQueue per monitor (same as always)
  - No urgentQueue needed

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

HOARE SEMANTICS TIMELINE
========================
 
Time →
                                              
Thread P (Producer):    [────────── executing in monitor ──────────]
                        │                                          │
                        ▼ signal(hasData)                          │
                        [YIELD TO C1]────────────────────┐         │
                        [urgent queue: waiting...]       ▼         │
                                                   [resume]────────┘
                                                   [finish & exit]
                                              
Thread C1 (Consumer):   [waiting on hasData]
                                    │
                                    ▼ signaled
                        [──── executing in monitor ────]
                        │                              │
                        ▼ finish procedure             │
                        [release → P resumes]──────────┘
                                              
Thread C2 (ready):      [entry queue: waiting...]
                                              [eventually gets turn]
 
Key observations:
- When P signals, control IMMEDIATELY transfers to C1
- P waits in urgent queue while C1 runs
- C2 cannot intervene between P's signal and C1's execution
- Data condition guaranteed valid for C1

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

MESA SEMANTICS TIMELINE
=======================
 
Time →
                                              
Thread P (Producer):    [──────────── executing in monitor ────────────]
                        │                                              │
                        ▼ signal(hasData)                              │
                        [continue executing...                         │
                         more code...                                  │
                         maybe do something else...         exit]──────┘
                        │
                        └── C1 moved to entry queue (just scheduled, not running)
                                              
Thread C1 (Consumer):   [waiting on hasData]
                                    │
                                    ▼ moved to entry queue
                        [entry queue: waiting...]
 
                                                               [acquires lock]
                                              ┌─────────────────────────┘
                                              ▼
                        [── executing in monitor ──]
                        Must recheck condition!
                        (C2 might have taken data)
                                              
Thread C2 (ready):      [entry queue: waiting...]
                        │
                        │   C2 might acquire lock before C1!
                        ▼
                        [── maybe executes first ──]
                        Takes data, exits
                        │
                        C1 finally runs:
                        └── finds no data, waits again!
 
Key observations:
- When P signals, P CONTINUES executing
- C1 competes with C2 for the lock
- C2 might consume data before C1 runs
- C1 must recheck condition (while loop)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

// HOARE: Signal at the "right" moment
procedure hoareProduce(item: T) {
    buffer.add(item);
    
    // Signal immediately - we'll be suspended
    // Any post-signal cleanup happens when we resume
    signal(hasData);
    
    // This code runs AFTER consumer finishes
    // (we resumed from urgent queue)
    cleanup();
}
 
// MESA: Signal whenever convenient
procedure mesaProduce(item: T) {
    buffer.add(item);
    
    // Can do more work after signaling
    signal(hasData);
    
    // This code runs immediately
    // Consumer won't execute until we release lock
    updateStatistics();
    logProduction();
    
    // Consumer runs after we exit
}

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

// ORIGINAL (Hoare semantics - from textbook)
monitor HoareBuffer {
    private slots: T[N];
    private count = 0;
    condition notFull, notEmpty;
    
    procedure put(x: T) {
        if (count == N) wait(notFull);  // Hoare: if is OK
        slots[count++] = x;
        signal(notEmpty);
    }
    
    procedure get(): T {
        if (count == 0) wait(notEmpty);  // Hoare: if is OK
        T x = slots[--count];
        signal(notFull);
        return x;
    }
}
 
// CONVERTED (Mesa semantics - for pthreads, Java, etc.)
monitor MesaBuffer {
    private slots: T[N];
    private count = 0;
    condition notFull, notEmpty;
    
    procedure put(x: T) {
        while (count == N) wait(notFull);  // Mesa: MUST use while
        slots[count++] = x;
        signal(notEmpty);
    }
    
    procedure get(): T {
        while (count == 0) wait(notEmpty);  // Mesa: MUST use while
        T x = slots[--count];
        signal(notFull);
        return x;
    }
}
 
// The conversion is mechanical: if → while
// The logic remains identical

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

// ORIGINAL (Mesa semantics - production code)
class ThreadSafeQueue<T> {
    synchronized void put(T item) {
        while (queue.size() >= maxSize) {
            wait();
        }
        queue.add(item);
        notify();
    }
    
    synchronized T take() {
        while (queue.isEmpty()) {
            wait();
        }
        T item = queue.remove(0);
        notify();
        return item;
    }
}
 
// CONVERTED (Hoare semantics - for verification)
monitor VerifiableQueue<T> {
    condition notFull, notEmpty;
    
    procedure put(item: T) {
        // Hoare allows if since condition is preserved
        if (queue.size() >= maxSize) {
            wait(notFull);
            // ASSERTION: queue.size() < maxSize
        }
        queue.add(item);
        signal(notEmpty);  // Asserts: !queue.isEmpty()
    }
    
    procedure take(): T {
        if (queue.isEmpty()) {
            wait(notEmpty);
            // ASSERTION: !queue.isEmpty()
        }
        T item = queue.remove(0);
        signal(notFull);  // Asserts: queue.size() < maxSize
        return item;
    }
}

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

// Brinch Hansen's Signal-and-Exit semantics
// (Used in Concurrent Pascal and some educational systems)
 
monitor BrinchHansenStyle {
    condition cv;
    
    procedure producer() {
        prepareData();
        signal(cv);  // This MUST be the last statement
        // Signaler exits monitor immediately
        // Cannot do more work after signal
    }
    
    // This is ILLEGAL in signal-and-exit:
    procedure illegalProducer() {
        prepareData();
        signal(cv);
        cleanup();  // COMPILE ERROR: code after signal
    }
    
    // Advantage: No urgent queue needed
    // Disadvantage: Less flexible procedure structure
}

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

// Java notifyAll = Mesa broadcast
 
public class MultiConditionMonitor {
    private boolean conditionA = false;
    private boolean conditionB = false;
    
    public synchronized void waitForA() throws InterruptedException {
        while (!conditionA) {
            wait();  // Waits on implicit condition queue
        }
        // conditionA was true when we rechecked
    }
    
    public synchronized void waitForB() throws InterruptedException {
        while (!conditionB) {
            wait();  // Same implicit queue as waitForA
        }
    }
    
    public synchronized void setA() {
        conditionA = true;
        notifyAll();  // Wake everyone
        // Those waiting for A: recheck, find true, proceed
        // Those waiting for B: recheck, find false, wait again
    }
}