CSP: Four Lectures
CSP: Overview
•	Communicating Sequential Processes
>	C.A.R. Hoare
•	Based on events
>	processes interact by coordinating events
>	semantics defined by traces of events
•	One of many similiar kinds of notations
>	CCS
>	Lotos
>	Occam
•	Has an associated algebraic theory
•	Has compositional semantics
The Challenge of Concurrency

A look back
•	Up to now, we have seen primarily state machines 
>	 State Machines
>	 Z
>	 Algebraic models
>	 Shared Variable Concurrency
Transitions as State Relations
•	Each of these describes conditions for changing from one state  to another.
>	Z = operations relate schemas
>	State machine = precondition/postcondition
>	Shared memory communication = local/global variables
•	CSP describes processes, and focuses on the events that take place
		Process1 = event Æ Process2
Events
•	Events are simply names
•	Examples
>	coin
>	chocolate
>	output!2 	(read output-bang-2)
>	input?x		(read input-query-x)
>	handin-homework
•	Each process has associated with it a set of events that it “understands”
>	this is called it’s alphabet
>	if P is  a process aP is its alphabet
STOP: The Stuck Process
STOPA

•	The process with alphabet A that never does anything when any event of A occurs.
•	I.e., the broken process.
•	Different from (succesfully) terminating process -- but that will come later.
Prefix
Æ 
•	If P is a process and e is an event in its alphabet, then
•	Q = e Æ  P represents the process that does (or “engages in) e and then behaves like process P
•	Verbally, we say “e then P”
•	The operator Æ  associates to the right, so a Æ  b Æ STOP = a Æ  (b Æ STOP) 

Prefix Example
a BROKEN_VEND = {coin, choc}
Example (Better)
More Simple Examples
1. Clock = tick Æ Clock
a Clock = {tick}
2. Clock = tickÆ tockÆ Clock
a Clock = {tick, tock}
Choice
|  - the choice operator
Choice
The choice operator (|) combines two proceses, prefixed by a events.
If a Æ P and  b Æ Q are processes
with a ≠ b, then
a Æ P |  b Æ Q is a process that will do either an “a” event or a “b” event, and then behave like P or Q (resp.)
Verbally, we say “P choose Q”
May be used as an n-ary operator:
a Æ P |  b Æ Q |  c Æ R
Combining operations
More Interesting Example
Diagram of VEND
Note on Representing State
•	In CSP states are represented through process names.
•	A process P with state S  will be represented as PState
•	Not all transitions need be associated with a pair of named states, as illustrated in the previous example.
•	Could introduce names for all of these (eg. “Dispense”) but this would clutter the description.
Another example
Stack< > 	= push.x  Æ Stack<x>
Stack<y> ^ S = push.x  Æ Stack<x> ^ <y> ^ S
 			  | popÆ StackS
Generalized Choice
•	When there are too many events to enumerate all of the choices we can write

(x:B Æ  P(x))

•	This is the process that can do any event, x, in B, and then becomes P(x)

•	Verbally, “x from B then P of x”
Examples
1. Square = x: N Æ  (x2 Æ  Square)
The process that squares a number
P is the function P(x) = x2 Æ Square
2. RUNA = (x:A Æ RUNA)
The process that will accept any event of A
P is the function P(x) = RUN
Interacting Processes
SIMPLE_VEND = 
 		coin Æ choc Æ SIMPLE_VEND
GREEDY_CUST =  
 		  (choc Æ GREEDY_CUST)
 		| (coin Æ choc Æ GREEDY_CUST)

How do we combine these?
The Parallel operator (||) 
SIMPLE_VEND || GREEDY_CUST

"SIMPLE_VEND in parallel with GREEDY_CUST"
Meaning: 
	for every event, SIMPLE_VEND and GREEDY_CUST must both participate in the event.
SIMPLE_VEND || GREEDY_CUST = P
where P =  coin Æ choc Æ P
Problem
SIMPLE_VEND = 
 		coin Æ choc Æ SIMPLE_VEND
STUPID_CUST =  
 		coin Æ STUPID_CUST

SIMPLE_VEND || STUPID_CUST =
	coin Æ STOP
This is called deadlock.
Partial Synchronization
Suppose
 	CLOCK 	= tick Æ tock Æ CLOCK
 	GAME 	= tick Æ tack Æ toe Æ GAME

CLOCK || GAME = ???
Alphabets and ||
aCLOCK = {tick,tock}
aGAME = {tick,tack,toe}
aCLOCK « aGAME = {tick}
CLOCK and GAME must synchronize on {tick}.
P || Q means that P and Q must synchronize on every event in the intersection of their alphabet.
So CLOCK || GAME = P, where
 	P =  tick Æ 
 			(tock Æ tack Æ toe Æ P |
 			 tack Æ tock Æ toe Æ P |
			 tack Æ toe Æ tock Æ P )
Dining Philosophers
Dining Philosophers
PHILi =  thinki Æ upfork(i,i) Æ upfork(i,i+1 mod n) Æ eati Ædownfork(i,i) Æ downfork(i,i+1 mod n)  Æ PHILi

FORKi = 
 	(upfork(i,i) Æ downfork(i,i) Æ FORKi )
 	| 
 	(upfork(i-1 mod n,i) Æ downfork(i-1 mod n,i) Æ FORKi )
Dining Philosophers (cont.)
PHILOSOPHERS = 
PHIL0 || PHIL1 || PHIL2 || PHIL3 || PHIL4

FORKS = 
FORK0 || FORK1 || FORK2 || FORK3 || FORK4

ROOM = PHILOSOPHERS || FORKS
Summary
a P: alphabet of P
the events that P can engage in
e Æ P    : e then P
the process that does event e and then acts like P
a Æ P | b Æ Q : a then P choose b then Q
do a then act like P or do b then act like Q
(x:B Æ P(x))   : x from B then P of x
do one of the events from B
P || Q 	: P parallel Q
run P and Q in parallel, synchronizing on shared events
Special processes: STOP, RUN

Last Slide
Semantics
•	The meaning of a CSP process is the set of traces that it can produce.
•	That is, we only care about the visible event behavior.
•	Example:
>	SIMPLE_VEND = coin Æ choc Æ SIMPLE_VEND
>	has meaning
>	{<>, <coin>, <coin,choc>, <coin,choc,coin>, ...}
•	Note:
>	Each trace is finite.
>	There can be an infinite number of them.
>	The set of traces is “prefix closed”
Operations on Traces
•	Since traces are just sequences then can perform the usual operations on them
concatenation, size, head, tail, etc.
•	One useful operator is the one that counts the number of occurrences of a given event
tr Ø e
•	Example:
<coin,choc,coin,choc,coin>Ø coin = 3
Specifications
•	A specification is a predicate that all traces of a desired process should satisfy.
•	Example
Let   VMS = coin Æ  choc Æ VMS
and
NOLOSS = (tr Ø choc) ≤ (tr Ø coin)
FAIR 	= (tr Ø coin) ≤ (tr Ø choc + 1)

Does the process satisfy the specification?
How would you prove it?
Alternate Description of Recursion
More Alphabets