key: cord-0047710-pbj8my6n
authors: Brotherston, James; Costa, Diana; Hobor, Aquinas; Wickerson, John
title: Reasoning over Permissions Regions in Concurrent Separation Logic
date: 2020-06-16
journal: Computer Aided Verification
DOI: 10.1007/978-3-030-53291-8_13
sha: 4b20ba8d83fb3d3417c1b7603d88c20ed7002a7c
doc_id: 47710
cord_uid: pbj8my6n

We propose an extension of separation logic with fractional permissions, aimed at reasoning about concurrent programs that share arbitrary regions or data structures in memory. In existing formalisms, such reasoning typically either fails or is subject to stringent side conditions on formulas (notably precision) that significantly impair automation. We suggest two formal syntactic additions that collectively remove the need for such side conditions: first, the use of both “weak” and “strong” forms of separating conjunction, and second, the use of nominal labels from hybrid logic. We contend that our suggested alterations bring formal reasoning with fractional permissions in separation logic considerably closer to common pen-and-paper intuition, while imposing only a modest bureaucratic overhead.

Concurrent separation logic (CSL) is a version of separation logic designed to enable compositional reasoning about concurrent programs that manipulate memory possibly shared between threads [6, 26] . Like standard separation logic [28] , CSL is based on Hoare triples {A} C {B}, where C is a program and A and B are formulas (called the precondition and postcondition of the code respectively). The heart of the formalism is the following concurrency rule:

where is a so-called separating conjunction. This rule says that if two threads C 1 and C 2 are run on spatially separated resources A 1 A 2 then the result will be the spatially separated result, B 1 B 2 , of running the two threads individually. However, since many or perhaps even most interesting concurrent programs do share some resources, typically does not denote strict disjoint separation of memories, as it does in standard separation logic (where it is usually written as * ).

Instead, it usually denotes a weaker sort of "separation" designed to ensure that the two threads at least cannot interfere with each others' data. This gives rise to the idea of fractional permissions, which allow us to divide writeable memory into multiple read-only copies by adding a permission value to each location in heap memory. In the usual model, due to Boyland [5] , permissions are rational numbers in the half-open interval (0, 1], with 1 denoting the write permission, and values in (0, 1) denoting read-only permissions. We write the formula A π , where π is a permission, to denote a "π share" of the formula A. For example, (x → a) 0.5 (typically written as x 0.5 → a for convenience) denotes a "half share" of a single heap cell, with address x and value a. The separating conjunction A B then denotes heaps realising A and B that are "compatible", rather than disjoint: where the heaps overlap, they must agree on the data value, and one adds the permissions at the overlapping locations [4] . E.g., at the logical level, we have the entailment:

Happily, the concurrency rule of CSL is still sound in this setting (see e.g. [29] ). However, the use of this weaker notion of separation causes complications for formal reasoning in separation logic, especially if one wishes to reason over arbitrary regions of memory rather than individual pointers. There are two particular difficulties, as identified by Le and Hobor [24] . The first is that, since denotes possibly-overlapping memories, one loses the main useful feature of separation logic: its nonambiguity about separation, which means that desirable entailments such as A 0.5 B 0.5 |= (A B) 0.5 turn out to be false. E.g.:

Here, the two "half-pointers" on the LHS might be aliased (x = y and a = b), meaning they are two halves of the same pointer, whereas on the RHS they must be non-aliased (because we cannot combine two "whole" pointers). This ambiguity becomes quite annoying when one adds arbitrary predicate symbols to the logic, e.g. to support inductively defined data structures.

The second difficulty is that although recombining single pointers is straightforward, as indicated by Eq. (1), recombining the shares of arbitrary formulae is challenging. E.g., A 0.5 A 0.5 |= A, as shown by the counterexample

The LHS can be satisfied by a heap with a 0.5-share of x and a 0.5-share of y, whereas the RHS requires a full (1) share of either x or y.

Le et al. [24] address these problems by a combination of the use of tree shares (essentially Boolean binary trees) rather than rational numbers as permissions, and semantic restrictions on when the above sorts of permissions reasoning can be applied. For example, recombining permissions (A 0.5 A 0.5 |= A) is permitted only when the formula is precise in the usual separation logic sense (cf. [28] ). The chief drawback with this approach is the need to repeatedly check these side conditions on formulas when reasoning, as well as that said reasoning cannot be performed on imprecise formulas.

Instead, we propose to resolve these difficulties by a different, two-pronged extension to the syntax of the logic. First, we propose that the usual "strong" separating conjunction * , which enforces the strict disjointness of memory, should be retained in the formalism in addition to the weaker . The stronger * supports entailments such as A 0.5 * B 0.5 |= (A * B) 0.5 , which does not hold when is used instead. Second, we introduce nominal labels from hybrid logic (cf. [3, 10] ) to remember that two copies of a formula have the same origin. We write a nominal α to denote a unique heap, in which case entailments such as (α ∧ A) 0.5 (α ∧ A) 0.5 |= α ∧ A become valid. We remark that labels have been adopted for similar "tracking" purposes in several other separation logic proof systems [10, 21, 23, 25] .

The remainder of this paper aims to demonstrate that our proposed extensions are (i) weakly necessary, in that expected reasoning patterns fail under the usual formalism, (ii) correct, in that they recover the desired logical principles, and (iii) sufficient to verify typical concurrent programming patterns that use sharing. Section 2 gives some simple examples that motivate our extensions. Section 3 then formally introduces the syntax and semantics of our extended formalism. In Sect. 4 we show that our logic obeys the logical principles that enable us to reason smoothly with fractional permissions over arbitrary formulas, and in Sect. 5 we give some longer worked examples. Finally, in Sect. 6 we conclude and discuss directions for future work.

In this section, we aim to motivate our extensions to separation logic with permissions by showing, firstly, how the failures of the logical principles described in the introduction actually arise in program verification examples and, secondly, how these failures are remedied by our proposed changes.

The overall context of our work is reasoning about concurrent programs that share some data structure or region in memory, which can be described as a formula in the assertion language. If A is such a formula then we write A π to denote a "π share" of the formula A, meaning informally that all of the pointers in the heap memory satisfying A are owned with share π. The main question then becomes how this notion interacts with the separating conjunction . There are two key desirable logical equivalences:

Equivalence (I) describes distributing a fractional share over a separating conjunction, whereas equivalence (II) describes combining two pieces of a previously split resource. Both equivalences are true in the |= direction but, as we have seen in the Introduction, false in the =| one. Generally speaking, is like Humpty Dumpty: easy to break apart, but not so easy to put back together again.

The key to understanding the difficulty is the following equivalence:

In other words, either x and y are not aliased, or they are aliased and the permissions combine (the additive operation ⊕ on rational shares is simply normal addition when the sum is ≤ 1 and undefined otherwise). This disjunction undermines the notational economies that have led to separation logic's great successes in scalable verification [11] ; in particular, (I) fails because the left disjunct might be true, and (II) fails because the right disjunct might be. At a high level, is a bit too easy to introduce, and therefore also a bit too hard to eliminate.

One of the challenges of the weak separating conjunction is that it interacts poorly with inductively defined predicates. Consider porting the usual separation logic definition of a possibly-cyclic linked list segment from x to y from a sequential setting to a concurrent one by a simple substitution of for * :

Now consider a simple recursive procedure foo(x,y) that traverses a linked list segment from x to y:

foo(x,y) { if x=y then return; else foo([x],y); } It is easy to see that foo leaves the list segment unchanged, and therefore satisfies the following Hoare triple:

The intuitive proof of this fact would run approximately as follows:

However, because of the use of , the highlighted inference step is not sound:

To see this, consider a heap with the following structure, viewed in two ways:

This heap satisfies the LHS of the entailment in (2) , as it is the -composition of a 0.5-share of x → z and a 0.5-share of ls z z, a cyclic list segment from z back to itself (note that here z = y). However, it does not satisfy the RHS, since it is not a 0.5-share of the -composition of x → z with ls z z, which would require the pointer to be disjoint from the list segment. The underlying reason for the failure of this example is that, in going from (x → z ls z z) 0.5 to x 0.5 → z (ls z z) 0.5 , we have lost the information that the pointer and the list segment are actually disjoint. This is reflected in the general failure of the distribution principle A π B π |= (A B) π , of which the above is just one instance. Accordingly, our proposal is that the "strong" separating conjunction * from standard separation logic, which forces disjointness of the heaps satisfying its conjuncts, should also be retained in the logic alongside , on the grounds that (II) is true for the stronger connective:

If we then define our list segments using * in the traditional way, namely

then we can observe that this second definition of ls is identical to the first on permission-free formulas, since and * coincide in that case. However, when we replay the verification proof above with the new definition of ls, every in the proof above becomes a * , and the proof then becomes sound. Nevertheless, we can still use to describe permission-decomposition of list segments at a higher level; e.g., ls x y can still be decomposed as (ls x y) 0.5 (ls x y) 0.5 .

Unfortunately, even when we use the strong separating conjunction * to define list segments ls, a further difficulty still remains. Consider a simple concurrent program that runs two copies of foo in parallel on the same list segment:

foo(x,y); || foo(x,y);

Since foo only reads from its input list segment, and satisfies the specification {(ls x y) 0.5 } foo(x,y); {(ls x y) 0.5 }, this program satisfies the specification {ls x y} foo(x,y); || foo(x,y); {ls x y}.

Now consider constructing a proof of this specification in CSL. First we view the list segment ls x y as the -composition of two read-only copies, with permission 0.5 each; then we use CSL's concurrency rule (see Sect. 1) to compose the specifications of the two threads; last we recombine the two read-only copies to obtain the original list segment. The proof diagram is as follows:

However, again, the highlighted inference step in this proof is not correct:

A countermodel is a heap with the following structure, again viewed in two ways:

According to the first view of such a heap, it satisfies the LHS of (4), as it is the -composition of two 0.5-shares of ls x y (one of two cells, and one of a single cell). However, it does not satisfy ls x y, since that would require every cell in the heap to be owned with permission 1.

Like in our previous example, the reason for the failure of this example is that we have lost information. In going from ls x y to (ls x y) 0.5 (ls x y) 0.5 , we have forgotten that the two formulas (ls x y) 0.5 are in fact copies of the same region. For formulas A that are precise in that they uniquely describe part of any given heap [12] , e.g. formulas x → a, this loss of information does not happen and we do have A 0.5 A 0.5 |= A; but for non-precise formulas such as ls x y, this principle fails.

However, we regard this primarily as a technical shortcoming of the formalism, rather than a failure of our intuition. It ought to be true that we can take any region of memory, split it into two read-only copies, and then later merge the two copies to re-obtain the original region. Were we conducting the above proof on pen and paper, we would very likely explain the difficulty away by adopting some kind of labelling convention, allowing us to remember that two formulas have been obtained from the same memory region by dividing permissions.

In fact, that is almost exactly our proposed remedy to the situation. We introduce nominals, or labels, from hybrid logic, where a nominal α is interpreted as denoting a unique heap. Any formula of the form α ∧ A is then precise (in the above sense), and so obeys the combination principle

where ⊕ is addition on permissions. Thus we can repair the faulty CSL proof above by replacing every instance of the formula ls x y by the "labelled" formula α ∧ ls x y (and adding an initial step in which we introduce the fresh label α).

However, this is not quite the end of the story. Readers may have noticed that replacing ls x y by the "labelled" version α ∧ ls x y also entails establishing a slightly stronger specification for the function foo, namely:

This introduces an extra difficulty in the proof (cf. Sect. 2.1); at the recursive call to foo([x],y), the precondition now becomes α 0.5 ∧ (x 0.5 → z * (ls z y) 0.5 )), which means that we cannot apply separation logic's frame rule [32] to the pointer formula without first weakening away the label-share α 0.5 .

For this reason, we shall also employ hybrid logic's "jump" modality @ , where the formula @ α A means that A is true of the heap denoted by the label α. In the above, we can introduce labels β and γ for the list components x → z and ls z y respectively, whereby we can represent the decomposition of the list by the assertion @ α (β * γ). Since this is a pure assertion that does not depend on the heap, it can be safely maintained when applying the frame rule, and used after the function call to restore the label α, using the easily verifiable fact that

Similar reasoning over labelled decompositions of data structures is seemingly necessary whenever treating recursion; we return to it in more detail in Sect. 5.

Following the motivation given in the previous section, here we give the syntax and semantics of a separation logic, SL LP , with permissions over arbitrary formulas, making use of both strong and weak separating conjunctions, and nominal labels (from hybrid logic [3, 10] ). First, we define a suitable notion of permissions and associated operations.

Perm is a set (of "permissions"), 1 ∈ Perm is called the write permission, and ⊕ and ⊗ are respectively partial and total binary functions on Perm, satisfying associativity, commutativity, cancellativity and the following additional axioms:

The most common example of a permissions algebra is the Boyland fractional permission model (0, 1] ∩ Q, ⊕, ×, 1 , where permissions are rational numbers in (0, 1], × is standard multiplication, and ⊕ is standard addition but undefined if p + p > 1. From now on, we assume a fixed but arbitrary permissions algebra.

With the permissions structure in place, we can now define the syntax of our logic. We assume disjoint, countably infinite sets Var of variables, Pred of predicate symbols (with associated arities) and Label of labels. Definition 3.2. We define formulas of SL LP by the grammar:

where x, y range over Var, π ranges over Perm, P ranges over Pred, α ranges over Label and x ranges over tuples of variables of length matching the arity of the predicate symbol P . We write x π → y for (x → y) π , and x = y for ¬(x = y).

The "magic wands" − − * and − − are the implications adjoint to * and , as usual in separation logic. We include them for completeness, but we use − − * only for fairly complex examples (see Sect. 5.3) and in fact do not use − − at all.

Semantics. We interpret formulas in a standard model of stacks and heapswith-permissions (cf. [4] ), except that our models also incorporate a valuation of nominal labels. We assume an infinite set Val of values of which an infinite subset Loc ⊂ Val are considered addressable locations. A stack is as usual a map s : Var → Val. A heap-with-permissions, which we call a p-heap for short, is a finite partial function h : Loc fin Val × Perm from locations to value-permission pairs. We write dom (h) for the domain of h, i.e. the set of locations on which h is defined. Two p-heaps h 1 and h 2 are called disjoint if dom (h 1 ) ∩ dom (h 2 ) = ∅, and compatible if, for all ∈ dom (h 1 ) ∩ dom (h 2 ), we have h 1 ( ) = (v, π 1 ) and h 2 (v, π 2 ) and π 1 ⊕ π 2 is defined. (Thus, trivially, disjoint heaps are also compatible.) We define the multiplication π · h of a p-heap h by permission π by extending ⊗ pointwise:

We also assume that each predicate symbol P of arity k is given a fixed interpretation P ∈ (Val k × PHeaps), where PHeaps is the set of all p-heaps. Here we allow an essentially free interpretation of predicate symbols, but they could also be given by a suitable inductive definition schema, as is done in many papers on separation logic (e.g. [7, 8] ). Finally, a valuation is a function ρ : Label → PHeaps assigning a single p-heap ρ(α) to each label α. Strong and weak heap composition) . The strong composition h 1 • h 2 of two disjoint p-heaps h 1 and h 2 is defined as their union: 

(h 1 • h 2 )( ) = h 1 ( ) if ∈ dom (h 2 ) h 2 ( ) if ∈ dom (h 1 )(h 1 • h 2 )( ) = ⎧ ⎪ ⎨ ⎪ ⎩ (v, π 1 ⊕ π 2 ) if h 1 ( ) = (v, π 1 ) and h 2 ( ) = (v, π 2 ) h 1 ( ) if ∈ dom (h 2 ) h 2 ( ) if ∈ dom (h 1 )

In this section, we establish the main logical entailments and equivalences of SL LP that capture the various interactions between the separating conjunctions and * , permissions and labels. As well as being of interest in their own right, many of these principles will be essential in 

Additionally, the following residuation laws hold:

In addition, we can always weaken * to : A * B |= A B.

Next, we establish an additional connection between the two separating conjunctions and * . 

We can merge the first and fourth cases by noting that h(

, and similarly for the second and fifth cases. We can also rewrite the last two cases by observing that / ∈ dom (h 3 ) implies h 1 ( ) = (h 1 • h 3 )( ), and so on, resulting in Next, we establish principles for distributing permissions over various connectives, in particular over the strong * , stated earlier as (3) in Sect. 2.

h = (h 1 • h 2 ) • (h 3 • h 4 ),

The following equivalences hold for all formulas A and B, and permissions π and σ:

Proof. We just show the most interesting case, ( * π ). First of all, we establish a corresponding model-theoretic property: for any permission π and disjoint pheaps h 1 and h 2 , meaning h 1 • h 2 is defined,

To see this, we first observe that for any ∈ dom (h 1 • h 2 ), we have that either ∈ dom (h 1 ) or ∈ dom (h 2 ). We just show the case ∈ dom (h 1 ), since the other is symmetric. Writing h 1 ( ) = (v 1 , π 1 ), and using the fact that ∈ dom (h 2 ), π · (h 1 • h 2 )( ) = (v 1 , π ⊗ π 1 ) = (π · h 1 )( ) = ((π · h 1 ) • (π · h 2 ))( ). Now for the main result, let s, h and ρ be given. We have s, h, ρ |= (A * B) π ⇔ h = π · h and s, h , ρ |= A * B ⇔ h = π · h and h = h 1 • h 2 and s, h 1 , ρ |= A and s, h 2 , ρ |= B ⇔ h = π · (h 1 • h 2 ) and s, h 1 , ρ |= A and s, h 2 , ρ |= B ⇔ h = (π · h 1 ) • (π · h 2 ) and s, h 1 , ρ |= A and s, h 2 , ρ |= B by (7)

We now establish the main principles for dividing and combining permissions formulas using . As foreshadowed in Sect. 2, the combination principle holds only for formulas that are conjoined with a nominal label (cf. Eq. (5)).

For all formulas A, nominals α, and permissions π 1 , π 2 such that π 1 ⊕ π 2 is defined: 

Now we define p-heaps h 1 and h 2 , both with domain exactly dom (h), by 

To see this, we observe that for any ∈ dom (h), writing h( ) = (v, π) say,

Thus h 1 = h 2 = ρ(α) and so, by (8), we have h = (π 1 ⊕ π 2 ) · h 1 , where s, h 1 , ρ |= α ∧ A. This gives us s, h, ρ |= (α ∧ A) π1⊕π2 , as required.

Lastly, we state some useful principles for labels and the "jump" modality.

Proof. We just show the case (@/ * / ), the others being easy. Suppose s, h, ρ |= @ α (β 1 π * β 2 σ ) ∧ (β 1 π β 2 σ ), meaning that s, ρ(α), ρ |= β 1 π * β 2 σ and s, h, ρ |= β 1 π β 2 σ . Then we have ρ(α) = (π · ρ(β 1 )) • (σ · ρ(β 2 )), while h = (π · ρ(β 1 )) • (σ · ρ(β 2 )). Since • is defined only when its arguments are disjoint p-heaps, we obtain that h = ρ(α) = (π · ρ(β 1 )) • (σ · ρ(β 2 )). Thus s, h, ρ |= α ∧ (β 1 π * β 2 σ ). 

In this section, we demonstrate how SL LP can be used in conjunction with the usual principles of CSL to construct verification proofs of concurrent programs, taking three examples of increasing complexity. Our examples all operate on binary trees in memory, defined as usual in separation logic (again note the use of * rather than ):

Our proofs employ (a subset of) the standard rules of CSL-with the most important being the concurrency rule from the Introduction, the separation logic frame rules for both * and , and a new rule enabling us to introduce fresh labels into the precondition of a triple (similar to the way Hoare logic usually handles existential quantifiers). These key rules are shown in Fig. 2 . We simplify our Hoare triple to remove elements to handle function call/return and furthermore omit the presentation of the standard collection of rules for consequence, load, store, if-then-else, assignment, etc.; readers interested in such aspects can consult [1] . Both of our frame rules have the usual side condition on modified program variables. The strong frame rule (Frame * ) has an additional side condition that will be discussed in Sect. 5.3; until then it is trivially satisfied.

Consider the following program:

; } This is intended to be a straightforward example where we take a tree rooted at x and, if x is non-null, split into parallel threads that run the program read on x, and whose specification is {α π ∧ tree(x) σ } read(x) {α π ∧ tree(x) σ }. We prove that check satisfies the specification {tree(x) π } check(x) {tree(x) π }; the verification proof is in Fig. 3 . The proof makes use of the basic operations of our theory: labelling, splitting and joining. The example follows precisely these steps, starting by labelling the formula tree(x) π ∧ x = null with α. The concurrency rule (Par) allows us to put formulas back together after the parallel call, and the two copies (α ∧ tree(x) π ) 0.5 that were obtained are glued back together to yield tree(x) π , since they have the same label. 

Consider the following program, which was also employed as an example in [24] :

print(x->d); proc(x->l);

proc(x->l); proc(x->r);

proc(x->r); } This code takes a tree rooted at x and, if x is non-null, splits into parallel threads that call proc recursively on its left and right branches. We prove, in Fig. 4 , that proc satisfies the specification {α ∧ tree(x) π } proc(x) {α ∧ tree(x) π }. First we unroll the definition of tree(x) and distribute the permission over Boolean connectives and * . If the tree is empty the process stops. Otherwise, we label each component with a new label and introduce the "jump" statement @ α (β 1 * β 2 * β 3 ), recording the decomposition of the tree into its three components. Since such statements are pure, i.e. independent of the heap, we can "carry" this formula along our computation without interfering with the frame rule(s). Now that every subregion is labelled, we split the formula into two copies, each with half share, but after distributing 0.5 over * and ∧ we end up with half shares in the labels as well. We relabel each subregion with new "whole" labels, and again introduce pure @-formulas that record the relation between the old and the new labels. At this moment we enter the parallel threads and recursively apply proc to the left and right subtrees of x. Assuming the specification of proc for subtrees of x, we then retrieve the original label α from the trail of crumbs left by the @-formulas. We can then recombine the α-labelled threads using (Join ) to arrive at the desired postcondition.

Our previous examples involve only "isolated tank" concurrency: a program has some resources and splits them into parallel threads that do not communicate with each other before-remembering Humpty Dumpty!-ultimately re-merging. For our last example, we will show that our technique is expressive enough to handle more sophisticated kinds of sharing, in particular inter-thread coarsegrained communication. We will show that we can not only share read-only data, but in fact prove that one thread has acquired the full ownership of a structure, even when the associated root pointers are not easily exposed.

To do so, we add some communication primitives to our language, together with their associated Hoare rules. Coarse-grained concurrency such as locks, channels, and barriers have been well-investigated in various flavours of concurrent separation logic [19, 26, 31] . We will use a channel for our example in this section but with simplified rules: the Hoare rule for a channel c to send message

We ignore details such as identifying which party is allowed to send/receive at a given time [14] or the resource ownership of the channel itself [18] .

These rules interact poorly with the strong frame rule from Fig. 2 :

The revealed side condition ( ‡) means that C does not contain any subcommands that "transfer in" resources, such as unlock, receive, etc.; this side condition is a bit stronger than necessary but has a simple definition and can be checked syntactically. Without ( ‡), we can reach a contradiction. Assume that the current → a, can reason as follows:

The postcondition is a contradiction as no location strongly separates from itself. However, given ( ‡) the strong frame rule can be proven by induction.

The consequence of ( ‡), from a verification point of view, is that when resources are transferred in they arrive weakly separated, by , since we must use the weak frame rule around the receiving command. The troublesome issue is that this newly "arriving" state can thus -overlap awkwardly with the existing state. Fortunately, judicious use of labels can sort things out.

Consider the code in Fig. 5 . The basic idea is simple: we create some data at the top (line 101) and then split its ownership 50-50 to two threads. The left thread finds a subtree, and passes its half of that subtree to the right via a channel. The right thread receives the root of that subtree, and thus has full ownership of that subtree along with half-ownership of the rest of the tree. Accordingly, the right thread can modify that subtree before notifying the left subtree and passing half of the modified subtree back. After merging, full ownership of the entire tree is restored and so on line 401 the program can delete it. Figure 5 only contains the proof and line numbers for the top and bottom shared portions. The left and the right thread's proofs appear in Fig. 6 .

By this point the top and bottom portions of the verification are straightforward. After creating the tree tree(rt) at line 102, we introduce the label α, split the formula using (Split ), and then pass (α ∧ tree(rt)) 0.5 to both threads. After the parallel execution, due to the call to modify(sub) in the right thread, the tree has changed in memory. Accordingly, the label for the tree must also change as indicated by the ( ∧ tree(rt)) 0.5 in both threads after parallel processing. These are then recombined on line 400 using the re-combination principle (Join ), before the tree is deallocated via standard sequential techniques. Let us now examine the more interesting proofs of the individual threads in Fig. 6 . Line 201 calls the find function, which searches a binary tree for a subtree rooted with key key. Following Cao et al. [13] we specify find as follows:

Here ret is bound to the return value of find, and the postcondition can be considered to represent the returned subtree tree(ret ) separately from the treewith-a-hole tree(ret ) − − * tree(x), using a * /− − * style to represent replacement as per Hobor and Villard [20] . This is the invariant on line 202. Line 203 then attaches the fresh labels β and γ to the * -separated subparts, and line 204 snapshots the formula current at label α using the @ operator; @ π α P should be read as "when one has a π-fraction of α, P holds"; it is definable using @ and an existential quantifier over labels. On line 205 we forget (in the left thread) the label α for the current heap for housekeeping purposes, and then on line 206 we weaken the strong separating conjunction * to the weak one before sending the root of the subtree sub on line 207.

In the transfer program, the invariant for the first channel message is (β ∧ tree(sub)) 0.5 ∧ @ 0.5 α ((β ∧ tree(sub)) * (γ ∧ (tree(sub) − − * tree(rt)))) 0.5

In other words, half of the ownership of the tree rooted at sub plus the (pure) @-fact about the shape of the heap labeled by α. Comparing lines 206 and 208 we can see that this information has been shipped over the wire (the @-information has been dropped since no longer needed). The left thread then continues to process until synchronizing again with the receive in line 211. Before we consider the second synchronization, however, let us instead jump to the corresponding receive in the right thread at line 303. After the receive, the invariant on line 304 has the (weakly separated) resources sent from the left thread on line 206. We then "jump" label α using the @-information to reach line 305. We can redistribute the β inside the * on line 306 since we already know that β and γ are disjoint. On line 307 we reach the payoff by combining both halves of the subtree sub, enabling the modification of the subtree in line 308.

On line 310 we label the two subheaps, and specialize the magic wand so that given the specific heap δ it will yield the specific heap ; we also record the pure fact that γ and δ are disjoint, written γ ⊥ δ. On line 311 we snapshot γ and split the tree sub 50-50; then on line 312 we push half of sub out of the strong * . On line 313 we combine the subtree and the tree-with-hole to reach the final tree . We then send on line 314 with the channel's second resource invariant:

After the send, on line 315 we have reached the final fractional tree . Back in the left-hand thread, the second send is received in line 211, leading to the weakly-separated postcondition in line 212. In line 213 we "jump" label γ, and then in line 214 we use the known disjointness of γ and δ to change the to * . Finally in line 215 we apply the magic wand to reach the postcondition.

We propose an extension of separation logic with fractional permissions [4] in order to reason about sharing over arbitrary regions of memory. We identify two fundamental logical principles that fail when the "weak" separating conjunction is used in place of the usual "strong" * , the first being distribution of permissions-A π B π |= (A B) π -and the second being the re-combination of permission-divided formulas, A π A σ |= A π⊕σ . We avoid the former difficulty by retaining the strong * in the formalism alongside , and the latter by using nominal labels, from hybrid logic, to record exact aliasing between read-only copies of a formula.

The main previous work addressing these issues, by Le and Hobor [24] , uses a combination of permissions based on tree shares [17] and semantic side conditions on formulas to overcome the aforementioned problems. The rely-guarantee separation logic in [30] similarly restricts concurrent reasoning to structures described by precise formulas only. In contrast, our logic is a little more complex, but we can use permissions of any kind, and do not require side conditions. In addition, our use of labelling enables us to handle examples involving the transfer of data structures between concurrent threads.

On the other hand, we think it probable that the kind of examples we consider in this paper could also be proven by hand in at least some of the verification formalisms derived from CSL (e.g. [16, 22, 27] ). For example, using the "concurrent abstract predicates" in [16] , one can explicitly declare shared regions of memory in a fairly ad-hoc way. However, such program logics are typically very complicated and, we believe, quite unlikely to be amenable to automation.

We feel that the main appeal of the present work lies in its relative simplicity-we build on standard CSL with permissions and invoke only a modest amount of extra syntax-which bodes well for its potential automation (at least for simpler examples). In practical terms, an obvious way to proceed would be to develop a prototype verifier for concurrent programs based on our logic SL LP . An important challenge in this area is to develop heuristics-e.g., for splitting, labelling and combining formulas-that work acceptably well in practice.

An even greater challenge is to move from verifying user-provided specifications to inferring them automatically, as is done e.g. by Facebook Infer. In separation logic, this crucially depends on solving the biabduction problem, which aims to discover "best fit" solutions for applications of the frame rule [9, 11] . In the CSL setting, a further problem seems to lie in deciding how applications of the concurrency rule should divide resources between threads.

Finally, automating the verification approach set out in this paper will likely necessitate restricting our full logic to some suitably tractable fragment, e.g. one analogous to the well-known symbolic heaps in standard separation logic (cf. [2, 15] ). The identification of such tractable fragments is another important theoretical problem in this area. It is our hope that this paper will serve to stimulate interest in the automation of concurrent separation logic in particular, and permission-sensitive reasoning in general.

Program Logics for Certified Compilers

A decidable fragment of separation logic

Modal Logic

Permission accounting in separation logic

Checking interference with fractional permissions

A semantics for concurrent separation logic

Formalised inductive reasoning in the logic of bunched implications

A decision procedure for satisfiability in separation logic with inductive predicates

Biabduction (and related problems) in array separation logic

Parametric completeness for separation theories

Compositional shape analysis by means of bi-abduction

Local action and abstract separation logic

Proof pearl: magic wand as frame

Automated modular verification for relaxed communication protocols

On symbolic heaps modulo permission theories

Concurrent abstract predicates

A fresh look at separation algebras and share accounting

Oracle semantics for concurrent separation logic

Barriers in concurrent separation logic: now with tool support!

The ramifications of sharing in data structures

Proof search for propositional abstract separation logics via labelled sequents

The essence of higher-order concurrent separation logic

Exploring the relation between intuitionistic BI and Boolean BI: an unexpected embedding

Logical reasoning for disjoint permissions

A proof system for separation logic with magic wand

Resources, concurrency and local reasoning

CoLoSL: concurrent local subjective logic

Separation logic: a logic for shared mutable data structures

Concurrent separation logic and operational semantics

A marriage of rely/guarantee and separation logic

Tracking heaps that hop with heap-hop

A semantic basis for local reasoning