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