Week 9: Concurrent Computation Models

4 properties of concurrent computation

- Non-termination (output may not be the focus of the program)

- Parallelism

- Interference

- Non-determinism

How is equivalence of 2 sequential programs defined?

2 sequential programs are equivalent if, and only if, for all inputs, the give all the same outputs

Why is it difficult to compare equivalence of concurrent programs?

Non-determinism and non-termination means we can't just compare the language of the programs

How can we compare behaviour of concurrent systems?

With the Calculus of Communicating Systems (CCS)!

What is Calculus of Communicating Systems (CCS)?

- An abstract model used to model concurrent systems

- Created by Robin Milner

What is a concurrent system?

A collection of processes

What is a process?

An independent agent that may

- perform internal activities in isolation, or

- interact with the environment to perform shared activities

What are the elements of the CCS?

- Actions (denoted a, b)

- Sequential composition (denoted a.b)

- Non-deterministic choice (denoted +)

- Terminal process (denoted 0)

CCS: Terminal process (0)

A terminated/inactive/deadlocked process

CCS: Action

A set of labels for actions A = N u N' u {τ} where N = set of all input actions, N' = set of all output actions, τ = internal action

CCS: Action prefixing

- Represents a sequence of actions

- For a process P and action a, a.P denotes a system ready to perform action and then it will behave as P

What does the notation a.P ->a P mean, for some action a and process P?

System a.P takes the action a, after which, it will behave as process P

CCS: Non-deterministic choice (+)

- For processes P and Q, P+Q denotes a choice between P and Q

- The system P+Q will either behave as P and discard Q, or behave as Q and discard P

CCS: Constants and recursion

- Constants defined with ::=

- Can be recursive e.g. C ::= tick.tock.C

What is a program?

A collection of process constants

How is concurrent behaviour modelled in CCS?

With parallel composition

CCS: Parallel composition

- For processes P and Q, write P|Q to denote that P and Q can run in parallel to one another

- Each process may proceed independently

- If a.P and a'.Q, P and Q may interact internally with ->τ

What is a CCS restriction?

Avoid unwanted process interaction with restricting action/co-action pairs

How is a CCS restriction denoted?

'v'

For a process P and action a, what does va.P mean?

- P cannot take the input action a or its output action a' from any external processes

- P can take a or a' internally

How can we represent CCS graphically?

With a Labelled Transition System (LTS)

How can LTS be denoted?

As a triple (P, A, {->a for all a in A})

For an LTS system denoted (P, A, {->a for all a in A}), what does the P represent?

P = set of processes

For an LTS system denoted (P, A, {->a for all a in A}), what does the A represent?

A = set of actions

For an LTS system denoted (P, A, {->a for all a in A}), what does the {->a for all a in A} represent?

{->a for all a in A} = the transition relation mapping processes to other processes

What are the nodes in an LTS?

Processes

What are the labels in an LTS?

Actions

What are the edges in an LTS?

A subset of PxP

How do we represent action prefixing (a.P ->a P) in an LTS?

Two nodes for a.P and P, and a directed edge from a.P to P labelled a

How do we represent non-deterministic choice (a.P + b.Q) in an LTS?

- A node for a.P + b.Q

- One directed edge from a.P + b.Q to P labelled a

- One directed edge from a.P + b.Q to Q labelled Q

How do we represent recursion (X ::= a.X) in an LTS?

One node for X, with a reflexive edge going back into itself labelled a

How do we represent parallel composition (a.P | b.Q) in an LTS?

- Start from node a.P | b.Q

- One directed edge from a.P | b.Q to node P | b.Q labelled a

- One directed edge from a.P | b.Q to node a.P | Q labelled b

- One directed edge from P | b.Q to P | Q labelled b

- One directed edge from a.P | Q to P | Q labelled a

How do we represent interaction of a and a' for parallel composition (a.P | a'.Q) in an LTS?

- Start from node a.P | a'.Q

- Same as for normal parallel composition with one extra directed edge from a.P | a'.Q to P | Q labelled τ

How do we represent a terminal process (0) in an LTS?

A single node for 0

How do we represent restriction (va. (a.P)) in an LTS?

A single node for va. (a.P)

How do we represent an internal interaction with a restriction in an LTS?

- One node for va. (a.A | a'.B)

- One directed edge from va. (a.A | a'.B) to va. (A | B)

How can we define equivalence of two concurrent processes?

Two concurrent processes are equivalent if and only if an external observer cannot tell their behaviour apart

What is another word for equivalence of two concurrent processes?

Bisimularity

What is a strong bisimulation (in mathematical terms)?

For two LTSes, a binary relation S that is a subset of PxP is a strong bisimulation if and only if whenever (P,Q) is in S, then for each action (excluding internal actions),

1. If P ->a P', then Q ->a Q' for some Q' such that (P',Q') is in S

2. If Q ->a Q', then P ->a P' for some P' such that (P',Q') is in S

What is a strong bisimulation (in layman's terms)?

Process equivalence should be based on observation: if process P is equivalent to process Q, then we should be able to perform the same actions with P and Q and obtain results that are equivalent.