{'fraction_non_alphanumeric': 0.037719012649374765, 'fraction_numerical': 0.012408204608761712, 'mean_word_length': 4.169232687153276, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 35, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Linearizability with Ownership Transfer

Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. Unfortunately, it assumes a complete isolation between a library and its client, with interactions limited to passing values of a given data type. This is inappropriate for common programming languages, where libraries and their clients can communicate via the heap, transferring the ownership of data structures, and can even run in a shared address space without any memory protection. In this paper, we present the first definition of linearizability that lifts this limitation and establish an Abstraction Theorem: while proving a property of a client of a concurrent library, we can soundly replace the library by its abstract implementation related to the original one by our generalisation of linearizability. This allows abstracting from the details of the library implementation while reasoning about the client. We also prove that linearizability with ownership transfer can be derived from the classical one if the library does not access some of data structures transferred to it by the client.


Introduction
The architecture of concurrent software usually exhibits some forms of modularity. For example, concurrent algorithms are encapsulated in libraries and complex algorithms are often constructed using libraries of simpler ones. This lets developers benefit from readymade libraries of concurrency patterns and high-performance concurrent data structures, such as java.util.concurrent for Java and Threading Building Blocks for C++. To simplify reasoning about concurrent software, we need to exploit the available modularity. In particular, in reasoning about a client of a concurrent library, we would like to abstract from the details of a particular library implementation. This requires an appropriate notion of library correctness.
Correctness of concurrent libraries is commonly formalised by linearizability [18], which fixes a certain correspondence between the library and its specification. The latter is usually just another library, but implemented atomically using an abstract data type; the two libraries are called concrete and abstract, respectively. A good notion of linearizability should validate an Abstraction Theorem [12,14]: the behaviours of any client using the concrete library are contained in the behaviours of the client using the abstract one. This makes it sound to replace a library by its specification in reasoning about its client.
Classical linearizability assumes a complete isolation between a library and its client, with interactions limited to passing values of a given data type as parameters or return values of library methods. This notion is not appropriate for low-level heap-manipulating languages, such as C/C++. There the library and the client run in a shared address space; thus, to prove the whole program correct, we need to verify that one of them does not corrupt the data structures used by the other. Type systems [8] and program logics [23] usually establish this using the concept of ownership of data structures by a program component: the right to access a data structure is given only to a particular component or a set of them. When verifying realistic programs, this ownership of data structures cannot be assigned statically; rather, it should be transferred between the client and the library at calls to and returns from the latter. The times when ownership is transferred are not determined operationally, but set by the proof method: as O'Hearn famously put it, "ownership is in the eye of the asserter" [23]. However, ownership transfer reflects actual interactions between program components via the heap, e.g., alternating accesses to a shared area of memory. Such interactions also exist in high-level languages providing basic memory protection, such as Java. In this case, we need to ensure that a client does not subvert a library by accessing a memory object after its ownership was transferred to the latter.
For an example of ownership transfer between concurrent libraries and their clients consider a memory allocator accessible concurrently to multiple threads. We can think of the allocator as owning the blocks of memory on its free-list; in particular, it can store free-list pointers in them. Having allocated a block, a thread gets its exclusive ownership, which allows accessing it without interference from the other threads. When the thread frees the block, its ownership is returned to the allocator. Trying to write to a memory cell after it was freed has dire consequences.
As another example, consider any container with concurrent access, such as a concurrent set from java.util.concurrent or Threading Building Blocks. A typical use of such a container is to store pointers to a certain type of data structures. However, when verifying a client of the container, we usually think of the latter as holding the ownership of the data structures whose addresses it stores [23]. Thus, when a thread inserts a pointer to a data structure into a container, its ownership is transferred from the thread to the container. When another thread removes a pointer from the container, it acquires the ownership of the data structure the pointer identifies. If the first thread tries to access a data structure after a pointer to it has been inserted into the container, this may result in a race condition. Unlike a memory allocator, the container code usually does not access the contents of the data structures its elements identify, but merely ferries their ownership between different threads. For this reason, correctness proofs for such containers [1,10,29] have so far established their classical linearizability, without taking ownership transfer into account.
We would like to use the notion of linearizability and, in particular, an Abstraction Theorem to reason about the above libraries and their clients in isolation, taking into account only the memory that they own. To this end, we would like the correctness of a library to constrain not only pointers that are passed between it and the client, but also the contents of the data structures whose ownership is transferred. So far, there has been no notion of linearizability that would allow this. In the case of concurrent containers, we have no way of using classical linearizability established for them to validate an Abstraction Theorem that would be applicable to clients performing ownership transfer. This paper fills in these gaps.
Contributions. In this paper, we generalise linearizability to a setting where a library and its client execute in a shared address space, and boundaries between their data structures can change via ownership transfers. Linearizability is usually defined in terms of histories, which are sequences of calls to and returns from a library in a given program execution, recording parameters and return values passed. To handle ownership transfer, histories also have to include descriptions of memory areas transferred. However, in this case, some histories cannot be generated by any pair of a client and a library: while generating histories of a library we should only consider its executions in an environment that respects ownership. For example, a client that transfers an area of memory upon a call to a library not communicating with anyone else cannot then transfer the same area again before getting it back from the library upon a method return. We propose a notion of balancedness that characterises those histories that treat ownership transfer correctly. We then define a linearizability relation between balanced histories, matching histories of a concrete and an abstract library (Section 3).
This definition does not rely on a particular model of program states for describing memory areas transferred in histories, but assumes an arbitrary model defined by a separation algebra [7]. By picking a model with so-called permissions [5,9], we can allow clients and libraries to transfer non-exclusive rights to access certain memory areas in particular ways, instead of transferring their full ownership. This makes our results applicable even when libraries and their clients share access to some areas of memory. Our definition of balancedness for arbitrary separation algebras relies on a new formalisation of the notion of a footprint of a state, describing the amount of permissions the state includes (Section 2).
The rest of our technical development relies on a novel compositional semantics for a language with libraries that defines the denotation of a library or a client considered separately in an environment that communicates with the component correctly via ownership transfers (Sections 4 and 5). In particular, the semantics allows us to generate the set of all histories that can be produced by a library solely from its code, without considering all its possible clients. This, in its turn, allows us to lift the linearizability on histories to libraries and establish the Abstraction Theorem (Section 6). On the way, we also obtain an insight into the original definition of linearizability without ownership transfer, showing a surprising relationship between one of the ways of its formulation and the plain subset inclusion on the sets of histories produced by concrete and abstract libraries.
We note that the need to consider ownership transfer makes the proof of the Abstraction Theorem highly non-trivial. This is because proving the theorem requires us to convert a computation with a history produced by the concrete library into a computation with a history produced by the abstract one, which requires moving calls and returns to different points in the computation. In the setting without ownership transfer, these actions are thread-local and can be moved easily; however, once they involve ownership transfer, they become global and the justification of their moves becomes subtle, in particular, relying on the fact that the histories involved are balanced (Section 7).
To avoid having to prove the new notion of linearizability from scratch for libraries that do not access some of the data structures transferred to them, such as concurrent containers, we propose a frame rule for linearizability (Section 8). It ensures the linearizability of such libraries with respect to a specification with ownership transfer given their linearizability with respect to a specification without one. We provide a glossary of notation at the end of the paper.

Footprints of States
2.1. Separation Algebras. Our results hold for a class of models of program states called separation algebras [7], which allow expressing the dynamic memory partitioning between libraries and clients.
Definition 2.1. A separation algebra is a set Σ, together with a partial commutative, associative and cancellative operation * on Σ and a unit element e ∈ Σ. Here commutativity and associativity hold for the equality that means both sides are defined and equal, or both are undefined. The property of cancellativity says that for each σ ∈ Σ, the function σ * · : Σ Σ is injective.
We think of elements of a separation algebra Σ as portions of program states and the * operation as combining such portions. The partial states allow us to describe parts of the program state belonging to a library or the client. When the * -combination of two states is defined, we call them compatible. Incompatible states usually make contradictory claims about the ownership of memory. We sometimes use a pointwise lifting * : Elements of separation algebras are often defined using partial functions. We use the following notation: g(x)↓ means that the function g is defined on x, g(x)↑ means that it is undefined on x, dom(g) denotes the set of arguments on which g is defined, [ ] denotes a nowhere-defined function, and g[x : y] denotes the function that has the same value as g everywhere, except for x, where it has the value y. We also write for an expression whose value is irrelevant and implicitly existentially quantified.
Below is an example separation algebra RAM: A (partial) state in this model consists of a finite partial function from allocated memory locations to the values they store. The * operation on RAM is defined as the disjoint function union , with the nowhere-defined function [ ] as its unit. Thus, * combines disjoint pieces of memory. More complicated separation algebras do not split memory completely, instead allowing heap parts combined by * to overlap. This is done by associating so-called permissions [5] with memory cells in the model, which do not give their exclusive ownership, but allow accessing them in a certain way. Types of permissions range from read sharing [5] to accessing memory in an arbitrary way consistent with a given specification [9]. We now give an example of a separation algebra with permissions of the former kind.
We define the algebra RAM π as follows: A state in this model consists of a finite partial function from allocated memory locations to values they store and so-called permissions-numbers from (0, 1] that show "how much" of the memory cell belongs to the partial state [5]. The latter allow a library and its client to share access to some of memory cells. Permissions in RAM π allow only read sharing: when defining the semantics of commands over states in RAM π , the permissions strictly less than 1 are interpreted as permissions to read; the full permission 1 additionally allows writing. The * operation on RAM π adds up permissions for memory cells. Formally, for σ 1 , σ 2 ∈ RAM π , we write σ 1 σ 2 if: If σ 1 σ 2 , then we define otherwise, σ 1 * σ 2 is undefined. The unit for * is the empty heap [ ]. This definition of * allows us, e.g., to split a memory area into two disjoint parts. It also allows splitting a cell with a full permission 1 into two parts, carrying read-only permissions 1/2 and agreeing on the value stored in the cell. These permissions can later be recombined to obtain the full permission, which allows both reading from and writing to the cell.
Since we develop all our results for an arbitrary separation algebra, by instantiating it with algebras similar to RAM π , we can handle cases when a library and its client share access to some memory areas.
Consider an arbitrary separation algebra Σ with an operation * . We define a partial operation \ : Σ × Σ Σ, called state subtraction, as follows: σ 2 \ σ 1 is a state in Σ such that σ 2 = (σ 2 \ σ 1 ) * σ 1 ; if such a state does not exist, σ 2 \ σ 1 is undefined. The cancellativity of * implies that σ 2 \ σ 1 is determined uniquely, and hence, the \ operation is well-defined. When reasoning about ownership transfer between a library and a client, we use the * operation to express a state change for the component that is receiving the ownership of memory, and the \ operation for the one that is giving it up. Proposition 2.2. For all σ 1 , σ 2 , σ 3 ∈ Σ, if σ 1 * σ 2 and σ 1 \ σ 3 are defined, then

2.2.
Footprints. Our definition of linearizability uses a novel formalisation of a footprint of a state, which, informally, describes the amount of memory or permissions the state includes. Definition 2.3. A footprint of a state σ in a separation algebra Σ is the set of states In the following, l ranges over footprints. The function δ computes the equivalence class of states with the same footprint as σ. In the case of RAM, we have δ(σ) = {σ | dom(σ) = dom(σ )} for every σ ∈ RAM. Thus, states with the same footprint contain the same memory cells. Definitions of δ for separation algebras with permissions are more complicated, taking into account not only memory cells present in the state, but also permissions for them. In the case of the algebra RAM π , for σ ∈ RAM π we have In other words, states with the same footprint contain the same memory cells with the identical permissions; in the case of memory cells on read permissions, the states also have to agree on their values.
Proposition 2.7. For all l 1 , l 2 , l 3 ∈ F(Σ), if l 1 • l 2 and l 1 \ \ l 3 are defined, then In the rest of the paper, we fix a separation algebra Σ with the * operation cancellative on footprints.

Linearizability with Ownership Transfer
In the following, we consider descriptions of computations of a library providing several methods to a multithreaded client. We fix a set ThreadID of thread identifiers and a set Method of method names. As we explained in Section 1, a good definition of linearizability has to allow replacing a concrete library implementation with its abstract version while keeping client behaviours reproducible. For this, it should require that the two libraries have similar client-observable behaviours. Such behaviours are recorded using histories, which we now define in our setting.
Definition 3.1. An interface action ψ is an expression of the form (t, call m(σ)) or (t, ret m(σ)), where t ∈ ThreadID, m ∈ Method and σ ∈ Σ. We denote the sets of all call and return actions by CallAct and RetAct, and the set of all interface actions by CallRetAct.
An interface action records a call to or a return from a library method m by thread t. The component σ in (t, call m(σ)) specifies the part of the state transferred upon the call from the client to the library; σ in (t, ret m(σ)) is transferred in the other direction. For example, in the algebra RAM, the annotation σ = [42 : 0] implies the transfer of the cell at the address 42 storing 0. In the algebra RAM π , σ = [42 : (0, 1/2)] implies the transfer of a read permission for this cell.

Definition 3.2.
A history H is a finite sequence of interface actions such that for every thread t, its projection H| t to actions by t is a sequence of alternating call and return actions over matching methods that starts from a call action.
In the following, we use the standard notation for sequences: ε is the empty sequence, τ (i) is the i-th element of a sequence τ , τ k is the prefix of τ of length k, and |τ | is the length of τ .
Not all histories make intuitive sense with respect to the ownership transfer reading of interface actions. For example, let Σ = RAM and consider the history in Figure 1(a). The history is meant to describe all the interactions between the library and the client. According to the history, the cell at the address 10 was first owned by the client, and then transferred to the library by thread 1. However, before this state was transferred back to the client, it was again transferred from the client to the library, this time by thread 2. This is not consistent with the intuition of ownership transfer, as executing the second action requires the cell to be owned both by the library and by the client, which is impossible in RAM.
As we show in this paper, histories that do not respect the notion of ownership, such as the one above, cannot be generated by any program, and should not be taken into account when defining linearizability. We now use the notion of footprints of states from Section 2 to characterise formally the set of histories that respect ownership. A finite history H induces a partial function H : F(Σ) F(Σ), which tracks how a computation with the history H changes the footprint of the library state: ε l = l; Hψ l = H l • δ(σ), if ψ = ( , call (σ)) ∧ ( H l • δ(σ))↓; Hψ l = H l \ \ δ(σ), if ψ = ( , ret (σ)) ∧ ( H l \ \ δ(σ))↓; Hψ l = undefined, otherwise.
Using this function, we characterise histories respecting the notion of ownership as follows. An interface set can be used to describe all the behaviours of a library relevant to its clients. In the following, H ranges over interface sets.
To keep client behaviours reproducible when replacing a concrete library by an abstract one, we do not need to require the latter to reproduce the histories of the former exactly: the histories generated by the two libraries can be different in ways that are irrelevant for their clients. We now introduce a linearizability relation that matches a history of a concrete library with that of the abstract one that yields the same client-observable behaviour.
We lift to BHistory as follows: (l, H) (l , H ) holds if l l and H H . Finally, we lift to interface sets as follows: Thus, a history H is linearized by a history H when the latter is a permutation of the former preserving the order of actions within threads and non-overlapping method invocations. The duration of a method invocation is defined by the interval from the method call action to the corresponding return action (or to the end of the history if there is none). An interface set H 1 is linearized by an interface set H 2 , if every history in H 1 may be reproduced in a linearized form by H 2 without requiring more memory. We now discuss the definition in more detail.
Definition 3.4 treats parts of memory whose ownership is passed between the library and the client in the same way as parameters and return values in the classical definition [18]: they are required to be the same in the two histories. In fact, the setting of the classical definition can be modelled in ours if we pass parameters and return values via the heap. Let Σ = RAM and let us fix distinct locations arg t ∈ Loc for t ∈ ThreadID meant for the transfer of parameters and return values. Then histories of the classical definition are represented in our setting by histories where all actions are of the form (t, call m([arg t : param])) or (t, ret m([arg t : retval ])), where param, retval ∈ Val.
The novelty of our definition lies in restricting the histories considered to balanced ones, which are the only ones that can be produced by programs (we formalise this fact in Section 5). The notion of balancedness also plays a key role in proving the Abstraction Theorem in the presence of ownership transfer (Section 6.1).
The fact that the linearizability relation allows us to permute actions by different threads lets us arrange method invocations into a linear sequence. For example the history in Figure 1(b) is linearized by that in Figure 1(c). The former might correspond to a concurrent stack implementation, where threads 1 and 2 pass parameters and return values via locations 1 and 2, respectively. Histories such as the one in Figure 1(c), where a call to every method is immediately followed by the corresponding return, are called sequential. Sequential histories correspond to abstract libraries with every method implemented atomically. When the histories in Figures 1(b) and 1(c) are members of interface sets defining the behaviour of concurrent and atomic stack implementations, the linearizability relationship ... ... between them allows us to justify that the call to pop by thread 1 in Figure 1(b) can return EMPTY, since this behaviour can be witnessed by the valid history of the atomic implementation in Figure 1(c). (In fact, the pop would also be allowed to return b, since the resulting history would be linearized by a sequential history with the push of b preceding the pop.) The requirement that the order of non-overlapping method invocations be preserved is inherited from the classical notion of linearizability [18]. As shown by Filipović et al. [12], this requirement is essential to validate an Abstraction Theorem for clients that can communicate via shared client-side variables. For example, since in Figure 1(b) the push of a returns before the push of b is called, the order between these method invocations has to stay the same in any linearizing history, such as the one in Figure 1(c).
Following Filipović et al. [12], we do not require the abstract history H to be sequential, like in the classical definition of linearizablity. This allows our definition to compare behaviours of two concurrent library implementations. We also allow a concrete history to contain calls without matching returns, arising, e.g., because the corresponding method invocation did not terminate. In this case, we require the same behaviour to be reproduced in the abstract history [14], which is possible because the latter does not have to be sequential. For example, the history in Figure 1(d) is linearized by that in Figure 1(e). This yields a simpler treatment of non-terminating calls than the use of completions in the classical definition of linearizability [18].
Definition 3.4 requires that the initial footprint of an abstract history H be smaller than that of the concrete history H. This requirement is standard in data refinement [13]: it ensures that, when we replace a concrete library by an abstract one in a program, the library-owned memory stays disjoint from the client-owned one. It does not pose problems in practice, as the abstract library generating H usually represents some of the data structures of the concrete library abstractly and, hence, more concisely.
So far we have defined the notion of linearizability on interface sets without taking into account library implementations that generate them. In the rest of the paper, we develop this notion for libraries written in a particular programming language and prove an Abstraction Theorem, which guarantees that a library can be replaced by another library linearizing it when we reason about its client program.

Programming Language
We consider a simple concurrent programming language: consists of a single library L implementing methods m ∈ Method and its client C 1 . . . C n , given by a parallel composition of threads. The language is parameterised by a set of primitive commands c ∈ PComm, meant to execute atomically. Commands also include method calls m ∈ Method, sequential composition C; C , nondeterministic choice C + C and finite iteration C * . We use + and * instead of conditionals and while loops for theoretical simplicity: as we show below, the latter can be defined in the language as syntactic sugar. Methods do not take arguments and do not return values, as these can be passed via special locations on the heap associated with the identifier of the thread calling the method (Section 3). We disallow nested method calls. We also assume that every method called in the program is defined by the library, and thus call S a complete program. An open program is a library L without a client, or a client C without a library implementation: C ::= let [−] in C . . . C P ::= S | C | L In C, we allow the client to call methods that are not defined in the program (but belong to the missing library). An open program represents a library or a client considered in isolation. The novelty of the kind of open programs we consider here is that we allow them to communicate with their environment via ownership transfers. We now define a way to specify a contract this communication follows.

Method Specifications.
A predicate is a set of states from Σ, and a parameterised predicate is a mapping from thread identifiers to predicates. We use the same symbols p, q, r for ordinary and parameterised predicates; it should always be clear from the context which one we mean. When p is a parameterised predicate, we write p t for the predicate obtained by applying p to a thread t. Both kinds of predicates can be described syntactically, e.g., using separation logic assertions [26].
We define possible ownership transfers between components with the aid of method specifications Γ, which are sets of Hoare triples {p} m {q}, at most one for each method.
Here p and q are parameterised predicates such that p t describes pieces of state transferred when thread t calls the method m, and q t , those transferred at its return. Note that the intention of the pre-and postconditions in method specifications is only to identify the areas of memory transferred; in other words, they describe the "type" of the returned data structure, but not its "value". As usual for concurrent algorithms, a complete specification of a library is given by its abstract implementation (Section 6).
For example, as we discussed in Section 1, when programmers store pointers in a concurrent container, they often intend to transfer the ownership of the data structures these pointers identify at calls to and returns from the container's methods. In Figure 2(a) we give an example of such a container-a bounded stack represented by an array. For readability, we write examples in C instead of the minimalistic language introduced above. The library protects the array by a lock; more complicated algorithms allow a higher degree of concurrency [17]. Take Σ = RAM and for x ∈ Loc let Obj(x) ⊆ RAM denote the set of states representing all well-formed data structures of a certain type allocated at the address x. For example, for objects with a single integer field we have Then the specification of the stack when it stores pointers to such data structures can be given as follows: Here we use the separation logic syntax to describe predicates parameterised by the thread identifier t. Thus, emp denotes the empty heap [ ], x → y the heap [x : y], and * the combination of heaps with disjoint domains. In the following we also use the assertion x..y → for x ≤ y, denoting all the heaps with the domain {x, x + 1, . . . , y}. We use distinguished locations arg t , t ∈ ThreadID to pass parameters and return values. According to the specification, the stack gets the ownership of an object when a pointer to it is pushed, and gives it up when the pointer is popped.
We specify an allocator managing blocks of size memory cells as follows: 2) The specification corresponds to the ownership transfer reading of allocator calls explained in Section 1. In Figure 2(b) we give an example allocator corresponding to the specification (we have omitted initialisation code from the figure). Note that, unlike the stack, the allocator does access the blocks of memory transferred to it by the client, since it stores free-list pointers inside them.
To define the semantics of ownership transfers unambiguously (Section 5), we require pre-and postconditions in method specifications to be precise [23]. Definition 4.1. A predicate r ∈ 2 Σ is precise if for every state σ there exists at most one substate σ 1 satisfying r, i.e., such that σ 1 ∈ r and σ = σ 1 * σ 2 for some σ 2 .
Since the * operation is cancellative, when such a substate σ 1 exists, the corresponding substate σ 2 is unique and is denoted by σ \ r. A parameterised predicate r is precise if so is r t for every t.
Informally, a precise predicate carves out a unique piece of the heap. A specified open program is of the form Γ C or L : Γ. In the former, the specification Γ describes all the methods that C may call. In the latter, Γ provides specifications for the methods in the open program that can be called by its external environment. In both cases, Γ specifies the type of another open program that can fill in the hole in C or L. When we are not sure which form a program has, we write Γ P : Γ . In this case, if P does not have a client, then Γ is empty; if P does not have a library, then Γ is empty; and if P is complete, then both Γ and Γ are empty. For specified open programs L : Γ agreeing on the specification Γ of library methods, we denote by C(L) the complete program let L in C 1 . . . C n .

Primitive Commands.
We now discuss primitive commands in more detail. Consider the set 2 Σ ∪ { } of subsets of Σ with a special element used to denote an error state, resulting, e.g., from dereferencing an invalid pointer. We extend the * operation on 2 Σ to 2 Σ ∪ { } by letting * p = p * = * = for all p ∈ 2 Σ .
We assume an interpretation of every primitive command c ∈ PComm as a transformer f t c : Σ → (2 Σ ∪ { }), which maps pre-states to states obtained when thread t ∈ ThreadID executes c from a pre-state. The fact that our transformers are parameterised by t allows atomic accesses to areas of memory indexed by thread identifiers. This idealisation simplifies the setting in that it lets us do without special thread-local or method-local storage for passing method parameters and return values.
Some typical primitive commands are: where expressions E are defined as follows: Here tid refers to the identifier of the thread executing the command, [E] returns the contents of the address E in memory, and !E is the C-style negation of an expression E-it returns 1 when E evaluates to 0, and 0 otherwise. The assume(E) command filters out all the input states where E evaluates to 0. Hence, after assume(E) is executed, E always has a non-zero  value. Using it, the standard commands for conditionals and loops can be defined in our language as follows: For the above commands c and t ∈ ThreadID, we define f t c : RAM → 2 RAM ∪ { } using the transition relation ; t : RAM × (RAM ∪ { }) in Figure 3: In the figure, E σ,t ∈ Val∪{ } denotes the result of evaluating the expression E in the state σ with the current thread identifier t. When this evaluation dereferences illegal memory addresses, it results in the error value . We define f t c : RAM π → 2 RAMπ ∪ { } similarly, but using the transition relation ; t : RAM π × (RAM π ∪ { }) in Figure 4. The transformers formalise the semantics of permissions explained in Section 2: permissions less than 1 allow reading, and the full permission 1 additionally allows writing. Note that assume yields an empty set of post-states when its condition evaluates to zero, leading to the program getting stuck. Thus, even though, when executing the if statement (4.3), both branches of the non-deterministic choice will be explored, only the branch where the assume condition evaluates to true will proceed further.
For our results to hold, we need to place some restrictions on the transformers f t c for every primitive command c ∈ PComm and thread t ∈ ThreadID: Footprint Preservation prohibits primitive commands from allocating or deallocating memory. This does not pose a problem, since in the context of linearizability, an allocator is just another library and should be treated as such. The Strong Locality of f t c says that, if a command c can be safely executed from a state σ 1 , then when executed from a bigger state σ 1 * σ 2 , it does not change the additional state σ 2 and its effect depends only on the state σ 1 and not on the additional state σ 2 . The Strong Locality is a strengthening of the locality property in separation logic [7]: Locality rules out commands that can check if a cell is allocated in the heap other than by trying to access it and faulting if it is not allocated. For example, let Σ = RAM and consider the following transformer f t : The transformer f t defines the denotation of a 'command' that writes 0 to the cell at the address 1 if it is allocated and acts as a no-op if it is not. This violates locality. Indeed, take σ 1 = [ ] and σ 2 = [1 : 1]. Then While locality prohibits the command from changing the additional state, it permits the effect of the command to depend on this state [13]. The Strong Locality forbids such dependencies. To see this, consider another 'command' defined by the following transformer The command does not access the cell at the address 2, since it does not fault if the cell is not allocated. However, when the cell is allocated, the effect of the command depends on its value. It is easy to check that f t is local. However, it is not strongly local, since for σ 1 = [1 : 0] and σ 2 = [2 : 0], we have The property of Strong Locality subsumes the one of contents independence used in situations similar to ours in previous work on data refinement in a sequential setting [13]. The transformers for standard commands, except memory (de)allocation, satisfy the conditions of Footprint Preservation and Strong Locality.

Client-Local and Library-Local Semantics
We now give the semantics to complete and open programs. In the latter case, we define component-local semantics that include all behaviours of an open program under any environment satisfying the specification associated with it. In Section 6, we use these to lift linearizability to libraries and formulate the Abstraction Theorem.
Programs in our semantics denote sets of traces, recording every step in a computation. These include both internal actions by program components and calls and returns. We define program semantics in two stages. First, given a program, we generate the set of the possible execution traces of the program. This is done solely based on the structure of its statements, without taking into account restrictions arising from the semantics of primitive commands or ownership transfers. The next step filters out traces that are not consistent with the above restrictions using a trace evaluation process and, for open programs, annotates calls and returns appropriately.

5.1.
Traces. Traces consist of actions, which include primitive commands performed internally by a component and calls or returns, possibly annotated with states. Thus actions, include all interface actions ψ from Definition 3.1.
Definition 5.1. The set of actions is defined as follows: where t ∈ ThreadID, m ∈ Method and c ∈ PComm.
Definition 5.2. A trace τ is a finite sequence of actions such that for every thread t, the projection of τ to t's call and return actions is a sequence of alternating call and return actions over matching methods that starts from a call action.
We classify actions in a trace as those performed by the client and the library based on whether they happen inside a method.
An action τ (i) is a library action if τ (i) = (t, c) for some t and c but τ (i) is not a client action, that is, A trace is a client trace, if all of its actions of the form (t, c) are client actions; it is a library trace, if they all of them are library actions.
In the following, κ denotes client traces, λ, ζ, α, β library traces, and τ arbitrary ones. We write client(τ ) for the projection of τ to client, call and return actions, lib(τ ) for that to library, call and return actions, and history(τ ) for that to call and return actions. Figure 5: Trace sets of commands and programs. Here prefix(T ) is the prefix closure of T and τ ∈ τ 1 . . . τ n if and only if every action in τ is done by a thread t ∈ {1, . . . , n} and for all such t, we have τ | t = τ t . We use λ for functions, in contrast to λ for library traces.

5.2.
Trace Sets. Consider a program Γ P : Γ and let M ⊆ Method be the set of methods implemented by its library or called by its client. We define the trace set Γ P : Γ ∈ 2 Trace of P in Figure 5. We first define the trace set C t η of a command C, parameterised by the identifier t of the thread executing it and a mapping η ∈ M × ThreadID → 2 Trace giving the trace set of the body of every method that C can call when executed by a given thread. The trace set of a client C 1 . . . C n η is obtained by interleaving traces of its threads.
The trace set C(L) of a complete program is that of its client computed with respect to a mapping λ(m, t). C m t ( ) associating every method m with the trace set of its body C m . Since we prohibit nested method calls, C m t η does not depend on η. We prefix-close the resulting trace set to take into account incomplete executions. In particular, this allows the thread scheduler to be unfair: a thread can be preempted and never scheduled again.
A program Γ C generates client traces Γ C , which do not include internal library actions. This is achieved by associating an empty trace with every library method. Finally, a program L : Γ generates all possible library traces L : Γ . This is achieved by running the library under its most general client, where every thread executes an infinite loop, repeatedly invoking arbitrary library methods.

5.3.
Evaluation. The set of traces generated using · may include those not consistent with the semantics of primitive commands or expected ownership transfers. We therefore define the meaning of a program Γ P : Γ ∈ Σ → (2 Trace ∪ { }) by evaluating every trace in Γ P : Γ from a given initial state to determine whether it is feasible. For open programs, this process also annotates calls and returns in a trace with states transferred.
The formal definition of Γ P : Γ is given in Figure 6 with the aid of a trace evaluation function Γ τ : Γ : Σ → 2 Σ×Trace ∪ { }. Given an initial state, this either yields multiple final states and annotated traces, or fails and produces . If the resulting set  Figure 6: Semantics of programs of state-trace pairs is empty, then the trace is infeasible and is discarded. If the evaluation produces on any trace from Γ P : Γ , then the program has no semantics for the given initial state and its denotation is defined to be . The evaluation of τ is defined inductively on its length using a function Γ ϕ : Γ : Σ → 2 Σ×Act ∪ { } that evaluates a single action ϕ. We explain this function by considering separately the cases of a complete program, open program with a library and open program with a client.
The evaluation ϕ for an action in a complete program has the standard semantics, with the effects of primitive commands computed using their transformers from Section 4. In this case, calls and returns are left unannotated, since no ownership transfers to or from the external environment are performed.
The function ϕ : Γ gives a library-local semantics to the program L : Γ , in the sense that it generates library traces under any client respecting Γ . When a method m from Γ is called by thread t, the library receives the ownership of any state consistent with the method precondition p t . This state has to be compatible with that of the library. After the method returns, the library has to give up the piece of state satisfying its postcondition. Since q t is precise, this piece of state is determined uniquely. The evaluation faults if the state to be transferred is not available; thus, a library has no semantics if it violates the contract with its client given by Γ . This also ensures that the histories produced by a library are balanced.

The function Γ
ϕ gives a client-local semantics to Γ C, in the sense that it generates traces of this client assuming any behaviour of the library consistent with Γ. When a thread t calls a method m in Γ, it transfers the ownership of a piece of state satisfying the method precondition p t to the library being called. As before, this piece is defined uniquely, because preconditions are precise. When such a piece of state is not available, the evaluation faults. This ensures that client respects the method specifications of the libraries it uses. When the method returns, the client receives the ownership of an arbitrary piece of state satisfying its postcondition q t , compatible with the current state of the client.

5.4.
Connection between Local and Global Semantics. We now formulate a lemma, used in the proof of the Abstraction Theorem (Section 6), that states the connection between the library-local and client-local semantics on one side and the semantics of complete programs on the other. We start by introducing some auxiliary definitions.
For a set of initial states I ⊆ Σ, let We define an operator ⊗ : 2 Σ×Trace × 2 Σ×Trace → 2 Σ×Trace combining the resulting sets X and Y of state-trace pairs produced by the client-local and library-local semantics into a set corresponding to the complete program: where cover(τ, κ, λ) ⇐⇒ history(κ) = history(λ) ∧ client(τ ) = ground(κ) ∧ lib(τ ) = ground(λ) and ground is a function on traces that erases the state annotations from their interface actions.
The lemma shows that the set of traces produced by C(L) can be obtained by combining pairs of traces with the same history produced by C and L. Note that, since the semantics of C(L) does not annotate calls and returns with the states transferred, in cover we have to erase these annotations from the local traces κ or λ before comparing the traces with τ . Unpacking the definition of ⊗ and using the fact that ∀κ, λ. history(κ) = history(λ) =⇒ ∃τ. cover(τ, κ, λ), from Lemma 5.6 we get the following two corollaries.
Corollary 5.7 can be viewed as carrying over properties of the local semantics, such as safety, to the global one, and in this sense is the statement of the soundness of the former with respect to the latter. The corollary also confirms that the client defined by L : Γ and λ : Γ is indeed most general, as it reproduces library behaviours under any possible clients. Corollary 5.8 carries over properties of the global semantics to the local ones, stating the adequacy of the latter. Lemma 5.6 is proved in Appendix A. Most of the proof deals with maintaining a splitting of the state of C(L) into the parts owned by L and C, which changes during ownership transfers. The proof relies crucially on the safety of the client and the libraries and the Strong Locality property of primitive commands. In more detail, safety is defined by considering executions of a component in the library-local or the client-local semantics. These execute the component code only on the memory it owns, whose amount only changes with ownership transfers to and from its environment according to method specifications. Because of the Strong Locality property, commands fault when accessing memory cells that are not present in the state they are run from, and their execution does not depend on any additional memory that might be present in the state. Hence, when we use a component inside a complete program, its safety guarantees that the component code does not touch the part of the heap belonging to other components in the program, and its execution is not affected by the state of such components. This guarantees that the behaviour a component produces as part of the complete program can be reproduced when we execute it in isolation and vice versa, allowing us to establish Lemma 5.6. In practice, the safety of a program can be established using existing program logics, such as separation logic [23,28].
Thus, (L 1 : Γ, I 1 ) is linearized by (L 2 : Γ, I 2 ) if every history generated by the librarylocal semantics of the former may be reproduced in a linearized form by the library-local semantics of the latter without requiring more memory. The relation (L 1 : Γ, I 1 ) (L 2 :  Figure 7: Specifications corresponding to the implementations in Figure 2: (a) a bounded stack storing pointers to objects; (b) a memory allocator managing memory blocks of a fixed size. The Node structure is defined in Figure 2(b).
Γ, I 2 ) allows us to specify a library by another piece of code, but possibly simpler than the original one. For example, the stack and the allocator from Figure 2 with method specifications (4.1) and (4.2) can be specified by the libraries in Figure 7. The libraries replace the array and the linked list in the implementations by the abstract data types of a sequence and a set (we assume a trivial extension of the RAM algebra from Section 2 to allow memory cells to store values of such types). Thus, the abstract libraries use less memory than the concrete ones. Instead of using locking, all operations on the abstract data types are done atomically; formally, we assume primitive commands corresponding to the code in the atomic blocks. The other relation (L 1 : Γ, I 1 ) H 2 introduced in Definition 6.1 allows us to specify a library directly by an interface set, without fixing a piece of code generating it. The interface set H 2 can still be simpler than that of (L 1 : Γ, I 1 ), e.g., containing only sequential histories. Even though the two forms of defining linearizability may seem very similar, as we show in Section 6.1, their mathematical properties are fundamentally different.
Thus, when reasoning about a client C(L 1 ) of a library L 1 , we can soundly replace L 1 by a library L 2 linearizing it: if a safety property over client traces holds of C(L 2 ), it will also hold of C(L 1 ). In practice, we are usually interested in atomicity abstraction, a special case of this transformation when methods in L 2 are atomic. An instance is replacing one of the libraries from Figure 2 by its specification from Figure 7. The requirement that C be safe in the theorem restricts its applicability to well-behaved clients that do not access memory owned by the library: you cannot replace a library by another one if the client can access its internal data structures and thereby "look inside the box". Similarly, the safety of the libraries ensures that they cannot corrupt the data structures owned by the client.
The theorem shows that client behaviours of C(L 1 ) can be reproduced by the client-local semantics of C projected to histories in H 2 with initial footprints compatible with initial client states. Note that client(τ 1 ) = client(τ 2 ) in Theorem 6.2 implies that history(τ 1 ) = history(τ 2 ), i.e., C(L 2 ) can reproduce the history of C(L 1 ) exactly. In contrast, Theorem 6.4 does not guarantee this, since κ ∼ κ does not imply history(κ) = history(κ ); we only know that the projection to non-interface actions is reproduced. We discuss the reason for this discrepancy below.  The proof of the lemma is highly non-trivial and is a subject of Section 7. We point out Lemma 6.5 would not hold had we included unbalanced histories in our definition of linearizability. To show this, take Σ = RAM and consider the histories in Figure 8. In Figure 8(b) the library receives the cell 10 from the client, then returns it and then receives it again. Even though the history in Figure 8(a) is linearized by that in Figure 8(b), the former is not balanced, and by Proposition 5.4, cannot be produced by L. This shows that Lemma 6.5 does not hold for unbalanced H.
This fact is not a consequence of ownership transfer and also holds for the classical notion of linearizability. Intuitively, Lemma 6.5, and hence, Corollary 6.6 hold due to a closure property of the semantics of the language from Section 4. Namely, in this and other programming languages, there may always be a delay between the point when a library method is called and when it starts executing and, conversely, when it ends executing and when the control returns to the client. For example, when executing the code in Figure 7(a), there may be delays between a call to push, the execution of the atomic block and the return from push. Hence, this library can produce both of the histories in Figures 1(b) and 1(c). Due to this property of the program semantics, a trace from L , e.g., one producing the history in Figure 1(c), will stay valid if we execute some of the calls in it earlier and returns later, like in Figure 1(b). This is also (usually) safe given the ownership transfer reading of calls and returns in the library-local semantics defined by L : Γ : it just means that the library receives state from the client earlier and gives it up later. The proof of Lemma 6.5 uses such transformations on a history to "de-linearize" it, e.g., transforming  Figure 1(c) into that in Figure 1(b). The above closure property is also the reason for Theorem 6.2 guaranteeing that C(L 2 ) can reproduce the history of C(L 1 ) exactly.
Given that replacing a library L 1 by its linearization L 2 does not simplify its interface set, can Theorem 6.2 really simplify reasoning about a complete program C(L 1 )? Fortunately, the answer is yes, since the point of the theorem is to simplify the code of this program. For example, replacing the library in Figure 2(a) by the one in Figure 7(a) allows us to pretend in reasoning about a complete program that changes to the library state, shared between different threads, are atomic, and thus consider fewer possible thread interleavings. Calls and returns in such a complete program are merely thread-local operations that do not complicate reasoning. In Section 6.2, we discuss an example of using Theorem 6.2 to simplify proofs of complicated algorithms.
Specifying a library by an interface set H 2 instead of code, as in Theorem 6.4, does not allow us to get results such as Lemma 6.5 and Corollary 6.6, since the set H 2 is not guaranteed to satisfy any closure properties. For example, it might contain only sequential histories, where every call is immediately followed by the corresponding return without a delay. In fact, H 2 has to be simpler than the interface set of L 1 for Theorem 6.4 to be useful, since this is what the theorem replaces L 1 by. Fortunately, to prove Theorem 6.4 we can exploit a closure property of the client-local semantics, formalised by the following variant of the Rearrangement Lemma: any client trace can be transformed into an equivalent one with a given history linearizing the history of the original one. Lemma 6.7 (Rearrangement-client). If (l, H) (l , H ) and Γ C is safe at σ, then Intuitively, the lemma holds because, in the client-local semantics, it is safe to execute calls later and returns earlier. Like Lemma 6.5, this lemma would not hold if we allowed H to be unbalanced.
In summary, when a library is specified by the code of its abstract implementation, the ability to linearize a concrete history while looking for a matching abstract one allowed by Definition 3.4 is not strictly needed. However, it is indispensable when the library is specified directly by a set of histories. We were able to obtain this insight into the original definition of linearizability by formalising the guarantees the linearizability of a library provides to its clients as Abstraction Theorems.
Using Lemmas 6.5 and 6.7, we now prove the two versions of the Abstraction Theorem.
The above proof scheme can be described mnemonically as 'decompose, rearrange, compose'. We reuse its first two steps to prove Theorem 6.4.
6.2. Establishing and Using Linearizability with Ownership Transfer. Our preliminary investigations show that linearizability with ownership transfer can be established by generalising existing proof systems for proving classical linearizability based on separation logic [28]. The details of such a generalisation are out of the scope of this paper; we plan to report on it in the future.
The Abstraction Theorem is not just a theoretical result: it enables compositional reasoning about complex concurrent algorithms that are challenging for existing verification methods. For example, the theorem can be used to justify Vafeiadis's compositional proof [28,Section 5.3] of the multiple-word compare-and-swap (MCAS) algorithm implemented using an auxiliary operation called RDCSS [16] (the proof used an abstraction of the kind enabled by Theorem 6.2 without justifying its correctness). If the MCAS algorithm were verified together with RDCSS, its proof would be extremely complicated. Fortunately, we can consider MCAS as a client of RDCSS, with the two components performing ownership transfers between them. The Abstraction Theorem then makes the proof tractable by allowing us to verify the linearizability of MCAS assuming an atomic specification of the inner RDCSS algorithm.

Proof of the Rearrangement Lemma
We only give the proof of Lemma 6.5, as that of Lemma 6.7 is completely symmetric.
The proof transforms λ into λ by repeatedly swapping adjacent actions in it according to a certain strategy to make the history of the trace equal to H. The most subtle place in the proof is swapping (t 1 , ret m 1 (σ 1 )) (t 2 , call m 2 (σ 2 )) to yield (t 2 , call m 2 (σ 2 )) (t 1 , ret m 1 (σ 1 )), where t 1 = t 2 . This case is subtle for the following reason. Let the state of the library L before the return action be θ; then (θ \ σ 1 )↓ and the state of the library after executing the return and the call is (θ \ σ 1 ) * σ 2 . For the swapping to be possible, we need (θ * σ 2 )↓; then by Proposition 2.2 (θ \ σ 1 ) * σ 2 = (θ * σ 2 ) \ σ 1 , (7.1) which can be used to establish that the resulting trace is still produced by L. However, (θ * σ 2 )↓ is not guaranteed if the history H is arbitrary. For example, take Σ = RAM and let H and H be defined by Figures 8(a) and 8(b). Since H is unbalanced, it cannot be produced by any library, and hence, we cannot swap in H . In our proof we use the fact that the history H is balanced to show that a situation in which we cannot swap a return followed by a call while transforming λ into λ cannot happen. This is non-trivial, as the problematic situation can potentially happen midway through the transformation. We only know that the target history H of λ is balanced, but this does not straightforwardly imply that the histories of the intermediate traces obtained while transforming λ into λ are, since these histories might be quite different from H. Inferring their balancedness from that of H represents the most challenging part of the proof.
We therefore first do the proof under an assumption that allows swapping a return followed by a call easily and consider the general case later. This lets us illustrate the overall idea of the proof, which is then reused in the additional part of the proof dealing with the challenge presented by the general case. Namely, we make the following assumption: Σ = RAM and for any ζ ∈ L : Γ σ and interface actions ψ 1 = (t 1 , (σ 1 )) and ψ 2 = (t 2 , (σ 2 )) in ζ, if t 1 = t 2 , then dom(σ 1 ) ∩ dom(σ 2 ) = ∅.
For example, this holds when states transferred between the client and the library are always thread-local. It is easy to check that in RAM, if (θ \ σ 1 )↓, ((θ \ σ 1 ) * σ 2 )↓ and (σ 1 * σ 2 )↓, then (θ * σ 2 )↓ and thus (7.1) holds. Hence, (7.2) allows us to justify swapping a return followed by a call in a trace easily. We now proceed to prove Lemma 6.5 under this assumption. In our proof, we use the assumption in a single place, which we note explicitly; the rest of the proof is independent from it. Below we sometimes write ρ instead of to make the bijection ρ used to establish the relation between histories in Definition 3.4 explicit. For a bijection ρ between histories H and H , we write id k (ρ) if ρ is an identity on the first k actions in H.
We let β 0 = ε, so that the above conditions are initially satisfied. Thus, during the transformation, progressively longer prefixes β k of α k have histories coinciding with prefixes of H, while the linearizability relation between the history H and that of α k is preserved. We then take α |H| as the desired trace λ.
Lemma 7.1. Assume (7.2) holds. Consider a history H 1 ψH 2 and a trace λ 1 λ 2 ∈ L : Γ σ such that Then there exist traces λ 2 and λ 2 such that λ 1 λ 2 λ 2 ∈ L : Γ σ and history(λ 1 λ 2 ) = H 1 ψ; To prove Lemma 7.1, we convert λ 1 λ 2 into λ 1 λ 2 λ 2 by swapping adjacent actions in the trace a finite number of times while preserving its properties of interest. These transformations are described by the following proposition, which formalises the closure properties of the library-local semantics we alluded to in Section 6.1.
Since, in the library-local semantics, the library gains state at a call and gives it up at a return, intuitively, the transformation in the proposition allows the library to gain state earlier (i, ii) and give it up later (iii). The assumption that ϕ 2 precede ϕ 1 in case (ii) is needed to ensure that the transformation does not violate the linearizability relation. The proof of case (ii) is the only place where the assumption (7.2) is used.
2. ψ ∈ RetAct. Assume that λ 3 contains a call action ϕ, so that it precedes the return action ψ in history(λ 1 λ 2 ). Then by (7.3) and (7.4) the action in H 1 ψH 2 corresponding to ϕ according to ρ is in H 2 and thus follows ψ in H 1 ψH 2 . This violates the preservation of the order of non-overlapping method invocations required by (7.4). Hence, there are no call actions in λ 3 . Since λ 1 λ 2 is a library trace, this implies that for any action ϕ = (t, ret ) in λ 3 there are no actions by the thread t in λ 3 following ϕ. Thus, we can move all return actions in the subtrace λ 3 of λ 1 λ 2 to the position between ψ and λ 4 by swapping them with adjacent actions a finite number of times as described in Proposition 7.2(iii). We thus obtain the trace λ 1 λ 3 ψλ 4 λ 4 ∈ L : Γ σ , where λ 4 consists of all return actions in λ 3 , and λ 3 of the rest of actions in the subtrace; in particular, λ 3 does not contain any interface actions. Conditions (7.5)-(7.6) then follow from Proposition 7.2(iii) for λ 2 = λ 3 ψ and λ 2 = λ 4 λ 4 .
This completes the proof of Lemma 6.5 under the assumption (7.2). Let us now lift this assumption and consider the only place in the proof of the lemma that relies on it-that when we swap a return followed by a call using Proposition 7.2(ii) in case 1 in the proof of Lemma 7.1. Let us now identify precise conditions under which this situation happens. Let ψ = (t 1 , call m 1 (σ 1 )) and let the adjacent return action with which we are trying to swap it be (t 2 , ret m 2 (σ 2 )). Let S 1 be the target history H 1 ψH 2 from Lemma 7.1 and S 2 be the history of the trace in which we are trying to swap the return and the call. Then the two histories are of the form S 1 = S (t 1 , call m 1 (σ 1 )) S 1 (t 2 , ret m 2 (σ 2 )) S 2 ; S 2 = SS 1 (t 2 , ret m 2 (σ 2 )) (t 1 , call m 1 (σ 1 )) S 2 (7.7) for some S, S 1 , S 2 , S 1 , S 2 . Furthermore, from the conditions of Lemma 7.1, we have: (ii) S 1 and S 2 are balanced from some l 1 and l 2 , respectively, such that l 2 l 1 ; and (iii) S 1 ρ S 2 , where id |S| (ρ) and ρ maps (t 1 , call m 1 (σ 1 )) and (t 2 , ret m 2 (σ 2 )) in S 1 to the corresponding actions shown in S 2 . As the following proposition shows, we can always do the desired transformation if the history SS 1 (t 1 , call m 1 (σ 1 )) (t 2 , ret m 2 (σ 2 )) S 2 (7.8) resulting from swapping the return and the call in S 2 is balanced from l 2 . Proposition 7.3. Let L : Γ be safe at σ 0 . Consider traces Thus, the only problematic case we have is when the history (7.8) is not balanced from l 2 . We summarise all the conditions under which such case can happen in the following definition.
Definition 7.4. Histories S 1 and S 2 of the form (7.7) are conflicting if the conditions (i)-(iii) above are satisfied and the history (7.8) is not balanced from l 2 . Given Proposition 7.3, the only case when the transformation in the proof of Lemma 7.1 can fail to convert the trace is when H 1 ψH 2 and the history currently being transformed are conflicting. Thus, with the assumption (7.2) lifted, Lemma 7.1 turns into Lemma 7.5. Consider a history H 1 ψH 2 , and a trace λ 1 λ 2 ∈ L : Γ σ such that (7.3) and (7.4) hold. Then either H 1 ψH 2 and another history composed of actions from history(λ 1 λ 2 ) are conflicting, or there exist traces λ 2 and λ 2 such that λ 1 λ 2 λ 2 ∈ L : Γ σ and (7.5) and (7.6) hold.
We now show that no conflicting pairs of histories exist, hence guaranteeing that Lemma 7.5 can always be used to construct α k+1 from α k in transforming λ into λ. This completes the proof of Lemma 6.5 in the general case.
We first discuss the main idea of the proof. The history S 1 in (7.7) is similar to (7.8) in that the call precedes the return. We would like to use the fact that S 1 is balanced to prove that so is (7.8), thereby yielding a contradiction. As we noted at the beginning of this section, this is not straightforward due to the differences in the form of the histories S 1 and S 2 other than the precedence of the two call and return actions. We resolve this problem by adjusting the strategy we used above to transform λ into λ under the assumption (7.2) to iron out the differences between S 1 and S 2 . In particular, we use a variant of the transformation that, when the process of moving the call action ψ to the left in λ 1 λ 2 gets stuck (Figure 9), leaves the corresponding action in H 1 ψH 2 unmatched and continues bringing the rest of the trace λ 1 λ 2 in sync with the target history. Proof. Consider histories S 1 and S 2 satisfying the conditions in Definition 7.4. Since S 2 is balanced from l 2 , is defined. Since ( SS 1 l 2 ) \ \ δ(σ 2 ) is defined, by Proposition 2.7, we have: Then (7.8) is balanced from l 2 , contradicting our assumptions. Hence, (( SS 1 l 2 ) • δ(σ 1 ))↑.
A call action in S 1 cannot be in S 2 : in this case it would follow (t 2 , ret m 2 (σ 2 )) in S 1 , but precede it in S 2 , contradicting S 1 S 2 . Hence, all call actions in S 1 are in S 1 . Let S 1 = S 3 S 4 , where S 3 is the minimal prefix of S 1 containing all call actions from S 1 . Then If S 3 is non-empty, any return action in it precedes its last call action, which is also in S 1 . Since S 1 S 2 , such a return action also has to be in S 1 . Thus, all return actions in S 3 are in S 1 .
The traces S 1 and S 2 are of the following more general form, obtained by letting S 0 = S (t 1 , call m 1 (σ 1 )) and S 0 = S: where • S 1 and S 2 are balanced from some l 1 and l 2 , respectively, such that l 2 l 1 ; • S 0 and S 0 are identical, except S 0 may have some extra call actions; • S 1 ρ S 2 ; • ρ −1 maps all call actions in S 1 to actions in S 3 ; • ρ maps all return actions in S 3 to actions in S 1 ; • ρ −1 maps actions in S 0 to those in S 0 , in particular (t 1 , call m 1 (σ 1 )) to an action in S 0 , and (t 2 , ret m 2 (σ 2 )) to the same action shown in S 1 ; and • (( S 0 S 1 l 2 ) • δ(σ 1 ))↑. We denote this form by (F). The additional call actions in S 0 are the ones for which the transformation in Lemma 7.1 failed. The conditions relating S 3 and S 1 imply that S 3 may have more calls than S 1 , and S 1 more returns than S 3 . Thus, intuitively, S 0 S 3 gains more state than S 0 S 1 , including that transferred by (t 1 , call m 1 (σ 1 )), and S 0 S 1 gives up more than S 0 S 3 . In the following, we use this and the fact that S 1 is balanced from a bigger footprint than S 2 to show that (( S 0 S 1 l 2 ) • δ(σ 1 ))↓, thereby yielding a contradiction.
To this end, we describe a process that transforms the histories S 1 and S 2 into another pair of histories satisfying the conditions above, but such that S 3 is strictly smaller.
Repeatedly applying this process, we can make S 3 empty, obtaining histories satisfying (F): (7.9) In particular, (( S 0 S 1 l 2 ) • δ(σ 1 ))↑. Before describing the transformation process, we show that, given the above pair of histories, we can obtain a contradiction. We use the following simple proposition, proved in Appendix A.1.
Proposition 7.7. Assume S is identical to S , except it may have extra calls, and S and S are balanced from l 1 and l 2 , respectively, such that l 2 l 1 . Then the •-combination l c of footprints of states transferred at the extra call actions in S is defined, S is balanced from l 1 and S l 1 = ( S l 1 ) • l c ∧ S l 2 S l 1 .
Consider the histories in (7.9). Since all calls from S 1 are in S 3 = ε, S 1 contains only returns.
Since the histories are balanced from l 1 and l 2 , respectively, S 0 l 1 and S 0 l 2 are defined. The history S 0 is identical to S 0 , except it may have extra calls. By Proposition 7.7, the •-combination of footprints of states transferred at the extra call actions in S 0 is defined.
Since an action (t 1 , call m 1 (σ 1 )) is in S 0 , but not in S 0 , this combination is of the form δ(σ 1 ) • l c for some l c ; hence, Therefore, ( S 0 l 2 ) • δ(σ 1 ) is defined. Since S 1 contains only return actions, where l is the •-combination of the footprints of states transferred at these actions. This implies S 0 l 2 = ( S 0 S 1 l 2 ) • l , where both expressions are defined. But then so is Hence, ( S 0 S 1 l 2 ) • δ(σ 1 ) is defined, contradicting the opposite fact established above. This contradiction implies that a conflicting pair of histories does not exist. Now assume arbitrary histories S 1 and S 2 satisfying (F): We show that from these we can construct another pair of histories satisfying (F), but with S 3 strictly smaller. We use the same transformation as in the proof of Lemma 7.1. When this transformation gets stuck, we obtain another pair of histories of the form (F), but again with a smaller S 3 .
Let us make a case split on the next action in S 3 . • S 3 = (t, call m(σ)) S 5 , such that the action corresponding to (t, call m(σ)) according to ρ is not in S 1 . In this case we let S 0 := S 0 (t, call m(σ)) and S 3 := S 5 . Thus, the call action (t, call m(σ)) unmatched in S 1 becomes part of S 0 .

A. GOTSMAN AND H. YANG
• S 3 = (t, call m(σ)) S 5 , such that the action corresponding to (t, call m(σ)) according to ρ is in S 1 . Let S 1 = S 3 (t, call m(σ))S 4 , so that Using the transformations from case 1 in the proof of Lemma 7.1, we can try to move the action (t, call m(σ)) to the position between S 0 and S 3 while preserving the balancedness of the history. If this succeeds, we construct a new pair of histories of the form (F) by letting S 0 := S 0 (t, call m(σ)), S 3 := S 5 , S 0 := S 0 (t, call m(σ)) and S 1 := S 3 S 4 . Otherwise, we get a pair of conflicting histories, which are of the form (F) but with a smaller S 3 . Again, in this case the unmatched call action (t, call m(σ)) becomes part of S 0 . • S 3 = (t, ret m(σ)) S 5 . Then the action corresponding to (t, ret m(σ)) according to ρ is also in S 1 , so that S 1 = S 3 (t, ret m(σ)) S 4 : Using the transformations from case 2 in the proof of Lemma 7.1, we can move the return action to the position between S 0 and S 3 while preserving the balancedness of the history.

Frame Rule for Linearizability
Libraries such as concurrent containers are used by clients to transfer the ownership of data structures, but do not actually access their contents. We show that for such libraries, the classical linearizability implies linearizability with ownership transfer.
For example, the method specification (4.1) of the stack in Figure 2(a) extends the following specification: According to this specification, push just receives an arbitrary pointer x as a parameter; in contrast, the specification (4.1) additionally mandates that the object the pointer identifies be transferred to the library. We now identify conditions under which the linearizability between a pair of libraries satisfying Γ entails that of the same libraries satisfying an extended method specification Γ . This yields a result somewhat analogous to the frame rule of separation logic [26]. We start by introducing some auxiliary definitions. We first define operations for mapping between histories corresponding to extended and non-extended method specifications.
For the method specification Γ from Definition 8.1, we define operations · Γ and · Γ on interface actions as follows: (t, call m(σ)) Γ = (t, call m(σ \ (σ \ p m t ))); (t, ret m(σ)) Γ = (t, ret m(σ \ (σ \ q m t ))); (t, call m(σ)) Γ = (t, call m(σ \ p m t )); (t, ret m(σ)) Γ = (t, ret m(σ \ q m t )); otherwise, the result is undefined. Thus, ψ Γ selects the part of the state in ψ that is required by Γ and ψ Γ the extra piece of state not required by it. We then lift · Γ and · Γ to traces by applying them to every interface action. Given a history H 0 produced by a library L : Γ , we need to be able to check that the library does not modify the extra pieces of state not required by the original method specification Γ, which are given by H 0 Γ . To this end, we define an evaluation function similar to · from Section 3, which is meant to be applied to H 0 Γ . For an interface action ψ we define ψ : Σ → (Σ ∪ { }) as follows: We then define the evaluation H : Σ → (Σ ∪ { }) of a history H as follows: Thus, if the evaluation does not fail, then the history respects the notion of ownership and the pieces of state transferred to the library are returned to the client unmodified. (3) (L 1 : Γ, I 1 ) (L 2 : Γ, I 2 ); and (4) for every σ 0 ∈ I 1 , σ 0 ∈ I and λ ∈ L 1 : Γ (σ 0 * σ 0 ), we have history(λ) Γ σ 0 = . Then (L 1 : Γ , I 1 * I) (L 2 : Γ , I 2 * I).
The theorem allows us to establish the linearizability relation with respect to the extended specification Γ given the relation with respect to Γ. This enables the use of the Abstraction Theorem for clients performing ownership transfer. However, the theorem does not guarantee the safety of the libraries with respect to Γ for free, because it is not implied by their safety with respect to Γ. Intuitively, this is because Γ extends both preconditions and postconditions in Γ; hence, not only does it guarantee to the library that the client will provide extra pieces of state at calls, but it also requires the library to provide (possibly different) extra pieces of state at returns. For example, Γ might assign the specification {arg t → } m {arg t → } to every method m, and Γ , the specification {arg t → } m {∃x. arg t → x * x → }. Unless a library already has all the memory required by the postconditions in Γ in its initial state, it has no way of satisfying Γ .
This situation is in contrast to the frame rule of separation logic [26], which guarantees the safety of a piece of code with respect to an extended specification. However, the frame rule requires the latter specification to extend both pre-and postconditions with the same piece of state, so that the code returns it immediately after termination. In our setting, a library can return the extra state to its client after a different method invocation and, possibly, in a different thread. It can be shown that for the library L 1 in Figure 2(a), the library L 2 in Figure 7(a) and method specification Γ defined by (8.1), we have (L 1 : Γ, I 1 ) (L 2 : Γ, I 2 ). It is also not difficult to prove (e.g., using separation logic) that L 1 : Γ and L 2 : Γ are safe. Condition (4) in Theorem 8.2 is satisfied, since the proof of safety of L 1 : Γ would use only the extra state provided in the preconditions of Γ to provide the extra state required by its postconditions. Hence, by Theorem 8.2 we have (L 1 : Γ , I 1 ) (L 2 : Γ , I 2 ).
However, Theorem 8.2 is not applicable to the memory allocators in Figures 2(b) and 7(b): since the allocator implementation in Figure 2(b) stores free-list pointers inside the memory blocks, it is unsafe with respect to the variant of the method specification (4.2) that does not transfer their ownership.
The proof of Theorem 8.2 relies on the following two lemmas, proved in Appendices A.3 and A.4, that convert between library traces corresponding to extended and original method specifications. The first lemma shows that for a trace λ produced by L : Γ , the trace λ Γ can be produced by L : Γ. The safety of the library with respect to Γ and condition (4) from Theorem 8.2 guarantee that the smaller preconditions specified by Γ are enough for the library to execute safely and that the extra pieces of state in Γ do not influence its execution. Lemma 8.3. If λ ∈ L : Γ (σ 0 * σ 0 ), L : Γ is safe at σ 0 , and history(λ) Γ σ 0 = , then λ Γ ∈ L : Γ σ 0 .
The other lemma gives conditions under which we can conclude that a trace λ is produced by L : Γ given that λ Γ is produced by L : Γ.

Related Work
The original definition of linearizability [18] was proposed in an abstract setting that did not consider a particular programming language and implicitly assumed a complete isolation between the states of the client and the library. Furthermore, at the time it was not clear what the linearizability of a library entails for its clients. Filipović et al. [12] were the first to observe that linearizability implies a form of contextual refinement; technically, their result is similar to our Lemma 6.7, but formulated over a highly idealistic semantics. In a previous work [14], we generalised their result to a compositional proof method, formalised by an Abstraction Theorem, that allows one to replace a concrete library by an abstract one in reasoning about a complete program.
This paper is part of our recent push to propose notions of concurrent library correctness for realistic programming languages. So far we have developed such notions together with the corresponding Abstraction Theorems for supporting reasoning about liveness properties [14] and weak memory models [4,6,15]. All these results assumed that the library and its client operate in disjoint address spaces and, hence, are guaranteed not to interfere with each other and cannot communicate via the heap. Lifting this restriction is the goal of the present paper. Although the basic proof structure of Theorems 6.2 and 6.4 is the same as in [6,14], the formulations and proofs of the Abstraction Theorem and the required lemmas here have to deal with technical challenges posed by ownership transfer that did not arise in previous work. First, their formulations rely on the novel forms of client-local and library-local semantics (Section 5) that allow a component to communicate with its environment via ownership transfers. Proving Lemma 5.6 then involves a delicate tracking of a splitting between the parts of the state owned by the library and the client, and how ownership transfers affect it. Second, the key result needed to establish the Abstraction Theorem is the Rearrangement Lemma (Lemmas 6.5 and 6.7). What makes the proof of this lemma difficult in our case is the need to deal with subtle interactions between concurrency and ownership transfer that have not been considered in previous work. Namely, changing the history in the lemma requires commuting ownership transfer actions; justifying the correctness of these transformations is non-trivial and relies on the notion of history balancedness that we propose. These differences notwithstanding, we hope that techniques for handling ownership transfer proposed in this paper can be combined with the ones for handling other types of client-library interactions considered so far [4,6,14,15].
Recently, there has been a lot of work on verifying linearizability of common algorithms; representative papers include [1,10,28]. All of them proved classical linearizability, where libraries and their clients exchange values of a given data type and do not perform ownership transfers. This includes even libraries, such as concurrent containers, that are actually used by client threads to transfer the ownership of data structures. The frame rule for linearizability we propose (Theorem 8.2) justifies that classical linearizability established for concurrent containers entails linearizability with ownership transfer. This makes our Abstraction Theorem applicable, enabling compositional reasoning about their clients.
Turon and Wand [27] have proposed a logic for establishing refinements between concurrent modules, likely equivalent to linearizability [12]. Their logic considers libraries and clients residing in a shared address space, but not ownership transfer. As a result, they do not support separate reasoning about a library and its client in realistic situations of the kind we consider.
Elmas et al. [10,11] have developed a system for verifying concurrent programs based on repeated applications of atomicity abstraction. They do not use linearizability to perform the abstraction. Instead, they check the commutativity of an action to be incorporated into an atomic block with all actions of other threads. In particular, to abstract a library implementation in a program by its atomic specification, their method would have to check the commutativity of every internal action of the library with all actions executed by the client code of other threads. Thus, the method of Elmas et al. does not allow decomposing the verification of a program into verifying libraries and their clients separately. In contrast, our Abstraction Theorem ensures the atomicity of a library under any safe client.
The most common approach of decomposing the verification of concurrent programs is using thread-modular reasoning methods, which consider every thread in the program in isolation under some assumptions on its environment [20,24]. However, a single thread would usually make use of multiple program components. This work goes further by allowing a finer-grain intrathread-modular reasoning: separating the verification of a library and its client, the code from both of which may be executed by a single thread. Note that this approach is complementary to thread-modular reasoning, which can still be used to carry out the verification subtasks, such as establishing the linearizability of libraries and proving the safety of clients. Thread-modular techniques do enable a restricted form of intrathreadmodular reasoning, since they allow reasoning about the control of a thread in a program while ignoring the possibility of its interruption by the other threads. Hence, they allow considering a library method called by the thread in isolation, e.g., by using the standard proof rules for procedures. However, such a decomposition is done under fixed assumptions on the environment of the thread and thus does not allow, e.g., increasing the atomicity of the environment's actions. As the example of MCAS shows (Section 6.2), this is necessary to deal with complex algorithms.
Ways of establishing relationships between different sequential implementations of the same library have been studied in data refinement [19,25], including cases of interactions via ownership transfer [3,13,22]. Our results can be viewed as generalising data refinement to the concurrent setting. Moreover, when specialised to the sequential case, they provide a more flexible method of performing it in the presence of the heap and ownership transfer than previously proposed ones. In more detail, the way we define client safety (Section 5) is more general some of the ways used in data refinement [13]. There, it is typical to fix a (precise) invariant of a library and check that the client does not access the area of memory fenced off by the invariant. Here we do not require an explicit library invariant, using the client-local semantics instead: since primitive commands fault when accessing non-existent memory cells, the safety of the client in this semantics ensures that it does not access the internals of the library. We note that the approach requiring an invariant for library-local data structures does not generalise to the concurrent setting: while a precise invariant for the data structures shared among threads executing library code is not usually difficult to find, the state of data structures local to the threads depends on their program counters. Thus, an invariant insensitive to program positions inside the library code often does not exist. Such difficulties are one of reasons for using client-and library-local semantics in this paper.
Finally, we note that the applicability of our results is not limited to proving existing programs correct: they can also be used in the context of formal program development. In this case, instead of abstracting an existing library to an atomic specification while proving a complete program, the Abstraction Theorem allows refining an atomic library specification to a concrete concurrent implementation while developing a program topdown [2,21]. Our work thus advances the method of atomicity refinement to a setting with concurrent components sharing an address space and communicating via ownership transfers.