# SE547: Lecture 3

Safety

Concurrency

Pi calculus

Derived forms

## Safety

Most implementatations don't code up booleans / pairs / numbers etc. as functions!

They use efficient implementations (native binary, or pointers).

It's now important to avoid bad states such as:

if ( x.M ) { M } else { N }
True ( M )
False ( M )

How can we formally define this problem? How could we solve it?

## Safety

M ::=
x
M N
x.M
True
False
if ( L ) { M } else { N }
FAIL

Note these are now native, not derived forms!

## Safety

Add reduction rules for good states:

if ( True ) { M } else { N } M
if ( False ) { M } else { N } N

if ( x.M ) { M } else { N } FAIL
True ( M ) FAIL
False ( M ) FAIL

Define safety as:

M is safe       whenever       N . M * N implies FAIL N

## Safety

Define a type system with types:

, ::=
bool

Type system is of the form:

x1 : 1 ,..., xn : n M :

meaning:

If each variable xi has type i
then program M has type

As shorthand, write for ( x1 : 1 ,..., xn : n ).

## Safety

What should the types for these be?

Not = x. if ( x ) { False } else { True }
And = x. y. if ( x ) { y } else { False }
Or = x. y. Not ( And (Not x) (Not y) )

## Safety

Type rules for functions:

1. If x : then x : .
2. If , x : M : then x.M : .
3. If M : , and N : , then M N : .

Similar rules for booleans.

No rules for FAIL!

## Safety

Check to make sure we get the right types for these:

Not = x. if ( x ) { False } else { True }
And = x. y. if ( x ) { y } else { False }
Or = x. y. Not ( And (Not x) (Not y) )

## Safety

Types imply safety:

1. If M : then FAIL M
2. If M : and M N then N : .

Plug these two together, and we get:

If M : then M is safe.

Hooray, safety!

## Concurrency

What is concurrency? What makes concurrent programming different from sequential programming?

What are the core components of a concurrent language?

## Concurrency

• Locks.
• Monitors (a.k.a. wait/notify).
• Buffered streams.
• Unbuffered streams.
• ...

Which of these does Java support? Which should we include in a foundational calculus?

## Pi calculus

History:

Models of concurrency (late 1970s-80s): Communicating Sequential Processes (Hoare), Petri Nets (Petri), Calculus of Communicating Systems (Milner)...

Additional features to model dynamic network topologies (late 1980s-90s): Pi-calculus (Milner), Higher order pi-calculus (Sangiorgi), Ambients (Cardelli and Gordon)...

Pi-calculus is a minimal model, but with `enough stuff' to perform interesting computation (e.g. is more powerful than the lambda-calculus).

## Pi calculus

First shot:

P, Q, R ::=
0
out x y; P
in x (y); P
P | Q

What are these?

Note that Pierce uses `overbar' for `out', which is not very HTML friendly!

## Pi calculus

Example programs:

1. out stdout hello; out stdout world; 0

2. in stdin (name); out stdout hello; out stdout name; 0

3. (out c fred; 0) | (in c (name); out d name; 0)

4. (out c fred; out c wilma; 0) | (in c (x); out d x; 0) | (in c (y); out e y; 0)

5. (out c fred; in d x; 0) | (in c (y); out d wilma; 0)

6. (in d x; out c fred; 0) | (in c (y); out d wilma; 0)

7. (out c fred; in d (x); 0) | (out d wilma; in c (y); 0)

What do these programs do?

## Pi calculus

Dynamic semantics is defined in two steps...

Structural congruence P Q is generated by:

1. If P = Q then P Q.
2. P | Q Q | P.
3. (P | Q) | R P | (Q | R).

Dynamic semantics P Q is generated by:

1. (out x y; P) | (in x (z); Q) P | Q[y/z]

2. If P Q then P | R Q | R.
3. If P Q then P Q.

## Pi calculus

Examples:

1. (out c fred; 0) | (in c (name); out d name; 0)

2. (out c fred; out c wilma; 0) | (in c (x); out d x; 0) | (in c (y); out e y; 0)

3. (out c fred; in d x; 0) | (in c (y); out d wilma; 0)

4. (in d x; out c fred; 0) | (in c (y); out d wilma; 0)

5. (out c fred; in d (x); 0) | (out d wilma; in c (y); 0)

## Pi calculus

Missing feature: recursion/looping/infinite behavior.

Minimal solution replication: !P `acts like' P | P | P | ...

Examples:

1. !in x (z); out y z; 0
2. out acquire lock; 0 | !in release (lock); out acquire lock; 0

Replicated input !in accept (socket); P acts a lot like a multithreaded server (Java ServerSocket).

Dynamic semantics just given by:

!P P | !P

## Pi calculus

Last missing feature: create new channels.

Minimal solution channel generation: new (x); P generates a fresh channel for use in P.

Example:

1. new (c); out x c; in c (y1); .. in c (yn); P
2. in x (c); out c z1; .. out c zn; Q

Put these in parallel, and what happens?

New channel generation acts a lot like new object generation / new key generation / new nonce generation / ...

Dynamic semantics just given by:

(new (x); P) | Q new (x); (P | Q)       (as long as x Q)

If P Q then new (x); P new (x); Q.

## Derived forms

Multiple messages:

in x (y1,...,yn); P
= new (c); out x c; in c (y1); .. in c (yn); P

out x (z1,...,zn); Q
= in x (c); out c z1; .. out c zn; Q

Let's double check:

( in x (y1,...,yn); P | out x (z1,...,zn); Q ) *
P[z1/y1,...,zn/yn] | Q

## Derived forms

Oops, it's not quite true, we have to do a bit of garbage collection:

new (c); P =gc P       (when c P)

new (c); in c (x); P =gc 0

new (c); !in c (x); P =gc 0

new (c); out c x; P =gc 0

new (c); !out c x; P =gc 0

P | 0 =gc P

Let's double check:

( in x (y1,...,yn); P | out x (z1,...,zn); Q )
* =gc P[z1/y1,...,zn/yn] | Q

Revisit garbage collection later...

## Derived forms

Booleans:

True(b)
= !in b (x, y); out x (); 0

False(b)
= !in b (x, y); out y (); 0

if (b) { P } else { Q }
= new (t); new (f); ( out b (t, f); 0 | in t (); P | in f (); Q )

Sanity check:

True(b) | if (b) { P } else { Q }
* =gc True(b) | P

## Derived forms

Can also code integers, linked lists, ...

and the lambda-calculus...

and concurrency controls like mutexes, mvars, ivars, buffers, etc.

## Derived forms

Correctness of garbage collection:

If P =gc Q and P P'
then P' =gc Q' and Q Q'

Phew!

## Next week

Homework sheet 3.

Calculi for cryptographic protocols: spi-calculus.