Previous Up Next
6 Types and privacy

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

Nil
||- y   #  0 ||-

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   #  Py   #  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
  1. Failed privacy: l F and y' is not a prefix of y.

  2. Undeclared label: l dl(D).

  3. 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.

6.2 Type expressions

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) =
 
l l'
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:
  1. If K' = 0, we use cls(BW,K K') = W.
    (In this case, no new message with arguments is introduced.)

  2. 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.)

  3. If dl(K) W , we use cls(BW,K K') = dl( K') W.
    (In this case, all labels in K'' already appear in W.)

  4. 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
Object-Var
x : " X. t A
A |- x : t {a gaa X}
Message
A |- x : [ m : t; r ]
A |- x.m : t

Private-Message
x : " X. (f : t; B) A
A |- x.f : t{a gaa X}
Rules for processes
Null
A |- 0
Send
A |- x.l : (ti i I)      (A |- xi : ti) i I
A |- x.l (xi i I)

Join-Parallel
A |- x.M1    A |- x.M2
A |- x.(M1 & M2)
Parallel
A |- P    A |- Q
A |- P & Q

Class
A |- C :: z(r)BW,V
A + c : " Gen (r, B, A). z(r)BW,V |- P
A |- class c = C in P

Object
    
A |- obj x = C init P in Q

Figure 10: Typing rules for patterns, classes, and refinement clauses 
Rules for patterns
Empty-Pattern
A |- 0 ::
Message-Pattern
(xi : ti A)i I
A |- l(xi i I) :: (l : tii I)

Synchronization
A |- J1 :: B1      A |- J2 :: B2
A |- J1 & J2 :: B1 B2
Alternative
A |- J1 :: B1      A |- J2 :: B2
A |- J1 or J2 :: B1 B2
-2
Rules for classes
Sub
A |- c :: z(r)BW,V
A |- c :: z(r)BW W', V V'
Class-Var
c : " X. z(r)BW,V A
A |- c :: (z(r)BW,V) {a gaa X}

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(xC :: z(r)BW,V
Abstract
dom(B) = L
A |- L :: z(r)B, L

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-Clause
    
A |- K K' |> P :: BW B' W', dl(K) \ dl(K')

Modifier
(A |- Si :: BW BiWi, Vi)i I
A |- | i I Si :: BW (i IB'i)
 
i I
Wi,
 
i I
Vi
 

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 N
(x : sx)
 
x N
(x: " Yx. Bx)
For any string y of names in N, we define the restricted environment:
A y =
 
x N
(x : sx)
 
x y
(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
Chemical-Solution
A = y x   # D    D   Ax
(Ay |- D :: Ax)y x   # D    D
(Ay |- P)y   # P    P
|- D ||- P
Definition
r = B | M
X = Gen (r, B, A) \ ctv(B|W)
A |- self(xD :: 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]  
  1. Chemical reductions preserve chemical typings:
    if |-
    D ||- P and D ||- P D' ||- P' or D ||- P D' ||- P', then |- D' ||- P'.

  2. 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.

6.7 Example of typing

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).


Previous Up Next