Christian Haack

Clément Hurlin

Separation Logic Contracts for a Java-like Language with Fork/Join

We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional permissions with abstract predicates.

As an example, we present a separation logic contract for iterators that prevents data races and concurrent modifications. Our program logic is presented in an algorithmic style: we avoid structural rules for Hoare triples and formalize logical reasoning about typed heaps by natural deduction rules and a set of sound axioms. We show that verified programs satisfy the following properties: data race freedom, absence of null-dereferences and partial correctness.

Introduction 1.Context

Over the past ten years or so, substructural logics and type systems have proven to be very valuable formalisms for reasoning about pointer-manipulating programs. Examples include static capabilities [START_REF] Crary | Typed memory management in a calculus of capabilities[END_REF][START_REF] Deline | Enforcing high-level protocols in low-level software[END_REF], alias types [START_REF] Smith | Alias types[END_REF] and separation logic [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. In these systems, the underlying specification language contains linear formulas for specifying memory access policies. Whereas traditional program logics control memory access via frame conditions, separation logic tightly integrates access policy specifications into the formula language itself. Formulas represent access tickets to heap space, and possession of access tickets gets verified statically. Access policies are tightly coupled with assertions about memory content, so that separation logic's Hoare rules make it impossible to maintain assertions that can be invalidated by thread interference or memory updates through unknown aliases. This is achieved without annoying side conditions like non-interference tests or frame conditions.

While initially separation logic mostly focused on low level programs, researchers have more recently started to adapt it to object-oriented features for use in contract languages for OO [START_REF] Parkinson | Local reasoning for Java[END_REF][START_REF] Parkinson | Separation logic and abstraction[END_REF], and very recently [START_REF] Chin | Enhancing modular OO verification with separation logic[END_REF][START_REF] Parkinson | Separation logic, abstraction and inheritance[END_REF].

Contributions

We present the careful design of a small Java-like model language with separation logic contracts, including the definition of a program logic and its soundness proof. Our language has simple threads, with fork/join as concurrency primitives. In order to facilitate concurrent reads we employ fractional permissions [START_REF] Boyland | Checking interference with fractional permissions[END_REF]. Our rules allow multiple threads to join on the same thread, in order to read-share the dead thread's resources. This is not possible with a lexically scoped parallel composition operator or with Posix threads, and is thus not supported by recent work that adapts separation logic to Posix threads [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF]. To support data abstraction and recursive data types, we use abstract predicates [START_REF] Parkinson | Separation logic and abstraction[END_REF]. Class axioms complement abstract predicates to export relations between predicates without revealing their full definitions. Abstract predicates satisfying a split/merge axiom generalize datagroups [START_REF] Leino | Data groups: Specifying the modification of extended state[END_REF], which are common in specification languages for OO. In order to support concurrent read access to whole datagroups (rather than single fields), access permission to datagroups can be split by splitting their permission parameters. In order to allow fine-grained permission-splitting for overlapping datagroups, we support datagroups with multiple permission parameters. To achieve modular soundness in the presence of subclassing, we axiomatize the "stack of class frames" [START_REF] Deline | Typestates for objects[END_REF][START_REF] Barnett | Verification of object-oriented programs with invariants[END_REF] in separation logic. We support value-parametrized classes, where class parameters have the same purpose as final ghost fields in specification languages like JML [START_REF] Leavens | Preliminary design of JML: a behavioral interface specification language for Java[END_REF]. In particular, class parameters can represent static ownership relations.

Background on Separation Logic and Fractional Permissions

Separation logic combines the usual logical operators with the points-to predicate x. f → v, the resource conjunction F * G, and the resource implication F -* G.

The predicate x. f → v has a dual purpose: firstly, it asserts that the object field x. f contains data value v and, secondly, it represents a ticket that grants permission to access the field x. f . This is formalized by separation logic's Hoare rules for reading and writing fields:

{x. f → * F}x. f = v{x. f → v * F} {x. f → v * F}y = x. f {x. f → v * v == y * F}
The crucial difference to standard Hoare logic is that both these rules have a precondition of the form x. f → . 3 This formula functions as an access ticket for x. f . It is important that tickets are not forgeable. One ticket is not the same as two tickets! For this reason, the resource conjunction * is not idempotent: F is not equivalent to F * F. The resource implication -* matches the resource conjunction *, in the sense that the modus ponens law is satisfied: F * (F -* G) implies G. However, F * (F -* G) does not imply F * G. In English, F -* G is pronounced as "consume F yielding G". In terms of tickets, F -* G permits to trade ticket F and receive ticket G in return.

Separation logic is particularly useful for concurrent programs: two concurrent threads simply split the resources that they may access, as formalized by the rule for the parallel composition t | t ′ of threads t and t ′ [START_REF] O'hearn | Resources, concurrency and local reasoning[END_REF].

{F}t{G} {F ′ }t ′ {G ′ } {F * F ′ }t | t ′ {G * G ′ }
With this concurrency rule, separation logic prevents data races. There is a caveat, though. The rule does not allow concurrent reads. Boyland [START_REF] Boyland | Checking interference with fractional permissions[END_REF] solved this problem with a very intuitive idea, which was later adapted to separation logic [START_REF] Bornat | Permission accounting in separation logic[END_REF]. The idea is that (1) access tickets are splittable, (2) a split of an access ticket still grants read access and (3) only a whole access ticket grants write access. To account for multiple x

. f π -→ v is equivalent to x. f π/2 -→ v * x. f π/2 -→ v.
In the Hoare rules, writing requires the full fraction 1, whereas reading just requires some fraction π:

{x. f 1 -→ * F}x. f = v{x. f 1 -→ v * F} {x. f π -→ v * F}y = x. f {x. f π -→ v * v == y * F}
Permission-accounting separation logic maintains the global invariant that the sum of all fractional permissions to the same cell is always at most 1. This prevents read-write and write-write conflicts, but permits concurrent reads.

In our Java-like language, we use ASCII and write Perm(x. f , π) for x. f π -→ , and PointsTo(x. f , π, v) for x. f π -→ v.

Example: A Usage Protocol for Iterators

Often one wants to constrain object clients to adhere to certain usage protocols. Object usage protocols can, for instance, be specified in typestate systems [START_REF] Deline | Typestates for objects[END_REF] or, using ghost fields, in general purpose specification languages. A limitation of these techniques is that state transitions must always be associated with method calls. This is sometimes not sufficient. Consider for instance a variant of Java's Iterator interface (enriched with an init method to avoid constructor contracts):

interface Iterator { void init(Collection c); boolean hasNext(); Object next(); void remove(); } If iterators are used in an undisciplined way, there is the danger of unwanted concurrent modification of the underlying collection (both of the collection elements and the collection itself). Moreover, in concurrent programs bad iterator usage can result in data races. It is therefore important that Iterator clients adhere to a usage discipline. Figure 1 shows a state machine that defines a safe iterator usage discipline. Unfortunately, the dashed transitions are not supported by existing typestate systems, because they are not associated with method calls. Specifying this protocol with classical program logics would be clumsy. In [START_REF] Girard | Linear logic: Its syntax and semantics[END_REF] The interface has two parameters: firstly, a permission p and, secondly, the iteratee. If the permission parameter is instantiated by a fraction p < 1, one obtains a read-only iterator, otherwise a read-write iterator. The states of our our state diagram are represented by three abstract predicates: ready, readyForNext and readyForRemove.

Class axioms express relations between abstract predicates, without revealing the complete predicate definitions. Implementations must define the abstract predicates by separation logic formulas such that the class axioms are tautologically true. In the example, the two class axioms represent the dashed transitions of the state machine. We represent the heap space associated with an object by a generic datagroup state, which has a default definition in the Object class and needs to be overridden by each class. The definition of this state predicate should describe the heap space associated with the object. Often this heap space will consist of the object's fields only, but sometimes it will also include other objects and change dynamically, as in the case of Collection objects. The state predicate is parametrized by a fraction so that it can be read-shared.

The precondition of init() consumes a fraction p of the access right for the iteratee and puts the iterator in the ready state. The crux is that, by linearity, the iterator client temporarily looses a p-fraction of the access right on the collection, which he can only gain back by "invoking" the first class axiom. The init predicate in init()'s precondition is a special abstract predicate that every object enters right after object creation and that grants access to all of the object's fields.

The postcondition of hasNext() uses a resource implication whose antecedent is a boolean expression. We treat boolean expressions as copyable resources that satisfy e -* (e * e). 4 Furthermore, hasNext()'s postcondition uses additive conjunction &. A resource satisfies F & G, if it satisfies both F and G. 5 Operationally, & represents choice. If F & G holds, then F and G are available, but are interdependent: using either one of them destroys the other one, too. Additive conjunction can conveniently represent nondeterministic state transitions, as exhibited in hasNext()'s postcondition. Note that this postcondition allows clients to stay in the ready-state, even if hasNext()==true. This can, for instance, be useful for removing the 10th element of an ordered collection.

In our companion report [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF], we have implemented the Iterator interface for a doubly linked list implementation of the Collection interface. In [START_REF] Haack | Resource usage protocols for iterators[END_REF], we refine the protocol to support unrestricted access to immutable collection elements, and to support shallow collections that do not govern access to their elements.

Example: Representing Datagroups

We represent datagroups [START_REF] Leino | Data groups: Specifying the modification of extended state[END_REF] req state<p>; ens state<p>; void display(); } intuitionistic separation logic F -* G is a tautology if and only if F ⇒ G is. However, in our implementations of the Iterator interface, we use true resource implications that cannot be replaced by classical implications. In this paper, we avoid classical implication because having just one implication simplifies the natural deduction rules for reasoning about resources.

Example: Recursive and Overlapping Datagroups

Our next example illustrates that multiple threads can concurrently access overlapping datagroups, as long as they only read-access their intersection. Consider a linked list that implements a simple class roster. Each node stores a student identifier and a grade. We design the roster interface so that multiple threads can concurrently read the roster. Moreover, when a thread updates the grades we allow other threads to concurrently read the student identifiers. To this end, the interface defines two datagroups ids and links<p,q> and grades and links<p,q> that overlap in the links of the list. The permission parameter p is associated with the student id fields and grade fields, respectively. The permission parameter q is associated with the links. The updateGrade() method requires write access (permission 1) for the grades and read access for the links and ids. The contains() method requires read permission for the ids and the links. The axiom exposes that the state datagroup is the union of the datagroups ids and links and grades and links and that these datagroups overlap on the links. In our companion report [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF], we have implemented this interface.

A Model Language with Separation Logic Contacts

Syntax

We distinguish between read-only variables ı, read-write variables ℓ, and logic variables α. Method parameters (including this) are read-only. Logic variables can only occur in specifications and types. They range over both fractional permissions and values (like integers, object identifiers and null).

C, D ∈ ClassId I ∈ InterId s,t ∈ TyId = ClassId ∪ InterId o, p, q ∈ ObjId f ∈ FieldId m ∈ MethId P ∈ PredId ı ∈ RdVar ℓ ∈ RdWrVar α ∈ LogVar x, y, z ∈ Var = RdVar ∪ RdWrVar ∪ LogVar
We include read-only variables (but not read-write variables) in the syntax domain of values. This is convenient for our substitution-based operational semantics. Fractional permissions are represented symbolically: split n (1) represents the concrete fraction In examples, we often leave these quantifiers over logic variables implicit. Interfaces may declare abstract predicates and classes must implement them by providing concrete definitions as separation logic formulas. Like [START_REF] Parkinson | Separation logic and abstraction[END_REF], we allow abstract predicates to have parameters in addition to the implicit self-parameter (as listed in the typed formal parameter lists T ᾱ). The types T for predicate parameters range over all Java types and the distinguished type perm for fractional permissions.

We assume that the Object class declares a distinguished datagroup called state: Semantically, the extension F of abstract predicate P gets *-conjoined with P's definition in C's superclass D. We do not allow arbitrary predicate redefinitions in subclasses in order to facilitate modular verification, avoiding re-verification of inherited methods. • The type "perm" may only occur inside angle brackets or specification formulas.

• Cyclic predicate definitions in ct must be positive.

The first syntactic restriction ensures that fractional permissions do not spill into the executable part of the language. The second syntactic restriction ensures that predicate implementations (which can be recursive) are well-founded. We allow negative dependencies of predicate P on predicate Q as long as Q does not also depend on P. We use the symbol ct for the partial order on type identifiers induced by class table ct, usually leaving the subscript ct implicit. We write s ≺ 1 t when s and t are neighbours with respect to . Subtyping is inductively defined by the following rules:

T <: T T <: U,U <: V ⇒ T <: V s< T ᾱ> ext t< π′ > ⇒ s< π> <: t< π′ [ π/ ᾱ]> t< π> <: Object t< T ᾱ> impl I<π ′ > ⇒ t< π> <: I< π′ [ π/ ᾱ]>
We assume that class tables always contain the following class declaration:

class Thread ext Object { final void fork(); final void join(); req false; ens true; void run() { null } }

The run-method is meant to be overridden. The contracts for fork and join are omitted, because our verification system ignores them anyway. Instead, it uses the precondition for run as the precondition for fork and the postcondition for run as the postcondition for join. The methods fork and join do not have implementations, but the operational semantics treats them in a special way 6

= ℓ = v | ℓ = op( v) | ℓ = v. f | v. f = v | ℓ = (T )v | ℓ = new C< π> | if (v){c}else{c ′ } | ℓ = v.m< π>( v) | assert(F) Synt.
Restr.: Logic variables that occur in ℓ = new C< π> must be bound by class parameters.

Our command language assumes that Java-like commands have been transformed so that intermediate values are always assigned to local variables. Following [START_REF] Igarashi | Featherweight Java: a minimal core calculus for Java and GJ[END_REF], we assume that methods only return at the end of their body. We omit the return-command. Values are included in the syntax domain of commands, so that a terminating, nonblocking execution of a command results in the return value. Methods of type void return null, which is the only member of type void. We usually omit terminating occurrences of null. The operator for existential unpacking has no effect at runtime. It makes the existential variable α available in the continuation c for instantiation of logic method parameters. In examples, we often omit explicit existential unpacking and instantiation of logic method parameters. Making these explicit helps with the theory.

Operational Semantics

Runtime Structures: ,c) programs Each thread "s in c" consists of a thread-local stack s and a process continuation c. In thread pools, each thread t is associated with a unique object identifier, which serves as a thread identifier. The dynamic semantics of our language is a small-step operational semantics st → ct st ′ and can be found in [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF].

ClVal = Val \ RdVar closed values s ∈ Stack = RdWrVar ⇀ ClVal stacks t ∈ Thread = Stack × Cmd ::= s in c threads ts ∈ ThreadPool = ObjId ⇀ Thread ::= o 1 is t 1 | • • • | o n is t n thread pools os ∈ ObjStore = FieldId ⇀ ClVal object stores obj ∈ Obj = Ty × ObjStore ::= (T, os) objects h ∈ Heap = ObjId ⇀ Obj heaps st ∈ State = Heap × ThreadPool ::= h, ts states prog ∈ Program = ClassTable × Cmd ::= (ct
There is one (and only one) reduction rule where our operational semantics depends on class parameters, namely the reduction rule for type casts. Downcasts to parametrized types require a runtime check that looks at the type parameters, which the standard JVM does not keep track of. There are at least three ways how one could deal with that in practice: Firstly (and most pragmatically), one could simply forbid downcasts to reference types that have a non-empty parameter list. Secondly, one could develop an enhanced virtual machine that keeps track of class parameters. Thirdly, one could devise a syntactic translation that erases class parameters such that the target of this translation throws a ClassCastException whenever the source does. e. f points to e ′ and the access permission for e. f is π Perm(e.join, π) permission to use a split of join's postcondition π.κ< π′ > predicate π.κ applied to π′ F lop G binary logical operator

Specification Formulas and Their Semantics

(qt T α)(F) quantifier Derived forms: F *-* G ∆ = (F -* G) & (G -* F) F assures G ∆ = F -* (F * G) F ispartof G ∆ = G -* (F * (F -* G))
The formula semantics is defined by a Kripke resource interpretation [START_REF] O'hearn | The logic of bunched implications[END_REF] of the form Γ ⊢ E ; R; s |= F, where Γ is a type environment, E is a predicate environment that maps predicate names to predicates, R is a resource, and s is a stack. Resources are triples R = (h, P, Q) of heaps h and two permission tables P and Q. Permission tables are functions of type ObjId × (FieldId × {join}) → [0, 1] that map fields and join to fractional permissions. The resource components h and P are local resources, whereas Q is a global resource. We denote the projections to the resource components by R hp , R loc and R glo . The definition of the forcing relation |= is pretty standard, and we refer to [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF] for details.

Soundness Theorems

Below, we define a verification system whose top level judgment is prog : ⋄ (read: "prog is verified"). We have proven a preservation theorem from which we can draw several corollaries, namely, data race freedom, null error freedom and partial correctness.

A pair (hc, hc ′ ) of head commands is called a data race iff hc = (o. f = v) and either

hc ′ = (o. f = v ′ ) or hc ′ = (ℓ = o. f ) for some o, f , v, v ′ , ℓ. A head command hc is called a null error iff hc = (ℓ = null. f ) or hc = (null. f = v) or hc = (ℓ = null.m< π>( v)). We define initial states: init(c) = {main → (Thread, / 0)}, main is ( / 0 in c)
, where main is some distinguished object id for the main thread. The main thread has an empty set of fields (hence the first / 0), and its stack is initially empty (hence the second / 0).

Theorem 1 (Verified Programs are Data Race Free). ) for some Γ , E , R such that R hp = h, and σ ∈ LogVar ⇀ SpecVal.

If (ct, c) : ⋄ and init(c) → * ct h, ts | o 1 is (s 1 in hc 1 ; c 1 ) | o 2 is (s 2 in hc 2 ; c 2 ) , then (hc 1 , hc 2 ) is not a data race.

Method Subtyping

Method types are of the following form:

< T ᾱ> req F; ens G; U m(V 0 ı 0 ; V ī)
In method types, we make the self-parameter explicit, separated from the other formal parameters by a semicolon. In the scheme above, ı 0 is the self-parameter.

Before presenting the method subtyping rule in full generality, we present its instance for method types without logic parameters:

U,V 0 , V ′ <: U ′ ,V ′ 0 , V Γ , ı 0 : V 0 , ī : V ′ ; ı 0 ; true ⊢ F ′ -* (F * (fa U result)(G -* G ′ )) Γ ⊢ req F; ens G; U m(V 0 ı 0 ; V ī) <: req F ′ ; ens G ′ ; U ′ m(V ′ 0 ı 0 ; V ′ ī)
This rule has the following two derived rules (where types are elided):

⊢ F ′ -* F ⊢ G ′ -* G ⊢ req F; ens G <: req F ′ ; ens G ′ ⊢ req F; ens G <: req F * H; ens G * H
The first of these derived rules is standard behavioural subtyping, the second one abstracts separation logic's frame rule. In order to see that these two rules follow from the above rule, note that the following two formulas are tautologies (as can be easily proven by natural deduction):

(F ′ -* F) * H -* F ′ -* F * H F * H -* F * (fa U x)(G -* G * H)
The general method subtyping rule also accounts for logic parameters:

8 m = run T ′ ,U,V 0 , V ′ <: T ,U ′ ,V ′ 0 , V Γ , ı 0 : V 0 ; ı 0 ; true ⊢ (fa T ′ ᾱ)(fa V ′ ī)(F ′ -* (ex W ᾱ′ )(F * (fa U result)(G -* G ′ ))) Γ ⊢ < T ᾱ, W ᾱ′ > req F; ens G; U m(V 0 ı 0 ; V ī) <: < T ′ ᾱ> req F ′ ; ens G ′ ; U ′ m(V ′ 0 ı 0 ; V ′ ī)
Note that the subtype may have more logic parameters than the supertype. For instance, we obtain the following derived rule:

⊢ <T α> req F; ens G <: req (ex T α)(F); ens (ex T α)(G)
This derived rule is an abstraction of separation logic's auxiliary variable rule. It follows from the method subtyping rule by the following tautology:

(ex T α)(F) -* (ex T α)(F * (fa U x)(G -* (ex T α)(G)))

Hoare Triples

Our Hoare rules are syntax-directed, omitting structural rules. Separation logic's frame rule is admissible. Separation logic's auxiliary variable rule is subsumed by our syntax for existential unpacking. We omit the rules of conjunction and disjunction, and did not need them in the examples we considered. We could soundly add the rule of disjunction.

To add the rule of conjunction, we would need to assume that preconditions of run() are supported [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF]. 9Hoare triples have the forms (Γ ; v ⊢ {F}c : T {G}) and (Γ ; v ⊢ {F}hc{G}), where v is the receiver parameter. We present a few selected rules and refer to [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF] for the complete rule system.

The rules for reading and writing fields are standard:

Γ ; v; F ⊢ PointsTo(w. f , π, u) Γ ⊢ w : U T f ∈ fld(U) T [w/this] <: Γ (ℓ) ℓ ∈ F Γ ; v ⊢ {F}ℓ = w. f {F * ℓ == u} Γ ⊢ v, F : Object, ⋄ Γ ⊢ u : U T f ∈ fld(U) Γ ⊢ w : T [u/this] Γ ; v ⊢ {F * PointsTo(u. f , 1, T )}u. f = w{F * PointsTo(u. f , 1, w)}
The rule for forking a thread consumes run's precondition. The postcondition of fork() is empty. 10 The rule makes use of the function mtype(m, T ), which looks up m's type in the smallest supertype of T that declares m:

mtype(run, T ) = req G; ens G ′ ; void run(T ı 0 ; ) ℓ ∈ F Γ (ℓ) = void Γ ⊢ u : T <: Thread Γ ; v; F ⊢ u != null Γ ; v ⊢ {F * G[u/ı 0 ]}ℓ = u.fork(){F}
The most interesting rule is the one for joining threads. It allows the caller to exchange a fraction fr of the join-permission Perm(u.join, 1) for a fraction fr of u.run's postcondition: 11mtype(run, T ) = req G; ens G ′ ; void run(T ı 0 ;

) fr = all or G ′ is supported ℓ ∈ F Γ (ℓ) = void Γ ⊢ u : T <: Thread Γ ; v; F ⊢ u != null Γ ; v ⊢ {F * fr • Perm(u.join, 1)}ℓ = u.join(){F * fr • G ′ [u/ı 0 ]}
Here, fr ranges over linear combinations. These represent numbers of the forms 1 or Via the bijection fr(bits) → ∑ n i=1 bit i • 1 2 i , we can define an addition on linear combinations that reflects the addition on concrete binary fractions. For proving soundness of the join()-rule, it is crucial that join()'s postcondition satisfies the following distributivity law, which holds if G ′ is supported:

∑ n i=1 bit i • 1 2 i : bit ∈ {0, 1} bits
(fr 1 + fr 2 ) • G ′ *-* (fr 1 • G ′ * fr 2 • G ′ )

Comparison to Related Work and Conclusion

Parkinson/Bierman are the first to adapt separation logic to a Java-like language [START_REF] Parkinson | Local reasoning for Java[END_REF][START_REF] Parkinson | Separation logic and abstraction[END_REF]. We build on their work, using abstract predicates, but extend it to a concurrent language and combine abstract predicates with fractional permissions.

Boyland and Retert [START_REF] Boyland | Connecting effects and uniqueness with adoption[END_REF] explain the relation between write-effects, uniqueness and datagroups in terms of a linear type-and-effect system. Their system features a nesting operation and recursive definitions, which serve as an abstraction mechanism similar to abstract predicates, but in addition promote linear formulas to non-linear ones. Recently, Boyland presented a semantics for formulas that combine nesting and fractional permissions [START_REF] Boyland | Semantics of fractional permissions with nesting[END_REF]. His semantics is quite different from ours. Generally speaking, our semantics is closer to standard semantics of BI [START_REF] O'hearn | The logic of bunched implications[END_REF]. Boyland facilitates permission splitting for datagroups through an operation that scales formulas by fractions, whereas we require datagroups to be fully permission-parametrized and scale the parameters. Because we allow multiple parameters, our approach permits more fine-grained scaling for overlapping datagroups (see Section 1.6 for an example).

Bierhoff and Aldrich [START_REF] Bierhoff | Modular typestate verification of aliased objects[END_REF] combine typestates and fractional permissions to specify object usage protocols. They use iterators as an example, but they do not allow linear implications in method contracts. As a result, their usage protocol regulates access to the collection itself, but not access to the elements of the collection, and their protocol would not prevent data races in concurrent programs. Krishnaswami [START_REF] Krishnaswami | Reasoning about iterators with separation logic[END_REF] (in higherorder separation logic) and Boyland et al [START_REF] Boyland | Iterators can be independent "from" their collections[END_REF] (in their linear type-and-effect system) present iterator contracts that use linear implication and are related to ours.

Gotsman et al [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF] recently adapted concurrent separation logic to Posix threads, treating storable locks. They do not support read-sharing of join's postcondition like us.

Regarding the interplay between abstract predicates and subclassing, we axiomatize the "stack of class frames" [START_REF] Deline | Typestates for objects[END_REF][START_REF] Barnett | Verification of object-oriented programs with invariants[END_REF] to control predicate extensions in subclasses. The stack of class frames supports the use of subclassing for specialization and is well-suited for dealing with extended object state. Furthermore, the stack of class frames facilitates fully modular verification, avoiding the need to re-verify inherited methods, which is required in [START_REF] Parkinson | Local reasoning for Java[END_REF][START_REF] Parkinson | Separation logic and abstraction[END_REF] where unrestricted predicate re-definitions in subclasses are allowed. In recent work, Parkinson and Bierman argue that a verification systems should support subclassing for code reuse in addition to subclassing for specialization, and present a system that supports both uses of subclassing while avoiding re-verification of inherited methods [START_REF] Parkinson | Separation logic, abstraction and inheritance[END_REF]. To this end, they associate with each method two contracts: a concrete "static" contract, and an abstract "dynamic" contract. Their system checks that predicate re-definitions in subclasses are compatible with concrete static contracts of inherited methods, thereby avoiding re-verification of implementations of inherited methods. The advantage over the stack of class frames is increased flexibility, the disadvantage is heavier specification machinery, although much of this can be hidden behind good defaults. Chin et al [START_REF] Chin | Enhancing modular OO verification with separation logic[END_REF] make a similar proposal.

Conclusion. We have presented a variant of concurrent separation logic with fractional permissions for a Java-like language with fork/join and proved it sound. Future work includes algorithmic checking and extension to handle lock synchronization.

Fig. 1 .

 1 Fig. 1. Usage Protocol for Iterators

  n ∈ Int integers b ∈ Bool = {true, false} booleans u, v, w ∈ Val ::= null | n | b | o | ı values π ∈ SpecVal ::= v | 1 | split(π) | α specification values T,U,V,W ∈ Ty ::= void | int | bool | t< π> | perm types Interface Declarations: F ∈ Formula ::= . . . specification formulas (defined in Section 2.3) spec ::= req F; ens F; pre-and postconditions mt ::= < T ᾱ> spec U m( V ī) method types (scope of ᾱ, ī is T , spec,U, V ) pt ::= pred P< T ᾱ> predicate types ax ::= axiom F class axioms int ∈ Interface ::= interface I< T ᾱ> ext Ū {pt* ax* mt*} interfaces (scope of ᾱ is T , Ū, pt*, ax*, mt*) Syntactic restriction: The type "perm" may only occur inside angle brackets or formulas.Method types include pre-and postconditions and are parametrized by logic variables.

class

  Object { group state<perm p> = true; } This datagroup represents the access permissions for the object state. Every class must extend it and thereby define what the object states of its instances are. Our syntax for predicate extensions is as follows: class C ext D { ... ext pred P< T x> by F; ... }

  P< T ᾱ> = F root definition (scope of ᾱ is F) final? ext pred P< T ᾱ> by F extension (scope of ᾱ is F) md ::= final? < T ᾱ> spec U m( V ī){c} method (scope of ᾱ, ī is T , spec,U, V , c) cl ∈ Class ::= final? class C< T ᾱ> ext U impl V {fd* pd* ax* md*} class (scope of ᾱ is T ,U, V ,fd*, pd*, ax*, md*) ct ⊆ Interface ∪ Class class tables Syntactic restrictions:

  Commands: op ∈ Op ⊇ {==, !, &, |} ∪ {C isclassof | C ∈ ClassId } c ∈ Cmd ::= commands v return value (or null in case of type void) T ℓ; c local variable declaration (scope of ℓ is c) final T ı = ℓ; c local read-only variable declaration (scope of ı is c) unpack (ex T α)(F); c unpacking an existential (scope of α is F, c) hc; c first do hc, then do c hc ∈ HeadCmd ::

  Specification Formulas: e ∈ Exp ::= π | ℓ | op( ē) lop ∈ {*, -*, &, |} qt ∈ {ex, fa} κ ∈ Pred ::= predicates P P at receiver's dynamic class P@C P at class C E, F, G, H ∈ Formula ::= specification formulas e boolean expression PointsTo(e. f , π, e ′ )

Theorem 2 (

 2 Verified Programs are Null Error Free). If (ct, c) : ⋄ and init(c) → * ct h, ts | o is (s in hc; c) , then hc is not a null error. Theorem 3 (Partial Correctness). If (ct, c) : ⋄ and init(c) → * ct h, ts | o is (s in assert(F); c) , then (Γ ⊢ E ; R; s |= F[σ ]

::= 1 |

 1 bit, bits fr ∈ BinFrac ::= all | fr() | fr(bits)To define the scalar multiplication fr • F, we first extend the split-operation from permissions to formulas:split(e) ∆ = e split(π.κ< π′ >) ∆ = π.κ<split( π′ )> split(PointsTo(e. f , π, e ′ )) ∆ = PointsTo(e. f , split(π), e ′ ) split(Perm(e.join, π)) ∆ = Perm(e.join, split(π)) split(F lop G) ∆ = split(F) lop split(G) split((qt T α)(F)) ∆ = (qt T α)(split(F))Now, the scalar multiplication fr • F is defined as follows: all • F = F, fr() • F = true, fr(1)•F = split(F), fr(0, bits)•F = fr(bits)•split(F), and fr(1, bits)•F = split(F) * fr(bits)• split(F). For instance, fr(1, 0, 1) • F *-* (split(F) * split 3 (F)).

  (Section 1.1.4), Girard explains how linear implications can be used to logically represent state transitions. Applying this idea to the iterator protocol, we obtain the following formalization where the dashed transitions are represented by resource implications:

	interface Iterator<perm p, Collection iteratee> {
	pred ready;	// prestate for iteration cycle
	pred readyForNext;	// prestate for next()
	pred readyForRemove<Object element>; // prestate for remove()
	axiom ready -* iteratee.state<p>;	// stop iterating
	axiom readyForRemove<e> * e.state<p> -* ready; // back to ready
	req init * c.state<p> * c==iteratee; ens ready;
	void init(Collection c);
	req ready; ens ready & (result -* readyForNext);
	boolean hasNext();
	req readyForNext; ens result.state<p> * readyForRemove<result>;
	Object next();
	req readyForRemove< > * p==1; ens ready;
	void remove();
	}

  as abstract predicates satisfying a datagroup axiom that says split/merging datagroup parameters split/merges datagroups:

	interface Sprite {
	group position<perm p>;
	group color<perm p>;
	axiom position<p> ispartof state<p>;
	axiom color<p> ispartof state<p>;
	req position<1>; ens position<1>;
	void updatePosition();
	req color<1>; ens color<1>;
	void updateColor();
	req state<1>; ens state<1>;
	void update();

group P< T x>; ∆ = pred P< T x>; axiom P< x> *-* (P< ē> * P< ē>); where e i ∆ = x i /2, if T i = perm, and e i ∆ = x i , otherwise The formula F *-* G is short for (F -* G) & (G -* F). Here are simple examples of a legal and an illegal datagroup definition (where | is disjunction): group P<perm p> = Perm(this.f, p) * Perm(this.g, p); legal because the datagroup axiom holds group P<perm p> = Perm(this.f, p) | Perm(this.g, p); illegal because the datagroup axiom's right-to-left direction does not hold On the right, you see a fractional permission version of Leino's running example [21]. The datagroups position and color are nested in state, as expressed by the two class axioms. The formula "F ispartof G" is a derived form for G -* (F * (F -* G)). Intuitively, this formula says that F is a physical part of G: one can take G apart into F and its complement F -* G, and one can put the two parts back together to obtain G back.

  1 2 n . In examples, we sometimes write1 2 n as syntax sugar for split n (1). Specification values union values and fractional permissions. Interfaces and classes are parametrized by specification values. Correspondingly, object types t< π> instantiate the parameters.

  : o.fork() creates a new thread, whose thread identifier is o, and executes o.run() in this thread. The o.fork-method should not be called more than once (on the same receiver o). A second call results in blocking. o.join() blocks until thread o has terminated.

x. f → is short for (∃v)(x. f → v).

We could equivalently use classical implication: result ⇒ readyForNext. Even the two class axioms could equivalently use classical implication, because they are tautologies, and in

In contrast, a resource satisfies F * G if it can be split into separate resources, one of which satisfies F and the other satisfies G.

In reality, they would be implemented natively.

The Verification System3.1 Proof TheoryMany presentations of separation logic are based on a model-theoretic logical consequence. We, instead, define logical consequence proof-theoretically. This gives our system an algorithmic flavour, similar to recent static assertion checkers for fragments of separation logic[START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF][START_REF] Chin | Enhancing modular OO verification with separation logic[END_REF] that are built upon proof-theoretic decision procedures[START_REF] Boyland | Connecting effects and uniqueness with adoption[END_REF] .Γ ; v; F ⊢ G from v's point of view, G is a logical consequence of the * -conjunction of F Γ ; v ⊢ F from v's point of view, F is an axiomIn the former judgment, F is a multiset of formulas. The parameter v represents the current receiver, which is needed to determine the scope of predicate definitions. The logical consequence judgment is driven by standard natural deduction rules that are common to the logic of bunched implications[START_REF] O'hearn | The logic of bunched implications[END_REF] and linear logic[START_REF] Wadler | A taste of linear logic[END_REF]. These rules are detailed in[START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF]. We admit weakening, because Java is a garbage-collected language. The link between Γ ; v; F ⊢ G and the axiom judgment Γ ; v ⊢ F is established by the following rule. (We omit the definitions of typing judgments Γ ⊢ v : T and Γ ⊢ F : ⋄.)[START_REF] Boyland | Connecting effects and uniqueness with adoption[END_REF] Unfortunately, these fragments do not include -*, as needed for our iterator implementation.

The subtyping rule for run is restricted to avoid dependencies between pre-and postcondition.

Supported formulas are formulas that have the property that, for any resource, the set of subresources that satisfy it is either empty or has a least element. They play a similar role for intuitionistic predicates, as precise formulas for non-intuitionistic predicates[START_REF] O'hearn | Separation and information hiding[END_REF]. In our variant of separation logic, all predicates are intuitionistic, as we admit weakening.

The permission Perm(u.join, 1) gets introduced when the thread object u is created.

We assume that postconditions of methods with return type void do not mention the resultvariable.

Acknowledgments. We thank John Boyland, Marieke Huisman, Erik Poll and anonymous reviewers for their very useful comments that helped to improve this paper.

⋆ Supported in part by IST-FET-2005-015905 Mobius project. ⋆⋆ Supported in part by IST-FET-2005-015905 Mobius and ANR-06-SETIN-010 ParSec project.

We now define the complete set of axioms. First, we repeat the split/merge law: For the following axioms, recall that "F assures G" abbreviates "F -* (F * G)".

The third of these axioms implies that boolean expressions are copyable: e -* (e * e).

The following axiom lifts semantic validity of boolean expressions (which we do not axiomatize) to our proof theory:

The next axiom allows to apply class axioms. Here, axiom(t< π′ >) is the *-conjunction of all class axioms in t< π′ > and its supertypes.

The open/close axiom allows predicate receivers to replace abstract predicates by their definitions. It uses a function pbody(v.P< π>,C< π′ >) that returns the extension F of predicate v.P< π> in class C< π′ >.

⇒ Γ ; v ⊢ v.P@C< π, π′ > *-* (F * v.P@D< π>)

Note that the current receiver, as represented on the left of ⊢, has to match the predicate receiver on the right. This rule is the only reason why our logical consequence judgment tracks the current receiver. Note also that P@C may have a higher arity than P@D: following [START_REF] Parkinson | Separation logic and abstraction[END_REF] we allow subclasses to extend predicate arities.

The following axiom deals with unqualified predicates with missing parameters:

The following axioms capture additional facts about abstract predicates. Recall that "F ispartof G" is defined as G -* (F * (F -* G)).

The next axioms allow to drop the class modifier C from π.P@C, if we know that C is π's dynamic class:

Here, the expression "π isclassof C" evaluates to true whenever C is π's dynamic class. "C isclassof π" surely holds right after object π of class C has been created. Consequently, our Hoare rules introduce it as a postcondition of object creation commands. The second axiom makes use of final classes (resp. predicates), which are classes (resp. predicates) that are prohibited to be extended.