Concurrent resource calculus

Syntax

Let x, y, z range over variables (Var).

Syntax of networks:

N ::= 0 (Net Empty)

| N | N (Net Par)

| [t] (Net Thread)

| new x : T; N (Net New resource)

Syntax of threads:

t ::= register v = v (Thread Register resource)

| stop (Thread Deadlock)

| D t (Thread Declaration)

Syntax of expressions:

e ::= D e (Exp Declaration)

| v v (Exp Apply function)

| access v (Exp Access resource)

| v (Exp Value)

Syntax of declations:

D ::= let p = e; (Dec Let)

| new x : T; (Dec New resource)

| spawn t; (Dec Spawn thread)

| D D (Dec Sequence)

| (Dec Empty)

Syntax of values (including basic values such as true, false, etc.):

v ::= x (Val Variable)

| k (Val Basic)

| function x p : T { e } (Val Function)

| (v,...,v) (Val Tuple)

Syntax of patterns:

p ::= x : T (Pat Variable)

| (p,...,p) (Pat Tuple)

Syntax of types (including base types such as int, boolean, etc.):

T ::= K (Type Basic)

| function p : T (Type Function)

| (T,...,T) (Type Tuple)

| resource T (Type Resource)

Dynamic semantics

Write fv t for the free variables of t, and bv p for the binding variables of p.

Structural equivalence is the congruence on networks generated by:

(M | N) | O
M | (N | O) ( Par Assoc)

M | N N | M ( Par Comm)

M | 0 M ( Par Unit)

new x : T; N new y : T; N[y / x] ( Alpha) [y not in fv N]

new x : T; (M | N) (new x : T; M) | N ( Extrusion) [x not in fv N]

new x : T; 0 0 ( Garbage)

[let p = D e; t] [D let p = e; t] ( Let Assoc) [bv D disjoint fv t]

Reduction is the precongruence on networks generated by:

[spawn t; u]
[t] | [u] ( Spawn)

[register x = v] | [let p = access x; t]
[register x = v] | [t[v/p]] ( Fetch)

[new x : resource T; t] new x : resource T; [t] ( Extrusion)

[let p = v w; t] [let p = e[v/x,w/q]; t] ( Fun beta) [v = function x q : T {e}]

[let p = v; t] [t[v/p]] ( Let beta)

[stop] 0 ( Garbage)

The reduction relation we are interested in is

given by

;

Static semantics

Note that throughout the static semantics, we view terms up to alpha-conversion, so in particular this type system doesn't worry about identifiers being rebound.

A context is an assignment of types to distinct variables x₁:T₁,...,x_n:T_n, typed as:

(Con Empty)

() : context

T : type

(Con Variable) [x not in ]

(x : T) : context

: context

, : context

(Con Sequence)

, : context

The judgements for when a type is well-formed are:

(Type Basic)

K : type

p :

, T : type

(Type Function)

(function p : T) : type

T₁: type

... T_n : type

(Type Tuple)

(T₁,...,T_n) : type

T : type

(Type Resource)

resource T : type

A value matches a pattern when:

v : T

(Match Variable)

v matches x : T

v₁ matches p₁

... v_n matches p_n

(Match Tuple)

(v₁,...,v_n) matches (p₁,...,p_n)

The binding rules for patterns are given by:

T : type

(Pat Bind Variable) [x not in ]

(x : T) : (x : T)

p₁: ₁

... , ₁,...,_n-1 p_n : _n

(Pat Bind Tuple)

(p₁,...,p_n) : (₁,...,_n)

The type rules for patterns are given by:

(Pat Type Variable)

(x : T) : T

p₁: T₁

... p_n : T_n

(Pat Type Tuple)

(p₁,...,p_n) : (T₁,...,T_n)

The type rules for networks are given by:

(Net Empty)

0 : network

M : network

N : network

(Net Par)

M | N : network

t : thread

(Net Thread)

[t] : network

resource T : type

, x : resource T N : network

(Net Resource) [x not in ]

new x : resource T; N : network

The type rules for threads are:

v : resource T

w : T

(Thread Register)

register v = w : thread

(Thread Deadlock)

stop : thread

D :

, t : thread

(Thread Declaration)

D t : thread

The type rules for expressions are:

D :

, e : T

(Exp Declaration)

D e : T

v : resource T

(Exp Access resource)

access v : T

v : function p : U

w matches p

(Exp Apply function)

v w : U

The type rules for declarations are:

resource T : type

(Dec New resource) [x not in ]

new x : resource T; : (x : resource T)

e : T

p : T

p :

(Dec Let)

(let p = e;) :

t : thread

(Dec Spawn thread)

(spawn t;) : ()

D :

, E :

(Dec Sequence)

D E : ,

(Dec Empty)

() : ()

The type rules for values extend basic type rules

k : K with:

(Val Variable)

, x : T, x : T

(x : function p : T, p) :

, e : T

(Val Function)

(function x p : T {e}) : (function p : T)

v₁ : T₁

... v_n : T_n

(Val Tuple)

(v₁,...,v_n) : (T₁,...,T_n)

Syntax sugar

Anywhere we have restricted the syntax to only require values, we can perform Moggi-style encoding, for example:

access e = let x : resource T = e; access x

register e = f = let x : resource T = e; let y : T = f; register x = y

e f = let x : function T : U = e; let y : T = f; x y

(e₁,...,e_n) ... let x₁ : T₁ = e₁; ... let x_n : T_n = e_n; (x₁,...,x_n)

We can write function p : T { e } for an anonymous non-recursive function,:

function p : T { e } = function $0 p : T { e }

register x p : T { e } = register x = function p : T { e }

We can supply syntax sugar for function declarations:

function x p : T { e } = let x : function p : T = function x p : T { e };

We can use expressions as declarations:

e; = let () = e;

We can use declarations as expressions:

D = D ()

Let the default return type of a function be ().

Write return e; as a synonym for the expression e and return; as a synonym for the expression ();

Write spawn e; as a synonym for the declaration spawn (let () = e; stop);

Write function (T₁,...,T_n) : U as a synonym for the type function ($1 : T₁,..., $n : T_n) : U.

Translating the pi-c into the concurrent resource calculus

We can use a similar coding technique as for the blue-calculus to encode the pi-calculus (although we only allow replicated input, and we translate the synchronous rather than the asynchronous calculus):

[[chan T]] = resource function [[T]]

The translation is then:

[[x!v.P]] = access x v; [[P]]

[[*x?p.P]] = register x p { [[P]] }

[[P | Q]] = spawn [[P]]; [[Q]]

[[(nu x : chan T) P]] = new x : resource function [[T]]; [[P]]

Alternatively, we can translate processes with replicated asynchronous output in the `direct style' with:

[[chan T]] = resource [[T]]

The translation is then:

[[*x!v]] = register x = v

[[x?p.P]] = let p = access x; [[P]]

[[P | Q]] = spawn [[P]]; [[Q]]

[[(nu x : chan T) P]] = new x : resource [[T]]; [[P]]

Subject reduction

Proposition If

N : network and N

* M then

M : network.

N	::=	0	(Net Empty)
	\|	N \| N	(Net Par)
	\|	[t]	(Net Thread)
	\|	new x : T; N	(Net New resource)

t	::=	register v = v	(Thread Register resource)
	\|	stop	(Thread Deadlock)
	\|	D t	(Thread Declaration)

e	::=	D e	(Exp Declaration)
	\|	v v	(Exp Apply function)
	\|	access v	(Exp Access resource)
	\|	v	(Exp Value)

D	::=	let p = e;	(Dec Let)
	\|	new x : T;	(Dec New resource)
	\|	spawn t;	(Dec Spawn thread)
	\|	D D	(Dec Sequence)
	\|		(Dec Empty)

v	::=	x	(Val Variable)
	\|	k	(Val Basic)
	\|	function x p : T { e }	(Val Function)
	\|	(v,...,v)	(Val Tuple)

T	::=	K	(Type Basic)
	\|	function p : T	(Type Function)
	\|	(T,...,T)	(Type Tuple)
	\|	resource T	(Type Resource)

(M \| N) \| O	M \| (N \| O)	( Par Assoc)
M \| N	N \| M	( Par Comm)
M \| 0	M	( Par Unit)
new x : T; N	new y : T; N[y / x]	( Alpha)	[y not in fv N]
new x : T; (M \| N)	(new x : T; M) \| N	( Extrusion)	[x not in fv N]
new x : T; 0	0	( Garbage)
[let p = D e; t]	[D let p = e; t]	( Let Assoc)	[bv D disjoint fv t]

[spawn t; u]	[t] \| [u]	( Spawn)
[register x = v] \| [let p = access x; t]	[register x = v] \| [t[v/p]]	( Fetch)
[new x : resource T; t]	new x : resource T; [t]	( Extrusion)
[let p = v w; t]	[let p = e[v/x,w/q]; t]	( Fun beta)	[v = function x q : T {e}]
[let p = v; t]	[t[v/p]]	( Let beta)
[stop]	0	( Garbage)

	p :
,	T : type
		(Type Function)
	(function p : T) : type

	T₁: type
...	T_n : type
		(Type Tuple)
	(T₁,...,T_n) : type

	v₁ matches p₁
...	v_n matches p_n
		(Match Tuple)
	(v₁,...,v_n) matches (p₁,...,p_n)

	p₁: ₁
... , ₁,...,_n-1	p_n : _n
		(Pat Bind Tuple)
	(p₁,...,p_n) : (₁,...,_n)

	p₁: T₁
...	p_n : T_n
		(Pat Type Tuple)
	(p₁,...,p_n) : (T₁,...,T_n)

	resource T : type
, x : resource T	N : network
		(Net Resource)	[x not in ]
	new x : resource T; N : network

		v : resource T
		w : T
			(Thread Register)
		register v = w : thread

		v : function p : U
		w matches p
			(Exp Apply function)
		v w : U

	(x : function p : T, p) :
,	e : T
		(Val Function)
	(function x p : T {e}) : (function p : T)

	v₁ : T₁
...	v_n : T_n
		(Val Tuple)
	(v₁,...,v_n) : (T₁,...,T_n)

access e	=	let x : resource T = e; access x
register e = f	=	let x : resource T = e; let y : T = f; register x = y
e f	=	let x : function T : U = e; let y : T = f; x y
(e₁,...,e_n)	...	let x₁ : T₁ = e₁; ... let x_n : T_n = e_n; (x₁,...,x_n)

function p : T { e }	=	function $0 p : T { e }
register x p : T { e }	=	register x = function p : T { e }

[[x!v.P]]	=	access x v; [[P]]
[[*x?p.P]]	=	register x p { [[P]] }
[[P \| Q]]	=	spawn [[P]]; [[Q]]
[[(nu x : chan T) P]]	=	new x : resource function [[T]]; [[P]]

[[*x!v]]	=	register x = v
[[x?p.P]]	=	let p = access x; [[P]]
[[P \| Q]]	=	spawn [[P]]; [[Q]]
[[(nu x : chan T) P]]	=	new x : resource [[T]]; [[P]]