Planche 1

Concurrency 3
CCS
Jean-Jacques Lévy
jeanjacqueslevy.net/dea

Planche 2

Minimal language for concurrency

The l-calculus is a minimal language for functional languages. It can also be used as a basis for imperative languages (via continuations).

What is a minimal language for concurrent processes ?

CCS [Milner]
p-calculus [Milner, Parrow, Walker, Sangiorgi]
CSP [Hoare]
Petri nets
Mazurkiewitz traces
Events structures Û True concurrency [Winskel]
IO-automatas [Lynch, Tuttle]

Planche 3

CCS (1/4)

Language

a, b, c

::=

(channel) names

::=

co-names

::=

a |

| t

actions

P,Q,R

::=

0 | a.P | P+Q | (P | Q) | (n a) P | K

processes

def

::=

constant definitions

Act = { a, b, c, ... } È { a, b, c, ... } È { t } Notation: a for a.0

0 null process
a.P sequential action
P+Q non-deterministic (external) choice
P| Q parallel composition
(n a)P restriction on a
K (recursively defined) constant

Planche 4

CCS (2/4)

Examples (coffee machine revisited)

P₀ = A

A = c.(k.d.A + t.d.A)

P₀' = B		C = (k.d.D + t.d.D)
B = c.C		D = c.C

P₀'' = E

E = (c.k.d.E + c.t.d.E)

P₀''' = F

F = c+(c.k.d.F + c.t.d.F)

Planche 5

CCS (3/4)

Semantics (SOS)

[Act] a.P

¾®

[Sum1]

P ¾®^a P'

P+Q ¾®^a P'

[Sum2]

Q ¾®^a Q'

P+Q ¾®^a Q'

[Par1]

P ¾®^a P'

P | Q ¾®^a P' | Q

[Par2]

Q ¾®^a Q'

P | Q ¾®^a P | Q'

[Com]

P ¾®^a P' Q ¾®^a Q'

P | Q ¾®^t P' | Q'

[Res]

P ¾®^a P' a Ï{a,a}

(n a) P ¾®^a (n a) P'

[Rec]

P ¾®^a P' K =^def P

K ¾®^a P'

¾®^t internal move
¾®^a (a¹t) interaction on external a-channel

By convention, ¾®^a input on a-channel and ¾®^a output on a-channel

Sum ¹ internal choice P+Q ¾®^t P or P+Q ¾®^t Q.

Planche 6

CCS (4/4)

At present time, no values passed on communication channels.
(see later for value passing calculi)

No buffering in communications. Different from TCP sockets, from Kahn/MacQueen flow systems.
Þ communication by rendez-vous.
º more basic calculus.

Rendez-vous exist in Occam, Ada, CML, Ocaml's processes.

Planche 7

CCS and strong bisimulation (1/4)

Theorem 1 Following relations hold.

P+0	~	P	P \| 0	~	P
P+Q	~	Q+P	P \| Q	~	Q \| P
(P + Q) + R	~	P + (Q + R)	(P \| Q) \| R	~	P \| (Q \| R)
P+P	~	P

(n a)(P \| Q)	~	((n a) P) \| Q	if a not free in Q
(n a)(n b)P	~	(n b)(n a)P
(n a) P	~	(n b) P{b/a}	if b not bound in Q
(n a) a.P	~	0	if a=a or a=a
(n a) a.P	~	a. (n a).P	otherwise

K	~	P	if K =^def P

Planche 8

CCS and strong bisimulation (2/4)

Proof of previous theorem

P+0 ~ P. Take R ={(P+0,P), (P,P+0), (P,P)} and show R is a bisimulation.

Let P+0 ¾®^a P'. Then P ¾®^a P' by rule [Sum1] since 0 ¾®^a P' is not possible. And P' R P'.

Conversely let P ¾®^a P'. Then P+0 ¾®^a P' by rule [Sum1] . And again P' R P'.
P+Q ~ Q+P. Show following R is a bisimulation. Take R ={P+Q, Q+P, (P,P)}.

Let P+Q ¾®^a S.
- Case 1: let P+Q ¾®^a S using [Sum1] . Then P ¾®^a S.
  But Q+P ¾®^a S using [Sum2] .
  QED since S R S.
- Case 2: let P+Q ¾®^a S using [Sum2] . Then Q ¾®^a S.
  But Q+P ¾®^a S using [Sum1] .
  QED since S R S.
Conversely let Q+P ¾®^a S. QED by symmetry.

Planche 9

CCS and strong bisimulation (3/4)

Proof of theorem (continued)

(P+Q)+R ~ P+(Q+R). Show following R is a bisimulation.
Take R ={(P+Q)+R, P+(Q+R), (P,P)}.

Let (P+Q)+R ¾®^a S.
- Case 1: let (P+Q) ¾®^a S using [Sum1] .
  - Case 1.1: let P ¾®^a S using [Sum1] .
    Then P+(Q+R) ¾®^a S by [Sum1] .
    QED since S R S.
  - Case 1.2: Let Q ¾®^a S. Then (Q+R) ¾®^a S by [Sum1] , and P+(Q+R) ¾®^a S by [Sum2] .
    QED since S R S.
- Case 2: Let R ¾®^a S by [Sum2] . Then (Q+R) ¾®^a S by [Sum2] , and P+(Q+R) ¾®^a S by [Sum2] .
  QED since S R S.
By symmetry when P+(Q+R) ¾®^a S.
other equations ...

Exercice 1 Give full proof of theorem.

Planche 10

CCS and strong bisimulation (4/4)

Theorem 2[Expansion]

a.P | b.Q

a.(P | b.Q) + b.(a.P | Q)

a.P |

a.(P |

.Q) +

.(a.P | Q) + t.(P | Q)

Exercice 2 Prove it.

Concurrency in CCS relies on interleaving. Never two actions occur at same time. Different from ``true concurrency''.

Exercice 3 Draw LTS for following processes:

(n a)((a+b) |

)

K₂

def

t.(n a) (a | (

+ b)) + c.K₃

K₁

def

a.(t.K₁ + b) + t.a.K₁

K₃

def

d.K₃

Exercice 4 Draw LTS for (n c) (K₁ | K₂) where

K₁

def

.K₁

K₂

def

b.c.K₂

Exercice 5 Give a CCS term for boolean semaphores.
Exercice 6 Give a CCS term for n-ary semaphores.

Planche 11

Strong bisimulation and congruence

Theorem 3 Strong bisimulation ~ is a congruence. Namely:

P ~ Q Þ C[P] ~ C[Q] for any context C[ ].

Exercice 7 Prove it.

This means that ~ can be used as standard equations.

Exercice 8 Prove by using equations of Theorems 1 and 2 that: (n b) (a.(b | c) + t.(b | b.c)) ~ a.c + t.t.c

Exercice 9 Show K | K ~ K when K =^def a.K.

Exercice 10 Show K ~ K' when K =^def a.K and K' =^def a.a.K'.

Exercice 11 Show K ~ a.K' when K =^def a.b.K and K' =^def b.a.K'.

Exercice 12 Show that a.(b+c) ¬ ~ab + ac.

This document was translated from L^AT_EX by H^EV^EA.