Shared-Variable Concurrency Xinyu Feng Nanjing University 12/14/2018 Xinyu Feng Shared-Variable Concurrency
Shared-Variable Concurrency Xinyu Feng Nanjing University 12/14/2018 Xinyu Feng Shared-Variable Concurrency
Parallel Composition(or Concurrency Composition) Syntax: (comm)c::=...I co ll c I... Note we allow nested parallel composition,e.g., (co;(cl‖c2)lc Operational Semantics: (co,)→(c6o) (c,）→(c1,) (colc1,g)→(c%lc,σ) (co‖c1,o)→(colc,o) (c,o）→(abort,o'),i∈{0,1} (Skip Il Skip,o）→(skip,o） (co‖c,o）→(abort,c) We have to use small-step semantics(instead of big-step semantics)to model concurrency. Xinyu Feng Shared-Variable Concurrency
Parallel Composition (or Concurrency Composition) Syntax: (comm) c ::= . . . | c0 k c1 | . . . Note we allow nested parallel composition, e.g., (c0 ;(c1 k c2)) k c3. Operational Semantics: (c0, σ) −→ (c 0 0 , σ0 ) (c0 k c1, σ) −→ (c 0 0 k c1, σ0 ) (c1, σ) −→ (c 0 1 , σ0 ) (c0 k c1, σ) −→ (c0 k c 0 1 , σ0 ) (Skip k Skip, σ) −→ (Skip, σ) (ci , σ) −→ (abort, σ0 ), i ∈ {0, 1} (c0 k c1, σ) −→ (abort, σ0 ) We have to use small-step semantics (instead of big-step semantics) to model concurrency. Xinyu Feng Shared-Variable Concurrency
Interference Example: y=x+1; y=x+1; X=y+1 X:=X+1 Suppose initially x=ay =0.What are the possible results? (1)y=1,×=2:(2)y=1,x=3;(3)y=3,×=3;(4)y=2,×=3 Two commands co and c are said to interfere if: (fv(co)n fa(c))U (fv(c1)n fa(co)) If co and c interfere,we say there are race conditions(or races)in Co ll C1. When co and ci do not interfere,nor terminate by failure,the concurrent composition co ll c1 is determinate. Xinyu Feng Shared-Variable Concurrency
Interference Example: y := x + 1 ; x := y + 1 k y := x + 1 ; x := x + 1 Suppose initially σx = σy = 0. What are the possible results? (1)y = 1, x = 2; (2)y = 1, x = 3; (3)y = 3, x = 3; (4)y = 2, x = 3 Two commands c0 and c1 are said to interfere if: (fv(c0) ∩ fa(c1)) ∪ (fv(c1) ∩ fa(c0)) , ∅ If c0 and c1 interfere, we say there are race conditions (or races) in c0 k c1. When c0 and c1 do not interfere, nor terminate by failure, the concurrent composition c0 k c1 is determinate. Xinyu Feng Shared-Variable Concurrency
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 Concumrency
Another 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
Conditional Critical Regions We could use a critical region to achieve mutual exclusive access of shared variables. Syntax: (comm)c ::await b then where c is a sequential command(a command with no await and parallel composition). Semantics: Iblboolexp=true(c,o）→*(Skip,r） (await b then c,o）→(skip,o) [Iblboolexp =false (await b then d,o）→(skip;await b then c,) The second rule gives us a"busy-waiting"semantics.If we eliminate that rule,the thread will be blocked when the condition does not hold. Xinyu Feng Shared-Variable Concurrency
Conditional Critical Regions We could use a critical region to achieve mutual exclusive access of shared variables. Syntax: (comm) c ::= await b then cˆ where cˆ is a sequential command (a command with no await and parallel composition). Semantics: ~bboolexp σ = true (cˆ, σ) −→∗ (Skip, σ0 ) (await b then cˆ, σ) −→ (Skip, σ0 ) ~bboolexp σ = false (await b then cˆ, σ) −→ (Skip ; await b then cˆ, σ) The second rule gives us a “busy-waiting” semantics. If we eliminate that rule, the thread will be blocked when the condition does not hold. Xinyu Feng Shared-Variable Concurrency
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
Fairness k=-1; (newvar i:=0 in while k =-1 do if f(i)>0 then k :=ielsei:=i+2 ll newvar i:=1 in while k=-1 do if f(i)0 then k:=ielse i:=i+2) Suppose f(i)<0 for all even number i.Then there's an infinite execution in the form of: ..→(clc',1)→(c2lc,o2)→..→(cnlc,on)→. An execution of concurrent processes is unfair if it does not terminate but,after some finite number of steps,there is an unterminated process that never makes a transition. Xinyu Feng Shared-Variable Concurrency
Fairness k := −1; (newvar i := 0 in while k = −1 do if f(i) ≥ 0 then k := i else i := i + 2 k newvar i := 1 in while k = −1 do if f(i) ≥ 0 then k := i else i := i + 2) Suppose f(i) < 0 for all even number i. Then there’s an infinite execution in the form of: . . . −→ (c1 k c 0 , σ1) −→ (c2 k c 0 , σ2) −→ . . . −→ (cn k c 0 , σn) −→ . . . An execution of concurrent processes is unfair if it does not terminate but, after some finite number of steps, there is an unterminated process that never makes a transition. Xinyu Feng Shared-Variable Concurrency
Fairness-More Examples A fair execution of the following program would always terminate: newvar y:=0 in (x :=0;((while y=0 do x:=x+1)lly:=1)) Stronger fairness is needed to rule out infinite execution of the following program: newvar y:=0 in (X=0; ((while y=0 do x:=1-x)ll (await x =1 then y =1)) Xinyu Feng Shared-Variable Concurrency
Fairness — More Examples A fair execution of the following program would always terminate: newvar y := 0 in (x := 0;((while y = 0 do x := x + 1) k y := 1)) Stronger fairness is needed to rule out infinite execution of the following program: newvar y := 0 in (x := 0; ((while y = 0 do x := 1 − x) k (await x = 1 then y := 1)) ) Xinyu Feng Shared-Variable Concurrency
