For process [A|B]:

1   Set Flag-[A|B]
2   Turn Coin to Face-[B|A]
3   Loop until Break:
4       if Flag-[B|A] is Clear, then Break
5       if Coin shows Face-[A|B], then Break
    ** ENTER CRITICAL SECTION **
X   ...
    ** LEAVE CRITICAL SECTION **
6   Clear Flag-[A|B]

Version without Coin: Safe but not Live. 

For process [A|B]:

1   Set Flag-[A|B]
3   Loop until Break:
4       if Flag-[B|A] is Clear, then Break
    ** ENTER CRITICAL SECTION **
X    ...
    ** LEAVE CRITICAL SECTION **
6   Clear Flag-[A|B]

Not live:
    If both A and B set their flags before either of A or B
    query the flags, neither can enter and neither can subsequently
    leave, to clear the flags.
    
    ( A1 ∣∣ B1 ) < ( A4 ∣∣ B4 ) means never AX and never BX.

    Note: an example of non-liveness is a proof of non-liveness

Safe:
    For AX, A4 must break, so B1 is after A4. Then B4 is after A1 and until A6
    B cannot enter.

    Once A6, and until B6, B's flag is set, and AX cannot be again.

    A4 < B1 < B4 < A6. So it is not possible that BX is such that,
    A4 < B4 < BX < A6. Since A4 < AX < A6, AX and BX do not occur
    together.

Version without Flags: Safe but not Live.

For process [A|B]:

2   Turn Coin to Face-[B|A]
3   Loop until Break:
5       if Coin shows Face-[A|B], then Break
    ** ENTER CRITICAL SECTION **
X    ...
    ** LEAVE CRITICAL SECTION **
    

Not live:
    If A2 but never B2, then never A5 so forever A3 and BX (because never B2)

    never B2 means never A2 < B2 < A5 means never AX and never BX
    
    Note: an example of non-liveness is a proof of non-liveness

Safe:
    Throughout the critical section (that is, any time X), the coin shows
    the process that has the critical section, and this does not change while
    a process is in the critical section (as the other process as begun to 
    loop after turning the coin).

Safety of Petersons

    A modified versin with the coin set first is not safe. Here is an unsafe sequence
    for this modified version. (To show that the algorithm is not the trivial composition
    of two algorithms. They must be composed in the correct order to main safety while
    adding liveness.)

    From time 0 time X: If A sets the coin and then B sets the coin, and we 
    now arrive at time X.
    
    From time X to time Y_B: B sets its flag first and checks; B sees A has not 
    set its flag, and enters at time Y_B based on the flag portion of the protocol.
    
    From time Y_B to time Y_A: A sets its flag and and checks; A sees B has set 
    its flag and the coin is towards A, and enters at time Y_A based on the 
    coin portion of the protocol.
    
    Hence at time Y_A safety is contradicted.
    
    
Arguing liveness in Petersons.

    If there is a deadlock, then both are looping at statement 3. The coin shows
    one face or the other, and the process whose face is shown proceeds. Contradicting
    that there is deadlock.
    

This work is licensed under a Creative Commons Attribution-ShareAlike 3.0 Unported License.

author: burton rosenberg
created: 23 oct 2019
update: 25 oct 2019