Concurrency : Functions vs Processes

Informations

• Publié par: Shiem
• Nombre de lectures: 23
• Langue: English

Extrait

.
Concurrency 2
Functions vs Processes
) Interaction
Jean-Jacques L´evy
jeanjacqueslevy.net/dea
1.
Concurrency ) Non-deterministism
Suppose x is a global variable. At beginning, x=0
Consider
P =[x:=x+1;x:=x+1jjx:=2⁄x]
after P, then x may have several values (x2f2;3;4g)
Hence P is not a function from memory states to memory states.
In concurrent programming, execution is not deterministic since it is
upto an external agent (the scheduler).
Let Σ=Variables7!Values be the set of memory states.
Let [P] be the meaning of P.
A concurrent program is not a (partial) function from memory states to
memory states. [P]62Σ7!Σ.
ΣA concurrent program is a relation on memory states. [P]2Σ7!2 .
26
.
Concurrency ) Interaction
Consider
P =[x:=1]
Q=[x:=0;x:=x+1]
P and Q are same functions on memory states : ¾7!¾[1=x]
However
after P jjP, then x2f1g
after P jjQ, then x2f1;2g
A semantic (meaning) is compositional iff [P]=[Q] implies
[C[P]]=[C[Q]] for any context C[].
In previous example, in any compositional semantics, [P]=[Q].
Conclusion
P and Q are not equivalent processes.
3.
Concurrency , Termination
Concurrent processes are often non terminating.
An operating system never terminates; same for the software of a
vending machine, or a traffic-light controler, or a human, etc.
A process P is a set of pairs (f ;P ), atomic action and a derivativei i
process. It starts by performing f and then becomes process P .i i
Atomic steps usually terminate.
(Σ7!Σ)£PRoughly speaking, let P be the set of processes. Then P =2
Is this equation meaningful? Answer : Scott’s domains, denotational
semantics. Remarkable and difficult theory of Plotkin (Scott’s
powerdomains 1976).
We try the simpler theory of labeled transition systems.
4.
Labeled Transition Systems
A LTS is triple (P;Act;T) where
† P is the set of processes
† Act is the set of actions
† T µP£Act£P is the transition relation
„
Let write P ¡!Q for (P;„;Q)2T.
Read P interacts with environment with action „, then becomes Q.
„ „ „n1 2Q is a derivative of P if P =P ¡!P ¡!P ¢¢¢¡!P =Q for n‚0.0 1 2 n
5e
.
Example (1/3)
A vending machine for coffee/tea. At beginning, P0
drink
P2
coffee
.20
P P0 1
tea
P3
drink
6e
e
.
Example (2/3)
0A different vending machine for coffee/tea. At beginning, P0
coffee drink
.20.200P0
tea drink
Is this LTS equivalent to previous one?
7e
e
e
e
.
Example (3/3)
00 000Two new vending machines P and P0 0
drink drink
coffee
coffee
.20
.20
.2000 000P P0 0
.20 tea
tea
drinkdrink
Why these LTS are not equivalent to previous ones?
8.
Concurrency , Automata (1/2)
Let abstract Act (actions) as an alphabet fa;b;c;:::g.
(Act may be infinite)
Then LTS look like automata (with possibly infinite number of states).
Consider the language of traces.
„ „ „1 2 nLet P =P ¡!P ¡!P ¢¢¢¡!P (n‚0), thenn0 1 2
„ „ „1 2 n
trace(P =P ¡!P ¡!P ¢¢¢¡!P )=„ „ ¢¢¢„0 1 2 n 1 2 n
We say that „ „ ¢¢¢„ is a trace of P1 2 n
Let Traces(P)=fwjwis a trace ofPg
9.
Concurrency , Automata (2/2)
In previous examples, write k for coffee, t for tea, c for :20e, d for drink.
⁄Traces(P )=prefixes((c(k+t)d) ),0
0 ⁄Traces(P )=prefixes(c((k+t)dc) ),0
00 ⁄Traces(P )=prefixes((ckd+ctd) ,0
000 ⁄Traces(P )=prefixes((c+c(k+t)dc) ),0
0 00 000Exercice 1 Show Traces(P )=Traces(P )=Traces(P )=Traces(P )0 0 0 0
0However, P and P seem equivalent0 0
00 000but both P and P look distinct from P .00 0
Why?
00After c, the set of choices are distinct in P and P .0 0
00Coffee button is always enabled in P , but not in P .0 0
Same for tea button.
000In P , both tea and coffee may be disabled after c.0
10