π-Calculus

Reasoning about concurrency and

communication (Part 1).

CS5204 – Operating Systems 1

 π Calculus
Robin Milner

1934-2010

1991
Dennis Kafura – CS5204 – Operating Systems 2
 π Calculus
Milner’s Approach

 “…most computing involves interaction – and

therefore involves system with components that are
concurrently active.”

 “…we shall work with a model whose basic action

is to communicate across an interface with a
handshake, which means that the two participants
synchronize this action.”

 “…a calculus for analysing properties of concurrent

communicating processes, which may grow and
shrink and move about.”
From: Communicating and Mobile Systems: the π-calculus

Dennis Kafura – CS5204 – Operating Systems 3

 π Calculus
Theoretical Foundations of Concurrency

A formal study of concurrency enables:

• understanding the essential nature of concurrency
• reasoning about the behavior of concurrent systems
• developing tools to aid in producing correct systems

The π-calculus of Robin Milner:

• an algebra (operators, expressions, reaction rules)
• an interpretation for concurrent/communicating/mobile
processes

CS 5204 – Operating Systems 4

 π Calculus
A Quick Overview

Operation Notation Meaning

prefix π.P sequencing

action x(y) communication

xy
a.P + b.Q
summation choice
Σ π[Link]
recursion P = {…}.P
repetition
replication !P
composition P|Q concurrency
restriction (ν x)P encapsulation

CS 5204 – Operating Systems 5

 π Calculus
The Structure of a Process
A process is an autonomous entity possessing named ports through which it may
communicate with other processes. The name of the process and its ports are introduced as:
ProcessName(port-list) = behavior of the process

In the description of the process’ behavior, port names with overbars are interpreted as
“output” ports while names without overbars are often interpreted as “input’” ports.
The process below models a simple client that has one output port, “request” and one input
port, “reply”.

request
Client(request, reply) = ….request…reply...
reply

graphical algebraic

The special behavior “0” (zero) represents a terminated process (e.g., a process that
takes no action).
CS 5204 – Operating Systems 6
 π Calculus
A Sequential Process

The behavior of a process is expressed by algebraic equations. Suppose that we want to

describe a process that behaves like a “client.” This behavior can be expressed as:

Client(open, close, request, reply) = open.request1.reply1. [Link].0

The dot (“.”) is a prefix operation expressing sequential behavior.

The above equation is read as follows: the Client process issues an “opens” message
followed by two request-reply exchanges. It then “closes” the session and terminates.

CS 5204 – Operating Systems 7

 π Calculus
A Repetitive Sequential Process

A Client that engages in repeated sessions can be expressed using a recursive definition as:

Client(open, close, request, reply) =

[Link]. [Link](open, close, request, reply)

The above equation is read as follows: the Client process issues an “open” message
followed by two request-reply exchanges. It then “closes” the session and acts like the
Client process again.

CS 5204 – Operating Systems 8

 π Calculus
A Process with Alternative Behavior

A typical sequential server must be able to enforce a protocol of interaction with its clients.
The behavior of a typical sequential server process can be modeled as follows.

IdleServer(open, request, reply, close) = [Link](open, request, reply,close)

BusyServer(open, request, reply, close)

= [Link](open, request, reply, close)
+ [Link](open, request, reply, close)

Notes:
•the “+” operator represents choice or alternative action
•the server will only engage in an “open” action interaction at the start
•the server can handle any number of request-reply sequences
•once the server engages in a “close” action, it returns to its original condition
•the server can iteratively handle

CS 5204 – Operating Systems 9

 π Calculus
Communicating Processes

Processes can be composed, allowing them to communicate through ports with complementary
names (i.e., one agent has an output port and the other has an input port with the same name).
Concurrent communicating agents can synchronize their behaviors through their willingness or
unwillingness to communicate. This reflects a rendezvous style of interaction.

x x
y z

xy.0 | x(z).0

CS 5204 – Operating Systems 10

 π Calculus
Binding Names on Input
When an input command is a prefix to a process description, the
actual name received on an input port replaces in the body of
the process description the formal name used in the input
command.

z
xy.0 | x(u).uv.0
x(u). …u….u…..u

z z z 0 | yv.0

CS 5204 – Operating Systems 11

 π Calculus
Semantics of Concurrent Communication

xy.0 | x(u).uv.0 | xz.0

0 | yv.0 | xz.0 xy.0 | zv.0 | 0

A system can evolve in different ways depending on the interactions

among processes.

CS 5204 – Operating Systems 12

 π Calculus
Mobility
Mobility in the π-calculus:

•refers to dynamic change in the communication topology

among processes
•is accomplished by a process acquiring and losing ports
through which it may communicate with other processes
•is realized by transmitting the name of a port as the value of
some communication between two processes allowing the
transmitted port to be known to the receiving process

B B x
y y

y y
A C A C
x x
x

CS 5204 – Operating Systems 13

 π Calculus
Mobility

B B x
y y

y y
A C A C
x x
x

A(x,y) = x.A(x,y) + y(x).A’(y) B(y) = y(z).z.B’(y,z)

A’(y) = … B’(y,z) = …

(A | B | C) = ( x.A(x,y) + y(x).A’(y) | y(z).z.B’(y,z) | C )

= (A’(y) | x.B’(y,x) | C )

CS 5204 – Operating Systems 14

 π Calculus
Mobility

CAR(talk1, switch1)

talk1
switch1

BASE1 IDLEBASE2
alert1 alert2

give1 give2
CENTRE1

CS 5204 – Operating Systems 15

 π Calculus
Mobility

CAR(talk2, switch2)

talk2
switch2

IDLEBASE1 BASE2
alert1 alert2

give1 give2
CENTRE2

CS 5204 – Operating Systems 16

 π Calculus
Mobility

The bases can be modeled by:

BASE(talk, switch, give, alert) = [Link](talk, switch, give, alert)

+ give(t, s).switch t s .IDLEBASE(talk, switch, give, alert)

IDLEBASE(talk, switch, give, alert) = [Link](talk, switch, give, alert)

The car’s behavior can be described as:

CAR(talk, switch) = [Link](talk, switch)

+ switch(talk’ switch’).CAR(talk’, switch’)

CS 5204 – Operating Systems 17

 π Calculus
Mobility

A simple control system, that alternates between the two

transmitters, is given by:

CENTRE1 = give1 talk2 switch2 .alert2.CENTRE2

CENTRE2 = give2 talk1 switch1 .alert1.CENTRE1

The mobile transmission system is:

SYSTEM1 = (ν talk1, switch1, give1, alert1, talk2, switch2, give2, alert2)

(Car(talk1, switch1) | BASE1 | IDLEBASE2 | CENTRE1)

where BASEi = BASE(talki, switchi, givei, alerti) for i = 1,2

IDLEBASEi = IDLEBASE(talki, switchi, givei, alerti) for i = 1,2

CS 5204 – Operating Systems 18

 π Calculus
Replication

The terminating process definition:

Client(open, close, request, reply) = open.request1.reply1. [Link].0

can be used to describe a longer-running system using replication as follows:

SYSTEM = ( ! Client | Server )

Which is equivalent to spawning/forking as many copies of the Client process

as desired.

CS 5204 – Operating Systems 19

 π Calculus
Restriction
A name that is private to a process or a group of collaborating processes can be
defined by restriction similar to the effect of scoping or encapsulation.

Suppose that two different process are each attempting to communicate two
values to a process using port x. The following will not work correctly:

xa. xb…. | x(f).x(g)…. | [Link]...

Because the middle process could receive the a from the left process and the c
from the right process. Encapsulation can be used to create a “private” link along
which the values can be passed with interference, as in:

(ν w)([Link] …) | x(u).u(f).u(g)… | (ν t)([Link]…)

CS 5204 – Operating Systems 20