.

Concurrency 2 Functions vs Processes

⇒ Interaction

Jean-Jacques Lévy

jeanjacqueslevy.net/dea

.

Concurrency ⇒ Non-deterministism

Suppose x is a global variable. At beginning, x = 0 Consider P = [x := x + 1; x := x + 1 || x := 2 ∗ x] after P, then x may have several values (x ∈ {2, 3, 4}) Hence P is not a function from memory states to memory states.

In concurrent programming, execution is not deterministic since it is upto an external agent (the scheduler).

Let Σ = Variables ↦ Values be the set of memory states. Let [[P]] be the meaning of P. A concurrent program is not a (partial) function from memory states to memory states. [[P]] ∉ Σ ↦ Σ. A concurrent program is a relation on memory states. [[P]] ∈ Σ ↦ 2^{Σ}.

.

Concurrency ⇒ Interaction

Consider P = [x := 1] Q = [x := 0; x := x + 1] P and Q are same functions on memory states : σ ↦ σ[1/x] However after P || P, then x ∈ {1} after P || Q, then x ∈ {1, 2} A semantic (meaning) is compositional iff [[P]] = [[Q]] implies [[ C[P] ]] = [[ C[Q] ]] for any context C[ ]. In previous example, in any compositional semantics, [[P]] ≠ [[Q]]. Conclusion P and Q are not equivalent processes.

.

Concurrency ⇔ Termination

Concurrent processes are often non terminating.

An operating system never terminates ; same for the software of a vending machine, or a traffic-light controler, or a human, etc.

A process P is a set of pairs (f_{i}, P_{i}), atomic action and a derivative process. It starts by performing f_{i} and then becomes process P_{i}.

Atomic steps usually terminate.

Roughly speaking, let P be the set of processes. Then P = 2^{(Σ↦Σ)×P}

Is this equation meaningful ? Answer : Scott’s domains, denotational semantics. Remarkable and difficult theory of Plotkin (Scott’s powerdomains 1976).

We try the simpler theory of labeled transition systems.

.

Labeled Transition Systems

A LTS is triple (P, Act, T ) where • P is the set of processes

• Act is the set of actions

• T ⊆ P × Act × P is the transition relation

Let write P ⟶^{μ} Q for (P, μ, Q) ∈ T . Read P interacts with environment with action μ, then becomes Q.

Q is a derivative of P if P = P_{0} ⟶^{μ_{1}} P_{1} ⟶^{μ_{2}} P_{2} ⋯ ⟶^{μ_{n}} P_{n} = Q for n ≥ 0.

.

Example (1/3)

A vending machine for coffee/tea. At beginning, P_{0}

P_{0}  .20  P_{1} coffee  P_{2} drink tea  P_{3} drink

.

Example (2/3)

A different vending machine for coffee/tea. At beginning, P′_{0}

P′_{0}  .20  coffee  drink .20 tea  drink

Is this LTS equivalent to previous one ?

.

Example (3/3)

Two new vending machines P′′_{0} and P′′′_{0}

P′′_{0} .20  coffee drink .20  tea drink  P′′′_{0} .20  .20  coffee drink tea drink

Why these LTS are not equivalent to previous ones ?

.

Concurrency ⇔ Automata (1/2)

Let abstract Act (actions) as an alphabet {a, b, c, …}. (Act may be infinite) Then LT S look like automata (with possibly infinite number of states). Consider the language of traces.

Let P = P_{0} ⟶^{μ_{1}} P_{1} ⟶^{μ_{2}} P_{2} ⋯ ⟶^{μ_{n}} P_{n} (n ≥ 0), then

trace(P = P_{0} ⟶^{μ_{1}} P_{1} ⟶^{μ_{2}} P_{2} ⋯ ⟶^{μ_{n}} P_{n}) = μ_{1}μ_{2} ⋯ μ_{n}

We say that μ_{1}μ_{2} ⋯ μ_{n} is a trace of P Let Traces(P) = {w | w is a trace of P }

.

Concurrency ⇔ Automata (2/2)

In previous examples, write k for coffee, t for tea, c for .20e, d for drink.

Traces(P_{0}) = prefixes((c(k + t)d)^{∗}), Traces(P′_{0}) = prefixes(c((k + t)dc)^{∗}), Traces(P′′_{0}) = prefixes((ckd + ctd)^{∗}, Traces(P′′′_{0}) = prefixes((c + c(k + t)dc)^{∗}),

Exercice 1 Show Traces(P_{0}) = Traces(P′_{0}) = Traces(P′′_{0}) = Traces(P′′′_{0})

However, P_{0} and P′_{0} seem equivalent but both P′′_{0} and P′′′_{0} look distinct from P_{0}.

Why ?

After c, the set of choices are distinct in P_{0} and P′′_{0}. Coffee button is always enabled in P_{0}, but not in P′′_{0}. Same for tea button.

In P′′′_{0}, both tea and coffee may be disabled after c.

.

Simulation – Bisimulation

Definition 1 Q simulates P (we write P ≲ Q) if whenever P ⟶^{μ} P′, there is Q′ such that Q ⟶^{μ} Q′ and P′ ≲ Q′. Definition 2 P strongly bisimilar to Q (we write P ∼ Q) if whenever

• P ⟶^{μ} P′, there is Q′ such that Q ⟶^{μ} Q′ and P′ ∼ Q′.

• Q ⟶^{μ} Q′, there is P′ such that P ⟶^{μ} P′ and P′ ∼ Q′.

Graphically,

Exercice 2 Give intuition for P_{0} ≲ P′′′_{0} ≲ P_{0} Exercice 3 Give intuition for P_{0} ∼ P′_{0}, P_{0} ≁ P′′_{0}, P_{0} ≁ P′′′_{0}

.

Definition of bisimulation (1/3)

Definition 3 A bisimulation is a binary relation R on processes such that P R Q implies whenever

• P ⟶^{μ} P′, there is Q′ such that Q ⟶^{μ} Q′ and P′ R Q′.

• Q ⟶^{μ} Q′, there is P′ such that P ⟶^{μ} P′ and P′ R Q′.

An alternative definition for strong bisimulation is : Definition 4 Let ∼ = ∪{R | R is a bisimulation }

Proposition 5 ∼ is an equivalence relation. (reflexive, symmetric, transitive) Exercice 4 Show above proposition. Exercice 5 What is the least bisimulation ?

.

Definition of bisimulation (2/3)

First definition of bisimulation is circular. To make it clear, better is to return to standard theory on fixpoints in complete lattices.

A complete lattice D is any set with • a partial ordering ⪯ (reflexive, transitive, antisymmetric)

• for any subset E ⊆ D, there is an upper bound ∪E and a lower bound ∩E in D.

Examples : 2^{P} with ⊆, 2^{P×P} with ⊆, etc.

f function D ↦ D is monotonic iff x ⪯ y implies f(x) ⪯ f(y).

Theorem 6 [Tarski] In a complete lattice D, any monotonic function f has a least fixpoint lfp(f) and greatest fixpoint gfp(f).

Moreover lfp(f) = ∩{x | f(x) ⪯ x} and gfp(f) = ∪{x | x ⪯ f(x)}

Exercice 6 Prove it.

.

Definition of bisimulation (3/3)

Proposition 7 ∼ is the largest relation ∼′ such that P ∼′ Q implies whenever

• P ⟶^{μ} P′, there is Q′ such that Q ⟶^{μ} Q′ and P′ ∼′ Q′.

• Q ⟶^{μ} Q′, there is P′ such that P ⟶^{μ} P′ and P′ ∼′ Q′.

Proof : Consider the complete lattice of binary relations on P with ⊆. Take P f(R) Q defined as whenever

• P ⟶^{μ} P′, there is Q′ such that Q ⟶^{μ} Q′ and P′ R Q′.

• Q ⟶^{μ} Q′, there is P′ such that P ⟶^{μ} P′ and P′ R Q′. Then f is monotonic, since R⊆S implies f(R) ⊆ f(S).

Moreover R is a bisimulation iff R⊆ f(R).

Hence ∼ = ∪{R | R ⊆ f(R)} = gfp(f).

Therefore ∼ = f(∼) and ∼ is largest ∼′ such that ∼′ = f(∼′).

First definition of ∼ was correct (just add “largest”).

.

Co-induction

In order to show P ∼ Q, it is sufficient to show that P R Q for some bisimulation R. I.e. (P R Q for some relation R such that R ⊆ f(R)) ⇒ P ∼ Q.

Exercice 7 Show P_{0} ∼ P′_{0}, P_{0} ≁ P′′_{0}, P_{0} ≁ P′′′_{0} in vending machines. Exercice 8 Give an alternative definition for ≲. Exercice 9 Show P_{0} ≲ P′′′_{0} ≲ P_{0}.

.

Co-continuity (1/2)

Let D be a complete lattice. Then

f function D ↦ D is co-continuous iff f(∩S) = ∩f(S) for any descending chain S = {d_{1}, d_{2}, … d_{n} …} where d_{1} ⪰ d_{2} ⪰ ⋯ ⪰ d_{n} ⪰ ⋯

Theorem 8 [Kleene] gfp(f) = ∩{f^{n}(⊤) | n ≥ 0} where ⊤ is maximum element of D.

Consider lattice of binary relations 2^{P×P} with ⊆.

Let the graph of derivatives of P be finitely branching, i.e. {Q | P ⟶^{μ} Q} is finite for any P.

Take P f(R) Q defined as whenever • P ⟶^{μ} P′, there is Q′ such that Q ⟶^{μ} Q′ and P′ R Q′.

• Q ⟶^{μ} Q′, there is P′ such that P ⟶^{μ} P′ and P′ R Q′. Then f is co-continuous.

If the graph of derivatives is finitely branching, then ∼ = ∩ {f^{n}(D) | n ≥ 0}

.

Co-continuity (2/2)

Exercice 10 Suppose P has a finite graph of derivatives. Give an algorithm for computing its minimal graph of derivatives, i.e. a graph where distinct states are not bisimilar. O(n log n) algorithm by Paige and Tarjan, (analogous of Hopcroft/Ullman algorithm for computing minimal finite automata).

Exercice 11 Suppose P and Q have finite graphs of derivatives. Give an algorithm for testing P ∼ Q.

.

Exercices

Definition 9 R is a bisimulation up-to ∼ if P R Q implies whenever

• P ⟶^{μ} P′, there is Q′ such that Q ⟶^{μ} Q′ and P′ ∼R∼ Q′.

• Q ⟶^{μ} Q′, there is P′ such that P ⟶^{μ} P′ and P′ ∼R∼ Q′.

Exercice 12 Let R is a bisimulation up-to ∼. Show R ⊆ ∼. (by firstly showing that ∼R∼ is a bisimulation).

Let μ^{+} ∈ Act^{+} (not empty words of actions)

Write P ⟶^{μ^{+}} Q if P = P_{0} ⟶^{μ_{1}} P_{1} ⟶^{μ_{2}} P_{2} ⋯ ⟶^{μ_{n}} P_{n} = Q and μ = μ_{1}μ_{2} ⋯ μ_{n}

(n > 0).

Exercice 13 Show that following definition of strong bisimulation is equivalent to previous one.

Definition 10 R is a (strong) bisimulation if P R Q implies whenever

• P ⟶^{μ^{+}} P′, there is Q′ such that Q ⟶^{μ^{+}} Q′ and P′ ∼R∼ Q′.

• Q ⟶^{μ^{+}} Q′, there is P′ such that P ⟶^{μ^{+}} P′ and P′ ∼R∼ Q′.

.

History

David Park invented bisimulation as maximal fixpoints. (1975) Robin Milner wrote a full book on them for CCS. (1979) Samson Abramsky added them in the lazy lambda calculus. (1984) See also phD of his student Luke Ong. Davide Sangiorgi did the theory of bisimulation in the pi-calculus. (1990) Marcelo Fiore et al put them in data types. (1992) Many people speak now of bisimulations, as a generic names for equivalences on infinite computations. For instance, Dave Sands and others use them for equivalence of Bohm trees in the lambda-calculus (which I never understood ! !).