Concurrency problems class

Catuscia Palamidessi, Jean-Jacques Lévy, James J. Leifer

Catuscia@lix.polytechnique.fr, Jean-Jacques.Levy@inria.fr, James.Leifer@inria.fr 11 December 2003

1 Definition: CCS processes

P ::= 0  empty
α.P  prefixing
P |P  parallel composition
(ν L)P  hiding
P + P  summation
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
K  constant (for expressing recursion)
!P  π-calculus-style replication (for expressing recursion)
μX.P  fixed-point (for expressing recursion)

2 Definition: CCS alphabetic conventions

a name
\overline{a} co-name
ℓ label (ranges over names and co-names)
L label set
f label map
α action (ranges over labels and τ)

3 Definition: CCS labelled transitions rules

• input: a.P ⟶^{a} P

• output: \overline{a}.P ⟶^{\overline{a}} P

• synchronization: \frac{P ⟶^{ℓ} P′ Q ⟶^{\overline{ℓ}} Q′}{P |Q ⟶^{τ} P′|Q′}

• choice: \frac{P ⟶^{α} P′}{P + Q ⟶^{α} P′} (and symmetrically)

• parallel composition: \frac{P ⟶^{α} P′}{P |Q ⟶^{α} P′|Q} (and symmetrically)

• hiding: \frac{P ⟶^{α} P′}{(ν L)P ⟶^{α} (ν L)P′} if α, \overline{α} ∉ L

• and others, for example...

• constant: \frac{P ⟶^{α} P′}{K ⟶^{α} P′} if K = P

• replication (many possible): \frac{P |!P ⟶^{α} P′}{!P ⟶^{α} P′}

• fixed-point (many possible): \frac{P \{μX.P/X\} ⟶^{α} P′}{μX.P ⟶^{α} P′}

4 Definition: CCS operational equivalences

• strong simulation: a relation R is a strong simulation if for all (P, Q) ∈ R and P ⟶^{α} P′, there exists Q′ such that Q ⟶^{α} Q′ and (P′, Q′) ∈ R.

• strong bisimulation: a relation R is a strong bisimulation if it and its inverse are strong simulations.

• strong bisimilarity: ∼ is the largest strong bisimulation.

• weak simulation: a relation R is a weak simulation if for all (P, Q) ∈ R we have:

1. if P ⟶^{τ} P′ then there exists Q′ such that Q ⟶^{τ}^{∗} Q′ and (P′, Q′) ∈ R.

2. if P ⟶^{ℓ} P′ then there exists Q′ such that Q ⟶^{τ}^{∗}⟶^{ℓ}⟶^{τ}^{∗} Q′ and (P′, Q′) ∈ R.

• weak bisimulation: a relation R is a weak bisimulation if it and its inverse are weak simulations.

• weak bisimilarity (also known as bisimilarity, also known as observational equivalence): ≈ is the largest weak bisimulation.

• observational congruence: ≅ is the largest symmetric relation satisfying the following property: if P ≅ Q and P ⟶^{α} P′ then there exists Q′ such that Q ⟶^{τ}^{∗}⟶^{ℓ}⟶^{α}^{∗} Q′ and P′ ≈ Q′.

5 Exercise (CCS): unreliable transmission medium

A transmitter T, an unrealiable transmission medium M, and a receiver R are modelled as follows:

T =^{def} in.\overline{i}.T′
T′ =^{def} r.\overline{i}.T′ + a.T
M =^{def} i.M′
M′ =^{def} \overline{o}.M + τ.\overline{r}.M
R =^{def} o.\overline{out}.\overline{a}.R

M is an unreliable medium: having received an input message from T (action i) it either outputs the message to R (action \overline{o}), or loses it (action τ) and then sends a request for retransmission (action \overline{r}). If R does receive the message, it delivers it (action \overline{out}) and sends an acknowledgement directly to T (action \overline{a}).

1. Calculate the transition graph of (ν i, o, r, a)(T |M|R) and hence show that this process is observationally equivalent to a simple reliable buffer B defined by:

B =^{def} in.\overline{out}.B

2. Are (ν i, o, r, a)(T |M|R) and B observationally congruent?

3. Do the two have the same behavior with respect to divergence, that is can either perform a series of actions ending in an infinite sequence of τ actions?

6 Exercise (CCS): semaphores

1. A semaphore is a mechanism to prevent more than a certain number n of clients from simultaneously entering their critical sections to access a precious resource. A client “brackets” its critical section by requesting entry permission (action \overline{wait}) and then signaling when it is finished (action \overline{signal}):

\overline{wait} ...critical section... \overline{signal}

Note that a mutual exclusion lock (mutex) is a special case (when n = 1) of a semaphore.

Define a CCS process to model a semaphore of capacity n. Hint: create a constant Sem_{k}^{n}, for 0 < n and 0 ≤ k ≤ n, that represent a semaphore in the state when k clients are in their critical sections. You will need to treat the cases k = 0 and k = n specially.

7 Exercise (CCS): deadlock

We say that a process can deadlock if it can perform a sequence of actions to enter a state that is observationally congruent (≅) to 0.

Let

C =^{def} g_{0}.g_{1}.p_{0}.p_{1}.C
D =^{def} g_{1}.g_{0}.p_{1}.p_{0}.D
S_{0} =^{def} \overline{g_{0}}.\overline{p_{0}}.S_{0}
S_{1} =^{def} \overline{g_{1}}.\overline{p_{1}}.S_{1}

1. For each of the following processes, determine whether or not it can deadlock:

(ν g_{0}, p_{0}, g_{1}, p_{1})(C|C|S_{0}|S_{1})
(ν g_{0}, p_{0}, g_{1}, p_{1})(C|D|S_{0}|S_{1})

2. Prove that P ≅ 0 iff P can do no action.

3. Prove that T ≈ 0 where T =^{def} τ.T.

4. Hence show that it is possible for a process that can deadlock to be observationally congruent to one that cannot deadlock.

8 Exercise (π-calculus): arithmetic

We can define a process N_{n} for representing the natural number n as follows:

\begin{matrix}N_{0}(s, z) =^{def} & \overline{z} \\ N_{n+1}(s, z) =^{def} & \overline{s}.N_{n}(s, z) \end{matrix}

Thus N_{n}(s, z) ouputs n times on s and then outputs on z.

Our goal is define a process A(s_{0}, z_{0}, s_{1}, z_{1}, s, z) for adding numbers which has the property that

(ν s_{0}, z_{0}, s_{1}, z_{1})(N_{n_{0}}(s_{0}, z_{0})|N_{n_{1}}(s_{1}, z_{1})|A(s_{0}, z_{0}, s_{1}, z_{1}, s, z)) ≈ N_{n_{0}+n_{1}}(s, z)  (*)

• First define a processes C(s, z, s′, z′) for copying a number from (s, z) to (s′, z′) and prove that

(ν s, z)(N_{n}(s, z)|C(s, z, s′, z′)) ≈ N_{n}(s′, z′)

• Then define addition A(s_{0}, z_{0}, s_{1}, z_{1}, s, z) and prove (∗) above.