Independent Composition Dependent Composition P.Q (sequential execution)
P and Q must have exactly the same state variables
Independent Composition P||Q (parallel execution)
P and Q must have completely different state variables
and the state variables of the composition are those of both P and Q
Ignoring time and space variables P||Q = P∧Q
1/19
Independent Composition example in integer variables x , y , and z
x:= x+1 || y:= y+2
= xʹ=x+1 || yʹ=y+2 ∧ zʹ=z
= xʹ=x+1 ∧ yʹ=y+2 ∧ zʹ=z
reasonable partition rule
If either xʹ or x:= appears in a process specification, then x belongs to that process (then neither xʹ nor x:= can appear in the other process specification).
If neither xʹ nor x:= appears at all, then x can be placed on either side of the partition.
partition the variables: put x in left part, put y and z in right part
2/19
Independent Composition example in variables x , y , and z
x:= y || y:= x partition: put x in left, y in right, z in either = xʹ=y ∧ yʹ=x ∧ zʹ=z
implementation of a process makes a private copy of the initial value of a variable belonging to the other process if the other process contains an assignment to that variable
3/19
Independent Composition example in binary variable b and integer variable x
b:= x=x || x:= x+1 = b:=⊤ || x:=x+1
example in integer variables x and y (x:= x+1. x:= x–1) || y:= x
= ok || y:= x
= y:= x
replace x=x by ⊤
4/19
Independent Composition
(x:= x+y. x:= x×y) || (y:= x–y. y:= x/y)
You should have written
(x:= x+y || y:= x–y). (x:= x×y || y:= x/y)
5/19
laws
Independent Composition
P||Q = ∃tP, tQ· (substitute tP for tʹ in P ) ∧ (substitute tQ for tʹ in Q )
∧ tʹ=maxtPtQ
(x:= e || y:= f). P = (for x substitute e and independently for y substitute f in P )
P||Q = Q||P
P||(Q||R) = (P||Q)||R
P || Q∨R = (P || Q) ∨ (P || R)
P||ifbthenQelseRfi = ifbthenP||QelseP||Rfi ifbthenP||QelseR||Sfi = ifbthenPelseRfi||ifbthenQelseSfi
symmetry associativity distributivity distributivity distributivity
6/19
List Concurrency
Li:=e = Lʹi=e ∧ (∀j:0,..#L·j i⇒Lʹj=Lj) ∧ xʹ=x ∧ yʹ=y ∧… Li:= e = Lʹi=e ∧ (∀j: (this part)· j i ⇒ Lʹj=Lj) ∧ xʹ=x ∧ …
example find the maximum item in a nonempty list findmax 0 (#L) where
findmax = 〈i,j→i
If abs (i–j) > 1
C i and C j in parallel
then S i and S j in parallel then S i and C j in parallel
C1S1 C1S1 C1S1 C1S1 C2S2 C2S2 C2S2
C3 S3
C3 S3
C4 S4
16/19
Dining Philosophers
17/19
If i⧧j , If i⧧j ,
If i⧧j , If i⧧j ,
life
Pi
up i down i eat i
= = = = =
Dining Philosophers
(P0∨P1∨P2∨P3∨P4). life
up i. up(i+1). eat i. down i. down(i+1) chopstick i:= ⊤
chopstick i:= ⊥
······chopstick i······chopstick(i+1)······
becomes (up i || up j) . (down i. up j) becomes (down i || up j) .
(down i. down j) becomes (down i || down j) . If i⧧j ∧ i+1⧧j , (eat i. up j) becomes (eat i || up j) .
(up i. up j)
(up i. down j) becomes (up i || down j) .
If i⧧j ∧ i⧧j+1 , (up i. eat j) becomes (up i || eat j) .
If i⧧j ∧ i+1⧧j , (eat i. down j) becomes (eat i || down j) .
If i⧧j ∧ i⧧j+1 , (down i. eat j) becomes (down i || eat j) .
If i⧧j ∧ i+1⧧j ∧ i⧧j+1 , (eat i. eat j) becomes (eat i || eat j) .
18/19
life = Pi = up i = down i = eat i =
(P0∨P1∨P2∨P3∨P4). life
up i. up(i+1). eat i. down i. down(i+1) chopstick i:= ⊤
chopstick i:= ⊥
······chopstick i······chopstick(i+1)······
Dining Philosophers
life = P0||P1||P2||P3||P4 ✗
P i = (up i || up(i+1)). eat i. (down i || down(i+1)). P i
19/19