SE547: Lecture 3

Overview

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

Problem definition: add native booleans, plus a bad state.

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

and bad states:

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

Possible inter-thread communication mechanisms:

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.