Peterson's Solution

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

// Shared variables
bool flag[2] = {false, false};
int turn;  // 0 or 1
 
// Process i (where i ∈ {0, 1})
void process(int i) {
    int j = 1 - i;  // The other process
    
    while (true) {
        // L0: Non-critical section
        
        // L1: flag[i] = true;          Entry section - step 1
        // L2: turn = j;                Entry section - step 2
        // L3: while (flag[j] && turn == j) { } // Entry section - step 3
        
        // L4: Critical Section
        
        // L5: flag[i] = false;         Exit section
    }
}
 
// Line labels for proof references:
// L0 = Non-critical section
// L1 = Set flag[i] = true
// L2 = Set turn = j
// L3 = While loop check
// L4 = Critical section
// L5 = Set flag[i] = false (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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

════════════════════════════════════════════════════════════════════════
THEOREM 1: MUTUAL EXCLUSION
════════════════════════════════════════════════════════════════════════
 
CLAIM: At most one process can be in the critical section at any time.
 
PROOF BY CONTRADICTION:
───────────────────────────────────────────────────────────────────────
 
Assume, for contradiction, that at some time T:
  - P0 is in the critical section (at L4), AND
  - P1 is in the critical section (at L4)
 
For P0 to be in CS:
  - P0 must have executed L1 (flag[0] = true)
  - P0 must have executed L2 (turn = 1)
  - P0 must have passed L3 (the while loop exited)
  
For the while loop to exit for P0:
  - The condition (flag[1] && turn == 1) was false
  - This means: flag[1] == false OR turn != 1 (i.e., turn == 0)
 
Similarly, for P1 to be in CS:
  - P1 must have executed L1 (flag[1] = true)
  - P1 must have executed L2 (turn = 0)
  - P1 must have passed L3 (the while loop exited)
  
For the while loop to exit for P1:
  - The condition (flag[0] && turn == 0) was false
  - This means: flag[0] == false OR turn != 0 (i.e., turn == 1)
 
───────────────────────────────────────────────────────────────────────
NOW, LET'S ANALYZE WHEN EACH PROCESS LAST SET 'turn':
───────────────────────────────────────────────────────────────────────
 
Let:
  - T0_turn = the time when P0 executed 'turn = 1' (L2)
  - T1_turn = the time when P1 executed 'turn = 0' (L2)
 
These are the last times each process set 'turn' before entering CS.
One of these must have happened LAST. Consider two cases:
 
CASE 1: P0 set turn last (T0_turn > T1_turn)
─────────────────────────────────────────────
- P0 executed 'turn = 1' AFTER P1 executed 'turn = 0'
- So the final value of turn is 1 (P0's write won)
- When P0 checked its while condition, turn == 1
- P0's condition: flag[1] && turn == 1 
- Since P1 already set flag[1] = true (before setting turn = 0, 
  which was before P0's turn = 1), we have flag[1] == true
- So P0's condition is: true && true = true
- P0 should be WAITING, not in CS! 
  
CONTRADICTION!
 
CASE 2: P1 set turn last (T1_turn > T0_turn)
─────────────────────────────────────────────
- P1 executed 'turn = 0' AFTER P0 executed 'turn = 1'
- So the final value of turn is 0 (P1's write won)
- When P1 checked its while condition, turn == 0
- P1's condition: flag[0] && turn == 0
- Since P0 already set flag[0] = true (before setting turn = 1,
  which was before P1's turn = 0), we have flag[0] == true
- So P1's condition is: true && true = true
- P1 should be WAITING, not in CS!
 
CONTRADICTION!
 
───────────────────────────────────────────────────────────────────────
CONCLUSION:
───────────────────────────────────────────────────────────────────────
Both cases lead to a contradiction. Therefore, our assumption that both
processes are in the critical section simultaneously must be false.
 
∴ At most one process can be in the critical section at any time. ∎

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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

════════════════════════════════════════════════════════════════════════
THEOREM 2: PROGRESS
════════════════════════════════════════════════════════════════════════
 
CLAIM: If the critical section is empty and one or more processes want
       to enter, some process will enter in finite time.
 
PROOF:
───────────────────────────────────────────────────────────────────────
 
Consider the case where no process is in CS and at least one process
(say P0) wants to enter (is in its entry section).
 
CASE 1: Only P0 wants to enter (P1 is at L0 with flag[1] = false)
─────────────────────────────────────────────────────────────────────
- P0 executes L1: flag[0] = true
- P0 executes L2: turn = 1
- P0 checks L3: while (flag[1] && turn == 1)
- Since P1 is at L0, flag[1] = false
- Condition: false && true = false
- P0 immediately exits the while loop
- P0 enters the critical section (L4)
 
PROGRESS ACHIEVED: P0 enters in finite time (three steps).
 
CASE 2: Only P1 wants to enter (P0 is at L0 with flag[0] = false)
─────────────────────────────────────────────────────────────────────
- By symmetric argument to Case 1, P1 enters in finite time.
 
PROGRESS ACHIEVED.
 
CASE 3: Both P0 and P1 want to enter (both in entry section)
─────────────────────────────────────────────────────────────────────
- Both processes will execute L1 and L2.
- After both have executed L2, turn has some value (0 or 1).
- Let's say turn = 0 (P1's write was last, or P1 was slower).
 
Sub-case 3a: turn = 0
- P0: checks (flag[1] && turn == 1) → (true && false) → false → ENTERS!
- P1: checks (flag[0] && turn == 0) → (true && true) → WAITS
 
P0 enters in finite time.
 
Sub-case 3b: turn = 1
- P0: checks (flag[1] && turn == 1) → (true && true) → WAITS
- P1: checks (flag[0] && turn == 0) → (true && false) → false → ENTERS!
 
P1 enters in finite time.
 
In either sub-case, exactly one process enters immediately.
 
PROGRESS ACHIEVED.
 
───────────────────────────────────────────────────────────────────────
IMPORTANT OBSERVATIONS:
───────────────────────────────────────────────────────────────────────
 
1. A process NOT in the entry section (at L0 with flag = false) cannot
   affect the decision. Only processes with flag = true participate.
 
2. The turn variable ensures that when both flags are true, exactly
   one process proceeds while the other waits.
 
3. No indefinite postponement is possible because:
   - If only one process wants entry, it enters immediately.
   - If both want entry, turn determines one enters immediately.
 
∴ Progress is guaranteed. ∎

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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

════════════════════════════════════════════════════════════════════════
THEOREM 3: BOUNDED WAITING (Bound = 1)
════════════════════════════════════════════════════════════════════════
 
CLAIM: Once Pi begins its entry section, Pj can enter the critical
       section at most once before Pi enters.
 
PROOF:
───────────────────────────────────────────────────────────────────────
 
Let Pi start its entry section at time T_start.
At T_start, Pi executes:
  L1: flag[i] = true
  L2: turn = j
  L3: while (flag[j] && turn == j) { /* wait */ }
 
We analyze what happens regarding Pj's potential entries.
 
SCENARIO 1: Pj is not interested (flag[j] = false)
─────────────────────────────────────────────────────────────────────
- Pi's while condition: false && (anything) = false
- Pi enters immediately without waiting.
- Bound satisfied: Pj entered 0 times (trivially ≤ 1).
 
SCENARIO 2: Pj is interested or in CS (flag[j] = true)
─────────────────────────────────────────────────────────────────────
- Pi must wait in the while loop until one of:
  a) flag[j] becomes false, OR
  b) turn becomes i (turn != j)
 
Let's trace Pj's possible actions:
 
Case 2a: Pj is currently in CS at time T_start
- Pj will eventually exit and execute L5: flag[j] = false
- When flag[j] becomes false, Pi's condition becomes false
- Pi enters immediately.
- Bound: Pj entered 1 time (the current execution). ✓
 
Case 2b: Pj is in its entry section at time T_start
- Pj will eventually pass L3 (the while loop)
- When Pj exits loop, Pj enters CS, then exits (flag[j] = false)
- Pi can then enter.
- Bound: Pj entered 1 time. ✓
 
BUT WAIT: What if Pj immediately tries to enter again?
─────────────────────────────────────────────────────────────────────
 
Suppose Pj exits CS (sets flag[j] = false) and IMMEDIATELY starts 
a new entry attempt:
 
1. Pj at L5: flag[j] = false     // Pi might exit its while loop here!
2. Pj at L1: flag[j] = true      // Pj's new attempt
3. Pj at L2: turn = i            // ← THIS IS KEY!
4. Pj at L3: while (flag[i] && turn == i)
 
Now analyze both processes' while conditions:
 
Pi's condition (entered before Pj's new attempt, still waiting):
  - flag[j] = true  (Pj just set it in step 2)
  - turn = i        (Pj just set it in step 3)
  - Condition: true && false = FALSE → Pi EXITS LOOP!
 
Pj's condition:
  - flag[i] = true  (Pi set it at T_start, still waiting)
  - turn = i        (Pj set it in step 3)
  - Condition: true && true = TRUE → Pj WAITS!
 
The key insight: When Pj re-enters, it sets turn = i.
This favors Pi over Pj, releasing Pi from its wait.
 
───────────────────────────────────────────────────────────────────────
FORMAL ARGUMENT:
───────────────────────────────────────────────────────────────────────
 
Suppose Pi is waiting (in while loop at L3).
For Pj to enter CS (again), Pj must:
  1. Execute L1: flag[j] = true
  2. Execute L2: turn = i    ← Sets turn to favor Pi!
  3. Pass L3: while (flag[i] && turn == i)
 
After step 2, turn = i.
 
Pi's while condition is: flag[j] && turn == j
  = true && (turn == j)
  = true && false  (because turn = i, which is not j)
  = false
 
So Pi's while loop terminates BEFORE Pj can even check its own 
while condition. Pi enters the critical section.
 
Pj, at step 3, checks: flag[i] && turn == i
  = true && true
  = true
 
Pj must wait.
 
───────────────────────────────────────────────────────────────────────
CONCLUSION:
───────────────────────────────────────────────────────────────────────
After Pi starts its entry section:
- If Pj is not interested → Pi enters immediately (0 CS by Pj)
- If Pj is in CS or entering → Pi enters after Pj's current CS (1 CS by Pj)
- If Pj tries to re-enter → Pj's turn = i releases Pi first
 
Therefore, Pj can execute its critical section AT MOST ONCE before
Pi enters.
 
∴ Bounded waiting is satisfied with bound = 1. ∎

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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

════════════════════════════════════════════════════════════════════════
INVARIANTS OF PETERSON'S SOLUTION
════════════════════════════════════════════════════════════════════════
 
INVARIANT I1: Flag Indicates Entry Section or CS
───────────────────────────────────────────────────────────────────────
  flag[i] = true  ⟹  Pi is at L1, L2, L3, or L4
  flag[i] = false ⟹  Pi is at L0 or L5 (not interested/just exited)
 
This invariant holds because:
  - flag[i] is set to true only at L1 (entry section)
  - flag[i] is set to false only at L5 (exit section)
  - After L5, process returns to L0
 
────────────────────────────────────────────────────────────────────────
INVARIANT I2: Turn Was Set By Someone
───────────────────────────────────────────────────────────────────────
  After initialization, turn ∈ {0, 1} always.
  At any time t > 0, turn was most recently set by either P0 or P1.
 
This is trivially true because:
  - turn is only written in L2 of each process
  - Each process sets turn to j (the other process)
  - So turn alternates between 0 and 1
 
────────────────────────────────────────────────────────────────────────
INVARIANT I3: Mutual Exclusion Invariant
───────────────────────────────────────────────────────────────────────
  ¬(P0 at L4 ∧ P1 at L4)
  
  "It is never the case that both processes are in the critical section."
 
This invariant is exactly what we proved in Theorem 1.
 
────────────────────────────────────────────────────────────────────────
INVARIANT I4: Waiting Implies Intent Is Known
───────────────────────────────────────────────────────────────────────
  If Pi is at L3 (spinning in while loop), then flag[i] = true.
 
This holds because:
  - L1 (flag[i] = true) is executed before L3
  - L5 (flag[i] = false) is executed after L4, which is after L3
 
────────────────────────────────────────────────────────────────────────
INVARIANT I5: CS Implies Flag Is True
───────────────────────────────────────────────────────────────────────
  If Pi is at L4 (in CS), then flag[i] = true.
 
This holds because:
  - Pi sets flag[i] = true at L1
  - Pi only clears flag[i] at L5, which is after L4
 
────────────────────────────────────────────────────────────────────────
DERIVED INVARIANT I6: One Waiter Rule
───────────────────────────────────────────────────────────────────────
  If flag[0] = flag[1] = true (both interested), then at most one 
  process is executing the while loop body (spinning) while the 
  other is either still before the while check or in CS.
 
This follows because:
  - If both flags are true, the turn variable distinguishes them
  - For one process, turn == j (other's id) → waits
  - For the other, turn != j → proceeds
  - They cannot both have turn == their_j (that would mean turn == 0 
    and turn == 1 simultaneously, impossible)

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

════════════════════════════════════════════════════════════════════════
THEOREM 4: DEADLOCK FREEDOM
════════════════════════════════════════════════════════════════════════
 
CLAIM: Peterson's Solution never experiences a deadlock where both
       processes wait forever in their while loops.
 
PROOF BY CONTRADICTION:
───────────────────────────────────────────────────────────────────────
 
Assume deadlock: both P0 and P1 are stuck at L3, spinning forever.
 
For P0 to be stuck at L3:
  - flag[1] = true AND turn = 1
 
For P1 to be stuck at L3:
  - flag[0] = true AND turn = 0
 
But this requires:
  - turn = 1 (for P0 to wait)
  - turn = 0 (for P1 to wait)
 
These cannot both be true simultaneously!
turn is a single integer; it has exactly one value at any time.
 
Therefore, at most one process can be stuck in its while loop.
The other process's condition must be false, so it can proceed.
 
∴ Deadlock is impossible. ∎

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
45

════════════════════════════════════════════════════════════════════════
THEOREM 5: LIVELOCK FREEDOM
════════════════════════════════════════════════════════════════════════
 
CLAIM: Peterson's Solution does not exhibit livelock behavior.
 
PROOF:
───────────────────────────────────────────────────────────────────────
 
A livelock would require processes to repeatedly change state without
entering the critical section.
 
In Peterson's Solution, consider a process Pi at L3 (while loop).
 
Pi can only exit the loop (make progress) when:
  - flag[j] becomes false, OR
  - turn becomes i (turn != j)
 
Once either condition becomes true, Pi immediately exits the loop
and enters CS. There is no mechanism for the condition to oscillate.
 
Specifically:
  - flag[j] changes only when Pj modifies it at L1 or L5
  - turn changes only when a process executes L2
 
If Pj is also at L3 (spinning):
  - Pj cannot execute L2 (already past L2)
  - Pj cannot execute L1 or L5 (stuck in L3)
  - So flag and turn are STABLE while both are at L3
 
With stable flag and turn, one process's condition is false (by 
the deadlock freedom proof), so that process enters CS.
 
If Pj is not at L3:
  - Pj is at L0, L1, L2, L4, or L5
  - If at L0: flag[j] = false, Pi enters
  - If at L1, L2: flag[j] may become true, but Pj will set turn = i,
    releasing Pi
  - If at L4: Pj will eventually exit, setting flag[j] = false, 
    releasing Pi
  - If at L5: flag[j] = false, Pi enters
 
In all cases, the waiting process makes progress in finite time.
 
∴ Livelock is impossible. ∎

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

// PROMELA model for Peterson's Solution (SPIN model checker)
// This model can be automatically verified for correctness
 
bool flag[2];
byte turn;
byte critical = 0;  // Counter for processes in CS (should never exceed 1)
 
active [2] proctype process() {
    byte i = _pid;       // Process ID (0 or 1)
    byte j = 1 - i;      // Other process
    
    do
    :: // Main loop - repeat forever
        // Non-critical section
        skip;
        
        // Entry section
        flag[i] = true;
        turn = j;
        
        // Busy wait
        (flag[j] == false || turn != j);
        
        // Critical section
        critical++;
        assert(critical == 1);  // Mutual exclusion property
        critical--;
        
        // Exit section
        flag[i] = false;
    od
}
 
// To verify: spin -a peterson.pml && gcc -o pan pan.c && ./pan
// SPIN will explore all interleavings and check the assertion

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
45
46

----------------------------- MODULE Peterson -----------------------------
EXTENDS Integers
 
VARIABLES flag, turn, pc
 
Procs == {0, 1}
vars == <<flag, turn, pc>>
 
Init == /\ flag = [i \in Procs |-> FALSE]
        /\ turn \in Procs  \* Initial value doesn't matter
        /\ pc = [i \in Procs |-> "non-critical"]
 
\* Process i wants to enter critical section        
WantEnter(i) == /\ pc[i] = "non-critical"
                /\ flag' = [flag EXCEPT ![i] = TRUE]
                /\ pc' = [pc EXCEPT ![i] = "set_turn"]
                /\ turn' = turn
 
SetTurn(i) == /\ pc[i] = "set_turn"
              /\ turn' = 1 - i  \* Set turn to other process
              /\ pc' = [pc EXCEPT ![i] = "wait"]
              /\ flag' = flag
 
Wait(i) == /\ pc[i] = "wait"
           /\ (flag[1-i] = FALSE \/ turn = i)
           /\ pc' = [pc EXCEPT ![i] = "critical"]
           /\ UNCHANGED <<flag, turn>>
 
Critical(i) == /\ pc[i] = "critical"
               /\ pc' = [pc EXCEPT ![i] = "exit"]
               /\ UNCHANGED <<flag, turn>>
 
Exit(i) == /\ pc[i] = "exit"
           /\ flag' = [flag EXCEPT ![i] = FALSE]
           /\ pc' = [pc EXCEPT ![i] = "non-critical"]
           /\ turn' = turn
 
\* Mutual exclusion property
MutualExclusion == ~(pc[0] = "critical" /\ pc[1] = "critical")
 
\* The specification
Next == \E i \in Procs: WantEnter(i) \/ SetTurn(i) \/ Wait(i) 
                          \/ Critical(i) \/ Exit(i)
                          
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
=============================================================================