Planche 1

Concurrency 2
Functions vs Processes
Þ Interaction
Jean-Jacques Lévy
jeanjacqueslevy.net/dea

Planche 2

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 S = 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 ]] ÏS |® S.

A concurrent program is a relation on memory states. [[ P ]] Î S |® 2^S.

Planche 3

Concurrency Þ Interaction

Consider
P = [x := 1 ]
Q = [x := 0; x := x+1 ]
P and Q are same functions on memory states: s |® s[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.

Planche 4

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^{(S |® S) × 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.

Planche 5

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₀ ¾®^µ₁ P₁ ¾®^µ₂ P₂ ··· ¾®^µ_n P_n=Q for n ³ 0.

Planche 6

Example (1/3)

A vending machine for coffee/tea. At beginning, P₀

Planche 7

Example (2/3)

A different vending machine for coffee/tea. At beginning, P₀'

Is this LTS equivalent to previous one?

Planche 8

Example (3/3)

Two new vending machines P''₀ and P'''₀

Why these LTS are not equivalent to previous ones?

Planche 9

Concurrency Û Automata (1/2)

Let abstract Act (actions) as an alphabet {a, b, c, ...}.
(Act may be infinite)

Then LTS look like automata (with possibly infinite number of states).

Consider the language of traces.

Let P=P₀ ¾®^µ₁ P₁ ¾®^µ₂ P₂ ··· ¾®^µ_n P_n (n ³ 0), then

trace(P=P₀ ¾®^µ₁ P₁ ¾®^µ₂ P₂ ··· ¾®^µ_n P_n) = µ₁µ₂···µ_n

We say that µ₁µ₂···µ_n is a trace of P

Let Traces(P) = { w | w is a trace of P }

Planche 10

Concurrency Û Automata (2/2)

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

Traces(P₀) = prefixes((c(k+t)d)^*),
Traces(P'₀) = prefixes(c((k+t)dc)^*),
Traces(P''₀) = prefixes((ckd + ctd)^*,
Traces(P'''₀) = prefixes((c+c(k+t)dc)^*),
Exercice 1 Show Traces(P₀) = Traces(P'₀) = Traces(P''₀) = Traces(P'''₀)

However, P₀ and P₀' seem equivalent
but both P₀'' and P₀''' look distinct from P₀.

Why?

After c, the set of choices are distinct in P₀ and P''₀.
Coffee button is always enabled in P₀, but not in P''₀.
Same for tea button.
In P'''₀, both tea and coffee may be disabled after c.

Planche 11

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₀ P₀''' P₀

Exercice 3 Give intuition for P₀ ~ P₀', P₀ ¬ ~P₀'', P₀ ¬ ~P₀'''

Planche 12

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?

Planche 13

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.

Planche 14

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'').

Planche 15

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₀ ~ P₀', P₀ ¬ ~P₀'', P₀ ¬ ~P₀''' in vending machines.

Exercice 8 Give an alternative definition for .

Exercice 9 Show P₀ P₀''' P₀.

Planche 16

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₁, d₂, ... d_n ... } where d₁ d₂ ··· d_n ···

Theorem 8[Kleene] gfp(f) = Ç { fⁿ() | 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ⁿ(D) | n ³ 0 }

Planche 17

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(nlogn) 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.

Planche 18

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₀ ¾®^µ₁ P₁ ¾®^µ₂ P₂ ··· ¾®^µ_n P_n=Q and µ = µ₁µ₂···µ_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'.

Planche 19

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!!).

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