Carlos Olarte
email: caolarte@cic.puj.edu.co

Camilo Rueda
email: crueda@cic.puj.edu.co

Elaine Pimentel
email: elaine@mat.ufmg.br

Néstor Cataño
email: ncatano@uma.pt

A Linear Concurrent Constraint approach for the automatic verification of access permissions

Keywords: F.3.1 [Specifying and Verifying and Reasoning about Programs]: Logics of programs; D.3.2 [Language Classifications]: Constraint and logic languages. Concurrent, distributed, and parallel languages. General Terms Theory, Verification, Concurrency Concurrent Constraint Programming, Access Permissions, Linear Logic, Verification

A recent trend in object oriented programming languages is the use Access Permissions (AP) as abstraction to control concurrent executions. AP define a protocol specifying how different references can access the mutable state of objects. Although AP simplify the task of writing concurrent code, an unsystematic use of permissions in the program can lead to subtle problems. This paper presents a Linear Concurrent Constraint (lcc) approach to verify AP annotated programs. We model AP as constraints (i.e., formulas in logic) in an underlying constraint system, and we use entailment of constraints to faithfully model the flow of AP in the program. We verify relevant properties about programs by taking advantage of the declarative interpretation of lcc agents as formulas in linear logic. Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. We show that those properties are decidable and we present a complexity analysis of finding such proofs. We implemented our verification and analysis approach as the Alcove tool, which is available on-line.

Introduction

Reasoning about concurrent programs is much harder than reasoning about sequential ones. Programmers often find themselves overwhelmed by the many subtle cases of thread interaction they must be aware of so as to decide whether a concurrent program is correct or not. Also, the need of finding the right level of thread atomicity, avoiding race conditions, coping with mutual exclusion requirements, guaranteeing deadlock freeness, make it very hard to design reliable concurrent software. Furthermore, the attempt to find errors through testing is doomed to failure because of the nondeterminism caused by thread scheduling.

This complexity of concurrent software is aggravated when software designers, wishing to take advantage of object oriented (OO) design strategies, use OO languages to write concurrent programs. The distribution of state in objects that might have multiple references (aliases), probing or modifying concurrently their local contents, contributes significantly to the complexity of sound concurrent program design. This potential data race situation occurs when a reading and a writing trace both access a shared memory location. This should be considered a program error since it gives rise to inconsistent executions paths. To cope with this problem, a simple strategy is to wrap each object access up in an atomic block. However, this negatively affects program performance. A better strategy would be for the programmer to lock just those objects that are actually shared among threads. It is very hard, however, to figure out which objects are to be shared and what locations are really protected by the locks simply by looking at the program text.

Languages like AEminium [START_REF] Stork | Concurrency by default: using permissions to express dataflow in stateful programs[END_REF] and Plaid [START_REF] Sunshine | First-class state change in plaid[END_REF] propose a different strategy to concurrency based on access permissions (AP) [START_REF] Boyland | Capabilities for sharing: A generalisation of uniqueness and read-only[END_REF] to objects. AP are descriptions about how various references to an object can coexist. They permit a direct control about the access to the mutable state of an object. Making the access to a shared mutable state explicit facilitates verification and it also permits parallelization of code. For instance, a unique AP, which describes the case when only one reference to a given object exists, enforces absence of interference and simplifies verification. On the other hand, a shared AP, which describes the case when an object may be accessed and modified by multiple references, allows for concurrent executions and makes verification trickier.

Although AP greatly help to devise static strategies for correct concurrent sharing of objects, the interactions resulting from dynamic bindings (e.g., aliasing of variables) might still lead to subtle difficulties. Indeed, it may happen that apparently correct permissions assignments in simple programs lead to deadlocks.

We propose a Linear Concurrent Constraint (lcc) [START_REF] Fages | Linear concurrent constraint programming: Operational and phase semantics[END_REF] programming approach to the verification of AP annotated programs. In our approach, programs are interpreted as lcc agents that use constraints to keep information about AP, object references, object fields, and method calls. We use constraint entailment to verify compliance of methods and arguments to their AP based signatures. Furthermore, by exploiting the declarative view of lcc agents as logical formulas, we are able to analyze and verify programs. The proposed program verification includes (1) deadlock detection;

(2) whether it is possible for methods to be executed concurrently or not; and (3) whether annotations adhere to the intended semantics associated with AP or not.

The contributions of the this paper are four-fold (1) the definition of an elegant lcc semantics of AP for an object oriented concurrent programming language; (2) the definition of a decidable efficient verification procedure of non-recursive programs; (3) a complexity analysis of the effort required to verify a program; and (4) the implementation of the Alcove tool that automates our verification approach.

The rest of the paper is organized as follows. Section 2 presents the syntax of the AP based language used here and recalls lcc. Section 3 presents the model of AP as lcc agents. We also show how the proposed model is a runnable specification that allows users to observe the flow of program permissions. We implemented this models as the Alcove LCC Animator. Section 4 describes our approach to verify programs and its implementation as the Alcove LL prover. It also presents a complexity analysis about the proposed verification. Section 5 concludes the paper.

Preliminaries

Programs Syntax

Access permissions (AP) are abstractions describing how objects are accessed. Assume a variable x that points to the object o. The unique permission unq states that x is the sole reference to object o. The shared permission shr provides x with reading and modifying access to object o, which allows other references to o (called aliases) to exist and to read from it or to modify it. The immutable permission imm provides x with read-only access to o, and allows any other reference to object o to exist and to read from it. If x points to null, the permission none represents the fact that x is a null reference and it has no permission to access any object.

Figure 1 shows a program (taken and slightly modified from [START_REF] Stork | Concurrency by default: using permissions to express dataflow in stateful programs[END_REF]) that operates over a collection of elements. Starting at line 8, the program creates an object of type collection at Line 10 and an object of type stats at line 11. The program sorts the collection c at line 12, and prints it at line 13. It computes some statistics at line 14, and removes duplicates from the collection at line 15. Lines 3-7 declare the signatures for the methods. The signature of class collection constructor returns a unique reference to a new collection at line 3. Methods sort and removeDuplicates require a unique reference to the collection to exist and to return a unique permission to it. Method compStats requires and returns an immutable (read-only) AP to the collection c and a unique AP to the parameter s.

Given these method signatures, the AP flow for the program is computed. Permissions can be produced and consumed. Hence, the unique permission returned by the constructor of class collection is consumed by the call of sort. Once this method terminates, the unique permission is restored and split into two immutable permissions, and methods print and compStats can be executed concurrently. Once both methods have finished their execution, the immutable access permissions are joined back into a unique access permission, and the method removeDuplicates can be executed.

The analyses presented in this paper considers a subset of AEminium [START_REF] Stork | Concurrency by default: using permissions to express dataflow in stateful programs[END_REF], a concurrent-by-default object oriented programming language based on the above idea of AP (see Figure 2). Methods specify the required permissions for the caller (p(this)) and for each argument (p(y)) as well as the permissions restored to the environment when the method terminates (p (this) and p (y)).

Similarly for class constructors (CT R). We assume that in a call to a method (or constructor), the actual parameters are references (i.e., variables, object fields or this) and not arbitrary expressions. Since we have parameters by reference, we assume that the returned type is void and we omit it in the signature. For assignments we allow only statements of the form r l := rr, where the right and left hand side are references. Notice that we do not lose generality by imposing these syntactic restrictions since it is possible to unfold more general expressions by using local variables.

Linear ccp

Concurrent Constraint Programming (ccp) [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] is a model for concurrency that combines the traditional operational view of process calculi with a declarative view based on logic. This allows ccp to benefit from the large set of reasoning techniques of both process calculi and logic. Agents in ccp interact with each other by telling and asking information represented as constraints to a global store.

The basic constructs (processes) in ccp are: (1) the tell agent c, which adds the constraint c to the store, thus making it available to the other processes. Once a constraint is added, it cannot be removed from the store (i.e., the store grows monotonically). And (2), the ask process c → P , which queries if c can be deduced from the information in the current store; if so, the agent behaves like P , otherwise, it remains blocked until more information is added to the store. In this way, ask processes define a simple and powerful synchronization mechanism based on entailment of constraints.

Linear Concurrent Constraint (lcc) [START_REF] Fages | Linear concurrent constraint programming: Operational and phase semantics[END_REF] is a ccp-based calculus that considers constraint systems built from a fragment of Girard's intuitionistic linear logic (ILL) [START_REF] Girard | Linear logic[END_REF]. The move to a linear discipline permits ask agents to consume information (i.e., constraints) from the store. Definition 1 (Linear Constraint Systems [START_REF] Fages | Linear concurrent constraint programming: Operational and phase semantics[END_REF]). A linear constraint system is a pair (C, ) where C is a set of formulas (linear constraints) built from a signature Σ ( a set of function and relation symbols), a denumerable set of variables V and the following ILL operators: multiplicative conjunction (⊗) and its neutral element (1), the existential quantifier (∃), the exponential bang (!) and the constant top ( ). Let ∆ be a (possibly empty) subset of C × C defining the non-logical axioms of the constraint system (i.e, a theory). Then the entailment relation is the least set containing ∆ and closed by the rules of ILL (see Figure 3). The Language of Processes. Similar to other ccp-based calculi, lcc, in addition to tell and ask agents, provides constructs for parallel composition, hidden of variables, non-deterministic choices and process definitions and calls.

c c 1 Γ Γ c Γ, 1 c Γ, c1, c2 c Γ, c1 ⊗ c2 c Γ c1 ∆ c2 Γ, ∆ c1 ⊗ c2 Γ c[t/x] Γ ∃x.c Γ, c d x / ∈ f v(Γ, d) Γ, ∃x.c d Γ, c d Γ, ! c d Γ d Γ, ! c d Γ, ! c, ! c d Γ, ! c d ! Γ d ! Γ ! d
Definition 2 (lcc agents [START_REF] Fages | Linear concurrent constraint programming: Operational and phase semantics[END_REF]). Agents in lcc are built from constraints in the underlying linear constraint system, following the syntax below.

P, Q, ...

::= c | ∀x(c → P ) | P Q | ∃x(P ) | P + Q | p(x)
Tell Agent. Given a store d, the tell agent c adds c to d producing the new store d ⊗ c.

Linear ask agent. Let d be the current store and θ be the substitution [t/x] for some list of terms t. If d entails d ⊗ cθ for some d (i.e., d d ⊗ cθ ), the ask agent ∀x(c → P ) consumes cθ and executes P θ under the new store d . If c (the guard) cannot be deduced from d, the ask agent blocks until more information is added to the store. If the sequence of variables x is empty then ∀x(c → P ) is written as c → P .

Parallel Composition. P

Q stands for the interleaved parallel execution of agents P and Q, possibly communicating through shared variables in the store. Given a finite set of indexes I = {1, 2, ..., n}, instead of P1 P2 ... Pn, we write i∈I Pi.

Locality. The agent ∃x(P ) behaves like P and binds the variable x to be local to it.

Non-deterministic choice. The process P1 + ... + Pn nondeterministically chooses one Pi for execution whenever Pi can evolve (one-step guarded choice). The chosen alternative precludes the others. We assume here that each Pi is an ask agent. Hence, the agent i∈I ∀xi(ci → Pi) evolves into Pj[tj/xj] whenever the store entails cj[tj/xj] for some j ∈ I. Otherwise, the agent blocks until more information is added to the store.

Procedure Calls. Assume a process declaration:

p(x) ∆ = P
where all free variables of P are in the set of pairwise distinct variables x. The agent p(y) evolves into P [y/x].

We assume that "⊗" has a higher precedence than "→", hence

c1 ⊗ c2 → c 1 ⊗ c 2 should be read as (c1 ⊗ c2) → (c 1 ⊗ c 2 ).
Furthermore, "! " has a tighter binding than ⊗ so we understand ! c1 ⊗ c2 as (! c1) ⊗ c2. For the rest of the operators we shall explicitly use parenthesis to avoid confusions.

In the following example we show how lcc agents evolve. We shall use P, c → P , c to denote that the agent P under store c evolves into the agent P producing the store c . The reader may refer to [START_REF] Fages | Linear concurrent constraint programming: Operational and phase semantics[END_REF] for a complete account of the lcc operational semantics.

Example 2.1 (Consuming Permissions). Let's assume that we have a constraint system with a ternary predicate ref(•), constant symbols unq and shr and equipped with the axiom:

∆ = ref(x, o, unq) ref(x, o, shr). Let's assume also a process R = P Q such that P = ref(x, o, unq) Q = ∀y(ref(x, y, shr) → Q )
From the initial store (true), Q cannot deduce its guard and it remains blocked. Hence, P evolves by executing the tell agents ref(x, o, unq):

R, → Q, ⊗ ref(x, o, unq)
Afterwards, the store ⊗ ref(x, o, unq) is strong enough to entail the guard of Q by using the axiom ∆. We thus observe the following transition:

Q, ⊗ ref(x, o, unq) → Q [o/y],
Roughly speaking, P adds to the store the information required to state that x points to o and has a unique permission to o (i.e., ref(x, o, unq)). By using ∆, from ref(x, o, unq) we can deduce ref(x, o, shr), i.e., the unique permission of x can be downgraded to a share permission on o. Thereafter, Q consumes this information, leading to the store where the agent

Q [o/y] is exe- cuted.
We finish this section by introducing the derived operator P ; Q that delays the execution of Q until the "end" of the execution of P . This will be useful for the model we present in the forthcoming sections. Let z, w, w be variables that do not occur either in P or in Q and sync(•) be an uninterpreted predicate symbol. The pro-

3 2012/11/4 cess P ; Q can be defined as ∃z(C[[P ]]z sync(z) → Q) where C[[c]]z = c ⊗ sync(z) C[[∀y(c → P )]]z = ∀y(c → C[[P ]]z) C[[P R]]z = ∃w, w (C[[P ]]w C[[R]] w sync(w) ⊗ sync(w ) → sync(z)) C[[P + R]]z = C[[P ]]z + C[[R]]z C[[∃y(P )]]z = ∃y(C[[P ]]z) C[[p(x)]]z = p(x, z)
Intuitively C[[P ]]z adds the constraint sync(z) when it terminates. Then, the ask agent sync(z) → Q reduces to Q. Notice for example that in a parallel composition P R, we wait for both P and R to finish and then, the constraint sync(z) is emitted. As we shall see, we only use calls and process definitions when modeling aliasing of variables and AEminium constructs and methods declarations. Hence, in Section 3.2 we shall rewrite the signature of a process definition p(y) as p(y, w) ∆ = P . Then, the call p(x, z) evolves into P [x/y, z/w] that later adds the constraint sync(z) when needed to synchronize with the rest of the processes.

A LCC Interpretation of AP

Our lcc interpretation of access permissions in AEminium programs assumes a constraint system with the following axioms, predicate and constant symbols:

Permissions: We assume the set of constant symbols PER = {unq, shr, imm, none} in order to represent the permissions introduced in Section 2.1.

References and Fields:

We use the predicate symbol ref(x, o, p) (x points to object o with permission p ∈ PER), field(x, o, f ield) (x points to o.f ield), sync(z) (synchronizing on variable z) and ct(o, n) (there are n references pointing to o). For the last constraint, we also assume the constant 0 (zero) and the successor function s(•). Furthermore, we assume the constants nil (null reference) and cname f name for each field "f name" of class "cname".

Non-logical axioms: We assume the following axioms:

downgrade 1 : ref(x, o, unq) ref(x, o, shr) downgrade 2 : ref(x, o, unq) ref(x, o, imm) upgrade 1 : ref(x, o, shr) ⊗ ct(o, s(0)) ref(x, o, unq) ⊗ ct(o, s(0)) upgrade 2 : ref(x, o, imm) ⊗ ct(o, s(0)) ref(x, o, unq) ⊗ ct(o, s(0))
The axiom downgrade 1 (resp. downgrade 2 ) transforms a unique permission into a share (resp. immutable) permission. The axiom upgrade 1 (resp. upgrade 2 ) builds a unique permission from a share (resp. immutable) permission. Hence, to be able to upgrade a permission to unique, the reference x needs to be the unique reference with share or immutable permission to the pointed object o. Conversions from share permissions into immutable and vice versa require first to upgrade the permission to unique and then, apply the appropriate downgrade axiom.

Modeling Statements.

We interpret AEminium statements through the function S[[s]]z that given a statement s returns an lcc agent that synchronizes with the rest of the program by adding the constraint sync(z) to the store. We assume (by renaming variables if necessary) that z does not occur in s. In the following we define S[[s]]z for each type of statement in Figure 2.

Local variables in AEminium are defined as local agents in lcc. The local variable x points to nil with no permissions.

(RLOC) S[[let x in s end]]z = ∃x(ref(x, nil , none); S[[s]]z)
For the assignment x := y, we define the rule:

(RALIAS) S[[x := y]]z = assg(x, y, z)
where assg(x, y, z)

∆ = drop(x); gain(x, y); sync(z) drop(x) def = ∀o, n((ref(x, nil, none) → ) + p∈PER\{none} ref(x, o, p) ⊗ ct(o, s(n)) → ct(o, n)) gain(x, y) def = ref(y, nil , none) → ref(x, nil , none) ⊗ ref(y, nil , none) + ∀o, n((ref(y, o, unq) ⊗ ct(o, s(0)) → ref(y, o, shr) ⊗ ref(x, o, shr) ⊗ ct(o, s(s(0)))) + (ref(y, o, shr) ⊗ ct(o, n) → ref(y, o, shr) ⊗ ref(x, o, shr) ⊗ ct(o, s(n))) + (ref(y, o, imm) ⊗ ct(o, n) → ref(y, o, imm) ⊗ ref(x, o, imm) ⊗ ct(o, s(n)))
Here, the variable x loses its permission to the pointed object o, and the object o has one less reference pointing to it (Definition drop 1 ). Thereafter, x and y point to the same object and the permission of y is split between x and y (Definition gain) as follows: if y has a unique permission to o, this permission is split into two share permissions, one for x and one for y. If y has a share (resp. immutable) permission to o, then both x and y will have a share (resp. immutable) permission to o after the assignment. Recall that ask agents consume their guard when evolving. Therefore, we add back the permission for y in the right-hand side of the rule. Finally, once the permission to y is split, the constraint sync(z) is added to the store to synchronize with the rest of the program.

If the variable x points to the object o of class cname, then the field f name of o can be accessed by the variable u whenever field(u, o, cname f name) holds.

(RALIAS F ) S[[x.f := y]]z= ∀u, o, p( ref(x, o, p) ⊗ field(u, o, cname f ) → (ref(x, o, p); S[[u := y]]z))
The models for the statements S[[x.f name := y.f name]]z and S[[x := y.f name]]z are similar and thus omitted.

For the composition of statements {s1 s2 ... sn}, the agent modeling si runs in parallel with the other agents once the agent modeling the statement si-1 adds the constraint sync(zi-1). After the execution of the statement sn, the constraint sync(z) is added to the store to synchronize with the rest of the program.

(RCOMP) S[[{s1 ... si ... sn}]]z = ∃z1, ...zn(S[[s1]]z 1 sync(z1) → S[[s2]]z 2 ... sync(zn-1) → S[[sn]]z n sync(zn) → sync(z))
Method calls and Object instantiation. For the sake of simplicity, we write methods and constructors using functional nota- 1 Definitions ( def = ) must be understood as shorthands.

tion rather than object-oriented notation. For instance, x.meth(y) is written as cname meth(x, y) when x is an object of type cname. Similarly, the expression x := new cname(y) is written as cname cname(x, y). As we shall see, for each method of the form meth(x, y) in class cname, we shall generate a process definition cname meth(x, y, z) ∆ = P . The AEminium statement cname meth(x, y) is then modeled as the lcc call cname meth(x, y, z). This thus triggers the execution of the body of the method. Notice that we add the variable z as last parameter to be able to synchronize with the rest of the program. where m = |y| is the number of parameters of the method and |o| = |n| = m. The process PM first consumes the required permissions from the parameters y and from the caller x. If the required permission is share or immutable, those permissions are restored to allow concurrent executions in the environment that called the method. Unique and none permissions are consumed to later be transferred to the body of the method:

consume def = i∈1..m consumey i ; consumex consumey i def = ref(yi, oi, pi) ⊗ ct(oi, ni) → ref(yi, oi, pi) ⊗ ct(oi, s(ni)) if pi ∈ {shr,imm} consumey i def = ref(yi, oi, pi) → if pi ∈ {unq, none}
Definition consumex is similar to that of consumey i but it considers the variable x, the object ot and the permission p.

Once the permissions are consumed according to the signature of the method, the agent PM creates local variables y and x to replace the formal parameters (y) and the caller (x) by the actual parameters:

params def = ref(x , ot, p) ⊗ i∈1..m ref(y i , oi, pi)
At this point, PM adds sync(z) to release the program control. Thereafter the body of the method can be executed. This is done by modeling the statement s as the agent PB where s denotes s after replacing yi by y i and x by x :

PB def = ∃z (S[[ s]] z ; sync(z ) → (r env(x : p, x : p ) i∈1..m r env(yi : pi, y i : p i )))
Once the execution of s releases the control (i.e., it adds sync(z ) to the store), the references and permissions of the local variables created to handle the parameters are consumed and restored to the environment according to:

r env(x : p, x : p ) def = ∀o , n(ref(x , o , p ) ⊗ ct(o , s(n)) → ct(o , n)) if p, p ∈ {imm, shr} r env(x : p, x : p ) def = ∀o (ref(x , o , p ) → ref(x, o , p )) if p ∈ {unq, none} r env(x : p, x : p ) def = ∀o, n, o ((ref(x, o, p) ⊗ ct(o, s(n)) → ct(o, n)); ref(x , o , p ) → ref(x, o , p )) if p ∈ {shr, imm}, p ∈ {unq, none}
Let us give some intuition about the cases considered in the definitions above. Recall that consume duplicates the shr and imm permissions for the variables internal to the method. Then, we only need to consume such permissions and decrease the number of references pointing to object o . As for unq and none as input permissions, consume transfers such permissions to the local variables and consumes the external references. Then, r env needs to restore the external reference and consume the local one (the number of references pointing to o remains the same). When the method changes the input permission from share or immutable into a unique or none, we need to consume first the external reference. Then, we transfer the internal permission and reference to the external variable.

A constructor CD of the form cname(cname x, classy y) none(x), p(y) ⇒ p (x), p (y) {s} is modeled similarly as a method definition: ; sync(z)) Here consume is similar to consume but with ot = nil, i.e., x in x := new cname(y) is restricted to be a null reference. Definition params is similar to params except that it considers p = unq, i.e.

(RCDEF)D[[CD]] = cname(x,
x has a unique permission to onew. Furthermore, params adds ct(onew, s(0)) to the store. Class fields are initialized to nil and the link between the variable ui and the field onew.fi is established:

fields-init def = ! field(u1, onew, cname f1) ⊗ ref(u1, nil , none) ⊗ ...⊗ ! field(u k , onew, cname f k ) ⊗ ref(u k , nil , none)
Finally, notice that the synchronization constraint sync(z) is added only in the end of the rule since the constructor needs to be fully executed before returning the new reference.

The following example shows how the proposed model works.

Example 3.1 (Access Permission Flow). Assume the class definitions stats and collection in Figure 1 and the following main body written in functional notation. Hence, c (resp. s) points to oc (resp. os) with a unique permission. Since collection compStats(c, s) requires c to have an immutable permission to oc, the axiom downgrade1 is used to entail the guard of consume in the definition of the method (see Rule RMDEF). Let c be the representation of c inside the method (see params in Rule RMDEF). We notice that when the body of the method is being executed, both c and c have an immutable permission to oc. Before executing the body of method compStats, the constraint sync(z1) is added so as to allow possibly concurrent executions in the main body. The agent modeling the statement in line 5 can be then executed. However, this call requires c to have a unique permission to oc which is not possible since the axiom upgrade1 requires that c is the sole reference to oc. Hence, the guard consume for this call is delayed (synchronized) until the permission on c is consumed and restored to the environment (see definition r env). We then observe that statements in lines 4 and 5 are executed sequentially due to the way permissions evolve.

The Model as a Runnable Specification

ccp-based models can be regarded as runnable specifications, and so we can observe how permissions evolve during program execution by running the underlying lcc model. We implemented an interpreter of lcc on top of the Mozart system (http:// www.mozart-oz.org/). This interpreter uses records (Mozart data structures) to represent lcc linear constraints. The store was modeled as a multiset of records, and the entailment of constraints for universally quantified asks was implemented via record unification. On top of this interpreter, we implemented a parser that takes an AEminium program and generates the corresponding lcc agents. Output init(collection collection [c1 z9]) represents the call to a method (recall that parameter z is used for synchronization purposes). If a method is currently being executed, the constraint running(collection collection [c1 z9]) is present in the store. Notice that the execution of the method collection removeduplicates is delayed until the end of the execution of collection compstats (i.e., the store does not contain simultaneously both running(collection compstats) and running(collection removeduplicates)) as explained in Example 3.1. The last two lines of the trace show that both c and s ends with a unique permission to objects ot16 and ot27 respectively2 Example 3.3 (Deadlock Detection). Let us assume now the class definitions in Figure 1 and the following main: This code aliases svar and s after the assignment svar := s, so that they share the same permission afterwards. Therefore, s cannot recover the unique permission to execute the statement collection compStats(c, s), thus leading to a permission deadlock. This bug is detected by Alcove:

[init(collection_collection [c1 z10])] [running(collection_collection [c1 z10])] [init(stats_stats [s2 z11])] [running(stats_stats [s2 z11])] [init(collection_compstats [c1 s2 z14])]
c1(obj:ot17 objfields:none per:imm) svar9(obj:ot28 objfields:none per:shr) s2(obj:ot28 objfields:none per:shr) Error: Permissions for collection_compstats(c1 s2 z14)

could not be obtained.

We notice that in the trace above, the call to the method compstats is invoked (init) but the method was not executed (running). Furthermore, both s and svar have a share permission on the pointed object.

Verification Techniques

Besides playing the role of executable specifications, ccp-based models can be declaratively interpreted as formulas in logic (see e.g., [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]). This section provides additional mechanisms and tools for verifying properties of access-permission based programs. More concretely, we take the lcc agents generated by the Alcove LCC Animator and translate them into a linear logic (LL) formula. Then, a property specified in LL is verified with the Alcove LL Prover, a bespoken theorem prover implemented on top of λ-Prolog [START_REF] Miller | Programming with Higher-Order Logic[END_REF] based on the prover described in [START_REF] Hodas | Logic programming in a fragment of intuitionistic linear logic[END_REF].

Agents as Formulas

In lcc, processes are not only agents that evolve according to the rules of the underlying operational semantics, but also are formulas in linear logic [START_REF] Girard | Linear logic[END_REF]. The logical interpretation of lcc is defined with the aid of a function L[[•]] defined as [START_REF] Fages | Linear concurrent constraint programming: Operational and phase semantics[END_REF]:

L[[c]] = c L[[p(x)]] = p(x) L[[P Q]] = L[[Q]] ⊗ L[[P ]] L[[P + Q]] = L[[Q]] L[[P ]] L[[∀x(c → P )]] = ∀x(c L[[P ]]) L[[∃x(P )]] = ∃x(L[[P ]]).
where is the linear additive conjunction and is the linear implication. The first step of our approach for the verification of programs consists in interpreting the lcc model in Section 3 as a LL formula according to function L[[•]]. Furthermore, process definitions of the form p(x) ∆ = P (i.e., assignment and constructor and method definitions) are transformed into a LL clause ∀x.p(x) P . We shall call these clauses definition clauses and they are stored together with the axioms of the constraint system (upgrade and downgrade):

ref(x,
(w3) ⊗ sync(w3) sync(z))))).
The interpretation for methods is obtained similarly by following the rule RMDEF.

The assignment of variables is encoded by the predicate assg(x, y, z) resulting from the translation of the Rule RALIAS:

assg(x, y, z) ∃z1, z2(∀o, n((ref(x, o, none) ⊗ sync(z1) ref(x, o, unq) ⊗ ct(o, s(n)) ct(o, n) ⊗sync(z1) ref(x, o, shr) ⊗ ct(o, s(n)) ct(o, n) ⊗sync(z1) ref(x, o, imm) ⊗ ct(o, s(n)) ct(o, n) ⊗sync(z1))⊗ sync(z1) ref(y, nil , none) ref(x, nil , none) ⊗ ref(y, nil , none) ⊗ sync(z2)) (∀o, n(ref(y, o, unq) ⊗ ct(o, s(0)) ref(y, o,shr)⊗ ref(x, o, shr) ⊗ ct(o, s(s(0))) ⊗ sync(z2) ref(y, o, shr) ⊗ ct(o, n) ref(y, o, shr)⊗ ref(x, o, shr) ⊗ ct(o, s(n)) ⊗ sync(z2) ref(y, o, imm) ⊗ ct(o, n) ref(y, o, imm)⊗ ref(x, o, imm) ⊗ ct(o, s(n)) ⊗ sync(z2)))⊗ sync(z2) sync(z)).
Hence, for this example, the theory ∆ would contain the definition clauses for collection collection, stats stats, assig and collection compStats, together with axioms for upgrading and downgrading permissions.

Let A be the lcc agent related to the main program. Then,

F = ∃c, s, svar, z, z1, z2, z3, z4, z5(ref(c, nil , none)⊗ ref(s, nil , none) ⊗ ref(svar, nil , none) ⊗ sync(z1)⊗ sync(z1) collection collection(c, z2)⊗ sync(z2) stats stats(s, z3)⊗ sync(z3)
assig(svar, s, z4)⊗ sync(z4) collection compStats(c, s, z5)⊗ sync(z5) sync(z)).

corresponds to L[[A]

] (see Rules RCOMP, RNEW, RCALL and RALIAS in Section 3).

Linear Logic as a Framework for Verifying Access Permission Properties

Assume the translation L[[A]] as described in Example 4.1, producing a theory ∆ and a formula F . In order to verify a certain property T , specified by a LL formula T , we test if the sequent ! ∆, F T is provable. In this section, we will give an estimate of the complexity of finding such a proof.

First of all, observe that the fragment of ILL needed for encoding access permissions is given by the following grammar for guards G, processes P and properties T :

G := A | G ⊗ G P := ∀x.G P | P ⊗ P | ∃x.P | P P | !(∀x.p(x) P ) | 1 | |!A | A T := ∃x.T | G.
where A is an atomic formula. Notice that this grammar is well defined, since the left context in the sequent ! ∆, F T will be formed by P formulas, the right context will have only T formulas. Besides, implications on the left can only introduce guards on the right side of a sequent and G ⊂ T 3 .

We note that classical and intuitionistic provability coincide for this fragment, since the right side of sequents are composed by existentially quantified Horn clauses.

The fragment described above is undecidable in general, due to the presence of processes declarations [START_REF] Lincoln | Decision problems for propositional linear logic[END_REF]. It turns out that AEminium applications dealt in the present paper are such that process declarations p(x) do not have circular recursive calls. More precisely, in an AEminium program, there is no a sequence of methods or constructs of the form m1, m2, • • • mn such that mi calls mi+1 and mn calls m1. Hence, if a method m1 calls m2, we can syntactically expand the body of m2 into the body of m1. Therefore, it is straightforward to see that provability in the resulting LL translation is decidable (see Theorem 4.1). It is worth mentioning that the analyses presented here could be enhanced in order to deal with mutual recursive calls and some types of controlled recursion, as in [START_REF] Pimentel | On the specification of sequent systems[END_REF] (see more in Section 5).

Complexity Analysis. We will show now how to measure the complexity of proofs in our system. It is worth noticing that Alcove LL Prover actually uses the proposed measure as a limit on the proof search.

For reasoning about complexity of proofs in LL we need to use a proof system for it where proof search can be controlled and measured. We thus move from ILL to the focused classical linear logic system in one sided sequent style (LLF) [START_REF] Liang | A focused approach to combining logics[END_REF] 4 . In a nutshell, moving into the classical setting means adding the connectives ? (exponential dual to !) and ⊕, (additive and multiplicative versions of the disjunction) together with their neutral elements, 0 and ⊥ respectively. One sided means moving from sequents of the shape ! ∆, F T into sequents of the form ?∆ ⊥ , P ⊥ , T , where negation is a logical connective that has only atomic scope: if B is a general formula then B ⊥ denotes the result of moving negations inward until it has only atomic scope. We shall call literal an atomic formula or its negation. For convenience, the clause B C will be represented by the formula B ⊥ C.

Intuitively, the focusing discipline organizes proofs into two alternating phases, called negative and positive phases. In the negative phase, all (invertible) rules over the connectives of negative polarity (∀, , , ?, ⊥, ) are applied eagerly, while in the positive phase a formula of positive polarity (∃, ⊗, ⊕, !, 0, 1) is focused on and its positive subformulas are eagerly introduced.

Thus, on searching for proofs in focused systems, the only nondeterministic step is the one choosing the positive formula to focus on from the context. This determines completely the complexity of a proof in LLF and justifies the next definitions.

Definition 3 (Proof Depth). Let Π be a proof in LLF. The depth of Π is the maximum number of decisions over focused formulas along any path in Π from the root. Definition 4 (Degree of a positive formula). The degree of a positive formula is the maximum number of nested alternating polarities in it.

The next lemma shows the relation between depth of derivations in LLF and degree of a formula. The proof is discharged by structural induction.

⊥ ct(onew, s(0)) ⊥ sync(w2) ⊥ sync(w2) ⊗ ∀w3∃o (ref(x , o , unq) ⊗ ref(x, o , unq) ⊥ sync(w3) ⊥ sync(w3) ⊗ sync(z) ⊥ )))).
The degree of such a formula is 10. Hence the depth of decomposing the formula above into its literal or purely positive subformulas is 10/2 = 5.

We will now proceed with a careful complexity analysis of all the formulas produced by the specification of AEminium programs. The calculation of the complexity is done by counting the changes of nested polarities, which are produced mostly by synchronizations.

• If cname method(x, y, z) P is a definition clause (DC) in ∆, its negation cname method(x, y, z) ⊗ P ⊥ is a positive formula of degree at most 11 + n + m where m is the length of y and n is the degree of the formula encoding the body of the constructor, i.e., S[[ s]] ⊥ z . • If cname(x, y, z) P is a DC in ∆, its negation is a positive formula of degree at most 12 + n + m where m is the length of y and n is the degree of S[[ s]] ⊥ z .

• If assig(y, x, z) P is a DC in ∆, its negation is a positive formula of degree at most 5.

• For any formula F interpreting an AEminium main program with n statement calls, F ⊥ is a negative formula whose biggest positive subformula has degree at most (2n + 1) + m where m is the sum of the degrees of all negated definition clauses corresponding to the statement calls in F . • The negated upgrade (resp. downgrade) axiom is a positive formula of degree 1 (resp. degree 0).

The next theorem determines the complexity of the provability of sequents given by specification of AEminium programs. Theorem 4.1 (Complexity). Let ∆ be a theory containing the definition clauses for method and constructor definitions, the definition of assig and the upgrade and downgrade axioms. Let F be the formula interpreting the main program and T a formula interpreting a property to be proven. It is decidable whether or not the sequent ?∆ ⊥ , F ⊥ , T is provable. In fact, if such a sequent is provable, then its proof is bounded in LLF by the depth k 2 where k = degree F ⊥ .

Proof. As noted before, as there are no circular recursive definitions, we may assume that the heads of definition clauses in ∆ do not contain calls for other statements, i.e., the code of such calls can be directly written as part of the head. Hence, focusing over definition clauses is completely determined by the calls in F ⊥ . Due to the synchronization procedure, proving a sequent in AEminium is equivalent to decompose its formulas completely. Therefore, the complexity of the proof of the sequent ?∆ ⊥ , F ⊥ , T is completely determined by the degree of F ⊥ since T is a purely positive formula, hence having degree 0.

In the following, we explain our verification technique for three properties.

Deadlock Detection. Consider Example 3.3. We already showed that this code leads to a deadlock since the variable s cannot upgrade its unique permission to execute collection compStats(c, s). We are then interested in providing a proof to the programmer showing that the code leads to a deadlock. For doing this, let Def be the definition of the method collection compStats and the constructor collection collection, st be the statement in the main program and A be the ok. The verification technique consists in showing that the sequent ! ∆, F ok is not provable. This verification is done automatically by using Alcove-Prover, a theorem prover for LLF developed in λ-Prolog and integrated to the tool described in Section 3.3. Basically, we look for proofs with depth less or equal to 19, given by the depth of F . If the prover fails, that means there is no proof for the sequent above.

The URL of the Alcove tool includes the output of the theorem prover and the lcc interpreter for this example. It is worth noticing that the lcc interpreter only computes a possible trace of the program while the theorem prover gives a guarantee that a certain property is verified or not by the program. The use of "animators" and provers is complementary. Existing formal models for system construction, such as the Rodin ([1]) tool for the event B modeling language, usually include both. The idea is that by using the animator the user gain a global understanding of the behavior of the program before attempting the proof of more precise desirable properties. This usually avoids frustrations in trying to figure out corrections of the model to discharge unproved properties.

Concurrency Analysis. Assume now the Example in Figure 1. For the method collection print assume that we define D

[[•]] as D[[•]]
but replacing sync(z) with "sync(z); begin print (z)" and adding "; begin print (z) → endprint(z)" in Rule RMDEF. Similarly for method collection compStats. This will allow us to specify when a method starts its execution and when it terminates.

Let

A = ∃z(D [[Def ]] S[[st]]z)
where st corresponds to the main method. One can prove the linear logic sequent

L[[A]] ∃z1, z2(begin print (z1) ⊗ begin compStats (z2)) ⊗
The provability of such a sequent means that the statements collection print(c) and collection compStats(c, s) may be executed in parallel.

Verifying a Method Specification Finally, assume that we add the field "a" in class collection and the method: m1() unq(this) ⇒ unq(this) {this.a := this} Assume also that m1 is called in the main body. The signature of m1 requires that the unique permission to the caller must be restored to the environment. Nevertheless, the implementation of the method splits the unique permission into a share permissions for the field a and another for the caller (Rule RALIAS). Then, the axiom upgrade1 cannot be used to recover the unique permission and the ask agent in definition r env remains blocked. An analysis similar to that of deadlocks will warn the programmer about this.

Concluding Remarks

We presented an approach to verify programs annotated with access-permissions. We use lcc to verify properties related to concurrency. Hence, program statements are modeled as lcc agents that faithfully represent statement permissions flow. The declarative reading of lcc agents as formulae in Linear Logic permits the use of theorem provers to verify properties such as deadlocks, the ability to run in parallel, and whether programs are correct with respect to access permission specifications. Central to our verification approach is the synchronization mechanism based on constraints and the logical interpretation of lcc. Ours is certainly a novel application for ccp that opens a new window for the automatic verification of (object-oriented) concurrent programs.

We automated our verification approach as the Alcove tool that implements a simulator and a prover. The simulator serves to animate a program by observing the evolution of its permissions. The simulator issues a message if a program blocks. It is therefore a useful companion for a verifier. A good strategy for understanding the behavior of a concurrent program is to run the simulator first to observe the global program behavior and then to run the prover to verify additional properties. We used the Alcove tool to verify the examples presented in this paper and also to verify properties about ordering of method invocations for a critical zone management system (see Appendix A). The reader can find these and other examples at the Alcove tool web-site.

Related and Future work. ccp-based calculi have been extensively used to reason about concurrent systems. The work in [START_REF] Jagadeesan | Timed constraint programming: a declarative approach to usage control[END_REF] proposes a timed-ccp model for role-based access control in distributed systems. The authors combine constraint reasoning and temporal logic model-checking to reason about when a resource (e.g. a directory in a file system) can be accessed.

Languages like AEminium [START_REF] Stork | Concurrency by default: using permissions to express dataflow in stateful programs[END_REF] and Plaid [START_REF] Sunshine | First-class state change in plaid[END_REF] offer a series of guarantees such as (1) absence of AP usage protocol violation at run time; (2) when a program has deterministic results and (3) whether programs are free of race conditions on the abstract state of the objects [START_REF] Bierhoff | Modular typestate checking of aliased objects[END_REF][START_REF] Boyland | Checking interference with fractional permissions[END_REF]. Our verification technique is complementary to those works since we have shown that well-typed programs (i.e., they follow the usage protocol of AP) can lead to a blockage.

The constraint system we propose to model the downgrade and upgrade of axioms was inspired by the work of fractional permissions in [START_REF] Boyland | Checking interference with fractional permissions[END_REF] (see also [START_REF] Bierhoff | Modular typestate checking of aliased objects[END_REF]). Fractional in this setting means that an AP can be split into several more relaxed permissions and then joined back to form a more restrictive permission. For instance, a unique permission can be split into two share permissions of weight k/2. Therefore, to recover a unique permission, it is necessary to have two k/2-share permissions. The constraint system described in this paper keeps explicitly the information about the fractions by means of the predicate ct(•).

Chalice [START_REF] Leino | Verifying concurrent programs with Chalice[END_REF] is a program verifier for OO concurrent programs that uses permissions to control memory accesses. Unlike AEminium and Plaid, concurrency in Chalice is explicitly stated by the user by means of execution threads.

AP annotations in concurrent-by-default OO languages can be enhanced with the notion of typestates [START_REF] Beckman | Verifying correct usage of atomic blocks and typestate[END_REF][START_REF] Bierhoff | Modular typestate checking of aliased objects[END_REF]. Typestates describe abstract states in the form of state-machines, thus defining a usage protocol (or contract) of objects. For instance, consider the class File with states opened and closed. The signature of the method open can be specified as the agent unq(this) ⊗ closed(this) → unq(this) ⊗ opened(this). The general idea is to verify whether a program follows correctly the usage protocol defined by the class. For example, calling the method read on a closed file leads to an error. Typestates then impose certain order in which methods can be called. The approach our paper defines can be straightforwardly extended to deal with typestates annotations, thus widening its applicability.

The work in [START_REF] Stork | Concurrency by default: using permissions to express dataflow in stateful programs[END_REF] and [START_REF] Naden | A type system for borrowing permissions[END_REF] define more specific systems and rules for access permissions to deal respectively with group permissions and borrowing permissions. A group permission represents an abstract collection of objects and allows programmers to define containers that share the same permissions to an object. The approach of borrowing permissions aims at dealing more effectively with local variable aliasing, and how permissions flow from the environment to method formal parameters. Considering these systems in Alcove amounts to refine our model of permissions in Section 3. Verification techniques should remain the same.

We intend to relax the restriction about recursion imposed on AEminium programs for obtaining a decidable analysis. More precisely, we plan to translate more involving AP based programs with controlled recursion. This can be done by finding systems with a stratified set of definition clauses, hence allowing well formed recursion in the processes declarations. This shall allow us to take into account constructors like iterators in the source program.

Finally, we plan to undertake a case study on the verification of a commercial multi-task threaded application that has been used for massively parallelising computational tasks [START_REF] Cataño | Lightweight verification of a multi-task threaded server: A case study with the plural tool[END_REF].

1 class 8 main() { 9 let collection c, stats s in 10 c := new collection() 11 s := new stats() 12 cFigure 1 .

 1891011121 Figure 1. Example of an AEminium program.

  We shall use c, c , d, d ... to denote elements in C. We recall that ! c represents the arbitrary duplication of the resource c. The entailment d c means that the information c can be deduced from the information represented by d.

Figure 2 .

 2 Figure 2. Reduced Syntax of AEminium programs. x denotes a sequence of variables x1, ...., xn. This notation is similarly used for other syntactic categories.

Figure 3 .

 3 Figure 3. Rules for the 1,⊗, ∃, ! fragment of the Intuitionistic Linear Logic (ILL). f v(A) denotes the set of free variables of formula A. Γ, ∆ denote set of formulas.

  Intuitively, u points to o.f name and then a constraint ref(u, o , p) enforces o.f name to point to o with permission p. As we shall show later, the model of constructors adds the constraint ! field(u, o, cname f name) to establish the connection between objects and their fields. The model of the assignment S[[x.f name := y]] is thus obtained from that of S[[u := y]]:

(

  RCALL) S[[x.meth(y)]]z = cname meth(x, y1, .., yn, z) if x is of type cname The model of an object initialization is defined similarly: (RNEW) S[[x := new cname(y)]]z = cname cname(x, y, z) 3.2 Modeling Class Definitions. The model of method declarations and constructors is given by the function D[[•]]. Hence, a method definition MD of the class cname of the form meth(cname x, classy y) p(x), p(y) ⇒ p (x), p (y) {s} is modeled as a process definition:(RMDEF) D[[MD]] = cname meth(x, y, z) ∆ = PMRecall that the first parameter x of the method represents the object caller this and the last parameter z is used for synchronization. The body of the definition PM models the behavior of the method as follows: PM def = ∀o, ot, n, nt(consume; ∃y , x (params ; sync(z); PB))

=

  ∀o(consume ; ∃y , x , onew(params ; ∃u(fields-init ; ∃z (S[[ s]] z ; sync(z ) → (r env(x : p, x : p ) i∈1..m r env(yi : pi, y i : p i )))))

1 let collection c, stats s in 2 collection

 12 collection(c); //c := new collection() 3 stats stats(s); //s := new stats() 4 collection compStats(c, s); //c.compStats(s) 5 collection removeDuplicates(c); //c.rDup() end The lcc agent modeling the statement in line 2 performs the call collection collection(c, z1), which triggers the execution of the body of the constructor collection (see Rules RCDEF and RCALL ). Variable z1 is the local variable used to synchronize with the rest of the program (see Rule RCOMP). Once the agents modeling the statements in lines 2 and 3 are executed, the store below is observed. ∃c, s, oc, os(ref(c, oc, unq) ⊗ ref(s, os, unq)⊗ ct(oc, s(0)) ⊗ ct(os, s(0)))

1 let

 1 collection c, stats s, stats svar in 2 collection collection(c); //c := new collection() 3 stats stats(s); //s := new stats() 4 svar := s; 5 collection compStats(c, s); //c.compStats(s) 6 end

Lemma 4 . 1 . 2 .

 412 Decomposing a focused positive formula F of degree n into its literal or purely positive subformulas gives rise to a derivation of depth n Example 4.2 (Degree of a formula). Consider the negation of the definition clause for collection collection(x, z) in Example 4.1: col collection(x, z) ⊗ ∀w1(ref(x, nil, none) ⊗sync(w1) ⊥ sync(w1)⊗∀x ,onew, w2(ref(x ,onew,unq)

  lcc agent A = ∃z(D[[Def ]] (S[[st]]z sync(z) → ok)). This agent adds the constraint ok only when the process S[[st]]z adds sync(z). According to the definition of S[[•]] and D[[•]], this happens only when the call collection compStats(c, s) is able to successfully consume the permissions required for the method (see Rule RMDEF). The translation L[[A]] will give rise to the theory ∆ and the formula F described in Example 4.1. Let F = F ⊗ sync(z)

2012/11/4

2012/11/4

2012/11/4

The numbers that follow the variable names are generated each time a local variable is created to avoid clash of names. 6 2012/11/4

On examining a proof bottom-up, decomposing the implication on the sequent Γ 1 , Γ 2 , B C D will produce the premises Γ 1 , C D and Γ 2 B. Hence it is important to guarantee that B is a T formula.

As already noted, provability in the fragment used here is the same in intuitionistic and classical settings. 7 2012/11/4

2012/11/4

2012/11/4

Acknowledgments

This work has been partially supported by grant 1251-521-28471 from Colciencias. The work of E. Pimentel and C. Olarte has been partially carried out during their visit to the Equipe Comète, at LIX (Ecole Polytechnique). Their visits have been supported resp. by Digiteo and DGAR funds for visitors. The work of N. Cataño has been supported by the Portuguese Research Agency FCT through the CMU-Portugal program, R&D Project Aeminium, CMU-PT/SE/0038/2008.

A. Critical Zone Management System

Assume the class definitions for a critical zone management system in Figure 4. There are three classes, lock, process and cs. Each critical section has a private lock managed by an object of the class cs. When a process wants to enter a critical section, it tries first to invoke method acq of the cs manager. If successful, the process obtains a lock (i.e. an object of class lock) that it uses then to enter the critical zone. When the process wants to leave the critical zone, it invokes the method release. This releases ownership of the critical section lock.

Method acq has three parameters: this, the cs manager, b the process wanting to enter the critical zone and l, a field of b that will hold the lock of the cs supplied by the manager. Since this has unique permission, only one reference to the manager object can exist for acq to be invoked. The body of method acq stores the lock in l and a reference to the manager in field s1 or s2 of b, depending on whether the lock for cs1 or for cs2 is requested. Storing this reference to the manager implies that it can no longer have unique permission, so the output permission for this becomes shared. Moreover, l holds now the only reference to the private lock of the manager, so its output permission becomes unique. The effect is that field lock1 or lock2 of object b uniquely acquires the section lock. The method enter requires a unique permission on the lock. This ensures that only one process has a reference to the lock at any given time when entering the critical section. Method release restores conditions as they were before invocation to acq, i.e. the manager regains the unique permission and stores a unique reference to its private lock. Process fields loose the lock and the reference to the manager.

Assume now the following main code: x.acq1(y, y.lock1); y.lock1.enter(y); w.acq2(z, z.lock2); z.lock2.enter(z) ; x.acq1(z, z.lock1); z.lock1.enter(z); w.acq2(y, y.lock2); y.lock2.enter(y); } where there are two section manager objects, x for cs1 and w for cs2. There are also two processes, y and z. Consider the situation where y acquires the lock from x (i.e. for cs1) by invoking the method acq1(x, y, y.lock1) and enters cs1. Then z acquires the lock from w (i.e. for cs2) by invoking acq2(w, z, z.lock2) and enters cs2. Now, z tries to acquire the lock from x by invoking acq1(x,z, z.lock1), but this is not possible because x has no longer unique permission and execution blocks. The output of Alcove for this program is:

Error: The end of the program could not be reached. Error: The perm. for cs_acq1( x1 z12 __f__lock1121 z24 ) could not be obtained.

Consider now the program where processes leave the critical section before attempting to acquire another lock: main () { let cs x, cs w, process y, process z in x:= new cs(); w := new cs(); y := new process(); z := new process(); x.acq1(y, y.lock1); y.lock1.enter(y); w.acq2(z, z.lock2); z.lock2.enter(z) ; x.release1(y.lock1, y); x.acq1(z, z.lock1); z.lock1.enter(z); w.release2(z.lock2, z); w.acq2(y, y.lock2); y.lock2.enter(y); x.release1(z.lock1, z); w.release2(y.lock2, y); } In this case, all invocations run without blockage and Alcove successfully finishes the analysis.