concurrency 101

Informations

• Publié par: Saem
• Nombre de lectures: 85
• Langue: English

Extrait

.
Concurrency 4
Bisimulations
Jean-Jacques L´evy
jeanjacqueslevy.net/dea
1.
Bibliography
† Principles of Concurrent Programming
Mordechai Ben-Ari, Prentice Hall, 1982
† Communication and Concurrency
Robin Milner, Prentice Hall, 1989
† Algebraic Theory of Processes
Matthew Hennessy, MIT Press, 1988
† Communicating and Mobile Systems: the Pi-Calculus
Robin Milner, Cmabridge University Press, 1999.
† The Pi-Calculus : A Theory of Mobile Processes
Davide Sangiorgi, David Walker, Cambridge University Press, 2001
† System Porgramming in Modula-3
Greg Nelson, Prentice Hall, 1991
2.
CCS with values (1/4)
Language
x ::= variables
x˜ ::= x ;x ;:::x (n‚0)1 2 n
v ::= values
v˜ ::= v ;v ;:::v (n‚0)1 2 n
a;b;c ::= (channel) names
a;b;c ::= co-names a=a
fi ::= a(x)javj¿ actions
P;Q;R ::= 0jfi:P jP +Qj(P jQ)j(”fi)P jKhv˜i processes
def
Khx˜i = P ::= constant definitions
Act=fa(x);b(x);c(x);:::g[fav;bv;cv;:::g[f¿g
Notation: fi for fi:0
3.
CCS with values (2/4)
Memory register
def
Reghi = put(x):Ahxi
def
Ahxi = put(y):Ahyij getx:Ahxi
:::jP j put1j get(x):Qj put2:get(y):Rj:::
Exercice 1 What can be values of x and y in Q and R ?
Buffers
defin;out in;outBuf hi = in(x):outx:Buf hi1 1
defin;outBuf hi = in(x):Ahxi2
def in;outAhxi = in(y):outx:Ahyi+outx:Buf hi2
def0 in;c c;outBuf hi = (”c)(Buf hijBuf hi)1 1 1
0Exercice 2 Relate Buf and Buf .2 1
4.
CCS with values (3/4)
Semantics (SOS)
fifi 00fi Q¡!QP ¡!P[Act]fi:P ¡!P [Sum1] [Sum2]fi fi0 0P +Q¡!P P +Q¡!Q
fifi 00 Q¡!QP ¡!P[Par1] [Par2]fi fi0 0P jQ¡!P jQ P jQ¡!P jQ
a(x) a(x)av av0 0 0 0P ¡! P Q¡!Q P ¡!P Q¡! Q[Com1] [Com2]¿ ¿0 0 0 0P jQ¡!P fv=xgjQ P jQ¡!P jQfv=xg
fi fi def0 0P ¡!P fi62fa;ag Pfv˜=x˜g¡!P Khx˜i = P
[Res] [Rec]fi fi0 0(”a)P ¡!(”a)P Khv˜i¡!P
5.
CCS with values (4/4)
One can emulate CCS with values by pure CCS (with infinite sum).
P [P]
a(x):P Σ a :[Pfv=xg] (V set of values)vv2V
av:P a :[P]v
¿:P ¿:[P]
Σ P Σ [P ]i2I i i2I i
P jQ [P]j[Q]
:::
Exercice 3 Terminate the translation 4 Find the relation between P and [P].
6b
b
b
b
.
CCS and weak bisimulation (1/4)
¿ ¿ ¿ ¿⁄Write P(!) Q if P =P !P !P ¢¢¢!P =Q (k‚0).0 1 2 k
Let „=„ „ ¢¢¢„ (n>0)1 2 n
„ „ „ „1 2 nWrite P ¡!Q if P ¡!¡!¢¢¢¡!Q
„ „ „ „¿ ¿ ¿ ¿1 2 n⁄ ⁄ ⁄ ⁄Write P =)Q if P(!) ¡!(!) ¡!(!) ¢¢¢¡!(!) Q
Write „ be „ where all occurences of ¿ in „ have been erased.
nTake „=¿ab¿¿a, then „=aba. If „=¿ , then „=† (empty string).
„
Then ¡! specifies exactly the ¿ actions occuring in „
„
=) specifies at least the ¿
„
=) specifies nothing about the ¿ actions
7b
b
.
CCS and weak bisimulation (2/4)
Definition 1 P weakly bisimilar to Q (we write P …Q) if, for any
fi2Act, whenever
fi fi0 0 0 0 0† P ¡!P , there is Q such that Q=)Q and P …Q.
fi fi0 0 0 0 0† Q¡!Q, there is P such that P =)P and P …Q.
(… is the largest weak bisimulation)
Examples
def def
A = c:(k:A+t:A) C = (a:b:¿:C +b:a:¿:C
def def
B = (”d)c:(k:d:B+t:d:B) D = ((a:b:D+ba:D)
A…B C…D
Exercice 5 Find weak bisimulation when
def
A = a:A +b:A +¿:A0 0 1 1
def def
A = a:A +¿:A B = a:B +¿:B1 1 2 1 1 2
def def
A = b:A B = b:B2 0 2 1
8.
CCS and weak bisimulation (3/4)
Proposition 2 Following equations hold.
¿:P … P
P …Q ) P jR…QjR
P …Q ) RjP …RjQ
P …Q ) fi:P …fi:Q
P …Q ) (”x)P …(”x)Q
def
K = P andP …Q ) K…Q
Exercice 6 Prove it.
Fact 3 P …Q 6) P +R…Q+R
Take P =¿:Q, Q=a, R=b.
Then ¿:a…a. But we have not ¿:a+b…a+b.
Hence weak bisimulation is not a congruence in CCS
(differs from strong bisimulation)
9.
CCS and weak bisimulation (4/4)
Definition 4 [observation-congruence] P weakly congruent to Q (we
»write P Q) if, for any fi2Act, whenever=
fi fi0 0 0 0 0† P ¡!P , there is Q such that Q=)Q and P …Q.
fi fi0 0 0 0 0† Q¡!Q, there is P such that P =)P and P …Q.
»Exercice 7 Prove µ….=
»Proposition 5 is a congruence.=
Exercice 8 Prove it.
Proposition 6 The following ¿ laws are true:
fi:¿:P … fi:P
P +¿:P … ¿:P
fi:(P +¿:Q)+fi:Q … fi:(P +¿:Q)
Exercice 9 Prove them.
10