Safety
Concurrency
Pi calculus
Derived forms
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?
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!
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
Define a type system with types:
, ::=
bool
Type system is of the form:
x_{1} : _{1} ,..., x_{n} : _{n} M :
meaning:
If each variable x_{i} has type _{i}
then program M has type
As shorthand, write for ( x_{1} : _{1} ,..., x_{n} : _{n} ).
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) )
Type rules for functions:
Similar rules for booleans.
No rules for FAIL!
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) )
Types imply safety:
Plug these two together, and we get:
If M : then M is safe.
Hooray, safety!
What is concurrency? What makes concurrent programming different from sequential programming?
What are the core components of a concurrent language?
Possible inter-thread communication mechanisms:
Which of these does Java support? Which should we include in a foundational 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).
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!
Example programs:
out stdout hello; out stdout world; 0
in stdin (name); out stdout hello; out stdout name; 0
(out c fred; 0) | (in c (name); out d name; 0)
(out c fred; out c wilma; 0) | (in c (x); out d x; 0) | (in c (y); out e y; 0)
(out c fred; in d x; 0) | (in c (y); out d wilma; 0)
(in d x; out c fred; 0) | (in c (y); out d wilma; 0)
(out c fred; in d (x); 0) | (out d wilma; in c (y); 0)
What do these programs do?
Dynamic semantics is defined in two steps...
Structural congruence P Q is generated by:
Dynamic semantics P Q is generated by:
(out x y; P) | (in x (z); Q) P | Q[y/z]
Examples:
(out c fred; 0) | (in c (name); out d name; 0)
(out c fred; out c wilma; 0) | (in c (x); out d x; 0) | (in c (y); out e y; 0)
(out c fred; in d x; 0) | (in c (y); out d wilma; 0)
(in d x; out c fred; 0) | (in c (y); out d wilma; 0)
(out c fred; in d (x); 0) | (out d wilma; in c (y); 0)
Missing feature: recursion/looping/infinite behavior.
Minimal solution replication: !P `acts like' P | P | P | ...
Examples:
Replicated input !in accept (socket); P acts a lot like a multithreaded server (Java ServerSocket).
Dynamic semantics just given by:
!P P | !P
Last missing feature: create new channels.
Minimal solution channel generation: new (x); P generates a fresh channel for use in P.
Example:
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.
Multiple messages:
in x (y_{1},...,y_{n}); P
= new (c); out x c; in c (y_{1}); .. in c (y_{n}); P
out x (z_{1},...,z_{n}); Q
= in x (c); out c z_{1}; .. out c z_{n}; Q
Let's double check:
( in x (y_{1},...,y_{n}); P | out x (z_{1},...,z_{n}); Q ) ^{*}
P[z_{1}/y_{1},...,z_{n}/y_{n}] | Q
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 (y_{1},...,y_{n}); P | out x (z_{1},...,z_{n}); Q )
^{*} =_{gc} P[z_{1}/y_{1},...,z_{n}/y_{n}] | Q
Revisit garbage collection later...
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
Can also code integers, linked lists, ...
and the lambda-calculus...
and concurrency controls like mutexes, mvars, ivars, buffers, etc.
Correctness of garbage collection:
If P =_{gc} Q and P P'
then P' =_{gc} Q' and Q Q'
Phew!
Homework sheet 3.
Calculi for cryptographic protocols: spi-calculus.