Another Example A benign race: k=-1; (newvar i:=0 in while is nAk =-1 do if f(i)>0 then k :=ielse i:=i+2 ll newvar i:=1 in while is nAk=-1 do if f(i)>0 then k :=ielse i:=i+2) A problematic version: k=-1; (newvar i:=0 in while is nAk=-1 do if f(i)>0 then print(i);print(f(i))else i :=i+2 ll newvar i:=1 in while is nAk=-1 do if f(i)>0 then print(i);print(f(i)else i:=i+2) Xinyu Feng Shared-Variable ConcumrencyAnother Example A benign race: k := −1; (newvar i := 0 in while i ≤ n ∧ k = −1 do if f(i) ≥ 0 then k := i else i := i + 2 k newvar i := 1 in while i ≤ n ∧ k = −1 do if f(i) ≥ 0 then k := i else i := i + 2) A problematic version: k := −1; (newvar i := 0 in while i ≤ n ∧ k = −1 do if f(i) ≥ 0 then print(i); print(f(i)) else i := i + 2 k newvar i := 1 in while i ≤ n ∧ k = −1 do if f(i) ≥ 0 then print(i); print(f(i)) else i := i + 2) Xinyu Feng Shared-Variable Concurrency