concurrency 101

.Concurrency 4BisimulationsJean-Jacques L´evyjeanjacqueslevy.net/dea1.Bibliography† Principles of Concurrent ProgrammingMordechai Ben-Ari, Prentice Hall, 1982† Communication and ConcurrencyRobin Milner, Prentice Hall, 1989† Algebraic Theory of ProcessesMatthew Hennessy, MIT Press, 1988† Communicating and Mobile Systems: the Pi-CalculusRobin Milner, Cmabridge University Press, 1999.† The Pi-Calculus : A Theory of Mobile ProcessesDavide Sangiorgi, David Walker, Cambridge University Press, 2001† System Porgramming in Modula-3Greg Nelson, Prentice Hall, 19912.CCS with values (1/4)Languagex ::= variablesx˜ ::= x ;x ;:::x (n‚0)1 2 nv ::= valuesv˜ ::= v ;v ;:::v (n‚0)1 2 na;b;c ::= (channel) namesa;b;c ::= co-names a=afi ::= a(x)javj¿ actionsP;Q;R ::= 0jfi:P jP +Qj(P jQ)j(”fi)P jKhv˜i processesdefKhx˜i = P ::= constant definitionsAct=fa(x);b(x);c(x);:::g[fav;bv;cv;:::g[f¿gNotation: fi for fi:03.CCS with values (2/4)Memory registerdefReghi = put(x):AhxidefAhxi = 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 ?Buffersdefin;out in;outBuf hi = in(x):outx:Buf hi1 1defin;outBuf hi = in(x):Ahxi2def in;outAhxi = in(y):outx:Ahyi+outx:Buf hi2def0 in;c c;outBuf hi = (”c)(Buf hijBuf hi)1 1 10Exercice 2 Relate Buf and Buf .2 14.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¡!Qfifi 00 Q¡!QP ¡!P[Par1] [Par2]fi fi0 0P jQ¡!P jQ P jQ¡ ...