Achieving Mutual Exclusion k:=-1; (newvar i:=0 in while is nAk =-1 do (if f(i)>0 then (await busy =0 then busy =1); print(i);print(f(i));busy:=0 else i:=i+2) ll newvar i:=1 in while isnk =-1 do (if f(i)>0 then(await busy =0 then busy:=1); print(i);print(f(i));busy :=0 else i:=i+2)) Xinyu Feng Shared-Variable Concurrency
Achieving Mutual Exclusion k := −1; (newvar i := 0 in while i ≤ n ∧ k = −1 do (if f(i) ≥ 0 then (await busy = 0 then busy := 1); print(i); print(f(i)); busy := 0 else i := i + 2) k newvar i := 1 in while i ≤ n ∧ k = −1 do (if f(i) ≥ 0 then (await busy = 0 then busy := 1); print(i); print(f(i)); busy := 0 else i := i + 2)) Xinyu Feng Shared-Variable Concurrency
Atomic Blocks A syntactic sugar: atomicic)de await true then c We may also use the short-hand notation(c). Semantics: (c,σ）→*(Skip,o) (atomic{ch,σ）→(skip,r) It gives the programmer control over the size of atomic actions. Reynolds uses crit c instead of atomic(c). Xinyu Feng Shared-Variable Concurrency
Atomic Blocks A syntactic sugar: atomic{c} def = await true then c We may also use the short-hand notation hci. Semantics: (c, σ) −→∗ (Skip, σ0 ) (atomic{c}, σ) −→ (Skip, σ0 ) It gives the programmer control over the size of atomic actions. Reynolds uses crit c instead of atomic{c}. Xinyu Feng Shared-Variable Concurrency
Deadlock await busy0=0 await busy1 =0 then busy0:=1; then busy1:=1; await busy1 =0 await busy0=0 then busy1 :=1; then busy0:=1; busy0:=0; busy0:=0; busy1:=0; busy1:=0; Xinyu Feng Shared-Variable Concurrency
Deadlock await busy0 = 0 then busy0 := 1; await busy1 = 0 then busy1 := 1; . . . busy0 := 0; busy1 := 0; k await busy1 = 0 then busy1 := 1; await busy0 = 0 then busy0 := 1; . . . busy0 := 0; busy1 := 0; Xinyu Feng Shared-Variable Concurrency