#
# Lamport's fast mutex algorithm 1 (properly fenced), as presented in
#
# L. Lamport. A fast mutual exclusion algorithm. ACM Trans. Comput.
# Syst., 5(1), 1987.
#
# IS robust.
#
# Memory layout:
# 0 — x
# 1 — y

thread t0
initial start
transition	start	q0	local	i	0
transition	q0	q0_1	write	i	0
transition	q0_1	q1	mfence
transition	q1	q2	read	y	1
transition	q2	q0	check	!= y 0
transition	q2	q3	check	== y 0
transition	q3	q3_1	write	i	1
transition	q3_1	q4	mfence
transition	q4	q5	read	x	0
transition	q5	q6	check	!= x i
transition	q6	q7	read	y	1
transition	q7	q0	check	!= y i
transition	q5	enter	check	== x i

transition	enter	q9	write	0	1
end

thread t1
initial start
transition	start	q0	local	i	1
transition	q0	q0_1	write	i	0
transition	q0_1	q1	mfence
transition	q1	q2	read	y	1
transition	q2	q0	check	!= y 0
transition	q2	q3	check	== y 0
transition	q3	q3_1	write	i	1
transition	q3_1	q4	mfence
transition	q4	q5	read	x	0
transition	q5	q6	check	!= x i
transition	q6	q7	read	y	1
transition	q7	q0	check	!= y i
transition	q5	enter	check	== x i

transition	enter	q9	write	0	1
end

thread t2
initial start
transition	start	q0	local	i	2
transition	q0	q0_1	write	i	0
transition	q0_1	q1	mfence
transition	q1	q2	read	y	1
transition	q2	q0	check	!= y 0
transition	q2	q3	check	== y 0
transition	q3	q3_1	write	i	1
transition	q3_1	q4	mfence
transition	q4	q5	read	x	0
transition	q5	q6	check	!= x i
transition	q6	q7	read	y	1
transition	q7	q0	check	!= y i
transition	q5	enter	check	== x i

transition	enter	q9	write	0	1
end