The static semantics of our calculus extends those of the core
join calculus for concurrency and
synchronization [12] and of OCaml for
the class-layer [26], respectively.
As regards polymorphism, the type system supports ML parametric polymorphism
and uses row variables to enable some form of
subtyping [32, 26].
It also improves on [12],
so as to match at least the implementation [15]
and avoid the limitation pointed out in [24].
As regards classes, we supplement the typing
of [26] in order to deal with the new operator of
selective refinement and to collect some synchronization information.
6.1 |
A semantics with privacy |
|
In this section, we specify the dynamic errors that are detected by
typing.
For instance, the type system detects message-not-understood
errors: no message can be sent to an object with a label that is
undefined at that object. (Of course, the type system does not ensure
any processing of messages.)
In addition, the type system enforces object encapsulation; this is
stated for a chemical semantics extended with a notion of privacy.
We partition labels l Î L into
private labels f Î F and
public labels m Î M.
Informally, a message on a private label can only be sent
internally, that is, from within either a reaction rule or the init
part of the object.
Conversely, a message on a public label can be sent from any context
that has access to the object name.
However, the origin of a message is a static notion, which is not
preserved in the original chemical semantics given in
Section 2.
For instance, rule Obj in Figure 2,
used to create new
objects, immediately mixes its privileged init process with all
other running processes.
In order to express subject reduction and type safety with privacy, we
thus supplement our chemical semantics with privacy annotations at runtime.
In the state of the refined machine, every running process P and
active definition D is prefixed by a string of object
names y that records the nesting of objects. Precisely, the
string y1... yn x indicates that object x was created
within the definition (or the init process) of objects y1, ...,
yn and thereby can access their private labels.
The chemical state, or solution, is written D ||- P. It
consists of a set D of prefixed definitions y x # D
and a multiset of prefixed processes y # P.
A solution is well-formed when all prefixes agree on object nesting,
i.e., if y x and j x appear in prefixes, then y =
j. As before, we also assume that there is a single definition
for every object in the solution. These properties are preserved by
chemical rewriting.
We use the rules of Figure 6, with the following
side conditions: for Obj, D is a definition, i.e., a class of
the form ori = 1n Mi |> Pi; for Red, [ M |>
P] abbreviates a definition that contains the rule M |> P and
s is a substitution on the names bound in M.
Except for the bookkeeping on static environments, rules Nil,
Par, Join, Obj, Red,
Chemistry, and Chemistry-Obj are the same as in
Section 2.
Note that Red consumes only messages with a prefix that matches
the object definition, and triggers a process in the same environment
as the object definition.
Since messages can be sent from other objects, an intermediate routing step is called for. Such steps are modeled by rules
Public-Comm and Private-Comm that carry messages from
their emitter to their receiver.
This semantics is a refinement of the previous semantics. (Formally,
every reduction in this semantics can be mapped into zero or one
reduction in the previous semantics after removing all prefixes.)
Figure 6: Chemical semantics with privacy
|
Par |
||- y # (P & Q)
º ||- y # P, y # Q |
|
|
|
Join |
||- y # x.(M & M')
º ||- y # x.M, y # x.M' |
|
|
Obj |
||- y # obj x = D init P in Q
º y x # D ||- y x # P, y # Q |
|
|
Public-Comm |
y x # D ||- y' # x. m(u)
¾® y x # D ||- y x # x. m(u) |
|
|
Private-Comm |
y x # D ||- y x y' # x. f(u)
¾® y x # D ||- y x # x. f(u) |
|
|
Red |
y x # [ M |> P] ||- y x # x.(Ms)
¾® y x # [ M |> P] ||- y x # (Ps) |
|
|
Chemistry |
D0 ||- P1 º stackrel ¾® D0 ||- P2 |
|
|
D, D0 ||- P1, P º stackrel ¾® D, D0 ||- P2, P |
|
|
Chemistry-Obj |
||- P º y x # D ||- P' x Ïfn( D) È fn( P ) |
|
|
D ||- P , P º D , y x # D ||- P' , P |
|
|
|
Our privacy policy states that a message sent from object y to
object x on a private label is valid as long as y has been created
by a process of x (cf. rule Private-Comm). We take the
presence of
non-routable messages as our definition of a privacy error.
We also give a formal definitions for other errors, which do not
depend on privacy information.
Definition 1
A solution D ||- P fails
when one of the following holds:
- Free variables:
- the solution contains a free class variable, or
a free object name that is not defined in D.
- Runtime Failure:
-
for some y #
x.l(u) Î P and y'x # D Î D, we have
-
Failed privacy:
l Î F and y' is not a prefix of
y.
- Undeclared label:
l Ïdl(D).
- Arity mismatch:
l(y) appears in a pattern of D with different arities for
y and u.
- Class rewriting failure:
-
for some y # P Î P, the process P is a failure, as defined
in Lemma 1 of Section 3.3.
Figure 7: Syntax for type expressions
|
t |
::= |
q | [ r ] |
|
Object types |
r |
::= |
Ø | h | m : t; r |
|
Row types |
s |
::= |
" X. t |
|
Type schemes |
a |
::= |
q | h |
|
Variables |
t |
::= |
(tii Î I) |
|
Tuple types |
B |
::= |
Ø | l : t; B |
|
Internal types |
|
|
The grammar for type expressions is given in Figure 7.
We build types out of a countable set of type variables, ranged over
by q and a countable set of row variables, ranged over by h.
In the sequel, we write a for variables, regardless of their kinds, and
g for either object types t or row types r. We write X and Y
for sets of type variables. We also abbreviate type schemes " Ø. t
as t.
Object types [r] collect the types of public labels.
For instance the type of the object continuation from
Section 2.1
is [reply:(int)].
Object types may end with a
row variable (open object types), as in
OCaml [26].
For instance, consider a simple rendez-vous object join, with
an internal counter:
obj join = sync1(r1) & sync2(r2) & Count(x) |>
r1.reply() & r2.reply() & join.Count(x+1)
The type of the object join is [sync1 : ([reply
: (); h]); sync2 : ([reply : (); h'])], telling that the
sync labels accept messages composed of any object with a
reply label which in turn accepts empty messages. We assumed that
the label Count is private, hence it does not appear in the type
of join.
Internal types B are used to describe both public and private labels. Such
internal types appear in class types (see below). They are also used to
describe the internal type of self while typechecking class bodies where
sending messages on private names is
allowed (Section 6.4). We observe that B is a
partial function from labels to tuple types; therefore we will address types
of labels by function application.
We use the following standard notations. The operator l : _;
_ associates to the left. We often skip the trailing Ø,
i.e. we abbreviate l1 : t1; ... ln : tn; Ø by
l1 : t1; ... ln : tn and we abstract away from the
order of labels l1,... ln.
For a given set of labels L, we write B | L for the
restriction of B to the labels of L.
We also write B1 Å B2 for the union of B1 and B2, with
the statement that B1 and B2 coincide on their common labels,
and state B1 Í B2 when there is B1' such that B1
Å B1' = B2. We write dom(B) for the set of labels listed in B.
Class types have the form " X. z(r)BW,V.
The set X collects all object type variables and row type variables
appearing in r or B that are polymorphic.
The row type r collects all the constraints on the type [r] of
self, i.e. an object of the class being defined. (These constraints
originate from recursive calls, and also from passing self as a
parameter in messages.)
The internal type B lists the types for
all public and private labels declared in the class.
The consistency between r and B is checked only when objects are
created.
The set W collects the coupled labels of the class,
as explained below.
The set V Í dom(B) contains labels that are declared but
undefined; we call these labels ``virtual labels''; classes with
virtual labels cannot be instantiated.
Given the sophistication of class types, we delay the presentation of
a complete example until section 6.7. However,
if the previous definition of the join object is lifted into
a class definition, then the B component of its type is
sync1 : ([reply : (); h]); sync2 :
([reply : (); h']); Count : (int), there are no
virtual nor coupled labels, and both variables h and h' can be
made polymorphic. Moreover, the internal type for the
objet join should also contain Count : (int).
6.3 |
Polymorphism and inheritance |
|
We now discuss the interaction between synchronization, inheritance,
and polymorphism, in order to define the generalization conditions for
type variables. (The reader not interested in polymorphism may skip
these definitions and their usage in the type system.)
In contrast with functional method types, the types of messages sent
on labels appearing in the same pattern must agree on the
instantiation of any shared type variables.
Consider, for instance, the sbuffer of
Section 2.1:
obj sbuffer = get(r) & put(n,s) |> r.reply(n) & s.reply()
The types of get and put are ([ reply : (q);
h]) and (q, [ reply : (); h']), respectively.
In order to retain type consistency for messages on r.reply
, the
two occurrences of q in get
and put
must be
instantiated to the same type. Hence, variable q cannot be generalized.
Conversely, type variables h and h' appearing in the type
of a single method can be generalized; this is the main source of
polymorphism in the objective join calculus2.
We introduce auxiliary definitions to capture the sharing of messages
and type variables in patterns.
Let K be a pattern. The pattern é Kù is obtained from K by
erasing every message that carries an empty tuple.
The set of coupled labels of K, written cl(K),
collects the
labels whose contents are effectively synchronized in K: we let cl(M) = dl(é Mù) when the pattern é Mù contains at least two
messages, and cl(M) = Ø otherwise.
For more complex patterns of the form K = ori Î I Mi,
we let cl(K) = ÈiÎ I cl(Mi).
Similarly for types, é Bù is obtained from B by removing every
label with an empty tuple type.
We write ftv(_) for the the set of free type variables occurring
in a type, a tuple type, a type scheme, or a typing environment
(defined in Section 6.4).
We let ctv(B) be the subset of type variables in ftv(B) that occur
in at least two labeled entries of B:
ctv |
(B) =
|
|
ftv(B(l)) Ç ftv(B(l'))
|
Assuming that B gathers the types for all messages that can be
sent to an object, the set ctv(B) contains any variable that
cannot be generalized because of synchronization, independently of the
patterns for that object.
When the synchronization patterns are known, however, one can usually
compute a smaller set of such variables.
Since objects and classes can refine other classes, we compute a safe
approximation of non-generalizable variables in contexts where the
patterns for the objects are still unsettled.
To this end, the type of each class carries a set W of coupled labels, such that cl(J) Í W for all patterns
J that may appear in an object of a class of that type.
Eventually, the typing rule for object definition will generalize all
type variables except those that appear in ctv(B | W) ,
where B gathers the types for all messages of the object and W
collects all potentially-coupled labels.3
The main issue is to compute the coupled labels for a refined class, of the
form match C with S end.
Instead of the patterns for C, we only know B and W from its
class type. Since the refinement may leave unchanged some rules of
C, the refined class retains at least the coupled labels of W.
In addition, for every filter K Þ K' |> P of S, some
labels may become coupled as the filter matches a pattern K & K''
in C (for some K'') and produces a rule with
pattern K' & K''.
By definition of cl(_), the new coupled labels are:
cl( K' & K'' ) |
= |
cl(K')
È cl(K'')
È |
ì
í
î |
Ø when é K'ù = 0 or é K''ù = 0 |
dl(é K'ù) È dl(é K''ù) otherwise |
|
|
The three subsets correspond to the labels that appear in distinct pairs
in é K'ù×é K'ù,
é K''ù×é K''ù (with cl(é K''ù) Í W), and
é K'ù×é K''ù, respectively.
We define a safe approximation of the union of cl( K' & K'' ) for
all well-typed K & K'', written cls(BW,K Þ K'). The
definition is by cases:
-
If é K'ù = 0, we use cls(BW,K Þ K') = W.
(In this case, no new message with arguments is introduced.)
- If dl(K) Ç W = Ø and é Kù ¹ 0, we use
cls(BW,K Þ K') = cl(K').
(In this case, é Kù is a single message and é K''ù is empty.)
- If dl(K) Ç W ¹ Ø, we use
cls(BW,K Þ K') = dl(é K'ù) È W.
(In this case, all labels in é K''ù already appear in W.)
- Otherwise (é Kù = 0 and é K'ù ¹ 0),
we use cls(BW,K Þ K') = dl(é K'ù) È dom(é Bù).
Note that cls(BW,K Þ K') only depends on the domain of B and
not on its type assignment.
For example, consider the selective refinement of the class
locked_buff
of Section 4. Informally,
we may assume that the type of
buff is of the form BW where dom(B) = dom(é Bù) = {put,
get, Empty, Some, Full, Check, Init} and W = {put, get, Empty, Some,
Full} (every label of W synchronizes with at least another one). The
refinement involves the two rewriting clauses Init(size)
Þ Init(size) |> z.Free() and 0 Þ Free() |> z.Free().
By item 2 of the definition of cls, we get
cls(BW, Init(size) Þ Init(size)) = cl( Init(size)) = Ø,
which means that this refinement will not introduce any
new synchronization.
By item 1 of the definition of cls, since Free()
is 0, we obtain cls(BW, 0 Þ Free()) = W (label
Free may synchronize with other labels but it cannot exchange values
with them).
These two independent results may be combined together by taking their
union to get an approximation of the type of the whole
refinement.
6.4 |
Type checking processes and classes |
|
Figure 8: Typing judgments
A |- x : t |
the object x has type t in environment A; |
A |- x.l : t |
the label l conveys messages of type t for object x in
environment A; |
A |- P |
the process P is well-typed in environment A; |
A |- K :: B |
the pattern or selection pattern K binds variables well-typed in A
and joins labels in B. |
A |- C :: z(r)BW, V |
the class C is well-typed in environment A, declares the labels
of B, has coupled labels in W,
and has virtual labels V (with V Í dom(B) and W Í
dom(é Bù)). |
A |- S :: BWÞ B'W', V |
|
the refinement clauses S are well-typed in environment A, refine
patterns with labels in B and coupled labels W into patterns
with labels in B', coupled labels in W',
and virtual labels V
(with W' Í dom(é Bù) È dom(é B'ù) and V Í
dom(B)). |
|
The typing judgments are described in Figure 8.
They rely on type environments A that bind class names c to
class type schemes and bind object names x to (external) type
schemes s or to (internal) type schemes " X. B with dom(B)
Í F. In a given environment A, an object x can
have two complementary bindings x : " X. [r] and x : " X.
B. The binding x : " X. [r] represents the typing of public
labels, x : " X. B is the binding of private labels.
Since X is a set of type and row variables, we write
{a ¬ gaa Î X} for replacing
variables in X with object and row types, correspondingly.
We write dom(A) for the set of names bound in A.
We let A + A' be (A \ dom(A')) È A', where A
\ X removes from A all the bindings of names in X
and let A + x : " X. [r], x : " X. B be
A\ {x} È x : " X. [r] È x : " X. B.
The typing rules appear in figures 9 and 10. Generalization in objects and classes relies on
a standard auxiliary definition: Gen(r, B, A) is the set of free
type variables of r or B that are not free in A.
Figure 9: Typing rules for
names, messages, and processes
Rules for names and messages
Rules for processes
|
Send |
A |- x.l : (ti i Î I) (A |- xi : ti) i Î I |
|
| |
|
Class |
A |- C :: z(r)BW,V |
A + c : " Gen (r, B, A). z(r)BW,V |- P |
|
| |
|
Object |
|
|
A |- obj x = C init P in Q |
|
|
|
Figure 10: Typing rules for patterns, classes, and refinement
clauses
Rules for patterns
-2
Rules for classes
Sub |
|
|
A |- c :: z(r)BW È W', V È V' |
|
|
|
Reaction |
A' |- J :: B A + A' |- P dom(A') = fn(J) |
|
|
A |- J |> P :: z(r)Bcl(J),Ø |
|
|
Self-Binding |
A + x : [r], x : (B | F) |- C :: z(r)BW,V |
|
|
A |- self(x) C :: z(r)BW,V |
|
|
|
Disjunction |
A |- C1 :: z(r)B1W1, V1 V1' = V1 \ ( dom(B2) \ V2) |
A |- C2 :: z(r)B2W2, V2 V2' = V2 \ ( dom(B1) \ V1) |
|
|
A |- C1 or C2 :: z(r)(B1 Å B2)W1 È W2,
V1' È V2' |
|
|
Refinement |
A |- C :: z(r)B1W1, V1 |
A |- S :: B1W1 Þ B2W2, V2 dl(S) Ç dom(B1) = Ø |
|
|
A |- match C with S end :: z(r)(B1 Å B2)W1 È W2, V1 È V2 |
|
|
-2
Rules for refinement clauses
Modifier |
(A |- Si :: BWÞ BiWi, Vi)i Î I |
|
|
A |- | |
i Î I Si ::
BWÞ (Åi Î IB'i) |
|
|
|
|
|
Processes.
In rule Class, all type variables can be generalized, regardless of
synchronization. This is safe because classes are templates for object
definitions: the set W in the class type of c is used to restrict
polymorphism, but only at object instantiation.
In rule Object, the class C is first typechecked and yields a
class type z(r)BW,Ø. The shape of this type excludes
virtual labels, thus preventing the instantiation of a
partially-defined object.
The object type is the restriction of labels declared in B to public
ones. The constraint r = B | M checks, for each public label
m of B, that the type given to m in B and in r are the same.
The process Q is typed in an environment extended with the
object x bound to a generalized [r].
The process P is typed as Q, except that P can also use the private
labels of x.
Patterns.
Typing rules for join patterns check that the patterns are
well-formed, collect their typed labels, and check that the
environment agrees with received objects.
Classes.
Rule Reaction checks that join patterns and guarded
processes agree on the typing environment extended with the received
variables.
Rule Self-Binding folds two bindings for self, accounting for
public and private bindings, respectively.
Rules Disjunction and Refinement merge
virtual-label informations, as a disjunct or a parent class may
effectively define a virtual label.
Rule Refinement types match C with S end, out of typings of C and S.
It uses the auxiliary judgment for selection clauses
A |- S :: B1W1 Þ B2W2, V2;
This premise will ensure that labels in the selection
patterns are all defined in B1, hence declared in C.
On the contrary, the premise dl(S) Ç dom(B1) = Ø implies
that names in dl(S) are not already declared in C. In particular,
this ensures that the pattern of every refined reaction rule is linear
(condition (2) in Section 3.3).
Refinement clauses.
Refinement clauses are typed much like reaction rules and
class disjuncts.
Rule Modifier types a series of selection clauses and builds a superset
of the coupled labels after the refinement, as detailed in
Section 6.3.
Rule Modifier also checks that labels in the
pattern Ki' agree with those Ki of the parent class; the set of
virtual labels accounts for labels potentially eliminated by the
clause.
6.5 |
Type checking solutions |
|
We finally extend typing from programs to chemical solutions.
The typing judgment |- ( D ||- P) states that the chemical
solution D ||- P is well-typed. The auxiliary judgments A |-
D :: A' deals with active object definitions.
The typing rules appear in Figure 11.
Rule Chemical-Solution uses an additional notation Ay.
Let N be a set of object names
and A be a typing environment of the form
A = |
|
(x : sx) È |
|
(x: " Yx. Bx)
|
For any string y of names in N,
we define the restricted environment:
A |
y = |
|
(x : sx) È
|
|
(x : " Yx. Bx)
|
Namely, Ay removes from the environment A the private
labels of objects which did not create x. Actually, x
cannot access these labels.
Figure 11: Typing rules for solutions
|
Definition |
r = B | M |
X = Gen (r, B, A) \ ctv(B|W) |
A |- self(x) D :: z(r)BW,Ø |
|
|
A |- D ::
x : " X. [ r ], x : " X. (B | F) |
|
|
|
Rules Chemical-Solution and Definition are similar to
rule Object. The main difference is that, in A |- D ::
A', the typing environment A' is polymorphic. This allows polymorphic
type-checking for solutions.
6.6 |
Subject reduction with privacy |
|
We are now ready to state our main results on types for the chemical
semantics and the class rewriting, respectively. Additional lemmas
and the proofs appear in Appendix B.
Theorem 1 [Subject reduction]
-
Chemical reductions
preserve chemical typings:
if |- D ||- P and D ||- P º D' ||- P' or
D ||- P ¾® D' ||- P', then |- D' ||- P'.
-
Class rewriting
preserve typings:
if A |- P and P |® P' then A |- P'.
In combination, any interleaving of chemical reductions and class
rewritings preserves chemical typing.
Precisely, we can lift class rewriting steps from processes to chemical
solutions ( D ||- P, P |® D ||- P', P' when P |®
P') and we have that,
if D ||- P is well-typed and D ||- P (º stackrel ¾® È
|®)* D' ||- P', then D' ||- P' is also
well-typed.
The next theorem guarantees that chemical typing prevents any
runtime failure and class rewriting failure, as detailed in Definition 1 (Section 6.1):
Theorem 2 [Safety]
Well-typed chemical solutions
do not fail.
While we do not address type inference in this paper, our type system
has been carefully designed to allow type inference. We conjecture
that, given a typing environment A and a process P (or a class
C), it is decidable whether P (or C) is typable in A;
moreover, we conjecture that if C is typable then it has a principal
type.
We infer a type for the class buffer of
Section 3.1:
class buffer = self(z)
get(r) & Some(a) |> r.reply(a) & z.Empty()
or put(a,r) & Empty() |> r.reply() & z.Some(a)
The body of this class definition is of the form self(z) (J1 |> P1 or
J2 |> P2).
First, consider the typing of pattern J1.
By rules Message-Pattern and
Synchronization we have:
A1 |- get(r) & Some(a) :: B1 (1)
where the
type environment A1 and internal type B1 are
A1 = r:q1, a:q2
and
B1 = get : (q1) ; Some : (q2),
reflecting the presence of labels and their arities.
However, pattern J1 is not typed in isolation
but as the pattern of a reaction rule whose guarded process P1
includes r.reply(a).
Rule Reaction requires that P1 be typed
in an environment that subsumes A1.
Moreover, r.reply(a) connects
the types for r and a
(rule Send). Thus, we get:
q1 = [ reply : (q) ; h ] (reflecting that r is an
object with at least a reply label) and q2 = q.
Then, the type variable q is free in the types of both
Some and get which are joined in the same pattern
J1.
Skipping some details,
rule Reaction yields the following
typing of J1 |> P1:
A |- J1 |> P1 :: z(r)B1{get, Some}, Ø (2)
where r is the public type for self, A is
described below,
and B1 is get : ([ reply : (q) ; h ]) ;
Some : (q).
Similarly, the second reaction rule is typed as:
A |- J2 |> P2 :: z(r)B2 Ø, Ø (3)
where
B2 = put : (q',[ reply : () ; h' ]) ;
Empty : ().
Note that the set of coupled labels is empty, since pattern J2
contains only one label of non-zero arity.
Environment A must be the same in both (2) and (3) because these two
judgments are premises of a Disjunction rule:
A |- J1 |> P1 or J2 |> P2 :: z(r)B{get,Some}, Ø (4)
The internal type B is B1 Å B2. Here, this amounts to
B1 È B2 since patterns J1 and J2 have no label in common.
(In the general case where a label is declared in several patterns,
the ``Å'' operator enforces a compatibility check on label
types.)
Hence B = get : ([ reply : (q) ; h ]) ;
Some : (q) ; put : (q',[ reply : () ; h' ]) ;
Empty : ().
Rule Self-Binding
implies that environment A contains two bindings for
the self name z,
namely, z:[r] and z:Br.
The internal type of z, Br is the
restriction of B to private labels, i.e. we get
Br= Some : (q) ; Empty : ().
We can now detail the typing for P2 (which is an hypothesis for (3)).
Listing only pertinent parts of the typing environment A +
A2, we have:
... a:q', z:(Some:(q), ...)
|- P2 (5)
Now, observe that P2 includes the message
z.Some(a), which requires
the types for a and for any message on Some
to be equal. Thus, q = q'.
Hence, the type for class variable buffer finally is:
" {h, h', q}. z(r)B{get,
Some}, Ø (6)
where B is as before (after equating q and q'). That is:
B = get : ([ reply : (q) ; h ]) ;
Some : (q) ; put : (q,[ reply : () ; h' ]) ;
Empty : ().
Observe that, according to Class, all the type variables
(h, h' and q) are generalized. As a consequence
the type for class buffer is as polymorphic as it can be.
Also observe that the public type r is yet unconstrained.
Nevertheless, polymorphism will be restricted and
r will be made precise while
creating objects from class buffer (rule Object).