cours concurrency

Description

.Concurrency 3CCSJean-Jacques L´evyjeanjacqueslevy.net/dea1.Minimal language for concurrencyThe ‚-calculus is a minimal for functional languages. It canalso be used as a basis for imperative languages (via continuations).What is a minimal language for concurrent processes ?† CCS [Milner]† …-calculus [Milner, Parrow, Walker, Sangiorgi]† CSP [Hoare]† Petri nets† Mazurkiewitz traces† Events structures , True concurrency [Winskel]† IO-automatas [Lynch, Tuttle]2.CCS (1/4)Languagea;b;c ::= (channel) namesa;b;c ::= co-names a=afi ::= ajaj¿ actionsP;Q;R ::= 0jfi:P jP +Qj(P jQ)j(”fi)P jK processesdefK = P ::= constant definitionsAct=fa;b;c;:::g[fa;b;c;:::g[f¿g Notation: fi for fi:0† 0 null process† fi:P sequential action† P +Q non-deterministic (external) choice† P jQ parallel composition† (”fi)P restriction on fi† K (recursively defined) constant3.CCS (2/4)Examples (coffee machine revisited)0P =A P =B C =(k:d:D+t:d:D)0 0A=c:(k:d:A+t:d:A) B =c:C D =c:C00 000P =E P =F0 0E =(c:k:d:E+c:t:d:E) F =c+(c:k:d:F +c:t:d:F)Interaction with coffee machineP jc:k:d P jc:k:djc:t:d0 00 00 000P jClient1 P jClient1 P jClient1 P jClient10 0 0 000P jClient2 P jClient2jClient2 P jClient1jClient20 00wheredef defClient1 = c:k:d:Client1 Client2 = c:t:d:Client2466.CCS (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¡!P jQfia a 00 0 P ¡!P fi62fa;agP ¡!P Q¡!Q[Com] [Res]¿ fi0 0 0P ...

Informations

• Publié par: Kahej
• Nombre de lectures: 63
• Langue: English

Extrait

.

Concurrency

CCS

Jean-JacquesLevy

jeanjacqueslevy.net/dea

3

1

.

.

.

.

.

.

.

.

.

.