Thomas Given-Wilson

Daniele Gorla

Pattern Matching and Bisimulation

Concurrent Pattern Calculus (CPC) is a minimal calculus whose communication mechanism is based on a powerful form of symmetric pattern unification. However, the richness of patterns and their unification entails some flexibility in the challenge-reply game that underpins bisimulation. This leads to an ordering upon patterns that is used to define the valid replies to a given challenge. Such a theory can be smoothly adapted to accomplish other, less symmetric, forms of pattern matching (e.g. those of Linda, polyadic π-calculus, and πcalculus with polyadic synchronization) without compromising the coincidence of the two equivalences.

Introduction

Concurrent Pattern Calculus [START_REF] Given-Wilson | Concurrent pattern calculus[END_REF] is a minimal process calculus that uses symmetric pattern unification as the basis of communication. CPC's expressive power is obtained by extending the messages sent during interaction from traditional names to a class of patterns that are unified in an intensional manner (i.e., inspecting their internal structure). This unification supports equality testing and bi-directional communication in an atomic step.

The exploration of intensionality in the concurrent setting is inspired by the increased expressive power that the intensional S F-calculus has over λ-calculus [START_REF] Jay | A combinatory account of internal structure[END_REF]. Since intensionality, as captured by pattern matching, is more expressive in sequential computation, it is natural to explore the expressiveness of intensionality, as captured by pattern unification, in concurrent computation. Indeed, CPC formally generalises both the sequential intensional computation of S F-calculus and the traditional (nonintensional) concurrent computation of π-calculus [START_REF] Given-Wilson | Concurrent pattern unification[END_REF]. The expressive power of CPC is also testified to by the possibility of encoding some well-known process languages [START_REF] Given-Wilson | Concurrent pattern calculus[END_REF][START_REF] Given-Wilson | Concurrent pattern unification[END_REF]: π-calculus [START_REF] Milner | A calculus of mobile processes, part I/II[END_REF], Linda [START_REF] Gelernter | Generative communication in Linda[END_REF] and Spi-calculus [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF]. CPC's symmetric form of communication has similarities to Fusion [START_REF] Parrow | The fusion calculus: Expressiveness and symmetry in mobile processes[END_REF]; however, the two calculi are unrelated (neither one can be encoded in the other) [START_REF] Given-Wilson | Concurrent pattern calculus[END_REF][START_REF] Given-Wilson | Concurrent pattern unification[END_REF]. Finally, CPC has been implemented in [START_REF] Given-Wilson | Concurrent pattern calculus in bondi[END_REF].

The main features of CPC are illustrated in the following sample trade interaction:

(ν sharesID) ABCShares • sharesID • λx → charge x for sale | (ν bankAcc) ABCShares • λy • bankAcc → save y as proof -→ (ν sharesID)(ν bankAcc)( charge bankAcc for sale | save sharesID as proof )

The first line models a seller that will synchronise with a buyer, using the protected information ABCShares, and exchange its shares (sharesID) for bank account information to charge (bound to x). The second line models a buyer. Notice that the information exchange is bidirectional and simultaneous: sharesID replaces y in the (continuation of the) buyer and bankAcc replaces x in the (continuation of the) seller. Moreover, the two patterns ABCShares • sharesID • λx and ABCShares • λy • bankAcc also specify the details of the shares being traded, that must be matched for equality in the pattern matching as indicated by the syntax • .

Pattern unification in CPC is even richer than indicated in this example, as unification may bind a compound pattern to a single name; that is, patterns do not need to be fully decomposed in unification. For example, the bank account information could be specified, and matched upon, in much more detail. The buyer could provide the account name and number such as in the following pattern: (ν accName)(ν accNum) ABCShares • λy • (name • accName • number • accNum). This more detailed buyer would still match against the seller, now yielding charge name • accName • number • accNum for sale . Indeed, the seller could also specify a desire to only accept bank account information that includes a name and number with the following pattern: ABCShares •sharesID•( name •λa• number •λb) and continuation charge a b for sale . This would also match with the detailed buyer information by unifying name with name , number with number , and binding accName and accNum to a and b respectively. The second seller exploits the intensionality of CPC to only interact with a buyer whose pattern is of the right structure (four subpatterns) and contains the right information (the protected names name and number, and shared information in the other two positions). CPC is built up around this rich form of pattern unification by using three standard operators taken from the π-calculus: name restriction, parallel composition and replication (not used in this simple example).

The focus of this paper is the investigation of the behavioural theory for CPC. As usual in concurrency theory, this is done by first defining a notion of barbed congruence and then capturing this via a labelled bisimulation-based equivalence. The main difficulty relies in the richness of the pattern unification mechanism adopted, that entails some flexibility in the challenge-reply game underlying the definition of the bisimulation. For example, the challenge λx•λy can be replied to by λz, because of the non-fully decomposing form of pattern matching. (Such as the seller who accepts anything as bank account information.) Indeed, every pattern matching the challenge has the form p•q, where p and q are communicable (i.e., they do not contain protected names n nor binding names λw), yielding the substitution {p/x, q/y}. The same pattern also matches λz, now yielding the substitution {p • q/z}. Of course, for P λx•λy ----→ P to be simulated by Q λz -→ Q , it must be that {p/x, q/y}P is bisimilar to {p • q/z}Q . Another subtlety is in the unification of shared information n with protected information n . Since the latter is a request for the communicating party to also know this information, the two patterns unify. (Such as the more careful seller checking that the buyer provides name and number for a bank account.) These ideas are formalised via an ordering on patterns that characterises the valid replies to a given challenge: every pattern 'greater than' the challenge is a valid reply, provided that, by applying the resulting substitutions to the respective continuations, bisimilar processes are obtained.

The form of pattern unification adopted in CPC generalises other forms of pattern matching already presented in the literature. It is then desirable that CPC's theory and results can be adapted to such simpler forms. Section 4 shows that this job is rather straightforward for the form of pattern matching underlying Linda, for two simple extensions of Linda, for the polyadic π-calculus, and for the π-calculus with polyadic synchronization. This provides a complete behavioural theory for the languages adopting such forms of pattern matching. Moreover, for the π-calculus, the result coincides with the usual notions of barbed congruence and early bisimulation congruence; this can be seen as a confirmation of the validity of the theory presented here.

Concurrent Pattern Calculus

Suppose a countable set of names N (meta-variables n, m, x, y, z, . . . -even if in the examples symbolic names will be used). The patterns (meta-variables p, p , p 1 , q, q , q 1 , . . .) are built using names and have the following forms:

p ::= λx | x | x | p • p
Binding names λx denote information sought by a trader; variable names x represent such information. Protected names x represent recognised information that cannot be traded. A compound p • q combines the two patterns p and q; compounds are left associative.

Given a pattern p the sets of: variables names, denoted vn(p); protected names, denoted pn(p); and binding names, denoted bn(p), are as expected with the union being taken for compounds. The free names of a pattern p, written fn(p), is the union of the variable names and protected names of p. A pattern is well formed if its binding names are pairwise distinct and different from the free ones. All patterns appearing in the rest of this paper are assumed to be well formed.

As protected names are limited to recognition and binding names are being sought, neither should be communicable to another process. Thus, a pattern is communicable, able to be traded to another process, if it contains no protected or binding names. Protection of a name can be extended to a communicable pattern p by defining p • q = p • q .

A substitution σ is defined as a partial function from names to communicable patterns. The domain of σ is denoted dom(σ); the free names of σ, written fn(σ), is given by the union of the sets fn(σx) where x ∈ dom(σ). The names of σ, written names(σ), are dom(σ) ∪ fn(σ). Notationally, given two substitutions σ and θ, denote with θ[σ] the composition of σ and θ, with domain limited to the domain of σ, i.e. the substitution mapping every x ∈ dom(σ) to θ(σ(x)). For later convenience, define the identity substitution on a set of names X, written id X : it maps every name in X to itself.

Substitutions are applied to patterns as follows:

σx = σ(x) if x ∈ dom(σ) x otherwise σ x = σ(x) if x ∈ dom(σ) x otherwise σ(λx) = λx σ(p • q) = (σp) • (σq)
The symmetric matching (or unification) of two patterns p and q, written {p q}, attempts to unify p and q by generating substitutions for their binding names. When defined, the result is a pair of substitutions whose domains are the binding names of p and of q, respectively. The rules to generate the substitutions are:

{x x} = {x x } = { x x} = { x x } def = ({}, {}) {λx q} def = ({q/x}, {}) if q is communicable {p λx} def = ({}, {p/x}) if p is communicable {p 1 • p 2 q 1 • q 2 } def = (σ 1 ∪ σ 2 , ρ 1 ∪ ρ 2 ) if {p i q i } = (σ i , ρ i ) for i ∈ {1, 2}
Variable and protected names unify if they are the same name. A binding name unifies with any communicable pattern to produce a binding for its bound name. Two compounds unify if their corresponding components do; the resulting substitutions are given by taking the union of those produced by unifying the components (necessarily disjoint, as patterns are well-formed). Otherwise the patterns cannot be unified and the matching is undefined. Notice that pattern matching is deterministic because of left-associativity of compounds.

The processes of CPC are given by:

P ::= 0 | P | P | !P | (νx)P | p → P
The null process 0 is the inactive process; P | Q is the parallel composition of processes P and Q, allowing the two processes to evolve independently or by interacting; the replication !P provides as many parallel copies of P as desired; (νx)P declares a new name x, visible only within P and distinct from any other name. The traditional input and output primitives of process calculi are replaced by the case, viz. p → P, that has a pattern p and a body P. A case with the null process as the body may also be written by only specifying the pattern. For later convenience, n denotes a collection of names n 1 , . . . , n i ; for example, (νn 1 )(. . . ((νn i )P)) will be written (ν n)P.

The free names of processes, denoted fn(P), are defined as usual for all the traditional primitives and fn(p → P) = fn(p) ∪ (fn(P)\bn(p)) for the case, where the binding names of the pattern bind their free occurrences in the body.

The structural equivalence relation ≡ is defined just as in π-calculus [START_REF] Milner | The polyadic π-calculus: A tutorial[END_REF]: it includes α-conversion and its defining axioms are:

P | 0 ≡ P P | Q ≡ Q | P P | (Q | R) ≡ (P | Q) | R !P ≡ P | !P (νn)0 ≡ 0 (νn)(νm)P ≡ (νm)(νn)P P | (νn)Q ≡ (νn)(P | Q) if n fn(P)
The operational semantics of CPC is formulated via a reduction relation between pairs of processes. Its defining rules are:

(p → P) | (q → Q) -→ (σP) | (ρQ) if {p q} = (σ, ρ) P -→ P P | Q -→ P | Q P -→ P (νn)P -→ (νn)P P ≡ Q Q -→ Q Q ≡ P P -→ P
CPC has one interaction axiom, stating that, if the unification of two patterns p and q is defined and generates (σ, ρ), the substitutions σ and ρ are applied to the bodies P and Q, respectively. If the matching of p and q is undefined then no interaction occurs. The interaction rule is then closed under parallel composition, restriction and structural equivalence in the usual manner.

Behavioural Theory

This section follows a standard approach in concurrency to defining behavioural equivalences, beginning with a barbed congruence and following with a labelled transition system (LTS) and a definition of bisimulation for CPC. Some properties of patterns will be explored as a basis for showing coincidence of the semantics.

Barbed Congruence

The first crucial step is to characterise the interactions a process can participate in via barbs. Since a barb is an opportunity for interaction, a simplistic definition could be the following:

P ↓ iff P ≡ p → P | P , for some p, P and P

However, this definition is too strong: for example, (νn)(n → P) does not exhibit a barb according to [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], but it can interact with an external process, e.g. λx → 0. Thus, an improvement to (1) is as follows:

P ↓ iff P ≡ (ν n)(p → P | P ), for some n, p, P and P

Now, this definition is too weak. Consider (νn)( n → P): it exhibits a barb according to (2), but cannot interact with any external process. A further refinement on (2) could be:

P ↓ iff P ≡ (ν n)(p → P | P ), for some n, p, P , P s.t. pn(p) ∩ n = ∅ (3)
This definition is not yet the final one, as it is not sufficiently discriminating to have only a single kind of barb (the contexts in Definition 9 use two kinds of barbs, to define success and failure). Thus, like in CCS and π-calculus [START_REF] Milner | Barbed bisimulation[END_REF], barbs must be indexed, e.g. on some names that give an abstract account of the matching capabilities of the process. Because of the rich form of interactions, CPC barbs also include the set of names that may be tested for equality in an interaction, not just those that must be equal.

Definition 1 (Barb). Let P ↓ m mean that P ≡ (ν n)(p → P | P ) for some n, p, P and P such that pn(p) ∩ n = ∅ and m = fn(p)\ n.

Using this definition, a barbed congruence can be defined in the standard way [START_REF] Honda | On reduction-based process semantics[END_REF], by requiring three properties. Let denote a binary relation on processes and let a context C(•) be a process with the hole ' • ' replacing one instance of the null process.

Definition 2 (Barb preservation).

is barb preserving iff, for every (P, Q) ∈ , it holds that P ↓ m implies Q ↓ m . is reduction closed iff, for every (P, Q) ∈ , it holds that P -→ P implies Q -→ Q , for some Q such that (P , Q ) ∈ .

P (ν m)p ----→ P Q (ν n)q ---→ Q P | Q τ - → (ν m, n)(σP | ρQ ) {p q} = (σ, ρ) m ∩ fn(Q) = n ∩ fn(P) = ∅ m ∩ n = ∅ parext : P (ν n)p ---→ P P | Q (ν n)p ---→ P | Q ( n ∪ bn(p)) ∩ fn(Q) = ∅ parint : P τ - → P P | Q τ - → P | Q

Definition 4 (Context closure).

is context closed iff, for every (P, Q) ∈ and for every context C(•), it holds that (C(P), C(Q)) ∈ .

Definition 5 (Barbed congruence). Barbed congruence, , is the largest symmetric, barb preserving, reduction and context closed binary relation on processes.

Barbed congruence equates processes with the same behaviour, as captured by barbs: two equivalent processes must exhibit the same behaviours, and this property should hold along every sequence of reductions and in every execution context. This defines the strong version of barbed congruence; its weak counterpart can be obtained in the usual manner [START_REF] Milner | A calculus of mobile processes, part I/II[END_REF][START_REF] Milner | Barbed bisimulation[END_REF], with more complex contexts for proving the completeness theorem.

The problem in proving (strong/weak) barbed congruence is its closure under any context. As is typical we solve this by giving an easier to reason about coinductive (bisimulation-based) characterization using an alternate operation semantics; an LTS.

Labelled Transition System

The following is an adaption of the standard late LTS for the π-calculus [START_REF] Milner | A calculus of mobile processes, part I/II[END_REF]. Labels are defined as follows:

µ ::= τ | (ν n)p
Labels are used in transitions P µ -→ P between processes, whose defining rules are given in Figure 1. Rule case states that a case's pattern can be used to interact with external processes. Rule resnon is used when a restricted name does not appear in the names of the label: it simply maintains the restriction on the process after the transition. By contrast, rule resin is used when a restricted name occurs in the label: as the restricted name is going to be shared with other processes, the restriction is moved from the process to the label (this is called extrusion, by using a π-calculus terminology). Of course an extruded name cannot already be restricted, cannot be protected (as this would prevent interaction), and cannot be a binding name. Rule match defines when two processes can interact to perform an internal action: this can occur whenever the processes exhibit labels with unifiable patterns and with no possibility of clash or capture due to restricted names. Rule rep unfolds the replicated process to infer the action. Rule parint states that, if either process in a parallel composition can transition by an internal action, then the whole process can transition by an internal action. Rule parext is similar, but is used when the label is visible: when one of the processes in parallel exhibits an external action, then the whole composition exhibits the same external action, as long as the restricted or binding names of the label do not appear free in the parallel component that does not generate the label.

Note that α-conversion is always assumed to satisfy the side conditions whenever needed and the symmetric rules have been omitted for brevity.

The presentation of the LTS is concluded with the following two results. First, the LTS is structurally image finite, i.e. for every P and µ, there are finitely many ≡equivalence classes of µ-reducts of P (Proposition 1). Second, the τ's in the LTS induce the same operational semantics as the reductions (Proposition 2). Proposition 1. The LTS defined in Figure 1 is structurally image finite.

Proposition 2. If P τ -→ P then P -→ P . Conversely, if P -→ P then there exists P such that P τ -→ P ≡ P .

Bisimulation

The next step is to develop a bisimulation relation that equates processes with the same interactional behaviour as captured by the labels of the LTS. The complexity is that the labels for external actions contain patterns, and some patterns are 'more general' than others, in terms of their matching capabilities. Two examples can clarify the point.

Example 1. Consider the processes P = λx • λy → x • y and Q = λz → z. Every process that can interact with P (by exhibiting a pattern matching against λx • λy) can interact with Q, but not vice versa: e.g., n → 0 can interact with Q but not with P. In this sense, the pattern λz is considered 'more general' than λx • λy.

Example 2. Consider the processes P = n → 0 and Q = n → 0. Every process that can interact with P can interact with Q, but not vice versa: consider, e.g., λx → 0. Thus, the pattern n is considered 'more general' than n . Now define an order relation on patterns that can be used to develop the bisimulation. In most process calculi, a challenge is replied to with an identical action [START_REF] Milner | A calculus of mobile processes, part I/II[END_REF]. However, there are situations in which an exact reply would make the bisimulation equivalence too fine for characterising barbed congruence [START_REF] Amadio | On bisimulations for the asynchronous πcalculus[END_REF][START_REF] De Nicola | Basic observables for a calculus for global computing[END_REF]. This is due to the impossibility for the language contexts to force barbed congruent processes to execute the same action; in such calculi more liberal replies must be allowed, as here for CPC. To this aim, define σ as a normal substitution, except that it operates on binding names rather than on free ones. Formally:

σx = x σ x = x σ(λx) = σ(x) if x ∈ dom(σ) λx otherwise σ(p • q) = ( σp) • ( σq)
Definition 6. Let p, q, σ and ρ be such that bn(p) = dom(σ) and bn(q) = dom(ρ). Define inductively that p is compatible with q by σ and ρ, denoted p, σ q, ρ, whenever:

p, σ λy, { σp/y} if fn(p) = ∅ n, {} n, {} n , {} n , {} n , {} n, {} p 1 • p 2 , σ 1 ∪ σ 2 q 1 • q 2 , ρ 1 ∪ ρ 2 if p i , σ i q i , ρ i , for i ∈ {1, 2} .
The next result captures the idea behind the definition of compatibility: the patterns matched by p are a subset of the patterns matched by q. Lemma 1. p, σ q, ρ and {p r} = (σ, θ) implies {q r} = (ρ, θ).

Moreover, compatibility preserves information used for barbs, is stable under substitution composition, is reflexive and transitive. Proposition 3. If p, σ q, ρ then fn(p) = fn(q) and fn(σ) = fn(ρ). Moreover, vn(p) ⊆ vn(q) and pn(q) ⊆ pn(p). Lemma 2. If p, σ q, ρ then p, θ[σ] q, θ[ρ], for every θ. Proposition 4. Given p and σ such that dom(σ) = bn(p), then p, σ p, σ.

Proposition 5. p, σ q, ρ and q, ρ r, θ imply p, σ r, θ.

Definition 7 (Bisimulation).

A symmetric binary relation on processes is a bisimulation if, for every (P, Q) ∈ and P µ -→ P , it holds that:

-if µ = τ, then Q τ - → Q , for some Q such that (P , Q ) ∈ ; -if µ = (ν n)p, for (bn(p) ∪ n) ∩ fn(Q) = ∅,
then for all σ with dom(σ) = bn(p) and fn(σ) ∩ n = ∅ there exist q, Q and ρ such that Q

(ν n)q
---→ Q and p, σ q, ρ and (σP , ρQ ) ∈ .

Denote with ∼ the largest bisimulation closed under any substitution.

The definition is inspired by the early bisimulation congruence for the π-calculus [START_REF] Milner | A calculus of mobile processes, part I/II[END_REF]: first of all, to be a congruence, we need to consider its closure under all possible substitutions (otherwise, it would not be closed under prefixes). Then, for every possible instantiation σ of the binding names, there exists a proper reply from Q. Of course, σ cannot be chosen arbitrarily: it cannot use in its range names that were restricted in P. Also the action µ cannot be arbitrary, as in the π-calculus: its restricted and binding names cannot occur free in Q.

Differently from the π-calculus, however, the reply from Q can be different from the challenge from P: this is due to the fact that CPC contexts are not powerful enough to enforce an identical reply (as highligthed in Examples 1 and 2). Indeed, this notion of bisimulation allows a challenge p to be replied to by any compatible q, provided that σ is properly adapted (yielding ρ, as described by the compatibility relation) before being applied to Q . This feature somehow resembles the symbolic characterization of open bisimilarity given in [START_REF] Sangiorgi | A theory of bisimulation for the pi-calculus[END_REF][START_REF] Buscemi | Open bisimulation for the concurrent constraint picalculus[END_REF]. There, labels are pairs made up of an action and a set of equality constraints. A challenge can be replied to by a smaller (i.e. less constraining) set. However, the action in the reply must be the same (in [START_REF] Sangiorgi | A theory of bisimulation for the pi-calculus[END_REF]) or becomes the same once we apply the name identifications induced by the equality constraints (in [START_REF] Buscemi | Open bisimulation for the concurrent constraint picalculus[END_REF]).

Soundness and Completeness of Bisimulation

Soundness is proved by showing that the bisimilarity relation is included in barbed congruence; this is done by showing that ∼ is an equivalence, it is barb preserving, reduction closed and context closed. All the details can be found in [START_REF] Given-Wilson | Concurrent pattern calculus (extended version)[END_REF].

Theorem 1 (Soundness of bisimilarity). ∼ ⊆ .

Completeness is proved by showing that barbed congruence is a bisimulation. First, is to show that barbed congruence is closed under substitutions.

Lemma 3. If P Q then σP σQ, for every σ.

Second, is to show that, for any challenge, a proper reply can be yielded via closure under an appropriate context. When the challenge is an internal action, the reply is also an internal action; thus, the empty context suffices, as barbed congruence is reduction closed. The complex scenario is when the challenge is a pattern together with a set of restricted names, i.e., a label of the form (ν n)p. Observe that in the bisimulation such challenges also fix a substitution σ whose domain is the binding names of p.

First of all, define a notion of success and failure that can be reported. A fresh name w is used for reporting success, with a barb ↓ w indicating success, and ⇓ w indicating a reduction sequence that eventually reports success. Failure is handled similarly using the fresh name f . A process P succeeds if P ⇓ w and P ⇓ f ; P is successful if P ≡ (ν n)( w • p | P ), for some n, p and P such that w n and P ⇓ f . P becomes successful if it can reduce to a successful process. Now develop a reply for a challenge of the form ((ν n)p, id bn(p) ); the general setting (with an arbitrary σ) will be recovered by relying on Lemma 2. The context for forcing a proper reply is developed in three steps. The first step presents the specification of a pattern and a set of names N (to be thought of as the free names of the processes being compared for bisimilarity); this is the information required to build a reply context. The second step develops auxiliary processes to test specific components of a pattern, based on information from the specification. The third step combines these into a reply context that becomes successful if and only if it interacts with a process that exhibits a proper reply to the challenge. In what follows, we use the first projection fst(-) and second projection snd(-) of a set of pairs. Definition 10. A reply context C N p (•) for the challenge ((ν n)p, id bn(p) ) with a finite set of names N such that n is disjoint from N is defined as follows:

C N p (•) def = char N (p) | •
It can be proved (see [START_REF] Given-Wilson | Concurrent pattern calculus (extended version)[END_REF]) that the minimum number of reductions required for C N p (Q) to become successful (for any Q) is the number of reduction steps for θ(tests N F,R ) to become successful plus 1; this number only depends on N and p, i.e. not on θ. Denote this number as Lb(N, p). The main feature of C N p (•) is described by the following key Lemma.

Lemma 7. Suppose given a challenge ((ν n)p, id bn(p) ), a finite set of names N, a process Q and fresh names w and f such that

( n ∪ {w, f }) ∩ N = ∅ and (fn((ν n)p) ∪ fn(Q)) ⊆ N. If Q (ν n)q
---→ Q and there exists ρ such that p, id bn(p) q, ρ, then

C N p (Q) -→ k (ν n)(ρQ | w • n | Z),
where k = Lb(N, p) and Z 0. Conversely, if C N p (Q) becomes successful in Lb(N, p) reduction steps, then there exist q, Q and ρ such that Q

(ν n)q ---→ Q and p, id bn(p)
q, ρ.

The last result needed for proving Theorem 2 is an auxiliary Lemma that allows us to remove success and dead processes from both sides of a barbed congruence, while also opening the scope of the names exported by the success barb.

Lemma 8. Let (ν m)(P | w • m | Z) (ν m)(Q | w • m | Z)
, for w fn(P, Q, m) and Z 0; then P Q.

Theorem 2 (Completeness of the bisimulation). ⊆ ∼.

On Variations of Pattern Matching

The form of pattern unification used so far in CPC is very rich. More limited forms of pattern matching have been used in the literature; as shown below, they can all be adopted in our language without compromising the coincidence of barbed congruence and bisimilarity.

The first variant is the form of pattern matching used in Linda [START_REF] Gelernter | Generative communication in Linda[END_REF]. Differently from CPC, Linda distinguishes between input and output patterns (the latter are usually called tuples in a tuplespace):

p ::= π | π ::= λx | x | π • π ::= x | •
Thus, communication is asymmetric; consequently, the pattern matching function is defined only between an input and an output pattern and yields a single substitution. It is defined as:

{ x x} def = {} {λx n} def = {n/x} {π • π • } def = {π } ∪ {π } (4)
From the second rule, it is apparent that communicable patterns in Linda are single variable names. The operational rules for matching in the reductions and in the LTS are the following:

(π → P) | ( → Q) -→ σP | Q if {π } = σ P π -→ P Q (ν n) ----→ Q P | Q τ - → (ν n)(σP | Q ) {π } = σ n ∩ fn(P) = ∅
The theory of bisimulation is simplified in this setting, as is the identity. Barbed congruence can be defined as in Section 3.1 and the two equivalences do coincide.

Two interesting extensions of Linda's pattern matching (intermediate between Linda's and CPC's ones) are:

1. Accept a "non-fully decomposing" form of pattern matching; e.g., λx can match n • m. In this case, it suffices to modify the definition of pattern matching by generalizing the second axiom in (4) to

{λx n 1 • . . . • n k } def = {n 1 • . . . • n k /x} (i.e.
, by rolling back to the original definition of communicable patterns as sequences of variable names) and by defining as in Definition 6, except for the fourth axiom (that must be ignored). 2. Allow the output process to specify which names can be passed and which ones can only be used for testing equality; e.g., n • m can be matched by λx • m , but not by λx • λy. In this case, output patterns are defined as

::= x | x | •
This is resolved by adding to (4) the axiom { x x } def = {} and by defining as in Definition 6, except for the first axiom (that must be ignored).

In both cases, reductions and LTS are like Linda's ones; barbed congruence and bisimulation are defined as in Section 3 and, again, they do coincide.

Another well-known form of pattern matching is the one underlying the polyadic π-calculus [START_REF] Milner | The polyadic π-calculus: A tutorial[END_REF]. In this case, (input and output) patterns have the form

π ::= a • λx 1 • . . . • λx k ::= a • n 1 • . . . • n k
for any k > 0 (these are usually written as a(x 1 , . . . , x k ) and ā(n 1 , . . . , n k )). Now pattern matching is defined as in ( 4), but with { x x } def = {} in place of the first axiom. Reductions, LTS and compatibility are like in Linda. Notice that the first two relations are the usual ones for the polyadic π-calculus; similarly, the bisimulation arising in this framework is the same as the standard early bisimulation congruence defined for the calculus. It is worth noticing that the barbs we exploit are different from the traditional ones for the π-calculus [START_REF] Milner | Barbed bisimulation[END_REF], where only the channel and the kind of action (either input or output) are observed. In our formulation of the polyadic π-calculus, input and output barbs can be usually distinguished: a • λx generates ↓ {a} whereas a • n generates ↓ {a,n} (the two are indistinguishable only if n = a). In general, our barbs are more informative than π-calculus' ones, since they also observe the argument of the output. However, since this barbed congruence coincides with the early bisimulation (that, in turn, coincides with the barbed congruence relying on the "standard" π-calculus' barbs), by transitivity we obtain that the two kinds of barbs yield the same congruence.

Similarly, also the form of pattern matching underlying the π-calculus with polyadic synchronization [START_REF] Carbone | On the expressive power of polyadic synchronisation in picalculus[END_REF] can be easily rendered. It suffices to take

π ::= a 1 • . . . • a k • λx ::= a 1 • . . . • a k • n (usually written a 1 • . . . • a k (x) and a 1 • . . . • a k (n))
. Pattern matching, reductions, LTS and compatibility are then the same as in polyadic π-calculus.

5 Conclusions and Future Work CPC demonstrates the expressive power possible with a minimal process calculus whose interaction is defined by symmetric pattern unification. The behavioural theory required to capture CPC turns out to have some interesting properties based on patterns and pattern matching. Perhaps, the most curious one is that a symmetric relation (viz., bisimilarity) is defined by an (asymmetric) ordering upon patterns. Indeed, the resulting bisimulation can be smoothly and modularly adapted to cope with other forms of pattern matching and other process calculi. Related work. To the best of our knowledge, there are very few notions of behavioural equivalences for process calculi that rely on pattern matching. We start with a few calculi based on a Linda-like pattern matching. A first example is [START_REF] De Nicola | A process algebra based on linda[END_REF], where the authors develop a testing framework; however, no coinductive and label-based equivalence is provided. Another paper where a Linda-like pattern matching is explored for bisimulation is [START_REF] De Nicola | Basic observables for a calculus for global computing[END_REF]; however, there the focus is on the distribution and connectivity of processes and, consequently, the pattern matching is simplified by relying on patterns of length 1. A similar choice is taken in other works, e.g. [START_REF] Busi | A process algebraic view of linda coordination primitives[END_REF][START_REF] Ciancarini | Towards a calculus for generative communication[END_REF][START_REF] De Boer | Asynchronous communication in process algebra[END_REF]. Of course, this choice radically simplifies the theory.

Recently, Psi [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF] has emerged as a rich framework that can encode different process calculi, including calculi with sophisticated forms of pattern matching. However, CPC and Psi are uncomparable: CPC cannot encode formulae (e.g. the indirect computation of channel equality), while Psi cannot encode self-matching processes (same as π, see [START_REF] Given-Wilson | Concurrent pattern calculus[END_REF]). The same holds for the applied π-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], because of the presence of active substitutions.

A more complex notion of bisimulation is the one for the Join calculus [START_REF] Fournet | The reflexive cham and the join-calculus[END_REF] given in [START_REF] Fournet | Bisimulations in the join-calculus[END_REF]. The difficult part lays in the definition of the LTS, since some names can be marked as visible from outside their definition and, consequently, interact with the execution context. The definition of bisimilarity is then standard and, hence, the interplay with pattern matching is totally hidden within the LTS. We prefer to make it explicit in the bisimulation, both to keep the LTS as standard as possible and for showing the exact impact that pattern matching has on the semantics of processes. By the way, the form of pattern matching used in Join cannot be rendered in CPC. Indeed, in a process like def a(x) | b(y) P in R, process R can independently produce the outputs on a and b needed to activate P. This would correspond to some form of "unordered and multiparty pattern matching" that is far from the design choices of CPC.

Other complex notions of bisimulation equivalences for process calculi are [START_REF] Boreale | Proof techniques for cryptographic processes[END_REF][START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF]. However, these exploit environmental knowledge, whereas in our work we do not have such knowledge and need only satisfy compatibility.

Future work. One interesting path of further development is to introduce types into CPC and extend the pattern unification mechanism by taking types into account, as done e.g. in [START_REF] Castagna | Patterns and types for querying xml documents[END_REF]. The study of typed equivalences would then be the most natural path to follow, by combing the theory in this paper with the assumed types. Another intriguing direction is the introduction of richer forms of pattern matching, based, e.g., on regular expressions [START_REF] Hosoya | Regular expression pattern matching for XML[END_REF]; in this case, it would be very challenging to devise the ordering on patterns that defines the 'right' bisimulation. A natural way to follow is Kozen's axiomatization for inclusion of regular language [START_REF] Kozen | A completeness theorem for kleene algebras and the algebra of regular events[END_REF]. Indeed, in this proof system, a regular expression e 1 is smaller than e 2 if and only if every string belonging to the language generated by e 1 also belongs to the language generated by e 2 . This corresponds to the same intuition as our ordering on patterns (Lemma 1), once we consider the language generated by a pattern as the set of patterns that it matches, together with the associated substitutions.

  ,m)p -----→ P m ∈ vn(p) \ ( n ∪ pn(p) ∪ bn(p)) rep : !P | P µ

Fig. 1 .

 1 Fig. 1. LTS (the symmetric version of parint and parext have been omitted)

NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.

Definition 8. The specification spec N (p) of a pattern p with respect to a finite set of names N is defined as follows:

where F p F q denotes F p ∪ F q , provided that fst(F p ) ∩ fst(F q ) = ∅ (a similar meaning holds for R p R q ).

Given a pattern p, the specification spec N (p) = p , F, R of p with respect to a set of names N has three components: (1) p , called the complementary pattern, is a pattern used to ensure that the context interacts with a process that exhibits a pattern compatible with p; (2) F is a collection of pairs (x, n) made up by a binding name in p and the expected (free) name it will be bound to; finally, (3) R is a collection of pairs (x, n) made up by a binding name in p and the expected (restricted) name it will be bound to. Observe that can be assumed p well formed as all binding names can be taken as (pairwise) different.

From now on, adopt the following notation:

where x = {x 1 , . . . , x i } = fst(R) and y = {y 1 , . . . , y j } = fst(F) ∪ fst(R).

Although the details of the tests are omitted here (see [START_REF] Given-Wilson | Concurrent pattern calculus (extended version)[END_REF] for details), their behaviour is described by the following Lemmas. Lemma 4. Let θ be such that {n, w} ∩ dom(θ) = ∅; then, θ(free(x, n, w)) succeeds if and only if θ(x) = n. Lemma 5. Let θ be such that (N ∪ {w, f }) ∩ dom(θ) = ∅; then, θ(rest N (x, w)) succeeds if and only if θ(x) ∈ N \ N. Lemma 6. Let θ be such that (snd(R) ∪ {w, f, m}) ∩ dom(θ) = ∅; then, θ(equality R (x, m, w)) succeeds if and only if, for every (y, n) ∈ R, m = n if and only if θ(x) = θ(y).


Junwhan Kim
email: junwhan@vt.edu

Roberto Palmieri
email: robertop@vt.edu

Binoy Ravindran

Scheduling Open-Nested Transactions in Distributed Transactional Memory

Distributed transactional memory (DTM) is a powerful concurrency control model for distributed systems sparing the programmer from the complexity of manual implementation of lock-based distributed synchronization. We consider Herlihy and Sun's dataflow DTM model, where objects are migrated to invoking transactions, and the open nesting model of managing inner (distributed) transactions. In this paper we present DATS, a dependency-aware transactional scheduler, that is able to boost the throughput of open-nested transactions reducing the overhead of running expensive compensating actions and abstract locks in the case of outer transaction aborts. The contribution of the paper is twofold: (A) DATS allows the commutable outer transactions to be validated concurrently and (B) allows the non-commutable outer transactions, depending on their inner transactions, to commit be committed before others without dependencies.

Introduction

Transactional Memory (TM) is an emerging innovative programming paradigm for transactional systems. The main benefit of TM is synchronization transparency in concurrent applications. In fact, leveraging the proven concept of atomic and isolated transactions, TM spares programmers from the pitfalls of conventional manual lock-based synchronization, significantly simplifying the development of parallel and concurrent applications. Moreover lock-based concurrency control suffers from programmability, scalability, and composability challenges [START_REF] Herlihy | A flexible framework for implementing software transactional memory[END_REF] and TM promises to alleviate these difficulties. In TM, the developer simply organizes read and write operations on shared objects as transactions and leaves the responsibility of executing those transactions to the TM, ensuring atomicity, consistency and isolation. Two transactions conflict if they access to the same object and at least one access is a write. The contention manager, the component in TM responsible for resolving conflicts among concurrent transactions, typically aborts one and allows the other to commit, yielding (the illusion of) atomicity. Aborted transactions are typically re-started after rollingback the changes in memory.

The Transaction Scheduler (TS) is the component that supports the contention manager in making a decision on how to resolve conflicts (which transaction to abort). The goal of the TS is to order concurrent transactions as to avoid or minimize conflicts (and thereby aborts).

The hazards of manual implementation of lock-based concurrency control increases in distributed settings due to an additional synchronization level among nodes in the system. Distributed STM (DTM) has been motivated as an alternative to distributed lock-based concurrency control. DTM can be classified based on the system architecture: cache-coherent DTM (cc DTM) [START_REF] Herlihy | Distributed transactional memory for metric-space networks[END_REF][START_REF] Saad | HyFlow: a high performance distributed software transactional memory framework[END_REF], in which a set of nodes communicate by message-passing links over a communication network, and a cluster model (cluster DTM) [START_REF] Couceiro | D2STM: Dependable distributed software transactional memory[END_REF][START_REF] Palmieri | Osare: Opportunistic speculation in actively replicated transactional systems[END_REF], in which a group of linked computers work closely together to form a single computer. cc DTM uses a cache-coherence protocol [START_REF] Demmer | The arrow distributed directory protocol[END_REF][START_REF] Herlihy | Distributed transactional memory for metric-space networks[END_REF] to locate and move objects in the network.

Support for nesting (distributed) transactions is essential for DTM, for the same reasons that they are so for multiprocessor TM -i.e., code composability, performance, and fault-management [START_REF] Moss | Nested transactional memory: model and architecture sketches[END_REF][START_REF] Turcu | On open nesting in distributed transactional memory[END_REF][START_REF] Turcu | On closed nesting in distributed transactional memory[END_REF]. Three types of nesting have been studied for multiprocessor TM: flat, closed, and open. If an inner transaction I is flat-nested inside its outer transaction A, A executes as if the code for I is inlined inside A. Thus, if I aborts, it causes A to abort. If I is closed-nested inside A [START_REF] Moss | Open-nested transactions: Semantics and support[END_REF], the operations of I only become part of A when I commits. Thus, an abort of I does not abort A, but I aborts when A aborts. Finally, if I is open-nested inside A, then the operations of I are not considered as part of A. Thus, an abort of I does not abort A, and vice versa.

The differences between the nesting models are shown in Figure 1, in which there are two transactions containing a nested-transaction. With flat nesting, transaction T 2 cannot execute until transaction T 1 commits. T 2 incurs full aborts, and thus has to restart from the beginning. Under closed nesting, only T 2 's inner-transaction needs to abort and be restarted while T 1 is still executing. The portion of work T 2 executes before the data-structure access does not need to be retried, and T 2 can thus finish earlier. Under open nesting, T 1 's inner-transaction commits independently of its outer, releasing memory isolation over the shared data-structure. T 2 's inner-transaction can therefore proceed immediately, thus enabling T 2 to commit earlier than in both closed and flat nesting.

The flat and closed nested models have a clear negative impact on large monolithic transactions in terms of concurrency. In fact, when a large transaction is aborted all its flat/closed-nested transactions are also aborted and rolledback, even if they do not conflict with any other transaction. Closed nesting potentially offers better performance than flat nesting because the aborts of closed-nested inner transactions do not affect their outer transactions. However the open-nesting approach outperforms both in terms of concurrency allowed. When an open-nested transaction commits, its modifications on objects become immediately visible to other transactions, allowing those transactions to start using those objects without a conflict, increasing concurrency [START_REF] Moss | Nested transactional memory: model and architecture sketches[END_REF]. In contrast, if the inner transactions are closed-or flat-nested, then those object changes are not made visible until the outer transaction commits, potentially causing conflicts with other transactions that may want to use those objects.

To achieve high concurrency in open nesting, inner transactions have to implement abstract serializability [START_REF] Yang | Open nesting in software transactional memory[END_REF]. If concurrent executions of transactions result in the consistency of shared objects at an "abstract level", then the execu-tions are said to be abstractly serializable. If an inner transaction I commits, I's modifications are immediately committed in memory and I's read and write sets are discarded. At this time, I's outer transaction A does not have any conflict with I due to memory accessed by I. Thus, programmers consider the internal memory operations of I to be at a "lower level" than A. A does not consider the memory accessed by I when it checks for conflicts, but I must acquire an abstract lock and propagates this lock for A. When two operations try to acquire the same abstract lock, the open nesting concurrency control is responsible for managing this conflict (so this is defined "abstract level"). level of abstraction. Open-nested transactions are allowed to commit to the shared memory independently of their parent transactions, optimistically assuming that the parent will commit. If however the parent aborts, the open-nested transaction needs to run compensating actions to undo its effect. The compensating action does not simply revert the memory to its original state, but runs at the higher level of abstraction. For example, to compensate for adding a value to a set, the system would remove that value from the set. Although open-nested transactions breach the isolation property, this potentially enables significant increases in concurrency and performance.

We illustrate the differences between the three nesting models in Figure 1. Here we consider two transactions, which access some shared data-structure using a subtransaction. The data-structure accesses conflict at the memory level, but the conflict is not fundamental (we will explain fundamental conflicts later, in Section 3.3), and there are no further conflicts in either T 1 or T 2 . With flat nesting, transaction T 2 can not execute until transaction T 1 commits. T 2 incurs full aborts, and thus has to restart from the beginning. Under closed nesting, only T 2 's sub-transaction needs to abort and be restarted while T 1 is still executing. The portion of work T 2 executes before the d access does not need to be retried, and T 2 ca earlier. Under open nesting, T 1 's sub-transac independently of its parent, releasing memory the shared data-structure. T 2 's sub-transaction immediately after that, thus enabling T 2 to co than in both closed and flat nesting.

Besides providing support for code composa transactions are attractive when transaction a tively used for implementing specific behav ample, conditional synchronization can be aborting the current transaction if a pre-con met, and only scheduling the transaction to be the pre-condition is met (for example, a deque would wait until there is at least one element in shown in Figure 2). Aborts can also be used fo agement: a program may try to perform an acti case of failure, change to a different strategy (tr ample in Figure 3). In both these scenarios, per be improved with nesting by aborting and retr inner-most sub-transaction.

Previous DTM works have largely ignored partial aborts and nesting [START_REF] Ansari | Steal-on-abort: Improving transactional memory performance through dynamic transaction reordering[END_REF][START_REF] Attiya | Transactional scheduling for read-dominated workloads[END_REF][START_REF] Kim | On transactional scheduling in distributed transactional memory systems[END_REF][START_REF] Moravan | Supporting nested transactional memory in logTM[END_REF]. We ex algorithm [START_REF] Moravan | Supporting nested transactional memory in logTM[END_REF] If an outer transaction (with opennested inner transactions) aborts, all of its (now committed) open-nested inner transactions must rollback and their actions must be undone to ensure transaction serializability. Thus, with the open nesting model, programmers must provide a compensating action for each open-nested transaction [START_REF] Agrawal | Memory models for opennested transactions[END_REF]. In scenarios in which outer transactions increasingly encounter conflicts after that a large number of their open-nested transactions have committed (e.g., long running transactions), the overall performance could collapse and all the benefits of the open-nesting approach vanish due to the processing of compensating actions to undo the modifications provided by the committed open-nested transactions. In closed nesting, since closed-nested transactions are not committed in memory until the outer transaction commits (nested transactions' changes are visible only to the outer), no undo (e.g., compensation) is required. Moreover, in scenarios in which the load of the system is high, the probability of having concurrent conflicting transactions grows and with it the probability to abort outer transactions with a number of open-nested transactions (already committed in memory). Aborting outer transactions with dependencies, instead of alleviating the load of the system, will increase it due to the execution of compensating actions, possibly bringing the system toward dangerous states.

We focus on these problems: the overhead of compensating actions and abstract locks in the open-nested model. Our goal is to boost performance of nested transactions in DTM by increasing concurrency and reducing the aforementioned overhead through transactional scheduling. For these reasons, we designed a scheduler, called the Dependency-Aware Transactional Scheduler (or DATS). DATS is responsible for helping the concurrency control minimizing the number of outer-transactions aborted. In order to do that, DATS relies on the notions of commutable transactions and transaction dependencies. Commutable Transactions. Two transactions are defined as commutable if they conflict and they leave the state of the shared data-set consistent even if validated and committed concurrently. A very intuitive example of commutativity is when two operations, call1(X) and call2(X), both access the same object X but different fields of X (See Section 3.2 for discussion about commutativity). Transaction Dependencies. An outer transaction materializes dependencies with its inner transactions if (i) the inner transactions accesses the outer writeset for performing local computation or (ii) the results of outer processing are used to decide whether or not to invoke an inner transaction.

DATS is able to detect commutable transactions and validate/commit them, avoiding useless aborts. In the case of non-commutable transactions, DATS identifies how much each outer transaction depends on its inner transactions and schedules the outer transaction with the highest dependency to commit before other outer transactions with lower or no dependencies. Committing this outer transaction prevents its dependent inner transactions from aborting and reduces the number of compensating actions. Moreover, even though the other outer transactions abort, their independent inner transactions will be preserved, resulting in a reduced number of compensating actions and abstract locks without violating the correctness of the object.

We implemented DATS in a Java DTM framework, called HyFlow [START_REF] Saad | Supporting STM in distributed systems: Mechanisms and a Java framework[END_REF], and conducted an extensive experimental study involving both micro-benchmarks (e.g., Hash Table, Skip-, Linked-List) and a real application benchmark (TPC-C). Our study reveals that throughput is improved by up to 1.7× in microbenchmarks and up to 2.2× in TPC-C over open-nested DTM without DATS. To the best of our knowledge, DATS is the first ever scheduler that boosts throughput with open-nested transactions in DTM.

The rest of the paper is organized as follows. We present preliminaries of the DTM model and state our assumptions in Section 2. We describe DATS and analyze its properties in Section 3. Section 4 reports our evaluation. We overview past and related efforts in Section 5, and Section 6 concludes the paper.

Preliminaries and System Model

We consider a distributed system which consists of a set of nodes N = {n 1 , n 2 , • • • } that communicate with each other by message-passing links over a network. Similar to [START_REF] Herlihy | Distributed transactional memory for metric-space networks[END_REF], we assume that the nodes are scattered in a metric space. Transaction model. A set of shared objects O = {o 1 , o 2 , . . .} are distributed in the network among nodes. A transaction is defined as a sequence of requests, each of which is a read or write operation request to an a single object in O. An execution of a transaction is a sequence of timed operations that ends by either a commit (success) or an abort (failure). A transaction is in three possible states: live, aborted, or committed. Each transaction has a unique identifier and is invoked by a node in the system. We consider the data flow DTM model [START_REF] Herlihy | Distributed transactional memory for metric-space networks[END_REF]. In this model, transactions are immobile and objects move from node to node to invoking transactions. Each node has a TM proxy that provides interfaces allowing the local application to interact with the other proxies located on other nodes. When a transaction T i at node n i requests object o j , the TM proxy of n i first checks whether o j is in its local cache. If the object is not present, the proxy invokes a distributed cache-coherence protocol (CC) to fetch o j in the network. Atomicity, Consistency, and Isolation. We use the Transactional Forwarding Algorithm with Open Nesting (TFA-ON) [START_REF] Turcu | On open nesting in distributed transactional memory[END_REF], which extends the TFA algorithm [START_REF] Saad | Supporting STM in distributed systems: Mechanisms and a Java framework[END_REF] (which originally does not provide any transaction nesting support), to manage flat, closed and open-nested transactions. TFA provides early validation of remote objects, guarantees a consistent view of shared objects between distributed transactions, and ensures atomicity for object operations in presence of asynchronous clocks. The early validation of remote objects means that a transaction validated first commits its objects successfully. Validation in distributed systems includes global registration of object ownership. TFA is responsible for caching local copies of remote objects and changing the ownership.

TFA-ON changes the scope of object validations. The behavior of open-nested transactions under TFA-ON is similar to the behavior of regular transactions under TFA. In addition, TFA-ON manages the abstract locks and the execution of commit and compensating actions [START_REF] Turcu | On open nesting in distributed transactional memory[END_REF]. To provide conflict detection at the abstract level, an abstract locking mechanism has been integrated into TFA-ON. Abstract locks are acquired only at commit time, once the inner transaction is verified to be conflict free at the low level. The commit protocol requests the abstract lock of an object from the object owner and the lock is released when its outer transaction commits. To abort an outer transaction properly, a programmer provides an abstract compensating action for each of its inner transaction to revert the data-structure to its original semantic state.

TFA-ON is the first ever implementation of a DTM system with support for open-nested transactions [START_REF] Turcu | On open nesting in distributed transactional memory[END_REF]. DATS has been integrated in TFA-ON.

3 The DATS Scheduler When the inner transaction commits, its modification becomes immediately visible for other transactions. Thus, if the inner transaction commits, and its outer transaction T 1 or T 2 aborts, a delete operation as a compensating action (described in OnAbort) executes. Let us assume that T 2 aborts, and OnAbort ex- ecutes. Even though T 2 's inner transaction (INSERT) does not depend on its delete operation, unlike T 1 , OnAbort will execute. Thus, the conflict of object "tree-2" in T 2 causes the execution of compensating action on object "tree-1" in INSERT. The INSERT operation acquires the abstract lock again when it restarts. Finally, whenever an outer transaction aborts, its inner transaction must execute a compensating action, regardless of the operation's dependencies.

This drawback is particularly evident in distributed settings. In fact, distributed transactions typically have an execution time several orders of magnitude bigger than in a centralized STM, due to communication delays that are incurred in requesting and acquiring objects [START_REF] Kim | Scheduling closed-nested transactions in distributed transactional memory[END_REF]. If an outer transaction aborts, clearly the impact of the time needed for running compensating actions and for acquiring abstract locks for distributed open-nested transactions is exacerbated due to the communication overhead. Moreover it increases the likelihood of conflicts, drastically reducing concurrency and degrading performance.

Motivated by these observations, we propose the DATS scheduler for opennested DTM. DATS, for each outer transaction T a , identifies the number of inner transactions depending from T a and schedules the outer transactions with the greatest number of dependencies to validate first and (hopefully) commit. This behavior permits the transactions with high compensation overhead to commit; the remaining few outer transactions that are invalidated will be restarted excluding their independent inner transactions to avoid useless compensating actions and acquisition of abstract locks. In the next subsection the meaning of dependent transactions for DATS will be described.

Abstract and Object Level Dependencies

We consider two types of dependencies among transactions. (ALD) and it indicates the dependency between an outer transaction and its inner transactions at an abstract level. We define the dependency level (DL) as the number of inner transactions that will execute OnAbort when the outer transactions abort. For example, T 1 illustrated in Figure 2 depends on its INSERT due to the deleted variable. Thus, DATS detects a dependency between T 1 and its INSERT (its inner transaction) because the delete operations in T 1 shares the variable deleted with the conditional if statement declared for executing IN-SERT. In this case, the DL=1 for T 1 . Conversely, T 2 executes INSERT without checking any pre-condition so its DL=0 because T 2 does not have dependencies with its inner transactions. The purpose of the abstract level dependency is to avoid unnecessary compensating actions and abstract locks. Even though T 2 aborts, OnAbort in INSERT will not be executed because its DL=0, and the compensating action will not be processed. Meanwhile, executing OnAbort implies running INSERT and acquiring the abstract lock again when T 2 restarts. Summarizing, aborting outer transactions with smaller DLs leads to a reduced number of compensating actions and abstract lock acquisitions. Such identification can be done automatically at run-time by DATS using byte-code analysis or relying on explicit indication by the programmer. The first scenario is completely transparent from the application point of view but in some cases could add additional overhead. The second approach, although it requires the collaboration of the developer, is more flexible because it allows the programmer to bias the behavior of the scheduler. In fact, even though the logic of an outer transaction reveals a certain number of dependencies, the programmer may want to force running compensations in case of an abort. This can be done by simply changing the value of DL associated to the outer transaction. Object Level Dependency. The second is called object level dependency (OLD) and it indicates the dependency among two or more concurrent transactions accessing the same shared object. For example, in Figure 2, T 1 depends on T 2 because they share the same object "tree-2". If T 1 and T 2 work concurrently, a conflict between them occurs. However, delete(7) of T 1 and delete(9) of T 2 commute because they are two operations executing on the same object ("tree-2") but accessing different items (or fields when applicable) of the object (item "7" and item "9"). We recall that, two operations commute if applying them in either order they leave the object in the same state and return the same responses [START_REF] Herlihy | Transactional boosting: a methodology for highly-concurrent transactional objects[END_REF]. DATS detects object level dependency at transaction commit phase, splitting the validation phase into two. Say T a is the transaction that is validating. In the first phase, T a checks the consistency of the objects requested during the execution. If a concurrent transaction T b has requested and already committed a new version of some object requested by T a , then T a aborts in order to avoid isolation corruption. After the successful completion of the first phase of T a 's validation, DATS detects the object level dependencies among concurrent transactions that are validating with T a in the second phase. To do that, DATS relies on the notion of commutativity already introduced at the end of Section 1. Suppose T a and T b are conflicting transactions but simultaneously validating. If all of T a 's operations commute with all of T b 's operations, they can proceed to commit together avoiding a useless abort. Otherwise one of T a or T b must be aborted. This scheduler is in charge of the decision (see next sub-section).

In order to compute commutativity, DATS joins two supports. In the first, the programmer annotates each transaction class with the fields accessed. The second is a field-based timestamping mechanism, used for checking the field-level invalidation. The goal is to reduce the granularity of the timestamp from object to field. With a single object timestamp, it is impossible to detect commutativity because of fields modifications. In fact, writes to different fields of the same object are all reflected with the increment of the same object timestamp. In order to do that efficiently, DATS exploits the annotations provided by the developer on the fields accessed by the transaction to directly point only to the interested fields (instead of iterating on all the object fields, looking for the ones modified). On such fields, it uses field-based timestamping to detect object invalidation.

The purpose of the object level dependency is to enhance concurrency of outer transactions. Even though inner transactions terminate successfully, aborting their outer transactions affects these inner transactions (due to compensation). Thus, DATS checks for the commutativity of conflicting transactions and permits them to be validated, reducing the aborts.

Scheduler Design

We designed DATS using abstract level dependencies and object level dependencies. In Figure 1 is presented the pseudo-code with the procedures used by DATS for detecting ALD and OLD at validation/commit time. When outer transactions are invoked, the DL with their inner transactions is checked. When the outer transactions request an object from its owner, the requests with their DLs will be sent to the owner and moved into its scheduling queue. The object owner maintains the scheduling queue holding all the ongoing transactions that have requested the object with their DLs. When T 1 (one of the outer transactions) validates an object, we consider two possible scenarios. First, if another transaction T 2 tries to validate the same object, a conflict between T 1 and T 2 is detected on the object. Thus, DATS checks for the object level dependency. If T 1 and T 2 are independent (according to the object level dependency rules), DATS allows T 1 and T 2 to proceed with the validation. Otherwise, the transaction with lower DL will be aborted. In this way, dependent transactions with the minimal cost of abort and compensating actions are aborted and restarted, permitting transactions with a costly abort operation to commit. 3 shows four different cases when T 1 and T 2 terminate. When T 1 and T 2 are invoked, DATS analyzes their DLs, operations, and values. When T 1 requests o 1 from n 0 , the meta-data for DLs, operations and values of o 1 will be sent to n 0 . These are moved to the scheduling queue of n 0 . We consider four different cases regarding the termination of T 1 and T 2 . Case 1. T 1 and T 2 validate concurrently o 1 . DATS checks for the object level dependency. If T 1 and T 2 are not dependent at the object level (i.e., the operations of T 1 and T 2 over o 1 commute), T 1 and T 2 commit concurrently. Case 2. T 1 starts to validate and detects it is dependent with T 2 (that is still executing) at the object level on the object o 1 . In this case T 2 will abort due to early validation. When T 1 commits, the updated o 1 is sent to n 2 . Case 3. Another transaction committed o 1 before T 1 and T 2 validate. If T 1 and T 2 are not dependent at the object level, o 1 is sent to n 1 and n 2 simultaneously as soon as the transaction commits. Case 4. Another transaction committed o 1 before T 1 and T 2 validate. If T 1 and T 2 are dependent at the object level, DATS checks for the abstract level dependency, and o 1 is sent to n 2 because T 2 's DL is larger than that of T 1 . Aborting T 1 , the scheduler is forced to run a single compensation (for T 1-1 ) instead of two compensations (T 2-1 and T 2-2 ) in case of T 2 's abort. Further, considering the case in which the DL of T 1 is 0, the abort of T 1 does not affect T 1-1 . In fact, its execution will be preserved and only the operations of T 1 will be re-executed.

Implementation and Experimental Evaluation

Experimental Setup. We implemented DATS in the HyFlow DTM framework [START_REF] Saad | Supporting STM in distributed systems: Mechanisms and a Java framework[END_REF][START_REF] Turcu | On closed nesting in distributed transactional memory[END_REF]. We cannot compare our results with any competitor, as none of the DTMs that we are aware of support open nesting and scheduling. Thus, we compared DATS under TFA-ON (DATS) with only TFA-ON (OPEN) [START_REF] Turcu | On open nesting in distributed transactional memory[END_REF], closed nested transaction (CLOSED) [START_REF] Turcu | On closed nesting in distributed transactional memory[END_REF], and flat nested transaction (FLAT). We contrast with CLOSED and FLAT to show that OPEN does not always perform better than them, while DATS consistently outperforms OPEN.

We assess the performance of DATS using Hash Table, Skip List and Linked List as micro-benchmarks, TPC-C [START_REF]tpc-c benchmark[END_REF] as a real-application benchmark. Our testbed is comprised of 10 nodes, each one is an Intel Xeon 1.9GHz processor with 8 CPU cores. We varied the number of application threads performing operations for each node from 1 to 8, considering a spectrum between 2 and 80 concurrent threads in the system. We measured the throughput (number of committed transactions per second). All data-points reported are the result of multiple executions, so plots present for each data-point the mean value and the error-bar. In order to assess the goodness of DATS we also present the percentage of aborted transactions and the scheduler overhead.

Benchmarks.The Skip List and Linked List benchmarks are data structures maintaining sorted and unsorted, lists of items, respectively, whereas Hash Table is an associative array mapping keys to values. We configured the benchmarks with the small number of objects and a large number of inner transactions -eight inner transactions per transaction and ten objects, incurring high contention.

Regarding TPC-C, the write transactions consist of update, insert, and/or delete operations accessing a database of nine tables maintained in memory, where each row has a unique key. Multiple operations commute if they access a row (or object) with the same key and modify different columns. We configured the benchmark with a limited number of warehouses (#3) in order to generate high conflicts. We recall that, in the data flow model, objects are not bound on fixed nodes but move, increasing likelihood of conflicts. Evaluation. Figures 4, 5 and 6(a-f ) show the throughput of micro-benchmarks under 10% and 90% of read transactions. The purpose of DATS is to reduce the overheads of compensating actions and abstract locks. In 10% read transactions, the number of aborts increases due to high contention. Outer transactions frequently abort, and corresponding compensating actions are executed; so DATS outperforms OPEN in throughput because it mitigates the abort of outer transactions and the corresponding compensating actions.

For the experiments with TPC-C in Figure 6(g),6(h),6(i), we used the amount of read and write transactions that its specification recommends. TPC-C benchmark accesses large tables to read and write values. Due to the non-negligible transaction execution time, the number of compensating actions and abstract locks in TPC-C significantly degrades the overall performance. Thus, DATS increases the performance in high contention (a large number of threads and nodes). By these results, it is evident how much unnecessary aborts of inner transactions affects performance and how much performance is improved through minimizing aborts. Even if DATS reduces the number of compensating actions and acquisition of abstract locks, the performance of OPEN is degraded because of the commit overheads of inner transactions [START_REF] Turcu | On open nesting in distributed transactional memory[END_REF]; so the throughput of DATS is slightly better than CLOSED and FLAT, but significantly better than OPEN.

Figure 8 shows throughput speed-up relative to OPEN using Hash Table, Skip List, Linked List and TPC-C. Our results show that DATS performs up to 1.7× and 2.2× better than OPEN in micro-benchmarks and TPC-C, respectively.

Figure 7 shows the analysis of scheduling overhead and abort reduction. Checking dependencies occurs when a transaction validates, so we measure the average execution time and the average validation time of committed transactions as illustrated in Figure 7(b). The gap between the two validation times of DATS and OPEN proves the scheduling overhead. Even though the validation time of DATS is up to two times more than OPEN's, a large number of transactions validated simultaneously according to the increment of nodes, results in a shorten transaction response time, reducing the average validation time and aborts. Figure 7(a) the comparison between the percentage of aborted transactions of OPEN and DATS. As long as the number of threads increases, the number of aborts in DATS and OPEN increases too. However, the increasing abort ratio in DATS is less than in OPEN, proving how much DATS reduces the abort rate.

Related Work

Nested transactions (using closed nesting) originated in the database community and were thoroughly described in [START_REF] Moss | Nested transactions: An approach to reliable distributed computing[END_REF]. This work focused on the popular twophase locking protocol and extended it to support nesting.

Open nesting also originates in the database community [START_REF] Garcia-Molina | Using semantic knowledge for transaction processing in a distributed database[END_REF], and was extensively analyzed in the context of undo-log transactions [START_REF] Weikum | Principles and realization strategies of multilevel transaction management[END_REF]. In these works, open nesting is used to decompose transactions into multiple levels of abstraction, and maintain serializability on a level-by-level basis.

One of the early works introducing nesting to Transactional Memory has been presented in [START_REF] Moss | Nested transactional memory: model and architecture sketches[END_REF]. They describe the semantics of transactional operations in terms of system states, which are tuples that group together a transaction ID, a memory location, a read/write flag, and the value read or written. They also provide sketches for several possible HTM implementations, which work by extending existing cache coherence protocols. They further focus on open nested transactions in [START_REF] Moss | Open-nested transactions: Semantics and support[END_REF], explaining how using multiple levels of abstractions can help in differentiating between fundamental and false conflicts and therefore improve concurrency. The authors of [START_REF] Moravan | Supporting nested transactional memory in logTM[END_REF] implemented closed and open nesting in LogTM HTM. They implement nesting models by maintaining a stack of log frames, similar to the run-time activation stack, with one frame for each nesting level. In [START_REF] Agrawal | Safe open-nested transactions through ownership[END_REF] past closed nesting models [START_REF] Moss | Nested transactional memory: model and architecture sketches[END_REF][START_REF] Moravan | Supporting nested transactional memory in logTM[END_REF][START_REF] Agrawal | Safe open-nested transactions through ownership[END_REF] have been studied for multiprocessor STM. N-TFA [START_REF] Turcu | On closed nesting in distributed transactional memory[END_REF] and TFA-ON [START_REF] Turcu | On open nesting in distributed transactional memory[END_REF] are the first ever DTM implementation with support for closed and open-nesting, respectively, but do not consider transactional scheduling.

Transactional scheduling has been explored in a number of multiprocessor STM efforts [START_REF] Dragojević | Preventing versus curing: avoiding conflicts in transactional memories[END_REF][START_REF] Ansari | Steal-on-abort: Improving transactional memory performance through dynamic transaction reordering[END_REF][START_REF] Yoo | Adaptive transaction scheduling for transactional memory systems[END_REF][START_REF] Dolev | CAR-STM: scheduling-based collision avoidance and resolution for software transactional memory[END_REF][START_REF] Attiya | Transactional scheduling for read-dominated workloads[END_REF]. In [START_REF] Dragojević | Preventing versus curing: avoiding conflicts in transactional memories[END_REF], the authors describe an approach that schedules transactions based on their predicted read/write access sets. In [START_REF] Ansari | Steal-on-abort: Improving transactional memory performance through dynamic transaction reordering[END_REF], they discuss the Steal-On-Abort transaction scheduler, which queues an aborted transaction behind the non-aborted transaction, and thereby prevents the two transactions from conflicting again. The Adaptive Transaction Scheduler (ATS) is present in [START_REF] Yoo | Adaptive transaction scheduling for transactional memory systems[END_REF], that adaptively controls the number of concurrent transactions based on the contention intensity: when the intensity is below a threshold, the transaction begins normally; otherwise, the transaction stalls and does not begin until dispatched by the scheduler. The CAR-STM scheduling approach is presented in [START_REF] Dolev | CAR-STM: scheduling-based collision avoidance and resolution for software transactional memory[END_REF], which uses per-core transaction queues and serializes conflicting transactions by aborting one and en-queuing it on another queue, preventing future conflicts. CAR-STM pre-assigns transactions with high collision probability (application-described) to the same core, thereby minimizing conflicts. In [START_REF] Blake | Proactive transaction scheduling for contention management[END_REF] they propose the Proactive Transactional Scheduler (PTS). Their scheme detects "hot spots" of contention that can degrade performance, and proactively schedules affected transactions around the hot spots. Attiya and Milani present the BIMODAL scheduler [START_REF] Attiya | Transactional scheduling for read-dominated workloads[END_REF], which targets read-dominated and bimodal (i.e., those with only early-write and read-only) workloads. Kim and Ravindran extend the BIMODAL scheduler for DTM in [START_REF] Kim | On transactional scheduling in distributed transactional memory systems[END_REF]. Their scheduler, called Bi-interval, groups concurrent requests into read and write intervals, and exploits the tradeoff between object moving times (incurred in dataflow DTM) and concurrency of reading transactions, yielding high throughput. None of the past transactional schedulers for STM and DTM consider open-nested transactions.

Conclusions

When transactions with committed open-nested transactions conflict later and are re-issued, compensating actions for the open-nested transactions can reduce

Figure 1 .

 1 Figure 1. Simple example showing how the execution timeline for two transactions may differ under flat, closed and open nesting.

Figure 3 .

 3 Figure 3. Example usage for try...orElse c

Fig. 1 .

 1 Fig. 1. Two transactions under flat, closed and open nesting (From [24]).

3. 1 MotivationsFigure 2

 12 Figure 2 shows an example of open-nested transactions with compensating actions and abstract locks. Listings 1.1 and 1.2 in Figure 2 illustrate two outer transactions, T 1 and T 2 , and an inner transaction in Listing 1.3. The inner transaction INSERT includes an insert operation in a Linked List. T 1 has a delete operation with a value. If the operation of T 1 executes successfully, its inner transaction INSERT executes. Conversely, regardless of the success of T 2 's delete operation, its inner transaction INSERT will execute. OnCommit and OnAbort, which include a compensating action, are registered when the inner transaction commits. If the outer transaction (i.e., T 1 or T 2 ) commits, OnCommit executes.When the inner transaction commits, its modification becomes immediately visible for other transactions. Thus, if the inner transaction commits, and its outer transaction T 1 or T 2 aborts, a delete operation as a compensating action (described in OnAbort) executes. Let us assume that T 2 aborts, and OnAbort ex-

Fig. 2 .

 2 Fig. 2. Two open-nested transactions with abstract locks and compensating actions.

Fig. 3 .

 3 Fig. 3. Four Different Cases for Two Transactions T1 and T2 in DATS

Figure 3

 3 Figure 3 illustrates an example of DATS with two transactions T 1 and T 2 invoked on nodes n 1 and n 2 , respectively. The transaction T 1 has a single innertransaction and T 2 has two nested transactions. Let us assume that T 1 's DL=1 and T 2 's DL=2. The circles indicate written objects. The horizontal line corresponds to the status of each transaction described in the time domain.Figure3shows four different cases when T 1 and T 2 terminate. When T 1 and T 2 are invoked, DATS analyzes their DLs, operations, and values. When T 1 requests o 1 from n 0 , the meta-data for DLs, operations and values of o 1 will be sent to n 0 . These are moved to the scheduling queue of n 0 . We consider four different cases regarding the termination of T 1 and T 2 . Case 1. T 1 and T 2 validate concurrently o 1 . DATS checks for the object level dependency. If T 1 and T 2 are not dependent at the object level (i.e., the operations of T 1 and T 2 over o 1 commute), T 1 and T 2 commit concurrently. Case 2. T 1 starts to validate and detects it is dependent with T 2 (that is still executing) at the object level on the object o 1 . In this case T 2 will abort due to

Figure

  Figure 3 illustrates an example of DATS with two transactions T 1 and T 2 invoked on nodes n 1 and n 2 , respectively. The transaction T 1 has a single innertransaction and T 2 has two nested transactions. Let us assume that T 1 's DL=1 and T 2 's DL=2. The circles indicate written objects. The horizontal line corresponds to the status of each transaction described in the time domain.Figure3shows four different cases when T 1 and T 2 terminate. When T 1 and T 2 are invoked, DATS analyzes their DLs, operations, and values. When T 1 requests o 1 from n 0 , the meta-data for DLs, operations and values of o 1 will be sent to n 0 . These are moved to the scheduling queue of n 0 . We consider four different cases regarding the termination of T 1 and T 2 . Case 1. T 1 and T 2 validate concurrently o 1 . DATS checks for the object level dependency. If T 1 and T 2 are not dependent at the object level (i.e., the operations of T 1 and T 2 over o 1 commute), T 1 and T 2 commit concurrently. Case 2. T 1 starts to validate and detects it is dependent with T 2 (that is still executing) at the object level on the object o 1 . In this case T 2 will abort due to

  ), 90% Read (d) HT (1 thread), 90% Read

  ), 90% Read (e) HT (4 threads), 90% Read

Fig. 4 .

 4 Fig. 4. Performance of DATS Using Hash Table (HT).

  ), 90% Read (d) SL (1 thread), 90% Read

  ), 90% Read (e) SL (4 threads), 90% Read

  ), 90% Read (f) SL (8 threads), 90% Read

Fig. 5 .

 5 Fig. 5. of DATS Using Skip List (SL).

  ), 90% Read (d) LL (1 thread), 90% Read

  ), 90% Read (e) LL (4 threads), 90% Read

  ), 90% Read (f) LL (8 threads), 90% Read

Fig. 6 .

 6 Fig. 6. Performance of DATS Using Linked List (LL) and TPC-C.

Fig. 7 .

 7 Fig. 7. Analysis of Scheduling Overhead and Abort Reduction.

  Abstract Level Dependency. The first is called abstract level dependency Algorithm 1: Algorithms for checking AOL and OLD

	1 Procedure Commit	22 Abort(txid, DependentObjects);
		Input: txid, objects	23 return abort;
		Output: commit, abort	24
	2 foreach objects do	25
	3	if txid is open nesting then	26 Procedure Retrieve Object
	4	Extract <operations,values,DL>		Input: operation, value, DL, oid
	5	Send	27 object = findObject(oid);
		<operations,values,DL,object.id>	28 if object=null then
	6	o object.owner	29	Object just validated, checking object
	7	Wait until receive status from		level dependency (OLD)
		object.owner	30	if CheckOLD(operation, value) then
	8	if status=noncommute then	31	commutativity.put(object.id, new
	9	noncommutativity.put(object);		request(operation, values));
			32	return commute;
	10 if noncommutativity=∅ then	33	Dependency queue to track updates.
	11	All objects commute or no conflicts	34	dependency.put(oid, DL);
		detected
	12	Retrieve the dependency queue from
	13 14 15 16	object.owner ; Validate objects; Change the object ownership find highest DL from dependency.get(object.id); Send object to the node with the highest DL; return commit;	37 38 Procedure Abort Input: txid, objects 39 if txid is outer-transaction then 40 foreach objects do 41 nestedIds = NestedTxs.get(object.id); 42 if nestedIds = null then 43 foreach nestedIds do
			44	Execute onAbort() for
	18	Checking abstract level dependency		nestedId
		(ADL)	45	AbortNestedTx(nestedId);

17 foreach object ∈ noncommutativity do 19 nestedTxId = CheckALD(object); 20 Enqueue dependent nested transactions 21 NestedTxs.put(object.id,nestedTxId); 35 return non -commiute; 36 return no -conf lict; 46 AbortOuterTx(txid);

  Fig. 8. Speed-up (Throughput Relative to OPEN) in Hash Table, Skip List, Linked List, TPC-C.throughput. DATS avoids this by reducing unnecessary compensating actions, and minimizing inner transactions' remote abstract lock acquisitions through object dependency analysis. DATS shows the important of scheduling open-nested transactions in order to reduce the number of compensating actions and abstract locks in case of abort. Our implementation and experimental evaluation shows that DATS enhances transactional throughput for open-nested transactions over no DATS by as much as 1.7× and 2.2× with micro-benchmarks and real-application benchmark, respectively.

			1.8			Speedup(Hashtable)				1.7			Speedup(Skiplist)
					1 thread, 90						1 thread, 90
			1.7		1 thread,10				1.6		1 thread,10
					4 threads, 90						4 threads, 90
			1.6		4 threads, 10				1.5		4 threads, 10
					8 threads, 90						8 threads, 90
	Speedup	1.4 1.5		8 threads, 10		Speedup	1.3 1.4		8 threads, 10
			1.3							1.2
			1.2							1.1
			2 1.1	3	4	5 Number of Nodes 6 7	8	9 10		2 1.0	3	4	5 Number of Nodes 6 7	8	9 10
						(a) Hash Table						(b) Skip List
		1.8			Speedup(Linkedlist)			2.2			Speedup(TPC-C)
	Speedup	1.3 1.4 1.5 1.6 1.7	8 threads, 10 8 threads, 90 4 threads, 10 1 thread 90 1 thread, 10 4 threads, 90		Speedup	1.4 1.6 1.8 2.0	1 thread 4 thread 8 threads
		1.2
		1.1						1.2
		2 1.0	3	4	5 Number of Nodes 6 7	8	9 10	2 1.0	3	4	5 Number of Nodes 6 7	8	9 10
						(c) Linked List						(d) TPC-C

Acknowledgments. This work is supported in part by US National Science Foundation under grants CNS 0915895, CNS 1116190, CNS 1130180, and CNS 1217385.