Nicolas Tabareau
email: nicolas.tabareau@inria.fr

Éric Tanter
email: etanter@dcc.uchile.cl

Chemical Foundations of Distributed Aspects

published or not. The documents may come

Introduction

Distributed applications are complex to develop because of a plethora of issues related to synchronization, distribution, and mobility of code and data across the network. It has been advocated that traditional programming languages do not support the separation of distribution concerns from standard functional concerns in a satisfactory way. For instance, data replication, transactions, security, and fault tolerance often crosscut the business code of a distributed application. Aspect-Oriented Programming (AOP) promotes better separation of concerns in software systems by introducing aspects for the modular implementation of crosscutting concerns [START_REF] Kiczales | Aspect oriented programming[END_REF][START_REF] Elrad | Aspectoriented programming[END_REF]. Indeed, the pointcut/advice mechanism of AOP provides the facility to intercept the flow of control when a program reaches certain execution points (called join points) and perform new computation (called advice). The join points of interest are denoted by a predicate called a pointcut.

AOP is frequently used in distributed component infrastructures such as Enterprise Java Beans, appli-cation frameworks (such as Spring2 ) and application servers (such as JBoss3 ). Recently, there is a growing interest in the use of AOP for Cloud computing [START_REF] Mdhaffar | AOP4CSM: An aspect-oriented programming approach for cloud service monitoring[END_REF][START_REF] Chen | COCA: Computation offload to clouds using AOP[END_REF], including practical infrastructures such as Cloud-Stack 4 . In all these cases however, AOP systems do not support the remote definition or application of aspects. Rather, non-distributed aspects are used to manipulate distributed infrastructures [START_REF] Soares | Implementing distribution and persistence aspects with As-pectJ[END_REF].

To address these limitations, distributed AOP has been the focus of several practical developments: JAC [START_REF] Pawlak | JAC: an aspect-oriented distributed dynamic framework[END_REF], DJcutter [START_REF] Nishizawa | Remote pointcut -a language construct for distributed AOP[END_REF], QuO's ASL [START_REF] Gary Duzan | Building adaptive distributed applications with middleware and aspects[END_REF], ReflexD [START_REF] Tanter | A versatile kernel for distributed AOP[END_REF], AWED [START_REF] Daniel | Explicitly distributed AOP using AWED[END_REF][START_REF] Daniel | Modularization of distributed web services using AWED[END_REF], Lasagne [START_REF] Truyen | Run-time and atomic weaving of distributed aspects[END_REF], as well as a higher-order procedural language with distribution and aspects [START_REF] Tanter | Scoping strategies for distributed aspects[END_REF]. These languages introduce new concepts for distributed AOP such as remote pointcut (advice triggered by remote join points), distributed advice (advice executed on a remote host), migration of aspects, asynchronous and synchronous aspects, distributed control flow, etc. Most of these systems are based on Java and RMI in order to promote the role of AOP on commonly-used large-scale distributed applications. But the temptation of using a rich language to develop interesting applications has the drawback that defining the formal semantics of distributed aspects is almost impossible. While the formal foundations of aspects have been laid out in the sequential setting [START_REF] Wand | A semantics for advice and dynamic join points in aspectoriented programming[END_REF][START_REF] De Fraine | Essential AOP: the A calculus[END_REF], to date, no theory of distributed aspects has been developed. 5This paper develops the formal foundations of distributed AOP using a chemical calculus, essentially a variant of the distributed join calculus [START_REF] Fournet | The reflexive chemical abstract machine and the join-calculus[END_REF]. The join calculus is a functional name-passing calculus based on the chemical abstract machine and implemented in several mainstream languages like OCaml [START_REF] Fournet | JoCaml: A language for concurrent distributed and mobile programming[END_REF], C# [START_REF] Benton | Modern concurrency abstractions for C ♯[END_REF] and Scala [START_REF] Haller | Implementing joins using extensible pattern matching[END_REF]. Chemical execution engines are also being developed for Cloud computing [START_REF] Pazat | Towards a chemistry-inspired middleware to program the internet of services[END_REF][START_REF] Obrovac | Experimental evaluation of a hierarchical chemical computing platform[END_REF]. Due to its chemical nature, the join calculus is well-suited to describe parallel computation. The explicit treatment of localities and migration in the distributed join calculus makes it possible to express distribution-related concerns directly.

In the join calculus, communication channels are created together with a set of reaction rules that specify, once and for all, how messages sent on these channels are synchronized and processed. The crosscutting phenomena manifest in programs written in this style, just as they do in other languages. The reason is that reactions in the join calculus are scoped: it is not possible to define a reaction that consumes messages on external channels. Therefore, extending a cache process with replication implies modifying the cache definition itself. Similarly, establishing alternative migration policies based on the availability of locations requires intrusively modifying components.

The Aspect Join Calculus developed in this paper addresses crosscutting issues in the join calculus by introducing the possibility to define aspects that can react to chemical reactions. In doing so, it provides a formal foundation that can be used to understand and describe the semantics of existing and future distributed aspect languages. We also use it to describe interesting features that have not (yet) been implemented in practical distributed AOP systems.

Section 2 presents the distributed objective join calculus, which serves as the basis for the aspect join calculus. The syntax and semantics of the aspect join calculus are described in Section 3. In order to address the implementation of the aspect join calculus, Section 4 describes a translation from the aspect join calculus to the core join calculus; the correctness of this translation is proven by a bisimilarity argument. Section 5 discusses several design options. Then, Section 6 describes Aspect JoCaml, a prototype implementation of the aspect join calculus on top of JoCaml based on the translation described in Section 4. Finally, Section 7 discusses related work and Section 8 concludes.

The distributed objective join calculus

We start by presenting a distributed and object-oriented version of the join calculus. 6 This calculus, which we call the distributed objective join calculus, is an original, slightly adapted combination of an object-oriented version of the join calculus [START_REF] Fournet | Inheritance in the join calculus[END_REF] and an explicit notion of location to account explicitly for distribution [START_REF] Fournet | The join calculus: a language for distributed mobile programming[END_REF].

Message passing and internal states

Before going into the details of the distributed objective join calculus, we begin with the example of the object buffer presented in [START_REF] Fournet | Inheritance in the join calculus[END_REF]. The basic operation of the join calculus is asynchronous message passing over channels. In the objective join calculus, channels are associated with an object and called labels. Accordingly, the definition of an object describes how messages received on some labels can trigger processes. For instance, the term obj r = reply(n) ▷ out.print (n) defines an object that reacts to messages on its own label reply by sending a message with label print and content n to an object named out that prints on the terminal. In the definition of an object, the '▷' symbol defines a reaction rule that consumes the messages on its left hand side and produces the messages on its right hand side.

Note that labels may also be used to represent the internal state of an object. Consider for instance the definition of a one-place buffer object: A buffer can either be empty or contain one element. The buffer state is encoded as a message pending on empty or some, respectively. A buffer object is created empty, by sending a first message b.empty in the in clause. Note that to keep the buffer object consistent, there should be a single message pending on either empty or some. This remains true as long as external processes cannot send messages on these internal labels directly. This can be enforced by a privacy discipline, as described in [START_REF] Fournet | Inheritance in the join calculus[END_REF].

Syntax

The grammar of the distributed objective join calculus is given in Figure 1; it has syntactic categories for processes P , definitions D, patterns M , and named definitions D. We use three disjoint countable sets of identifiers for object names x, y, z ∈ O, labels l ∈ L and host names H ∈ H. Tuples are written (v i ) i∈I or simply v. We use v to refer indifferently to object or host names, i.e. v ∈ O ⋃ H.

To introduce all the syntactic constructs of the distributed objective join calculus, it is helpful to start by considering that a program is described as a configuration C, called a chemical solution, which is a set of machines running in parallel: Fig. 1 Syntax of the distributed objective join calculus (a combination of simplified versions of the distributed join calculus [START_REF] Fournet | The join calculus: a language for distributed mobile programming[END_REF] and the objective join calculus [START_REF] Fournet | Inheritance in the join calculus[END_REF])

C = D 1 ⊩ ϕ1 P 1 ∥ ⋯ ∥ D n ⊩ ϕn
A machine D ⊩ ϕ P consists of a set of named definitions D and of a multiset of processes P running in parallel at a given location ϕ.

Locations. A location ϕ (we also sometimes use metavariable ψ to denote locations) is a unique sequence of host names H, i.e. ϕ = H 1 ⋯H n . We assume that the rightmost host H n defines the location ϕ uniquely. Intuitively, a root location H can be thought of as an IP address on a network and a machine at host/root location H can be thought of as a physical machine at this address. Then, a machine at sub-location HH ′ can be thought of as a system process H ′ executing on a physical machine (whose location is H). This includes for example the treatment of several threads, or of multiple virtual machines executing on the same physical machine. For instance, a concrete representation of locations (using as a separator between Hs) could be 1.2.3.4:56 vm 1 t 2 to denote thread t 2 of virtual machine vm 1 running at IP address 1.2.3.4:56.

Named definitions. Named definitions D are a disjunction of object definitions x.D, where x is an object name, and D is a disjunction of reaction rules. Object definitions in D represent "active" objects ready to react to message sends. A reaction rule M ▷ P associates a pattern M with a guarded process P . Every message pattern l(v) in M binds the object names and/or hosts v with scope P . Note that in the join calculus, it is required that every pattern M guarding a reaction rule be linear, that is, labels and object names appear at

fn(0) = ∅ fn(x.M ) = {x} ∪ fn(M ) fn(obj x = D in P ) = (fn(D) ∪ fn(P )) ∖ {x} fn(go(H); P ) = {H} ∪ fn(P ) fn(H[P ]) = fn(P ) ∖ H fn(P & Q) = fn(P ) ∪ fn(Q) fn(M ▷ P ) = fn(P ) ∖ fn(M ) fn(D or D ′ ) = fn(D) ∪ fn(D ′ ) fn(l(v)) = {v i i ∈ I} fn(M & M ′ ) = fn(M ) ∪ fn(M ′ ) fn(x.D) = {x} ∪ fn(D) fn(H[D∶ P ]) = (fn(D) ∪ fn(P )) ∖ H fn(D or D ′ ) = fn(D) ∪ fn(D ′ ) fn(⊺) = ∅ Fig. 2 Definition of free names fn(⋅)
most once in M . Also, each object is associated with exactly one named definition. Named definitions also include sub-location definitions H[D∶ P ], hosting the named definitions D and process P at host H.

Processes. Processes include the null process 0, message sending x.M , and object definition obj x = D in P , which corresponds to the creation of a new object (not yet ready to react). An object definition binds the name x to the definitions of D. The scope of x is every guarded process in D (here x means "self") and the process P . Objects are taken modulo renaming of bound names (or α-conversion). H[P ] is the process that starts a fresh new location with process P . Note that H[P ] acts as a binder for creating a new host. A migration request is described by go(H ′ ); P . It is subjective in that it provokes the migration of the current host H to any location of the form ψH ′ (which must be unique by construction) with continuation process P .

The definitions of free names (noted fn(.)) for processes, definitions, patterns and named definitions are given in Figure 2.

Semantics

The operational semantics of the distributed objective join calculus is given as a reflexive chemical abstract machine [START_REF] Fournet | The reflexive chemical abstract machine and the join-calculus[END_REF]. Each rewrite rule applies to a configuration C. A chemical reduction is the composite of two kinds of rules: (i) structural rules ≡ that deal with (reversible) syntactical rearrangements, (ii) reduction rules → that deal with (irreversible) basic computational steps. The rules for the distributed objective join calculus are given in Figure 3. In chemical semantics, each rule is local in the sense that it mentions only definitions and messages involved in the reaction; but it can be applied to a wider chemical solution that contains those definitions and messages. By convention, the rest of the solution, which remains unchanged, is implicit.

Rules Or and Empty make composition of named definitions associative and commutative, with unit ⊺. Rules Par and Nil do the same for parallel composition of processes. Rule Join gathers messages that are meant to be matched by a reaction rule. Rule Obj-Def describes the introduction of an object (up-to αrenaming, we can consider that any definition of an object x appears only once in a configuration).

The reduction rule Red specifies how a message x.M ′ interacts with a reaction rule x.[M ▷ P ]. The notation x.[M ▷ P ] means that the unique named definition x.D in the solution contains reaction rule M ▷P . The message x.M ′ reacts when there exists a substitution σ with domain fn(M ) such that M σ = M ′ . In that case, x.M σ is consumed and replaced by a copy of the substituted guarded process P σ. Substitution is standard, replacing free occurrences (as defined by fn) of the variable to substitute.

Distribution. Rule Message-Comm states that a message emitted in a given location ϕ on an object name x that is remotely defined can be forwarded to the machine at location ψ that holds the definition of x. Later on, this message can be used within ψ to assemble a pattern of messages and to consume it locally, using a local Red step. Note that in contrast to some models of distributed systems [START_REF] Riely | A typed language for distributed mobile processes[END_REF], the routing of messages is not explicitly described by the calculus.

The handling of locations and migration is directly based on the join calculus mechanisms presented by Fournet and Gonthier [START_REF] Fournet | The join calculus: a language for distributed mobile programming[END_REF]. Rule Loc-Def describes the introduction of a sub-location (up-to α-conversion, we can consider that any host appears only once in a configuration). Rule Sub-Loc introduces a new machine at sub-location ϕH of ϕ with D as initial definitions and P as initial process. When read from right-to-left, the rule can be seen as a serialization process, and conversely as a deserialization process. The side condition "H frozen" means that there is no other machine of the form ⊩ ϕHψ in the configuration (i.e. all sub-locations of H have already been "serialized"). The notation {D} and {P } states that there are no extra definitions or processes at location ϕH. Sub-Loc rule is best understood in tandem with the Move rule, which gives the semantics of migration. Intuitively, the Move rule dispatches a pack of definitions and processes to a new location, and the Sub-Loc rule allows unpacking.

More precisely, in the Move rule a sub-location ϕH of ϕ is about to move to a sub-location ψH ′ of ψ. On the right hand side, the machine ⊩ ϕ is fully discharged of the location H. Note that P can be executed at any 3 Chemical semantics of the distributed objective join calculus (adapted from [START_REF] Fournet | The join calculus: a language for distributed mobile programming[END_REF][START_REF] Fournet | Inheritance in the join calculus[END_REF])

Structural rules

Or

(D or D ′ ) ⊩ ϕ ≡ D, D ′ ⊩ ϕ Empty x.⊺ ⊩ ϕ ≡ ⊺ ⊩ ϕ ≡ ⊩ ϕ Par ⊩ ϕ P & Q ≡ ⊩ ϕ P, Q Nil ⊩ ϕ 0 ≡ ⊩ ϕ Join ⊩ ϕ x.(M & M ′ ) ≡ ⊩ ϕ x.M & x.M ′ Sub-Loc H[D∶ P ] ⊩ ϕ ≡ {D} ⊩ ϕH {P } (H frozen) Obj-Def ⊩ ϕ obj x = D in P ≡ x.D ⊩ ϕ P (x fresh) Loc-Def ⊩ ϕ H[P ] ≡ H[⊺∶ P ] ⊩ ϕ (H fresh) Reduction rules Red x.[M ▷ P ] ⊩ ϕ x.M σ → x.[M ▷ P ] ⊩ ϕ P σ Message-Comm ⊩ ϕ x.M ∥ x.D ⊩ ψ → ⊩ ϕ ∥ x.D ⊩ ψ x.M Move H[D∶ (P & go(H ′ ); Q)] ⊩ ϕ ∥ ⊩ ψH ′ → ⊩ ϕ ∥ H[D∶ (P & Q)] ⊩ ψH ′ Fig.
time, whereas Q can only be executed after the migration. Rule Move says that migration on the network is based on sub-locations but not objects nor processes. When a migration order is executed, the continuation process moves with all the definitions and processes present at the same sub-location. Nevertheless, we can encode object (or process) migration by defining a fresh sub-location and uniquely attaching an object/process to it. Then the migration of the sub-location will be equivalent to the migration of the object/process.

Names and configuration binding. In the distributed join calculus, every name is defined in at most one local solution; rule Message-Comm hence applies at most once for every message, delivering the message to a unique location [START_REF] Fournet | The join calculus: a language for distributed mobile programming[END_REF]. Similarly, the freshness condition of rule Loc-Def preserves the assumption that the rightmost host H n uniquely defines the location ϕ.

In the semantics, the rule Obj-Def (resp. Loc-Def) introduces a fresh variable x (resp. H) that is free in the definitions and processes of the whole configuration. But the fact that x (resp. H) appears on the left hand side of the machine definition means that the free variable is bound in the configuration. More precisely, for a configuration C = (D i ⊩ ϕi P i ) i , we say that x is bound in C, noted C ⊢ x, when there exists i such that x.D appears in D i . Similarly, we say that H is bound in C, noted C ⊢ H, when there exists i such that H[D∶ P] appears in D i . This notion of configuration binding will be used in the definition of the semantics of pointcuts in Section 3.

A companion example

In the rest of the paper, we will use a cache replication example. To implement the running example, we assume a dictionary library dict with three labels:

create(x) returns an empty dictionary on x.getDict; update(d, k, v, x) updates the dictionary d with value v on key k, returning the dictionary on x.getDict; lookup(d, k, r) returns the value associated with k in d on r.reply

We also assume the existence of strings, which will be used for keys of the dictionary, written "name".

The cache we consider is similar to the buffer described in Section 2.1 but with a permanent state containing a dictionary and a getDict label to receive the (possibly updated) dictionary from the dict library: For the moment, we just consider a single cache and a configuration containing a single machine as follows:

obj c = put(k, v) & state(d) ▷ dict.
c.[put(k, v) & state(d) ▷ dict.update(d, k, v, c), get(k, r) & state(d) ▷ dict.lookup(d, k, r) & c.state(d), getDict(d) ▷ c.state(d)], r.[reply(n) ▷ out.print(n)] ⊩ H c.state(d 0 ) & c.get("foo", r) & c.put("foo", 5)
At this point, two reactions can be performed, involving c.state(d 0 ) and either c.get("foo", r) or c.put("foo", 5). Suppose that put is (non-deterministically) chosen. The configuration amounts to:

Rules ⊩ H dict.update(d 0 , "foo", 5, c) & c.get("foo", r)

where Rules represents the named definitions introduced so far. c.get("foo", r) can no longer react, because there are no c.state messages in the solution anymore. dict passes the updated dictionary d 1 , which is passed in the message c.state using reaction on label c.getDict.

Rules ⊩ H c.state(d 1 ) & c.get("foo", r) Now, c.get("foo", r) can react with the new message c.state(d 1 ), yielding:

Rules ⊩ H c.state(d 1 ) & r.reply [START_REF] Daniel | Modularization of distributed web services using AWED[END_REF] Finally, 5 is printed out (consuming the r.reply message) resulting in the terminal configuration:

Rules ⊩ H c.state(d 1 )

Bootstrapping distributed communication

Since the join calculus is lexically scoped, programs executed on different machines do not initially share any port name; therefore, they would normally not be able to interact with one another. To bootstrap a distributed computation, it is necessary to exchange a few names, using a name server. The name server NS offers a service to associate a name with a constant string-NS.register("x", x)-and to look up a name based on a string -NS.lookup("x", r), where the value is sent on r.reply.

For instance, in the above example we (magically) assumed that dict was in scope. Recall that we wrote:

obj c = . . . in dict.create(c)
The actual bootstrapping through the name server would occur as follows. First, the dictionary object should be created and registered:

obj dict = . . . in NS.register("dict", dict)
Then, the client program can query the name server to obtain the dictionary, and then use it:

obj client = reply(d) ▷ obj c = . . . in d.create(c) in NS.lookup("dict", client)
Finally, note that in order to make the definition of processes more readable, we present some part of processes in a functional programming style that can either be encoded in the join calculus, or can already be present in the language (e.g. in JoCaml). In particular, we will use the notions of lists, strings, integers, equality testing, conditionals (if-then-else), and a particular variable lhost that represents the current location on which a process is executing.

The aspect join calculus

We now describe the aspect join calculus, an extension of the distributed objective join calculus with as- pects. Support for crosscutting in a programming language is characterized by its join point model [START_REF] Masuhara | A compilation and optimization model for aspectoriented programs[END_REF]. A join point model includes the description of the points at which aspects can potentially intervene, called join points, the means of specifying the join points of interest, here called pointcuts, and the means of effecting at join points, called advices. We first describe each of these elements in turn, from a syntactic and informal point of view, before giving the formal semantics of aspect weaving in the aspect join calculus. The syntax of aspects is presented in Figure 4.

Defining the join point model

Join points. Dynamic join points reflect the steps in the execution of a program. For instance, in AspectJ [START_REF] Kiczales | An overview of AspectJ[END_REF] join points are method invocations, field accesses, etc. In functional aspect-oriented programming languages, join points are typically function applications [START_REF] Dutchyn | Semantics and scoping of aspects in higher-order languages[END_REF][START_REF] Walker | A theory of aspects[END_REF].

The central computational step of any chemical language is the application of a reaction rule, here specified by Rule Red. Therefore, a reaction join point jp in the aspect join calculus is a pair (ϕ, x.M ), where ϕ is the location at which the reduction occurs, and x.M is the matched synchronization pattern of the reduction.

In a pointcut definition, it is often of interest to know not only the current reaction join point but also the causality tree of reaction join points that gave rise to it. 7 Therefore, we introduce a general notion of join point (with causality) J to denote a tree of reaction join points. The syntax of join points is given in Figure 5: a join point is either an empty tree, noted •, or a join point with causality, noted jp, J, where jp is a reaction join point and J is a list of join points.

We note J ′ ≺ J to indicate that J ′ is a subtree of J, i.e. J ′ is a sub join point of J. Formally, J ′ ≺ J is inductively defined as by the following two rules:

≺ now ∶ ∀i, J = J i ⇒ J ≺ (jp, [J 1 , . . . , J n ]) ≺ next ∶ ∀i, J ≺ J i ⇒ J ≺ (jp, [J 1 , . . . , J n ])
For instance, consider messages c.state(d) with history J 1 and c.get("foo", r) with history J 2 . The join point of the corresponding reaction of both messages on host ϕ is:

((ϕ, c.state(d) & c.get("foo", r)), [J 1 , J 2 ])
We give an example of reduction with causality in Section 3.3.

Pointcuts. The aspect join calculus includes two basic pointcut designators, i.e. functions that produce pointcuts: contains for reaction rules selection, and host for host selection. The pointcut contains(x.M ) selects any reaction rule that contains the pattern x.M as left hand part, where the variables occurring in contains(x.M ) are bound to the values involved in the reaction join point. In the same way, the pointcut host(h) binds h to the location of the reaction join point. A pointcut can also be constructed by negations and conjunctions of other pointcuts. Finally, the pointcut causedBy(P c) says that P c matches for a subtree of the current join point. The semantics of pointcuts is formally described in Section 3.3.

The free variables of a pointcut (as defined in Figure 6) are bound to the values of the matched join points. In this way, a pointcut acts as a binder of the free variables occurring in the corresponding advice, as standard in aspect-oriented languages. Consider for instance the pointcut contains(x.M ). If x is free, the pointcut will match any reaction whose pattern includes M , irrespective of the involved object, and that object will be bound to the identifier x in the advice body. If x is not a free name, the pointcut will match any reaction on the object denoted by x, whose pattern includes M . Note that similarly to synchronization patterns in the join calculus, we require the variables occurring in a pointcut to be linear. This ensures that unions of substitutions used in the definition of a semantics of pointcuts (Figure 7) are always well defined.

In the following, when the variable to be matched is not interesting (in the sense that it is not used in the advice), we use the * notation. For instance, the pointcut contains( * .put(k, v)) matches all reactions containing put(k, v) on any object, without binding the name of the object.

Advices. An advice body Ad is a process to be executed when the associated pointcut matches a join point. This process may contain the special keyword proceed. During the reduction, proceed is substituted by the resulting process P of the matched reaction. Note that contrarily to the common practice in AOP, it is not possible to modify the process P by altering the substitution that is applied to it. This is because the notion of arguments of a reaction is not easy to set up in the join calculus as it should be induced by the substitution and not by the order in which they appear in the reaction join point. Nevertheless, it is still possible to skip using proceed and trigger another process instead. Free names of an advice are defined in Figure 6.

Aspects. To introduce aspects in the calculus, we extend the syntax of definitions D with pointcut/advice pairs (Figure 4). This means that an object can have both reaction rules and possibly many pointcut/advice pairs. This modeling follows symmetric approaches to pointcut and advice, like CaesarJ [START_REF] Aracic | An overview of CaesarJ[END_REF] and EScala [START_REF] Gasiunas | EScala: modular event-driven object interactions in Scala[END_REF],

where any object has the potential to behave as an aspect. Free names of an aspect are defined in Figure 6; the only interesting case is the last one, which specifies that the free variables of a pointcut act as binders in the advice.

The following example defines an object replicate that, when sent a deploy message with a given cache replicate object c and a host H ′ , defines a fresh sublocation ϕH, migrates it to host H ′ , and creates a new replication aspect:

⊩ ϕ obj replicate = deploy(c, H ′ ) ▷ H[go(H ′ ); obj rep = ⟨contains( * .put(k, v)) ∧ host(h), if (h ≠ H ′ ) then c.put(k, v) & proceed else proceed⟩] in NS.register("replicate", replicate)
The advice body replicates on c every put message received by a cache object and makes an explicit use of the keyword proceed in order to make sure that the intercepted reaction does occur. The condition (h ≠ H ′ ) in the advice is used to avoid replication to apply to reactions that happen on a sub-location of the location where the aspect is deployed. Indeed, the aspect must not replicate local modifications of the cache.

Customized reactions

With a single notion of reaction, we are forced to consider a single weaving semantics that applies uniformly to all reactions. In practice, however, exposing each and every join point to aspects can be a source of encapsulation breach as well as a threat to modular reasoning. This issue has raised considerable debate in the AOP community [START_REF] Kiczales | Aspect-oriented programming and modular reasoning[END_REF][START_REF] Steimann | The paradoxical success of aspectoriented programming[END_REF], and several proposal have been made to restrict the freedom enjoyed by aspects (e.g. [START_REF] Bodden | Join point interfaces for safe and flexible decoupling of aspects[END_REF][START_REF] Bruno | EffectiveAdvice: discplined advice with explicit effects[END_REF][START_REF] Bruno | MRI: Modular reasoning about interference in incremental programming[END_REF][START_REF] Steimann | Types and modularity for implicit invocation with implicit announcement[END_REF][START_REF] Sullivan | Modular aspect-oriented design with XPIs[END_REF]). We now present three variants of weaving semantics.

First of all, it is important for programmers to be able to declare certain reactions as opaque, in the sense that they are internal and cannot be woven. This is similar to declaring a method final in Java in order to prevent further overriding.

For the many cases in which the semantics of asynchronous event handling is sufficient, it is desirable to be able to specify that aspects can only observe a given reaction, meaning that advices are not given the ability to use proceed at all, and are all executed in parallel. This gives programmers the guarantee that the original reaction happens unmodified, just once, and that aspects can only "add" to the resulting computation.

The full aspect join calculus therefore includes three possible weaving semantics, which can be specified perreaction: opaque (▸), observable ( ), and asynchronously advisable (▷). The default semantics is asynchronous advisable.

Per-reaction weaving in practice. To illustrate the benefits of different weaving semantics, we refine the definition of a cache object to ensure strong properties with respect to aspect interference as follows:

obj c = put(k, v) & state(d) dict.update(d, k, v, c) or get(k, r) & state(d) dict.lookup(d, k, r) & c.state(d) or getDict(d) ▸ c.state(d) in dict.create(c)
Reactions on both put and get are declared observable, in order to ensure that aspects cannot prevent them from occurring normally. In particular, the replication aspect is not allowed to call proceed, which is anyway implicitly called in parallel with the advice:

(ϕ, x ′ .M ′ ), J ⊩ contains(x.M ) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ τ minimal substitution s.t. xτ = x ′ and M τ ⊆ M ′ otherwise (ϕ, x ′ .M ′ ), J ⊩ host(h) = {h ↦ ϕ} J ⊩ P c ∧ P c ′ = J ⊩ P c ∪ J ⊩ P c ′ J ⊩ ¬P c = { } when J ⊩ P c = otherwise J ⊩ causedBy(P c) = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ J ′ ⊩ P c for some J ′ s.t. J ′ ≺ J and J ′ ⊩ P c ≠ otherwise Fig. 7 Semantics of pointcuts ⊩ ϕ obj replicate = deploy(c, H ′ ) ▷ H[go(H ′ ); obj rep = ⟨contains( * .put(k, v)) ∧ host(h), if (h ≠ H ′ ) then c.put(k, v)⟩]
in NS.register("replicate", replicate)

Additionally, reactions on the internal getDict label of the cache object are now opaque, hence enforce strong encapsulation: no aspect can observe such reactions.

Semantics

Semantics of pointcuts. The matching relation, noted jp ⊩ P c, returns either a substitution τ from free names of P c to names or values of jp, or a special value meaning that the pointcut does not match. That is, we enriched the notion of boolean values to a richer structure (here substitutions), as commonly done in aspectoriented programming languages in particular. We note { } the empty substitution, and consider it as the canonical true value. We note ∪ the join operation on disjoint substitutions that returns as soon as one of the substitution is . Note that conjunction pointcuts are defined only on substitutions that are disjoint, but because variables occur linearly in pointcuts, we have the guarantee that this is always the case. The matching relation is defined by induction on the structure of the pointcut in Figure 7.

In the rule for the contains(x.M ) pointcut, the inclusion of patterns M τ ⊆ M ′ is defined as the inclusion of the induced multiset of messages. For instance, suppose that the cache replication aspect defined previously has been deployed and that the emitted join point is:

(ϕ, x.put("bar", 5) & state(d)) , J
Then, the pointcut of the aspect: matches, with partial bijection:

contains( * .put(k, v)) ∧ host(h) {0} J = 0 {x.M } J = x.{M } J {obj x = D in P } J = obj x = D in{P } J {go(H); P } J = go(H); {P } J {H[P ]} J = H[{P } J ] {P & P ′ } J = {P } J & {P ′ } J {l(v)} J = l J (v) {M & M ′ } J = {M } J & {M ′ } J
τ = {k ↦ "bar", v ↦ 5, h ↦ ϕ}
Note that the variable d is not mapped by τ because it is not captured by the pointcut.

The rule for the host(h) pointcut always returns the substitution that associates h with the location of the matched pattern. The semantics of the negation and conjunction is an extension of the traditional boolean semantics to truth values that are substitutions.

The rule for the causedBy(P c) pointcut returns the substitution that matches P c for any sub join point J ′ of J, that is any join point in the causal history of J. It returns when no join point matches P c.

Remembering causality in processes. In order to conserve and propagate the causal history during the reduction, each message l(v) is tagged with the join point J that causes it, noted l J (v). Given a pattern M that is matched during the reduction, we note {{M }} J the pattern tagged with the causal history of each message present in the pattern (note that M and J have to be of the same size) as defined by:

-{{l(v)} } [J] = l J (v) -{{M & M ′ } } J ++ J′ = {{M }} J & {{M ′ }} J′
where J ++ J′ denotes list concatenation, and [J] is a singleton list containing J.

Figure 8 presents tagging for processes that are produced by a reduction. Here, the idea is to tag each message that has been produced by a reduction. Initially, all messages have an empty history, so we take l as syntactic sugar for l • .

For instance, consider the reduction from Section 2.4, augmented with causality tagging (but without considering aspects, and omitting location ϕ):

Deploy x.[⟨P c, Ad⟩] ⊩ ϕ ○ → x.⟨P c, Ad⟩ ○ ⊩ ϕ Red/NoAsp x.[M ▷ P ] ⊩ ϕ x.{ {Mσ}} J ○ → x.[M ▷ P ] ⊩ ϕ {P σ} J ′
when no pointcut of an activated aspect matches J ′ .

Red/Asp

x.

[M ▷ P ] ⊩ ϕ x.{ {Mσ}} J ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i ○ → x.[M ▷ P ] ⊩ ϕ ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i {Ad i [P σ proceed]τ i } J ′
where J ′ ⊩ P c i = τ i for all i ∈ I and no other activated aspect matches J ′ .

Red/Opaque

x.

[M ▸ P ] ⊩ ϕ x.{ {M σ} } J ○ → x.[M ▸ P ] ⊩ ϕ {P σ} J ′ Red/Observable x.[M P ] ⊩ ϕ x.{ {M σ} } J ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i ○ → x.[M P ] ⊩ ϕ {P σ} J ′ ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i {Ad i τ i } J ′
where no Ad i contains proceed,

J ′ ⊩ P c i = τ i for all i ∈ I
and no other activated aspect matches J ′ .

In every reduction rule, J ′ stands for (ϕ, x.M σ), J.

c.state • (d 0 ) & c.get • ("foo", r) & c.put • ("foo", 5) → dict.update J 1 (d 0 , "foo", 5, c) & c.get • ("foo", r) → c.getDict J 2 (d 1 ) & c.get • ("foo", r) → c.state J 3 (d 1 ) & c.get • ("foo", r) → c.state J 4 (d 1 ) & dict.lookup J 4 (d 1 , "foo", r) → c.state J 4 (d 1 ) & r.reply J 5 (5)
where

J 1 = ((ϕ, c.state(d 0 ) & c.put("foo", 5)), []) J 2 = ((ϕ, dict.update(d 0 , "foo", 5, c)), [J 1 ]) J 3 = ((ϕ, c.getDict(d 1 )), [J 2 ]) J 4 = ((ϕ, c.state(d 1 ) & c.get("foo", r)), [J 3 ]) J 5 = ((ϕ, dict.lookup(d 1 , "foo", r)), [J 4 ])
Semantics of aspect weaving. Figure 9 presents the semantics of aspects. All rules of Figure 3 are preserved, except for Rule Red because this is where weaving takes place. This rule is split into four rules, all of which depend on currently activated aspects as expressed by the following rule. We use the notation ○ → to distinguish clearly between a reduction that occurs in the aspect join calculus and in the join calculus.

Rule Deploy corresponds to the asynchronous deployment of a pointcut/advice pair x.⟨P c, Adv⟩ by marking the pair as activated x.⟨P c, Adv⟩ ○ . Note that activated pairs are not directly user-definable. The presence of this rule is crucial in the semantics because it allows activating aspects one by one asynchronously. Another possible semantics would have been to deploy synchronously altogether pointcut/advice pairs of the same definition, but then it would have caused extra synchronization in the translation to the core join calculus, and hence also in our implementation.

Rule Red/NoAsp is a direct reminiscence of Rule Red in case where no activated pointcut matches. Note that the new causal history is propagated to the produced process P σ.

Rule Red/Asp defines the modification of Rule Red in presence of aspects. If there is an aspect x i with an activated pointcut/advice pair x i .⟨P c, Ad⟩ ○ such that P c matches the join point with substitution τ , then the advice Ad is executed with the process P substituting the keyword proceed and where the variables bound by the pointcut are substituted according to τ . The side condition of Rule Red/Asp is that all P c i s are the activated pointcuts that match the current join point (ϕ, x.M σ). In particular, when two pointcut/advice pairs of the same object definition match, we can have x i = x j and ψ i = ψ j . Note that all advices associated with a pointcut that matches are executed in parallel.

Rule Red/Opaque is computationally the same as Rule Red/NoAsp, since activated aspects are essentially ignored when an opaque reaction occurs.

Rule Red/Observable proceeds the original reaction in parallel with the application of all deployed pointcut/advice pairs that match the join point. Note that in this rule, an advice has to be a simple process, and hence cannot use proceed. This restriction could be guaranteed by a simple type system.

Coming back to the cache example, the synchronization pattern reacts to become:

x.put J 1 ("bar", 5) & state J 2 (d) ○ → c.put J ′ ("bar", 5) & dict.update J ′ (d, "bar", 5, x)
where J ′ = ((ϕ, x.put("bar", 5)),

[J 1 , J 2 ])
The original operation on dict to update d is performed, in addition to the replication on c.

Why objects?

When designing the aspect join calculus, we considered defining it on top of the standard join calculus with explicit distribution, but without objects. However, it turns out that doing so would make the definition of aspects really awkward and hardly useful. Consider the standard join calculus definition of a buffer producer (adapted from [START_REF] Fournet | The reflexive chemical abstract machine and the join-calculus[END_REF]): 8

8 Syntactically, the main differences with our calculus are that conjunction is noted instead of & and disjunction of rules is noted ∧ instead of or. Also, there are no objects with labels, only channels.

def make_buffer(k) ▷ def put(n) empty() ▷ some(n) ∧ get(r) some(n) ▷ r(n) empty() in empty() k(get, put)
make_buffer takes as argument a response channel k on which the two newly-created channels get and put are passed (hence representing the new buffer). Crucially, the channel names get and put are local and not meaningful per se; when the definitions are processed, they are actually renamed to fresh names (rule str-def in [START_REF] Fournet | The reflexive chemical abstract machine and the join-calculus[END_REF]). Therefore, there is no way for an aspect to refer to "a reaction that includes a message on the get channel". Doing so would require modifying make_buffer to explicitly pass the newly-created channels also to the aspect, each time it is executed. An aspect would then have to match on all reactions and check if the involved channels include one of the ones it has been sent. In addition, the explicit modification of make_buffer defeats the main purpose of aspects, which is separation of concerns. A make_buffer that explicitly communicates its created channels to a replication aspect is not a general-purpose entity that can be reused in different contexts (e.g. without replication).

The objective join calculus, on the other hand, includes both object names and labels. Conversely to object names, labels have no local scope and are not subject to renaming [START_REF] Fournet | Inheritance in the join calculus[END_REF]. They constitute a "shared knowledge base" in the system, which aspects can exploit to make useful quantification. This is similar to how method names are used in the pointcuts of object-based aspect-oriented languages.

The argumentation above also explains why we have chosen not to include classes as in [START_REF] Fournet | Inheritance in the join calculus[END_REF] in our presentation of the aspect join calculus. Classes support extensible definitions, but do not contribute anything essential with respect to naming and quantification.

From the aspect join calculus to the join calculus

In this section, we present a translation of the aspect join calculus into the core join calculus. This allows us to specify an implementation of the weaving algorithm, and to prove it correct via a bisimilarity argument. The translation is used in Section 6 to implement Aspect JoCaml on top of JoCaml [START_REF] Fournet | JoCaml: A language for concurrent distributed and mobile programming[END_REF], an implementation of the join calculus in OCaml.

General approach

The translation approach consists in considering that an aspect is a standard object that receives messages from the weaver to execute a particular method that represents its advice. This is the usual way to compile aspects to a target object-oriented language without aspects [START_REF] Hilsdale | Advice weaving in AspectJ[END_REF].

Aspect weaving. In order to determine whether an aspect applies or not, the translation must account for aspect weaving. Note that the description of the semantics of the aspect join calculus leaves open the question of the underlying aspect weaving infrastructure. The naive approach, described in [START_REF] Tabareau | A theory of distributed aspects[END_REF], consists in relying on a central weaver that coordinates all distributed computations and triggers the weaving of all aspects. This centralized approach is however not realistic in a distributed setting.

Decentralized weaving. We adopt a decentralized weaving architecture, in which essentially each reaction is in charge of its own weaving, that is, determining which aspects apply to it and subsequently triggering their execution. In other words, with each reaction rule is associated a local, dedicated weaver. Recall that each reaction can have a specific weaving semantics (Section 3.2), hence there are correspondingly different kinds of weavers.

In order to support dynamic deployment of aspects, weavers consult a central registry that holds the list of currently-deployed aspects. Similarly, all aspect definitions register aspects with this registry. In Section 5.3, we discuss the possibility of distributing the aspect registry as well, introducing different policies of aspect deployment.

More specifically, the key interactions for aspect deployment and weaving are as follows:

-For each reaction rule M ▷ P in object x, there is a local weaver W x.M , on the same host, that can receive weave messages. These weave messages are sent each time the reaction rule fires. -The aspect registry R is executing at location H w and is known by all other processes. It exposes the following definitions D R :

D R = get asp (k) & asp act (ā) ▷ k(ā) & asp act (ā) deploy(a) & asp act (ā) ▷ asp act (a , ā)
-Aspects get activated by registering to the aspect registry through the label deploy. -Upon each (advisable or observable) reaction that fires, local weavers get the current list of activated aspects from the aspect registry by passing a continuation to the label get asp .

Note that to prove correctness of the translation, it is important that local weavers ask for the current list of aspects before weaving a reaction because it guarantees the consistency of the knowledge of the list of

Processes 0 J ∶ = 0 x.M J ∶ = x. M J obj x = D in P J ∶ = obj W(D r , x) in obj x = D r x in D a & P J go(H); P J ∶ = go(H); P J H[P ] J ∶ = H[ P J ] P & P ′ J ∶ = P J & P ′ J P, P ′ J ∶ = P J , P ′ J Definitions M ▷ P x ∶ = M JM ▷ obj ret = proceed(J) ▷ P J in let J W = (lhost, x.M ) + JM in W x.M .weave(ret.proceed, J W ) M P x ∶ = M ▷ P x M ▸ P x ∶ = M JM ▷ let J = (lhost, x.M ) + JM in P J D or D ′ x ∶ = D x or D ′ x Messages l J (v) • ∶ = l(v, J) M & M ′ • ∶ = M • & M ′ • l(v) J ∶ = l(v, J) l(v) & M ′ J , J ∶ = l(v) J & M ′ J Pointcuts contains(x.M ) ∶ = λ(ϕ, x ′ .M ′ ), J. if M τ ⊆ M ′ then [[x ↦ x ′ , τ ]] else [] host(H) ∶ = λ(ϕ, x ′ .M ′ ), J. [[H ↦ ϕ]] ¬P c ∶ = λJ. if P c J = [] then [[]]
else [] P c ∧ P c ′ ∶ = λJ. product( P c J, P c ′ J) causedBy(P c) ∶ = λjp, J. concat(map P c rec J)

P c rec ∶ = λJ. match J with • ⇒ [] jp, J ⇒ P c (jp, J) ++ concat(map P c rec J) Aspects proceed J ∶ = proceed(J) ⟨P c, Ad⟩ x ∶ = obj adv = advice(proceed, J, vP c )▷ Ad J in R.deploy( P c , adv.advice)
where vP c is the list of variables occurring free in P c. Fig. 10 Translating the aspect join calculus to the join calculus (translation of named definitions is in Figure 12) activated aspects between local weavers-indeed, the reference semantics of the distributed aspect join (Figure 9) assumes a globally consistent view of the list of activated aspects.

Translation

The general idea of the translation is that, given an aspect join calculus configuration:

C = D 1 ⊩ ϕ1 P 1 ∥ ⋯ ∥ D n ⊩ ϕn P n
we construct a distributed join calculus configuration without aspects by translating definitions, processes and aspects, as defined in Figure 10, and introducing the aspect registry R on host H w , yielding the following configuration:

C = D 1 ⊩ ϕ1 P 1 • ∥ ⋯ ∥ D n ⊩ ϕn P n • ∥ R.D R ⊩ Hw R.asp act ( ā act )
where ā is the list of activated aspects in D 1 , . . . , D n . The translation of the list of activated aspects of R.asp act is given recursively by

x.⟨P c, Ad⟩ ○ , ā act = ( P c , x.advice) , ā act .

That is, the translation of a pointcut/advice pair is given by the pair of the translated pointcut and the label on which the advice can be called.

The rest of the translation is given as follows.

Processes. The rules for processes recursively propagate the translation in sub-processes and definitions.

The translation of objects requires to distinguish between reaction rules (D r ) and pointcut/advice pairs (D a ) in the original definition D, because each pointcut/advice is translated as a normal object. The translation of reaction rules is done in two steps. First, a local weaver is created for each reaction, using W(D r , x), and then each reaction is replaced by a reaction that communicates with its weaver. We describe weavers in details later on in this section.

Definitions. The central point of the translation is to replace a standard reaction rule by a rule that reifies the reaction through an explicit join point, and then triggers a protocol with the weaver to decide whether or not some aspect intercepts the reaction rule and must be executed. Specifically, the translation of a reaction rule M ▷ P in object x, denoted M ▷ P x , produces a call to the weaver W x.M .weave, passing a locally-created single-use label ret.proceed to perform the original computation P and the current join point J W , obtained by collecting join points of the matched pattern JM and adding the current reaction join point (lhost, x.M ).

Here, JM is a list of (local) variables (of size equal to the number of messages in the pattern M ) to be bound to the actual causal history (see the translation of messages explained below). It is important that the new label is locally-created and guarantees a single use because it ensures that different calls to proceed cannot be interleaved. Observable reactions are translated similarly, since the difference in semantics is encapsulated in the weaver itself. Opaque reactions are not woven.

Messages. There are two ways to translate messages: (1) Case -• corresponds to messages that occur on the right hand side of a definition. This means that the messages are already tagged with the join point J that causes them. The tagged join point J is simply converted to an argument of the (untagged) message.

(2) Case -J corresponds to messages that occur on the left hand side of a definition. In that case, the index J of the translation corresponds to the list of variables that are used to bind the causal history. There is the implicit hypothesis that the size of J is equal to the number of messages. Each variable J is added as an argument of the corresponding message.

Pointcuts. Pointcuts are recursively transformed into functions that operate on join points and return a list of substitutions (encoded as lists) that correspond to all the possible matches. When the list is empty, it means that the pointcut does not match. This is the usual folklore way of computing altogether the possible results of a non deterministic function in one step [START_REF] Wadler | How to replace failure by a list of successes[END_REF]. To preserve the non-deterministic nature of pointcut matching, only one substitution will be chosen randomly by the weaver.

In the definition of contains(x.M ) , the substitution τ is seen as the list, and contains only free variables of M . The definition of P c ∧ P c ′ uses the function product that takes two lists of lists and returns the list of lists of all possible concatenations, i.e.:

product(ls, ls

′ ) = [ l ++ l ′ l ∈ ls, l ′ ∈ ls ′ ].
The definition of causedBy(P c) is given by computing every possible match of P c on every sub join point. concat and map are the usual operations on lists.

Aspects. A pointcut/advice pair ⟨P c, Ad⟩ is translated as an object that holds the advice and is registered with the weaver. The advice has only one label advice which expects the proceed label, the current join point and the list of variables that are free in the pointcut P c. The initialization sends the pointcut/advice pair to the weaving registry R by using the dedicated label deploy. Note that the pointcut is sent to the weaver but is not checked explicitly in the aspect. Indeed, it is the responsibility of the weaver to decide whether the advice must be executed or not. This is because the weaver must have the global knowledge of which pointcuts match, to perform Rule Red/NoAsp.

Finally, the translation of proceed is obtained by adding the current join point J as argument to proceed.

W(M ▷ P , x) ∶ = W x.M = D ▷ W(M P , x) ∶ = W x.M = D W(M ▸ P , x) ∶ = W x.M = 0 W(D or D ′ , x) ∶ = W(D, x) in obj W(D ′ , x) D ∶ = weave(proceed, J)▷ obj W init = aspL(asps)▷ let ads = filter (λ( v, _). v ≠ [])
map (λ(P c, adv).( P c J, adv)) asps

in proceed(J)& iter (λ( v, adv). adv(0, J, select( v))) ads in R.get asp (W init .aspL) D ▷ ∶ = weave(proceed, J)▷ obj W init = aspL(asps)▷ let ads = filter (λ( v, _). v ≠ [])
map (λ(P c, adv).( P c J, adv)) asps in if ads = [] then proceed(J) else iter (λ( v, adv). adv(proceed, J, select( v))) ads in R.get asp (W init .aspL)

Fig. 11 Per-reaction weaving

Per-reaction weavers. The per-reactions weavers are defined altogether at the beginning of the translation of an object using the inductive definition W(D, x), given in Figure 11. As explained above, for each reaction, a weaver is defined as an object with a weave method, used to trigger weaving at a join point.

The definition of the weaver depends on the kind of reaction. In the opaque case, the weaver is the null process. In both the observable (D ) and advisable (D ▷ ) cases, when the weaver receives weave(proceed, J), it creates a new object W init that defines a fresh channel aspL() whose aim is to get the current list of activated aspects asps from the aspect registry by spawning get asp (W init .aspL). When the list is received, the weaver filters the advices that match the current join point, ads (using the usual filter functions on lists). It then triggers all matching advices (using the iter function on lists) by selecting randomly a substitution from the list of substitutions v, using the non-deterministic selection function select.

For observable reactions, the weaver D just spawns in parallel a call to proceed with all the advices, corresponding to Rule Red/Obs. For advisable reactions, the weaver D ▷ needs to distinguish between two cases. If no aspect applies, the weaver executes the original process by sending the message proceed(J); this corresponds to Rule Red/NoAsp. Otherwise, the weaver only executes all advices in ads, without calling proceed (Rule Red/Asp).

x

.[M ▷

P ] ∶ = x.[ M ▷ P x ] or W x.M .D ▷ ⊩ ϕ x.[M P ] ∶ = x.[ M P x ] or W x.M .D ⊩ ϕ x.[M ▸ P ] ∶ = x.[ M ▸ P x ] ⊩ ϕ x.⟨P c, Ad⟩ ○ ∶ = x.[advice(proceed, J, vP c ) ▷ Ad J ] ⊩ ϕ x.⟨P c, Ad⟩ ∶ = x.[advice(proceed, J, vP c ) ▷ Ad J ] ⊩ ϕ R.deploy( P c , x.advice) D or D ′ ∶ = D or D ′ ⊩ ϕ D, D ′ ∶ = D , D ′ ⊩ ϕ H[D∶ P ] ∶ = H[ D ∶ P • ] ⊩ ϕ ⊺ ∶ = ⊺ ⊩ ϕ
where vP c is the list of variables occurring free in P c. Fig. 12 Translation of named definitions at location ϕ Named Definitions. Each observable and advisable reactions introduce their weavers in addition to the named translation of the reaction itself (Figure 12). Opaque reactions do not introduce any weaver, since they cannot be advised.

The translation of an activated aspect is simply the translation of its advice, because the part dealing with its pointcut has been delegated to the weaver. When the pointcut/advice pair is not already activated, the translation must place the message R.deploy( P c , x.advice) in the solution for future consumption by the aspect registry (hence emulating Rule Deploy from Figure 9).

For the other kinds of named definitions, the translation is just applied recursively.

Correctness of the translation

The main interest of translating the aspect join calculus into the core join calculus is that it provides a direct implementation of the weaving algorithm that can be proved to be correct. The first thing to check for the correctness of the translation is that it preserves structural rules.

Lemma 1 Structural rules are preserved by the translation, that is if

C ≡ C ′ then C ≡ C ′ .
Proof By case analysis on the structural rule:

-Or:

D or D ′ ⊩ ϕ ≡ D or D ′ ⊩ ϕ ≡ D , D ′ ⊩ ϕ ≡ D, D ′ ⊩ ϕ -Empty: ⊺ ⊩ ϕ ≡ ⊺ ⊩ ϕ ≡⊩ ϕ -Par: ⊩ ϕ P & Q • ≡⊩ ϕ P • & Q • ≡⊩ ϕ P • , Q • ≡⊩ ϕ P, Q • -Nil: ⊩ ϕ 0 • ≡⊩ ϕ 0 ≡⊩ ϕ -Join: ⊩ ϕ x.(M & M ′ ) • ≡⊩ ϕ x.( M • & M ′ • ) ≡ ⊩ ϕ x.M • & x.M ′ • ≡⊩ ϕ x.M & x.M ′ • -Sub-Loc: H[D∶ P ] ⊩ ϕ ≡ H[ D ∶ P • ] ⊩ ϕ ≡ { D } ⊩ ϕH { P • } -Obj-Def:
To simplify, we consider the case of one definition and one aspect (the general case follows by induction).

⊩ ϕ obj x = (M ▷ P or⟨P c, Ad⟩) in Q • ≡ ⊩ ϕ obj W(M ▷ P, x) in obj x = M ▷ P x in ⟨P c, Ad⟩ & Q • ≡ W x.M .D ▷ or x. M ▷P x or adv.advice(proceed, J, vP c )▷ Ad J ⊩ ϕ R.deploy( P c , adv.advice) & Q • ≡ x.M ▷ P or adv.⟨P c, Ad⟩ ⊩ ϕ Q • ≡ x.(M ▷ P or⟨P c, Ad⟩) ⊩ ϕ Q • -Loc-Def: ⊩ ϕ H[P ] • ≡⊩ ϕ H[ P • ] ≡ H[⊺∶ P • ] ⊩ ϕ ≡ H[⊺∶ P ] ⊩ ϕ
It is also necessary to check that the translation of a pointcut is a function that computes all the possible substitutions returned by the (non-deterministic) semantics of this pointcut.

Lemma 2 For every pointcut P c and join point J, we have P c J = [τ J ⊩ P c ∶ τ and τ ≠ ]. In particular, when a pointcut does not match P c J returns the empty list.

Proof By structural induction on P c:

contains(x.M ): This case is just a unification problem. contains(x.M ) returns at most one substitution. -host(h): host(h) returns the singleton list containing the substitution that sends h to the current location of the join point. -P c ∧ P c ′ : By induction, P c and P c ′ compute the lists of all possible substitutions. The definition of P c ∧ P c ′ J thus returns the list of all possible disjoint union (computed as list concatenation) of two substitutions picked up in P c J and P c ′ J. -¬P c: By induction, P c J is the empty list if and only if J ⊩ P c = .

-causedBy(P c): By induction, P c J ′ computes the list of all possible substitutions for any pointcut J ′ . Using this, it is easy to prove by induction on J that

P c rec J = [τ J ′ ⊩ P c ∶ τ such that τ ≠ and (J ′ ≺ J or J ′ = J)].
It then follows that

causedBy(P c) J = [τ J ′ ⊩ P c ∶ τ such that τ ≠ and J ′ ≺ J].
As usual in concurrent programming languages, the correctness of the translation algorithm is given by a proof of bisimilarity. Namely, we prove that the original configuration with aspects (in the aspect join calculus) is bisimilar to the translated configuration without aspects (in the objective join calculus). The idea of bisimilarity is to express that, at any stage of reduction, both configurations can perform the same actions in the future. More formally, in our setting, a simulation R is a relation between configurations such that when C 0 R C 1 and C 0 reduces in one step to C ′ 0 , there exists C ′ 1 such that C ′ 0 R C ′ 1 and C 1 reduces (in 0, 1 or more steps) to C ′ 1 . We illustrate this with the following diagram:

C 0 R ○ C 1 * C ′ 0 R C ′ 1
A bisimulation is a simulation whose inverse is also a simulation.

With this definition, our notion of bisimulation is not barbed-preserving nor context-closed. This is not surprising as a context would be able to distinguish between the original and translated configuration by using messages sent on auxiliary labels (weave, proceed, advice or deploy). However, to prevent the trivial translation that sends every process to the null process 0 to be a correct translation, we need to be able to observe at least one reduction. To this end, we consider a special object name output, with a message result on which to write the output and only one reaction involving output.result(v) ▷ 0. This is essentially the channel on which one can observe the computational behavior of a configuration. In what follows, we assume that the definition of this object is always present in the configuration at location H output . To express that the reaction on output is observable, we additionally require that a simulation R satisfies that any two configurations (C 0 , C 1 ) ∈ R have the same number of messages output.result in the solution.

To relate a configuration C with its translation C , we need to tackle two difficulties:

1. During the evolution of C , auxiliary messages that have no correspondents in C are sent for communication between processes, weavers, aspects and the aspect registry. 2. In the execution of C, proceed is substituted by the process P to be executed, whereas in C , P is executed through a communication with the object where the reaction has been intercepted.

To see the auxiliary communication as part of a reduction rule of the aspect join calculus, we define a notion of standard form for the translated configurations. Let

T = {C ∃C 0 , C 0 → * C}
be the set of configurations that come from a translated configuration. We construct a rewriting system → T for T, based on the reduction rules of the join calculus. Namely, we take Rule Red and Message-Comm restricted to the case where the pattern contains either of the dedicated labels: weave, proceed, advice, get asp and aspL (the label deploy is treated differently as it corresponds to the application of Rule Deploy). In T, those labels only interact alone, or one-by-one with the constant label asp act . So the order in which reaction rules are selected has no influence on the synchronized pattern; in other words, the rewriting system → T is confluent. Furthermore, it is not difficult to check that this rewriting system is also terminating. However, the reduction is non-deterministic due to the presence of the non-deterministic function select in the definition of weavers. Therefore, it makes sense to talk about the normal forms of C ∈ T, whose set is noted C.

We note C gc ∼ C ′ when C ′ is equal to C where every named definition x.D for which x does not appear in the configuration (but in x.D of course) is removed from the configuration. This condition deals with auxiliary definitions appearing during the translation that are used linearly and must then be garbage collected. This is mandatory to synchronize the current auxiliary definitions available in the solution.

Theorem 1 The relation

R = {(C 0 , C 1 ) ∃C ′ 1 ∈ C1 . C 0 gc ∼ C ′ 1 }
is a bisimulation. In particular, any configuration is bisimilar to its translation.

Proof The fact that any two configuration in R have the same number of messages output.result in the solution is direct as the translation preserves messages and does not introduce any message of this form.

(A) R is a simulation. The fact that R is a simulation just says that the communication between aspects, processes and the weaver simulates the abstract semantics of aspects.

The crux of the proof lies in the confluence of → T which means that once the message weave(k, jp) is sent to the weaver, the translation introduces no further choice in the configuration. That is, every possible choice in C corresponds directly to the choice of a reduction rule in C.

More precisely, we show that for any reduction C 0 → C ′ 0 , one can find a corresponding reduction chains from C 0 to C ′ 0 :

C 0 R ○ C 1 * T / / C ′ 1 ∈ C1 gc ∼ C 0 * C ′ 0 R C ′′ 1 gc ∼ C ′ 0 Rule Deploy.
The activation of an aspect x.⟨P c, Ad⟩ is in one-toone correspondence with the consumption of the message R.deploy( P c , x.advice) by the aspect registry.

x.⟨P c, Ad⟩ ⊩ ϕ ∥ R.D R ⊩ H w R.asp act ( ā act ) ≡ x.⟨P c, Ad⟩ ○ ⊩ ϕ R.deploy( P c , x.advice) ∥ R.D R ⊩ H w R.asp act ( ā act ) → x.⟨P c, Ad⟩ ○ ⊩ ϕ ∥ R.D R ⊩ H w R.deploy( P c , x.advice), R.asp act ( ā act ) → x.⟨P c, Ad⟩ ○ ⊩ ϕ ∥ R.D R ⊩ H w R.asp act (( P c , x.advice), ā act )
Note at this point, that the fact that aspect activation is asynchronously described by Rule Deploy in the semantics is crucial in the proof.

Rule Red/NoAsp.

Consider the reduction

x.[M ▷ P ] ⊩ ϕ x.{ {M σ} } J ○ → x.[EM ▷ P ] ⊩ ϕ {P σ} J ′
This rule is simulated by the chain:

x

.[M ▷ P ] ⊩ ϕ x.{ {M σ} } J • R.D R ⊩ H w R.asp act ( ā act ) ≡ x. [M ▷ P ] x , W x.M .D ▷ ⊩ ϕ x. {{M σ} } J • R.D R ⊩ H w R.asp act ( ā act ) → x. [M ▷ P ] x , W x.M .D ▷ , ⊩ ϕ W x.M .weave(ret.proceed, J ′ ) ret.proceed(J) ▷ P σ J R.D R ⊩ H w R.asp act ( ā act ) → T
where J ′ = (ϕ, x.M σ), J

x. [M ▷ P ] x , W x.M .D ▷ , ret.proceed(J) ▷ P σ J , ⊩ ϕ R.get asp (W init .aspL) W init .aspL(asps) ▷ . . . R.D R ⊩ H w R.asp act ( ā act ) → T

x. [M ▷ P ] x , W x.M .D ▷ , ret.proceed(J)

▷ P σ J , ⊩ ϕ W init .aspL(asps) ▷ . . . R.D R ⊩ H w R.asp act ( ā act ), R.get asp (W init .aspL) → T x. [M ▷ P ] x , W x.M .D ▷ , ret.proceed(J) ▷ P σ J , ⊩ ϕ W init .aspL(asps) ▷ . . . R.D R ⊩ H w R.asp act ( ā act ), W init .aspL( ā • ) → T x. [M ▷ P ] x , W x.M .D ▷ , ret.proceed(J) ▷ P σ J , ⊩ ϕ W init .aspL( ā • ) W init .aspL(asps) ▷ . . . R.D R ⊩ H w R.asp act ( ā act ) → T gc ∼ x. [M ▷ P ] x , W x.M .D ▷ , ⊩ ϕ ret.proceed(J ′ ) ret.proceed(J) ▷ P σ J R.D R ⊩ H w R.asp act ( ā act ) → T gc ∼ x. [M ▷ P ] x , W x.M .D ▷ ⊩ ϕ P σ J ′ R.D R ⊩ H w R.asp act ( ā act ) ≡ x.[M ▷ P ] ⊩ ϕ {P σ} J ′ • R.D R ⊩ H w R.asp act ( ā act )
because by Lemma 2, P c J ′ = [] for every pointcut P c of activated aspects, so the result of filter in W init is empty. Here, the need for gc ∼ is for garbage collecting unused definitions such as ret.proceed(J) ▷ P σ J . Rule Red/Asp.

Consider the reduction

x.[M ▷ P ] ⊩ ϕ x.{ {Mσ}} J ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i ○ → x.[M ▷ P ] ⊩ ϕ ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i {Ad i [P σ proceed]τ i } J ′
This rule is simulated by the chain:

x.[M ▷ P ] ⊩ ϕ x.{ {M σ} } J • R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i →
similar steps than for Red/NoAsp:

x

. [M ▷ P ] x , W x.M .D ▷ , ret.proceed(J) ▷ P σ J , ⊩ ϕ W init .aspL( ā • ) W init .aspL(asps) ▷ . . . R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i → T gc ∼ x. [M ▷ P ] x , W x.M .D ▷ , ⊩ ϕ & i x i .advice(ret.proceed, J ′ , τ i ), ret.proceed(J) ▷ P σ J R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i → T gc ∼
because by Lemma 2, τ i ∈ P c i J ′ for every x i 's involved, so there are executions of select that pick up the right substitutions. Then,

x. [M ▷ P ] x , W x.M .D ▷ , ⊩ ϕ ret.proceed(J) ▷ P σ J R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i x i . Ad i J ′ [ret.proceed proceed] τ i ≡ gc ∼ x.[M ▷ P ] ⊩ ϕ R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i x i . {Ad i [P σ proceed]τ i } J ′ • Rule Red/Opaque. Consider the reduction x.[M ▸ P ] ⊩ ϕ x.{ {M σ} } J ○ → x.[M ▸ P ] ⊩ ϕ {P σ} J ′
This rule is simulated by the chain:

x

.[M ▸ P ] ⊩ ϕ x.{ {M σ} } J • ≡ x. [M ▸ P ] x ⊩ ϕ x. {{M σ} } J • → x. [M ▸ P ] x ⊩ ϕ P σ J ′ ≡ x.[M ▸ P ] ⊩ ϕ {P σ} J ′ • Rule Red/Observable.
Consider the reduction

x.

[M P ] ⊩ ϕ x.{ {Mσ}} J ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i ○ → x.[M P ] ⊩ ϕ {P σ} J ′ ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i {Ad i τ i } J ′
This rule is simulated by the chain:

x

.[M P ] ⊩ ϕ x.{ {M σ} } J • R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i →
similar steps than for Red/NoAsp:

x

. [M P ] x , W x.M .D , ret.proceed(J) ▷ P σ J , ⊩ ϕ W init .aspL( ā • ) W init .aspL(asps) ▷ . . . R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i → T gc ∼ x. [M P ] x , W x.M .D , ⊩ ϕ ret.proceed(J ′ ), ret.proceed(J) ▷ P σ J & i x i .advice(0, J ′ , τ i ) R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i → T gc ∼
because by Lemma 2, τ i ∈ P c i J ′ for every x i 's involved, so there are executions of select that pick up the right substitutions. Then, because no advice involved contains proceed (side condition of observable reactions):

x.

[M P ] x , W x.M .D ▷ , ⊩ ϕ P σ J ′ R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i (x i . Ad i J ′ )τ i ≡ gc ∼ x.[M P ] ⊩ ϕ {P σ} J ′ • R.D R ⊩ H w R.asp act ( ā act ) ∥ i∈I x i .⟨P c i , Ad i ⟩ ○ ⊩ ψ i x i . {Ad i τ i } J ′ • Rule Message-Comm.
Consider the reduction

⊩ ϕ x.M ∥ x.D ⊩ ψ ○ → ⊩ ϕ ∥ x.D ⊩ ψ x.M
This rule is simulated by the chain:

⊩ ϕ x.M • ∥ x.D ⊩ ψ ≡ ⊩ ϕ x. M • ∥ x.D ′ or D ⊩ ψ → ⊩ ϕ ∥ x.D ′ or D ⊩ ψ x. M • ≡ ⊩ ϕ ∥ x.D ⊩ ψ x.M •
where the fact that there exists D ′ and D such that x.D ≡ x.D ′ or D can be proven by induction on D.

Rule Move.

Consider the reduction

H[D∶ (P & go(H ′ ); Q)] ⊩ ϕ ∥ ⊩ ψH ′ ○ → ⊩ ϕ ∥ H[D∶ (P & Q)] ⊩ ψH ′
This rule is simulated by the chain:

H[D∶ (P & go(H ′ ); Q)] ⊩ ϕ ∥ ⊩ ψH ′ ≡ H[ D ∶ ( P • & go(H ′ ); Q • )] ⊩ ϕ ∥ ⊩ ψH ′ → ⊩ ϕ ∥ H[ D ∶ ( P • & Q • )] ⊩ ψH ′ ≡ ⊩ ϕ ∥ H[D∶ (P & Q)] ⊩ ψH ′ (B) R -1 is a simulation.
For the converse direction, we have to show that for (C 0 , C 1 ) ∈ R and any reduction C 1 → C 2 , one can fill the following diagram:

C 0 R ○ * C 1 * T / / C ′ 1 ∈ C1 gc ∼ C 0 * C ′ 0 R C 2 * T / / C ′ 2 ∈ C2 gc ∼ C ′ 0
Again, we proceed by analysis of the kind of reduction.

Rule Move.

Suppose we have H[D∶ (P &go(H

′ ); Q)] ⊩ ϕ ∈ C 1 and H[D∶ (P & Q)] ⊩ ψH ′ ∈ C 2 .
As no reduction in → T involves a migration and the rules are all left-linear, the migration rule is orthogonal to rules in → T . This means that we have

H[D∶ (P ′ & go(H ′ ); Q)] ⊩ ϕ ∈ C ′
1 for some P ′ , so a similar migration can be done on

C ′ 1 ending up in H[D∶ (P ′ &Q)] ⊩ ψH ′ ∈ C ′ 2
(by orthogonality, we have confluence). Then, by a direct inversion lemma, we know that

H[D∶ (P ′′ & go(H ′ ); Q ′ )] ⊩ ϕ ∈ C 0 for some P ′′ and Q ′ such that P ′′ • = P ′ and Q ′ • = Q.
So we can apply the migration rule on C 0 . We set C ′ 0 to be the resulting configuration. It is easy to check that

C ′ 0 gc ∼ C ′ 2 .
Rule Red.

-If the reduction is → T , the normal form has not changed, so

C ′ 1 = C ′ 2 gc ∼ C 0 and we set C 0 = C ′ 0 .
-If it consumes a message deploy(pc, ad), then C ′ 0 is obtained by applying Rule Deploy to the corresponding pointcut/advice pair and

C ′ 2 gc ∼ C ′ 0 .
-Otherwise, the reduction consumes a pattern x.M σ and produces a message of the form:

w.weave(k, jp).

By an inversion lemma, we know that x.M ′ in C 0 for some pattern M ′ such that M ′ • = M σ . Then, by analyzing the reduction from C 2 to C ′ 2 , we can recognize the simulation of one of the four possible reductions in the original configuration (as described above). Thus, it suffices to pick the right and define C ′ 0 as the result of this rule on C 0 (by setting the substitution computed by the pointcuts to be the one choosing by the executions of select). We conclude this case by noting that in the proof that R is a simulation, the four reductions were handled similarly, starting with the emission of the message w.weave(k, jp) and computing the normal form according to → T . So we have

C ′ 0 gc ∼ C ′ 2 . Rule Message-Comm.
-If the reduction is → T , the normal form has not changed, so

C ′ 1 = C ′ 2 gc ∼ C 0 and we set C 0 = C ′ 0 .
-Otherwise, the reduction migrates a pattern x.M that, by an inversion lemma corresponds to a pattern x.M ′ in C 0 , with M ′ • = M . So the same communication can occur in C 0 .

To conclude the proof, we need to show that any configuration is bisimilar to its translation. This follows from the fact that C 0 is a normal form for → T without message proceed(J), so that C 0 R C 0 . ⊓ ⊔

Discussion

We now elaborate on different design considerations, namely causality, synchronous weaving, and distributed aspect registries.

Dealing with Causality

In the aspect join calculus, we have introduced join points with causality, allowing pointcuts to discriminate join points based on the reactions that contributed to their occurrence. This choice is motivated by expressiveness, but it does make the calculus more complex and its implementation more challenging.

The motivation to deal with causality is inspired by prior work on aspect languages in different settings. Indeed, it is common in aspect languages to use controlflow related pointcuts in order to be able to discriminate join points based on call stack (e.g. cflow and cflowbelow in AspectJ [START_REF] Kiczales | An overview of AspectJ[END_REF]). Some proposals have even gone further, proposing history-based pointcuts that are not restricted to the call stack [START_REF] Douence | Tracebased aspects[END_REF][START_REF] Douence | A pointcut language for control-flow[END_REF][START_REF] Leger | An expressive stateful aspect language[END_REF][START_REF] Ostermann | Expressive pointcuts for increased modularity[END_REF]. Also, all distributed aspect languages and systems support distributed control flow, although in a synchronous setting [START_REF] Daniel | Explicitly distributed AOP using AWED[END_REF][START_REF] Nishizawa | Remote pointcut -a language construct for distributed AOP[END_REF][START_REF] Pawlak | JAC: an aspect-oriented distributed dynamic framework[END_REF][START_REF] Tanter | A versatile kernel for distributed AOP[END_REF][START_REF] Truyen | Run-time and atomic weaving of distributed aspects[END_REF]]. Leger et al. propose a library for distributed causality-based pointcuts in an asynchronous setting based on vector clocks [START_REF] Leger | Modular and flexible causality control on the web[END_REF].

Causality, be it synchronous or not, is important in practice for different reasons. A first basic motivation is that, more often than not, one needs to avoid advising aspects themselves. For instance, if a cache replication aspect is deployed on each host of interest, then aspects will indefinitely replicate the cache replicated by aspects on other hosts. These infinite loops can be avoided with control-flow pointcuts, or similar flow-based approaches [START_REF] Bodden | Avoiding infinite recursion with stratified aspects[END_REF][START_REF] Tanter | Execution levels for aspect-oriented programming: Design, semantics, implementations and applications[END_REF].

Let us illustrate with the cache replication example. To be able to identify aspect-specific activity, we declare an aspect object, with a specific label rput whose goal is to make the activity of the aspect visible. Then the new definition of the cache replication aspect below also excludes the activity caused by a cache replication aspect using the pointcut ¬ causedBy( * .rput).

⊩ ϕ obj replicate = deploy(c, H ′ ) ▷ H[go(H ′ ); obj rep = rput(k, v) ▷ c.put(k, v) or ⟨contains( * .put(k, v)) ∧ host(h) ∧ ¬ causedBy(contains( * .rput( * , * ))), if (h ≠ H ′ ) then c.put(k, v)⟩] in NS.register("replicate", replicate)
This ensures that a cache replication aspect never matches a put join point that has been produced by the rule rput(k, v)▷c.put(k, v), thereby ignoring aspect-related computation.

Causality in aspect languages is also very much useful for many typical applications of aspect-oriented programming. One salient example is security enforcement, such as access control [START_REF] Samarati | Access control: Policies, models, and mechanisms[END_REF], which can be handled by aspects. In particular, stack-based access control, as provided in Java, requires inspecting the call stack to determine whether a resource can be accessed or not; aspectizing these mechanisms requires pointcuts to access the call context [START_REF] Toledo | Aspectizing Java access control[END_REF]. Another related security mechanism that requires causality is integrity checking [START_REF] Kenneth | Integrity considerations for secure computer systems[END_REF]: enforcing that certain actions are performed (or not) depending on whether the data or code comes from trusted parties.

In models of synchronous aspect languages, join points in context are represented as a linked data structure where a join point has a reference to its parent in the call stack [START_REF] Dutchyn | Semantics and scoping of aspects in higher-order languages[END_REF]. The causality trees we have introduced in the aspect join calculus are a direct generalization of this model to the chemical setting. Of course, efficient implementations of aspect languages do not implement control-flow pointcuts or trace-based matching by relying on such costly structures [START_REF] Avgustinov | abc: an extensible AspectJ compiler[END_REF][START_REF] Masuhara | A compilation and optimization model for aspectoriented programs[END_REF][START_REF] Hilsdale | Advice weaving in AspectJ[END_REF]: instead, following the principles of partial evaluation [START_REF] Neil | Partial Evaluation and Automatic Program Generation[END_REF], they statically evaluate which join points might potentially affect causality-related decisions, and introduce as little statebased indicators and bookkeeping operations as possible. Related techniques have been explored outside of the AOP community as well. For instance, Clements and Felleisen show that stack-based security mechanisms can be efficiently implemented using continuation marks [START_REF] Clements | A tail-recursive machine with stack inspection[END_REF]. Accordingly, we do not expect practical, scalable implementations of the aspect join calculus to implement causality trees as such. Causality trees are a fine semantic device, not a realistic implementation technique. It remains to be studied how the existing optimization techniques mentioned above for stack-based and tracebased mechanisms could be extended and adapted to the general setting of the causality tree. Simple techniques might be quite effective. For instance, assuming aspect definitions are available ahead of time, if an aspect uses the pointcut causedBy("untrusted_label") in order to discriminate doubtful computation, the implementation could simply taint all such join points as they are produced, making the implementation of causedBy a simple tag check.

Synchronous aspects

A particularity of aspects compared to traditional event handling is the possibility to advise around join points and therefore have the power to proceed the original computation, either once, several times, or not at all. Doing so requires careful thinking about the synchronization of advices. The semantics we have presented corresponds to asynchronous reactions, in which all advices that match are triggered asynchronously. We could devise a weaving semantics that rather reflects the one of AspectJ by chaining implicitly advices and invoking them in a synchronous manner. First, this presents the issue of choosing the order in which advices are chained, which is not clear in an asynchronous setting. Second, the synchronous semantics can be encoded by an explicit chaining of advices and thus is not a primitive operations. For those two reasons, we have decided not to integrate a synchronous reaction in the semantics.

Also, note that the semantics of aspect weaving relies on the currently-deployed aspects. As we have seen, deployment is asynchronous, which means that to be sure that an aspect is in operation at a given point in time, explicit synchronization has to be setup. This design is in line with the asynchronous chemical semantics of the join calculus. For instance, the same nondeterminism occurs in the definition of an object, in which the initialization process is not guaranteed to be completed before the object process starts executing. In case such sequentiality is needed, it has to be manually encoded using the typical explicit continuation-passing style. Fournet and Gonthier show how a wide variety of synchronization primitives can be easily encoded in the join calculus [START_REF] Fournet | The join calculus: a language for distributed mobile programming[END_REF].

Distributed aspect deployment

Distributed aspect deployment is a complex task, for which several different policies can be conceived. This is reflected in the different designs and choices of specific distributed AOP systems, such as DJcutter (one central aspect server) [START_REF] Nishizawa | Remote pointcut -a language construct for distributed AOP[END_REF], AWED (aspects are either deployed on all hosts, or only on their local host of definition) [START_REF] Daniel | Explicitly distributed AOP using AWED[END_REF], and ReflexD (distributed aspect repositories to which base programs are connected at start-up time) [START_REF] Tanter | A versatile kernel for distributed AOP[END_REF], among others.

The formal model of the aspect join calculus that we have presented in this paper considers one central aspect registry. Extending this model to several registries is quite direct, does not affect the main results of this paper regarding the translation approach, and is straightforward to implement (in fact, our implementation of Aspect JoCaml supports multiple registries). We describe here such an extension, and discuss the possibility to define fine-grained policies that go beyond prior work.

As a first step, we should extend the syntax of reactions with an exponent M ▷ reg P to express that the reaction is registered in the aspect registry reg. In particular this means that only aspects deployed in registry reg are able to advise this reaction. (The case we have formally developed, where all aspects see all computations, corresponds to one global aspect registry to which all weavers and aspects are registered.)

An additional refinement of our model is to allow aspect registries to have different policies. For instance, the registry we have formalized is open, as it accepts dynamic aspect registration requests. One could allow some registries to be closed: a closed aspect registry is initiated with a fixed number of aspects deployed, and subsequently ignores any new aspect registration request. A closed registry would be defined with the following reactions:

D closed R = get asp (k) & asp act (ā) ▷ k(ā) & asp act (ā) deploy(a) & asp act (ā) ▷ asp act (ā)
Figure 13 illustrates some of the topological flexibility offered by weaving registries and their policies: objects can register their reaction weavers in different registries with specific policies.

For instance, suppose a closed aspect registry reg c with only a cache replication aspect and an open aspect registry reg o . The following definition of the cache example guarantees that only cache replication can have access to the cache history, while any aspect registered with reg o can observe accesses to the dictionary: (d, k, v, c) or Note that closed repositories would allow a more efficient (and still correct) implementation of weaving, whereby the communication between weavers and the aspect registry can be limited to one initial request. Since the list of aspects is known to be immutable, there is no need to request it again upon each firing reaction.

obj c = put(k, v) & state(d) reg c dict.update
An aspect registry policy may further specify that only weavers of a specific kind are accepted, such as observable reactions (Section 3.2). The design space of distributed deployment policies is wide and its exhaustive exploration is left open for future work.

Aspect JoCaml

Aspect JoCaml is a prototype implementation of the aspect join calculus on top of JoCaml, an extension of OCaml with join calculus primitives [START_REF] Fournet | JoCaml: A language for concurrent distributed and mobile programming[END_REF]. The implementation is directly based on the translation described in Section 4.

While slightly different in the syntax, Aspect Jo-Caml supports all the functionalities of the aspect join calculus, except for migration, which is not supported in JoCaml. Using the facilities provided by OCaml, we have also introduced new concepts not formalized in the aspect join calculus, such as classes for both objects and aspects, and the distinction between private and public labels.

This section presents a quick overview of the language through the implementation and deployment of the cache replication example. We then discuss salient points in the implementation.

Overview of Aspect JoCaml

Aspect JoCaml uses directly the class system of OCaml, providing a new dist_object keyword to define distributed objects with methods and reactions on public or private labels. For instance, a continuation class that defines a label k that expects an integer and prints it to the screen can be defined as: is not visible, and hence can be neither quantified over nor accessed by aspects. Private labels hence provide another level of encapsulation by hiding patterns, in addition to the possibility to hide reactions discussed in Section 3.2. The different per-reaction weaving semantics are specified by a quoted keyword, e.g. 'observable.

class continuation ip = dist_object ( self
A reaction definition is parametrized by an IP address using at. This IP address is meant to be the address of an aspect registry, just as the extension discussed in Section 5.3. The parameter ip is passed at object creation time, making it possible to choose a different aspect registry for each created continuation object.

The definition of the cache class is given in Figure 14 and can be directly inferred from the definition of Section 3.2. We omit the code for the dictionary class, which directly uses hash tables provided by the Hashtbl OCaml module. A message that creates a dictionary is initially emitted using spawn in the initializer process.

Aspects are defined as classes with a pointcut and an advice. The instantiation mechanism is identical to that of objects, using the new keyword. The cache replication aspect is defined in Figure 15. Labels in Contains pointcut are handled as strings and boolean pointcut combinators are defined by infix operators &&& and |||.

Deployment. Before creating any process, at least one aspect registry must be created and registered to the name server. For instance, the following code creates a permanent aspect registry at IP 12345: = new continuation ip in for arg = 1 to 10 do spawn z # put ( " key " , arg ); spawn z # get ( " key " ,k # k ) done ;

Implementation

We now briefly discuss some elements of the Aspect JoCaml implementation.

Architecture. An Aspect JoCaml file is translated into a JoCaml file and then compiled using the JoCaml compiler. To simplify the parser, there are { ... } separators for plain JoCaml code (for clarity, those separators have been omitted in Figure 15). While these separators clutter the code, they have the advantage that new features of JoCaml or OCaml can be directly back ported to Aspect JoCaml.

A more advanced solution would be to use Camlp5, the preprocessor-pretty-printer of OCaml, to produce a type-safe translation. Unfortunately, compatibility issues between Camlp5 and JoCaml forbids this solution at the moment.

Typing issues. As the code produced is compiled using JoCaml, everything needs to be typed. Sometimes, this requires type annotations in class definitions when dealing with parametric polymorphism.

However, as mentioned in the JoCaml manual: "communications through the name server are untyped. This weakness involves a good programming discipline" [START_REF] Mandel | The JoCaml language release 4.00[END_REF]. On the one hand, this limitation of distributed programming in OCaml simplifies the task of creating a list of aspects of different types. On the other hand, to avoid type errors at runtime, an anti-unification mechanism has to be developed to guarantee type safe application of aspects [START_REF] Tabareau | A typed monadic embedding of aspects[END_REF].

Static/dynamic pointcuts. Recall that the aspect registry is responsible for bootstrapping the communication between weavers and aspects. This is performed by adding aspects to the list of current aspects connected to the weaver. But part of communications between weavers and aspects can be avoided. Indeed, it is sometimes possible to statically decide whether a pointcut can match a join point coming from a given weaver. If the pointcut can never match, the aspect registry does not need to pass the aspect to the weaver for weaving.

To that end, our implementation differentiates between the static and dynamic parts of a join point. The static part is used at registration time, whereas the dynamic part is used during runtime weaving.

Depth of causality tree. As discussed in Section 5.1, an optimized, scalable management of the causality tree is a challenging research challenge. The current implementation of Aspect JoCaml is naive in this regard: it is a direct implementation of the calculus, and as such keeps track of every causal match. This means that the causality tree may grow unboundedly. A simple general optimization to implement is to put a bound on the maximum depth of the tree, although this would change the semantics of pointcut matching. For instance, keeping only a bounded version of the causality tree may imply that a causedBy("untrusted_label") pointcut does not match, whereas the compromised label occurs is in fact in the complete causality tree, thus introducing a security flaw. In this sense, partial evaluation techniques, which sacrifice dynamism but preserve the matching semantics, might be preferable.

Non-determinism. The family of join calculi are nondeterministic. Similarly, the aspect join calculus is nondeterministic. In the translation, weavers rely on a random selection of a matching substitution (Figure 11). Aspect JoCaml is a direct implementation of the translation, and as such, uses the non-deterministic select function. This non-deterministic behavior in the translated code is important to prove the bisimulation with the direct semantics, which is also non-deterministic. Of course, a given implementation could make an arbitrary choice, which would be more efficient than an actual random selection. But programmers should not rely on determinism. In essence, this is similar to how the evaluation order of procedure arguments is left unspecified in the standards of some languages (such as C, C++, and Scheme): technically, an implementation can choose any arbitrary (even random) order for evaluating function arguments. This forces programmers to not rely on a specific evaluation order in their programs, even though most sequential implementations will (arbitrarily) adopt a left-to-right order. The same happens with JoCaml as an implementation of the objective join calculus in OCaml. It is supposed to be non-deterministic in the order of matching reactions, but it might very well be implemented using a FIFO strategy internally.

Related work

We first discuss work related to the formal semantics of aspects, and then relate to existing distributed aspect languages and systems.

Formal semantics of aspects

There is an extensive body of work on the semantics of aspect-oriented programming languages (e.g. [START_REF] Wand | A semantics for advice and dynamic join points in aspectoriented programming[END_REF][START_REF] Clifton | MiniMAO 1 : An imperative core language for studying aspect-oriented reasoning[END_REF][START_REF] Dutchyn | Semantics and scoping of aspects in higher-order languages[END_REF][START_REF] Jagadeesan | Typed parametric polymorphism for aspects[END_REF][START_REF] De Fraine | Essential AOP: the A calculus[END_REF]). These languages adopt either the lambda calculus or some minimal imperative calculus at their core. To the best of our knowledge, this work is the first to propose a chemical semantics of aspects. In addition, none of the formal accounts of AOP considers distributed aspects. Among practical distributed aspect systems, only AWED exposes a formal syntax; the semantics of the language is however only described informally [START_REF] Daniel | Explicitly distributed AOP using AWED[END_REF].

The approach of starting from a direct semantics with aspects, and then defining a translation to a core without aspects and proving the correctness of the transformation is also used by Jagadeesan et al., in the context of an AspectJ-like language [START_REF] Jagadeesan | Typed parametric polymorphism for aspects[END_REF].

Distributed aspect languages and systems

We now compare specific features of practical distributed aspect languages and systems-in particular JAC [START_REF] Pawlak | JAC: an aspect-oriented distributed dynamic framework[END_REF], DJcutter [START_REF] Nishizawa | Remote pointcut -a language construct for distributed AOP[END_REF], ReflexD [START_REF] Tanter | A versatile kernel for distributed AOP[END_REF], and AWED [START_REF] Daniel | Explicitly distributed AOP using AWED[END_REF]-and relate them to the aspect join calculus.

Quantification. Remote pointcuts were first introduced in DJcutter and JAC, to specify on which hosts joint points should be detected. Remote pointcuts are also supported in AWED, ReflexD, and in the aspect join calculus, in a very similar fashion. Remote pointcuts can be seen as a necessary feature for distributed AOP (as opposed to using standard AOP in a distributed setting).

Hosts. Remote pointcuts bring about the necessity to refer to execution hosts. In DJcutter and AWED, hosts are represented as strings, while in ReflexD they are reified as objects that give access to the system properties of the hosts. The host model in ReflexD is therefore general and expressive, since host properties constitute an extensible set of metadata that can be used in the pointcuts to denote hosts of interest. In the aspect join calculus, we have not developed locations beyond the fact that they are first class values. A peculiarity is that locations are organized hierarchically, and can possibly represent finer-grained entities than in existing systems (for instance, a locality can represent an actor within a virtual machine within a machine). A practical implementation should consider the advantages of a rich host metadata model as in ReflexD. AWED and Re-flexD support dynamically-defined groups of hosts, as a means to deal with the distributed architecture in a more abstract manner than at the host level.

Weaving semantics. Most distributed AOP languages and systems adopt a synchronous aspect weaving semantics. This is most probably due to the fact that the implementation is done over Java/RMI, in which synchronous remote calls is the standard. Notably, AWED supports the ability to specify that some advices should be run asynchronously. The aspect join calculus is the dual: the default is asynchronous communication, but we can also express synchronous weaving (Section 5.2). In addition, we have developed the ability to customize the weaving semantics on a per-reaction basis. An interesting consequence of this granularity is that we are able to express opaque and observable reactions. Both kinds of reactions support stronger encapsulation and guarantees in presence of aspects, and therefore fit in the line of work on modular reasoning about aspects [START_REF] Bodden | Join point interfaces for safe and flexible decoupling of aspects[END_REF][START_REF] Bruno | EffectiveAdvice: discplined advice with explicit effects[END_REF][START_REF] Steimann | Types and modularity for implicit invocation with implicit announcement[END_REF][START_REF] Tabareau | A typed monadic embedding of aspects[END_REF].

Advanced quantification. DJcutter, AWED, and ReflexD support reasoning about distributed control flow, in order to be able to discriminate when a join point is in the (distributed) flow of a given method call. AWED also supports state-machine-like pointcuts, called stateful aspects, which are able to match sequences of events that are possibly unrelated in terms of control flow. However, stateful aspects per se do not support reasoning about causality; additional mechanisms are needed, for instance as developed in WeCa [START_REF] Leger | Modular and flexible causality control on the web[END_REF]. In Section 3.3, we describe how join points can capture their causality links, which can then be used for pointcut matching. While the synchronous communication pattern can be recognized in order to support a similar notion of distributed control flow, the causality tree model is much more general. An interesting venue for future work is to develop a temporal logic for pointcuts that can be used to reason precisely about causality. Temporal logic has been used in some aspect-oriented systems to perform semantic interface conformance checks [START_REF] Bodden | Tracechecks: Defining semantic interfaces with temporal logic[END_REF]. Causality in widely-asynchronous (distributed) contexts is a topic of major interest. It would be interesting to study how our approach relates to the notion of causality in the π-calculus proposed by Curti et al. in the context of modeling biochemical systems [START_REF] Curti | Causal π-calculus for biochemical modelling[END_REF].

Aspect deployment. DJcutter adopts a centralized architecture with an aspect host where all aspects reside and advices are executed. JAC supports distributed aspect deployment onto various containers with a consistency protocol between hosts, to ensure a global view of the aspect environment. Both AWED and ReflexD adopt a decentralized architecture, in which it is possible to execute advices in different hosts: multiple parallel advice execution in specific hosts is possible, and programmers can control where aspects are deployed. Re-flexD is more flexible than AWED in the localization of advices and in deployment, by supporting stand-alone aspect repositories to which a Reflex host can connect. The weaving registries mechanism we have described in Section 5.3 subsumes these mechanisms, and also adds support for controlling the openness of the distributed architecture.

JAC, AWED and Reflex support dynamic undeployment of aspects. While we have not introduced undeployment in this paper, it is trivial to add it to the core calculus. More interesting, in previous work we explore structured deployment through scoping strategies [START_REF] Tanter | Scoping strategies for distributed aspects[END_REF]. Scoping strategies make it possible to specify the computation that is exposed to a given aspect in a very precise manner. The model of scoping strategies relies on per-value and per-control-flow propagation of aspects; it would be not trivial, but interesting, to study how these strategies can be adapted to a chemical setting.

Parameter passing. In Java, remote parameter passing is by-copy, unless for remote objects that are passed byreference. ReflexD allows programmers to customize the remote parameter passing strategy for each parameter passed to a remote advice. The join calculus has a byreference strategy, where names act as references. It would be possible to add a by-copy mechanism in the aspect join calculus, by adding a rule to clone named definitions.

Conclusions

This article describes a formal foundation for distributed aspect-oriented programming based on a chemical calculus. More precisely, we extend an objective and distributed version of the join calculus with means to address crosscutting through pointcuts and advices. The semantics of the aspect join calculus is given both directly and by translation to the standard join calculus. The latter translation is proven correct by a bisimilarity argument, and is the basis for implementing the Aspect JoCaml language on top of JoCaml. The aspect join calculus exposes causality trees for join points, supports customized weaving semantics and decentralized aspect weaving. In particular, customized weaving supports strong encapsulation (some reactions can be totally hidden from aspects) and non-interference guarantees (some reactions can be restricted to observer aspects [START_REF] Rinard | A classification system and analysis for aspect-oriented programs[END_REF]).

This work shows that the main features of previous distributed AOP systems can be expressed by the few relatively simple constructs of the calculus, and that the calculus can even go beyond existing proposals. We believe the aspect join calculus can serve as a solid formal basis on top of which to explore and compare distributed aspect language features. A particular feature of interest, which we have not addressed so far, is dealing with failures. Fournet and Gonthier briefly describe an extension of the join calculus with partial failure and remote failure detection [START_REF] Fournet | The join calculus: a language for distributed mobile programming[END_REF]. The aspect join calculus can also serve as a basis to implement concurrent and distributed aspects in other languages for which a variant of the join calculus has been developed, such as Cω [START_REF] Benton | Modern concurrency abstractions for C ♯[END_REF] and Scala Joins [START_REF] Haller | Implementing joins using extensible pattern matching[END_REF]. Another interesting perspective is to study the application of aspects in chemical engines for Cloud computing.

  obj b = put(n) & empty() ▷ b.some(n) or get(r) & some(n) ▷ r.reply(n) & b.empty() in b.empty()

Fig. 5

 5 Fig. 5 Syntax of join points

Fig. 6

 6 Fig. 6 Definition of free names for aspects

Fig. 8

 8 Fig.8Tagging of causal history.

Fig. 9

 9 Fig. 9 Semantics of aspect weaving

Fig. 13

 13 Fig.[START_REF] Clifton | MiniMAO 1 : An imperative core language for studying aspect-oriented reasoning[END_REF] Objects registering their public weavers to an open aspect registry (white), and the weavers of their sensitive reactions to a closed registry with only two trusted aspects (grey).

Fig. 14

 14 Fig. 14 Cache class in Aspect JoCaml

(

  * create a permanent aspect registry *) let () = let _ = new a s pe ct _ re gi s tr y 12345 in while true do Thread . delay 1.0 done Then, a cache replication aspect can be registered to this aspect registry: (* register a cache replication aspect *) let () = let ip = 12345 in let dict = new Dict . dict ip in let buf = new cache ip dict in let repl = new replication ip buf in let _ = my_asp ip repl in while true do () done Finally, the execution of the cache process defined below is replicated on the machine where the aspect has been deployed: (* a cache process loop *) let () = let ip = 12345 in let dict = new Dict . dict ip in let z = new cache ip dict in let k

  get(k, r) & state(d) reg o dict.lookup(d, k, r) & c.state(d) or getDict(d) ▸ reg o c.state(d)

	in dict.create(c)

  The label k is declared as public, meaning that it is visible in a reaction join point. Conversely, a private label

	(* cache class *)
	class cache ip dict =
	dist_object ( self )
	reaction
	r_get at ip : ' observable
	state ( d ) & get (k , r ) =
	dict # lookup (d ,k , r ) & state ( d )
	or
	r_put at ip : ' observable
	state ( d ) & put (k , v ) =
	dict # update (d ,k ,v , getDict )
	or
	r_getDict at ip : ' opaque
	getDict ( d ) = state ( d )
	private label state
	public label get , put , getDict
	initializer spawn dict # create ( self # getDict )
	end
	)
	reaction react_k at ip : ' opaque k ( n ) =
	print_int ( n ); print_string ( " is read \ n " );0
	public label k
	end

The implementation of Aspect JoCaml, together with running examples, is available online at: https://tabareau.github.io/AJoCaml/

http://spring.io

http://www.jboss.org

http://cloudstack.apache.org/

This article builds upon a previous conference publication[START_REF] Tabareau | A theory of distributed aspects[END_REF]. Much of the text has been completely rewritten. The aspect join calculus has been simplified and clarified, in particular by removing the type system and the management of classes, because they are orthogonal to the extensions considered in this work. In addition, the technical treatment has been extended in many ways, including more expressive quantification, per-reaction weaving, and decentralized weaving. The translation from the aspect join calculus to the standard join calculus has been updated accordingly, as well as the proof of correctness of the translation. Finally, an implementation based on JoCaml is presented and provided online.

There is a good reason why we choose a variant of the join calculus with objects; we discuss it later in Section 3.4, once the basics of aspects in the calculus are established.

Acknowledgments

We thank the anonymous reviewers for their valuable and detailed suggestions on how to improve this article.