# # Dekker's mutex algorithm (fully fenced): # http://en.wikipedia.org/wiki/Dekker's_algorithm # # IS robust. # # q0: flag[0] = true; # q1: while (flag[1] == true) { # q2: if (turn ≠ 0) { # q3: flag[0] = false; # q4: while (turn ≠ 0) { # q5: } # q6: flag[0] = true; # q7: } # q8: } # # // critical section # ... # q9: turn = 1; # q10: flag[0] = false; # // remainder section # # Memory layout: # 0 — flag[0] # 1 — flag[1] # 2 — turn thread t0 initial q0 transition q0 q1_a write 1 0 transition q1_a q1 mfence transition q1 q1_1 read flag 1 transition q1_1 q2 check == flag 1 transition q1_1 q9 check == flag 0 transition q2 q2_1 read turn 2 transition q2_1 q3 check != turn 0 transition q2_1 q1 check == turn 0 transition q3 q4_a write 0 0 transition q4_a q4 mfence transition q4 q4_1 read turn 2 transition q4_1 q4 check != turn 0 transition q4_1 q6 check == turn 0 transition q6 q1_a write 1 0 transition q9 q10 write 1 2 transition q10 q11 write 0 0 transition q11 q0 noop end # Thread t1 is symmetric. thread t1 initial q0 transition q0 q1_a write 1 1 transition q1_a q1 mfence transition q1 q1_1 read flag 0 transition q1_1 q2 check == flag 1 transition q1_1 q9 check == flag 0 transition q2 q2_1 read turn 2 transition q2_1 q3 check != turn 1 transition q2_1 q1 check == turn 1 transition q3 q4_a write 0 1 transition q4_a q4 mfence transition q4 q4_1 read turn 2 transition q4_1 q4 check != turn 1 transition q4_1 q6 check == turn 1 transition q6 q1_a write 1 1 transition q9 q10 write 0 2 transition q10 q11 write 0 1 transition q11 q0 noop end