Che Tong
email: tong.che@epfl.ch

Construction 2015 Linearizability

Hal

Tong Che

Linearizability By Construction

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Highly concurrent shared objects are extremely hard to design and prove correct. On one hand, the vast number of interference possibilities makes formal proof impractical and makes human proof error-prone. On the other hand, people who design data structures usually use their intuition to avoid mistakes, they usually have an intuition of some invariants that capture part of the algorithm, but such intuition is sometimes hard to be transformed into a rigorous proof.

It is a general belief that "well specified program does not go wrong". In concurrent programming, ensuring correctness by careful specification can be difficult, because programmers have to specify not only the behavior of the current thread, but also the behavior of other threads (the environment) which it relies on. This is usually called rely-guarantee reasoning [START_REF] Jones | Specification and design of (parallel) programs[END_REF]. With this method we can specify and verify many concurrent algorithms, but just writing correct specifications is a big challenge, not to mention the implementation.

In this paper, we argue that highly concurrent algorithms can be easy to design and prove. We present a way to combine these, namely, to combine the design, specification and rigorous proof of an algorithm into a single procedure. For an important class of concurrent algorithms, after the algorithms are designed, their correctness are, to a large extent, indicated by their construction and specifications.

The class of shared objects that we consider, is highly concurrent optimistic implementation of data structures, such as linked lists, search trees, skip lists and graphs. These implementations may contain atomic sections which can be implemented using locks, but such sections usually only access a small number of memory locations. The most important property of these implementations is that their search operation is sequential, i.e., is without any retry, locks or synchronization. Such implementations usually perform very well in practice, because most operations are search operations (even to remove or add an element, you need to first search for the location where the operation should take place), but they are usually very hard to be proved correct, because of the huge number of possible executions.

Traditionally, the designers implement highly concurrent shared objects in an ad-hoc manner. They start from a sequential specification, think of different interleaving of executions, especially cases that might go wrong, and use their experiences, established mechanisms and techniques to eliminate these wrong cases. And finally they try to rigorously prove the algorithm. In this manner, it is usually impractical to expect that the proof can be purely thread local, because the designer himself may not have thread local proof in mind, and this may result in algorithms which is extremely hard to prove correct or even wrong.

We take a different route. First, we establish several requirements of the algorithm. Especially, we ask the search operation of the data structure to be sequential, and then, we determine what kind of properties that the other operations have to preserve, to make these search operations correct, i.e. linearizable. We use rigorous mathematical argument, to identify a set of thread local invariants which are reasonable and necessary for the search operation to be correct. Then, we carefully design the other operations preserving these invariants and using small atomic sections. Finally we refine the algorithm to achieve more concurrency using mechanisms such as locks, synchronization primitives, etc. Sometimes the resulting algorithms can even be made lock-free. Every step can be supported by state-off-the-art tools, such as interactive theorem provers, to guarantee correctness. So, after the algorithm is written down, the proof itself is completed.

Our basic tools are generalized versions of the Hindsight lemma [START_REF] Peter | Verifying linearizability with hindsight[END_REF] and a new Data-Expansion lemma. The Hindsight lemma plays an essential rule in the verification of the lazy list based set 1 algorithm, but we show that our generalized version applies to a large class of linked data structures, made it possible to verify correctness of them, and we will show how to use it in designing new objects. Our temporal data expansion lemma is a new lemma which guarantees that "failed" search operations are correct. Briefly, it says our search operation can never "miss" existing nodes on the data structure due to interference. For linked lists the lemma is almost trivial, but for trees this is not this case. Its proof depend on several important thread local information, and is the most surprising and technical part in this paper. We also show that the conclusion indicated by two lemmas is "necessary" for the sequential search operation to perform correctly in some sense.

To summerize, the main contribution of this paper is the following: 1. It presents a novel highly concurrent binary search tree algorithm, and a surprising simple thread modular proof, which is, to a large extent, depend on only a few natural thread local invariants, and can be applied to other algorithms.

2. It presents a systemic study of linked objects with sequential search operation, and a new methodology to design them.

3. It greatly generalizes the Hindsight lemma, and proposes a new data-expansion lemma, which are proved to hold on linked lists and search trees. These lemmas only based on several natural local invariants, and we believe they are important in constructing simple proofs of linearizability of operations with non-fixed linearization points.

Related Work

Our work is based on the paper on Hindsight lemma [START_REF] Peter | Verifying linearizability with hindsight[END_REF]. We go one significant step further for providing a new binary search tree algorithm, and a first purely thread modular proof for tree algorithms. In fact, most tree algorithms are extremely complicated and are hard to prove correct or verified rigorously. We only aware of one highly concurrent tree algorithm [START_REF] Ellen | Non-blocking binary search trees[END_REF] which was proved correct rigorously. The search tree is external, and the search operation in their algorithm is also "sequential", just like ours. In fact, following our methodology, we can also devise a similar implementation of external search tree, and have a purely thread modular proof. But using an internal-external tree can save not only memory space, but also search time. When the key universe is small, the performance gain would be much clearer. This is also an example showing why our methodology can be used elsewhere.

In [START_REF] Peter | Verifying linearizability with hindsight[END_REF], two lemmas, the Hindsight lemma and the Local Window Lemma, play essential rules. The hindsight lemma can be generalized to other data structures as we will show, and the local window lemma is not applicable on structures like trees.

The first algorithm can be adopted in our design and verification framework is Heller's lazy list [START_REF] Heller | A lazy concurrent list-based set algorithm[END_REF]. The concurrent skip list [START_REF] Herlihy | A provably correct scalable concurrent skip list[END_REF] is also an example which can be adapted to our framework. Note that most of our verification technique is algorithm-independent, if we can adapt one data structure implementation to this framework, we actually adapted a class of implementations of that data structure. Namely, our concurrent linked data structure contains a single node as entry node, and every node contain a list of pointers to neighbor nodes. If a client want to access some nodes, it has to follow a heap path(a sequence of pointers) from Root. Without any shape/data invariants, our data strucuture can be an arbitary graph with a single marked node storing any data any where. By imposing different shape invariants, this data structure can be linked lists, binary trees, skip lists, etc.

Executions, states, and transitions. Program states are combinations of local stores and a shared heap. The ith local store s i is a map from the local variables of thread i to values. A shared heap h is a finite map from memory locations L to values, which can be accessed by all threads. A memory state can be written as σ = (s, h). In our specific setting, h = h a ∪ h b , where h a is the set of memory locations can be accessed by following heap links starting from Root, h b is the locations which cannot be accessed from Root. Memory locations in h b may be garbage collected after some time, but we don't assume any garbage collection in this paper. We further assume that when we talk about state transitions, we only consider share state, that is, a shared heap, and an immutable Root pointer. Unless otherwise noted, when we talk about an execution trace σ 0 , σ 1 , • • • , σ n , we in fact view σ i as heap states, because thread local transitions will not change the content of our data structure.

For a state σ, a link u → σ v is a pair of nodes such that for some i, u.succ[i] = v in state σ. A node/link is called a backbone node/link in state σ, if and only if in state σ, there is a link path from Root to the node/link.

For any thread t, we define a computation step s of t as a transition κ from state σ to σ , we write s = σ → t κ σ , and denote src(s) = σ, trg(s) = σ . A computation step is either an invocation of an operation, a return from an operation, or an atomic action in an operation. We call it a heap computation step if it modifies the heap.

An execution Π is an alternating sequence of states and computation steps σ 0 , s 0 , σ 1 , s 1 , • • • , where σ i = src(s i ) and σ i+1 = trg(s i ). We define an execution trace of the execution by omiting all the computation steps, namely σ 0 , σ 1 , • • • . An execution trace π can be simplified if we consider only heap computation steps, these simplified execution traces are called heap execution traces, they are simplification of corresponding full execution traces.

We define an abstract linked data type T as a tuple T = (I T , L T , O T ), in which L T is a set of all the set of all legal data structure of type T satisfying all the shape and data invariants (can be represented in seperation logic), L T is a subset set of directed graphs, satisfying certain shape and data invariants, O T is a set of operations satisfying sequential specifications. Usually, L T can be viewed as the set all the "static" legal data structure layout when no modification operation is pending.

Example: Consider Heller's lazy concurrent list algorithm [START_REF] Herlihy | A provably correct scalable concurrent skip list[END_REF]. Here I T , L T are just the shape/data invariants and set of all strictly sorted linked list with head and tail nodes , and O T = add(), remove(), search(), with their sequential specifications just as usual implementation of sequential linked lists.

A concurrent object o T of an abstract linked data type T , is a concurrent object with the following properties: When no modification operations are pending, the heap content which is accessible from Root satisfies invariants I T . All its operations are linearizable w.r.t the sequential specifications.

Linearizability. Linearizability [START_REF] Maurice | Linearizability: A correctness condition for concurrent objects[END_REF] is a widely-used correctness property of concurrent objects. Intuitively, it means each operation can be viewed as taking effect at some unique point in time between the invocation and reponse. A full execution trace T is an execution trace take account in both shared and local computation steps. Its corresponding history H(T ) is its maximal subsequence consists of invocation and responses. Note H(T ) is a well formed history. We have: Definition 3. Denote O(T ) the set of operations in H(T ). A partial function p : O(T ) → T is a linearizability point assignment, if o ∈ Dom(p) for each completed operation o, and for any two operations t 1 , t 2 with the response of t 1 is before the invocation of t 2 , we have p(t 1 ) is before p(t 2 ), and p(t) happens between invocation and reponse of operation t. Reorder the operations to sequential order according to the order of p(t), the resulting history complies the sequential specification. Then for operation t, p(t) is called its linearizability point.

A Methodology for Designing Concurrent Objects 4.1 Design Principles

Sequential specification We study basically dictionary-like concurrent objects. They usually have three basic operations, contains(), add(), remove(). The sigature of these three operations is listed below:

Boolean contains ( KeyType key ); Boolean add ( KeyType key ); Boolean remove ( KeyType key );

The sequential specification of the algorithm can be viewed as a set of operations which operates on an abstract set S of keys.

We want to implement this object using shared memory linked data structures. The keys are stored in linked nodes, which connect to neighboring nodes by pointers.

S = A contains(k) S = A ∧ ret = k ∈ A S = A add(k) S = A ∪ {k} ∧ ret = k / ∈ A S = A remove(k) S = A -{k} ∧ ret = k ∈ A
We are interested in a special kind of linked concurrent data structure. In this kind of structure, all the three operations are implemented using a special operation, called search(). Search operation takes a key as input, and it looks up the key in the data structure, then return a few pointers near either the pointers to the node with the key or some nodes where the key with the new node with the key ought to be inserted. Our fundamental design principle is the following:

Search-And-Perform Methodology: To perform an add, contains or remove operation, first reach the place where the operation should take place highly concurrently, and try to perform it atomically.

The idea why this principle can potentially produce high performance objects is that usually, when performing an operation such as add() or remove(), only a small portion of memory locations need to be accessed. And in this way, the successful operations are automatically linearized, at the point they take effect. This is not true for, for example, an internal binary search tree, but true for linked lists, external binary search trees, and skip lists. A good such example is Heller's linked list algorithm [START_REF] Heller | A lazy concurrent list-based set algorithm[END_REF].

In this paper, we assume the search operation is of "highest" concurrency, it does not use any synchronization primitives and does not retry. It just perform a search of the data structure just like sequential way. This kind of data structure is usually very efficient, because usually there are a lot of search operation than modification operations, if we use synchronization primitives such as locks, then many search operations may be blocked by a modification operation, which hurts performance.

Sequential search puts strict restrictions on the data structure itself. They can be stated as 4 principles:

State consistent principle: Every visible state(between execution of atomic sections), the visible heap should be a consistent instance of the data structure.

Locality Principle: Operations should be performed locally and atomically, only accesses a small amount of memory locations.

Successful Search Principle: If a node with key k is visited by some search operation, the node was on the abstract set in some past state between the invocation and response of the search operation.

Failed Search Principle: If a search operation search for key k, and it failed, then there is a past state between invocation and response such that k is not in the abstract set.

The first principle is needed if we want the search operation always sees a valid state. Second principle is a requirement to achieve high concurrency. The last two principles are needed for the search operation to be correct and linearizable.

Generalized Hindsight-like Lemmas

One of our key observation is that, for a large number of search data structures, state consistent principle and the locality principle imply the successful and failed search principles. Now we prove an rather general result to support this observation, it is the most general version of hindsight lemma. We use the symbols and notations mentioned in the last chapter. In particular, consider the linked data type of directed graphs with one entry node T g = (I T , L T , O T , Root), where O T is the three operations of dictionary objects, I T is empty set, and L T is the set of all directed graphs. We assume according to the locality principle that each heap computation step s either insert a node to accessible heap h 0 , or remove a node from it. Also, we further assume that when and after the node is removed, it cannot become backbone again, its successor pointers in the field succ remains the same. We call this assumption "Removed Unchanged Assumption (RUA)", it is natural because we need it to guarantee the remove operation is local and atomic.

Lemma 1. Generalized Hindsight Lemma

For data type T g , assume RUA, Consider an execution trace σ 0 , σ 1 , • • • σ n . For 0 ≤ i ≤ j ≤ n, if there is a backbone link u → σ i v, and a link v → σ j w (u, v, w are different nodes), then there is i ≤ k ≤ j, such that v → σ k w is a backbone link.

Proof. If in state σ j , node v is a backbone node, then choose k = j and we are done. If not, then v is not a backbone node in σ j , let l be the largest index such that v is a backbone node in σ l , so l ≥ i. In σ l+1 , it is removed. But the link v → σ j w exists, according to the RUA, v → w exists from state σ l to σ j . But in state σ l , v is a backbone node, so the link v → σ k w is a backbone link.

We see that hindsight lemma exists on not only linked list, but also on a large class of concurrent linked data structures, since it only requires the successor pointers remain unchanged. This help us to prove the graph version temporal backbone lemma. Before that, we first review what is a temporal backbone. In an execution trace σ

0 , σ 1 , • • • σ n , a sequence of consecutive pairs of different nodes (u 0 , u 1 ), (u 1 , u 2 ), • • • (u m-1 , u m ) is called an node path. It is a temporal backbone, if there is a sequence of integers 0 ≤ i 1 ≤ i 2 • • • i m ≤ n, such that (u k-1 , u k ) is a backbone link in state σ i k for each 1 ≤ k ≤ m.
Sometimes, we also call the sequence u 0 , u 1 , • • • u m a temporal backbone going through the subsequence

T s = {σ i 1 , • • • σ im }.

Lemma 2. Generalized temporal backbone lemma

For data type T g , assume RUA. Given an execution trace T = (σ 0 , σ 1 , • • • , σ n ) and a node path N = {(u 0 , u 1 ), (u 1 , u 2 ), • • • (u m-1 , u m )}, such that there is a subsequence(may have duplicated terms) of execution trace

T s = {σ i 1 , • • • σ im }, such that (u 0 , u 1 ) is a backbone link in σ i 1 , and (u k-1 , u k ) is a link in σ i k , for all 1 ≤ k ≤ m.
Then there is another subsequence of execution trace

T s = {σ j 1 , • • • σ jm } such that for all 1 ≤ k ≤ m -1, j k-1 ≤ j k ≤ i k ,
and N is a temporal backbone going through T s .

Proof. This lemma simply follows by applying the hindsight lemma m times.

The temporal backbone lemma implies that, since the node path a search operation goes through is a temporal backbone, the successful search principle is automatically satisfied, because all the nodes the search operation visits was on the backbone at some past state.

Data-Expansion Like Lemmas

Hindsight like lemmas are not enough for our methodology. Because we need a mechanism to guarantee the failed search principle. We will discuss a class of lemmas, which is needed for the sequential search operation behave correctly.

Usually, the sequential search operation is based on the following mechanism: In an execution trace of the algorithm σ 0 , • • • σ k , let {u i } n i=1 be the sequence of nodes visited by the search operation. When the search operation arrives at a new node u j , j < n, it reads u j 's key and decide which way to go next. We denote V j the set of possible keys the algorithm would expect to show up in the future.

Example: For a sorted linked list, the set of keys are (1, 2, 5, 7), a search operation arrives at node v 3 with key 5. Then the search operation expects to find nodes with keys in V 3 = {x|x > 5} in the future search.

Data expansion lemmas guarantee that no node with key k in V j can be not on a search path search for k passing through u j . (Or there may be a node with key k on the tree at every state, but the search operation fail to find it).

For some data structures, like linked lists, skip lists, data-expansion lemmas are almost trivial, for example, the local window lemma in [START_REF] Peter | Verifying linearizability with hindsight[END_REF]. We prove one such lemma for binary search trees, and it can be easily generalized to other tree-like data structures, such as k-ary search trees.

Internal-External BST: An Example

This section is about a concrete example, an Internal-External binary search tree.

We choose this example mostly because this is a new data structure and is potentially better than external binary search trees for a small key universe. Briefly, it is a binary search tree with some Internal node as routing nodes. An internal node can be marked, which is used just for routing, or unmarked, which can be used to store real data. A leaf node is used only to store data. When deleting an internal node with two children, it is simply marked, while deleting an internal node with one child or a leaf node, we delete the node itself and restore tree structure. Namely the shape of the tree satisfy the invariant that all marked node have two children. When we say loggically adding/removing a node, it is not removed from the tree, but only with the marked bit set. When we say physically adding/removing a node, the node is physically added and removed from the tree, with the removed bit set. For example, figure 1 is the configuration of a state of the I-E BST, for each node the removed bit is omitted, since its value can be inferred from the position of the node. The corresponding set contains values [START_REF] Peter | Verifying linearizability with hindsight[END_REF]7,10,11). Figure 1: An example configuration of I-E BST so it cannot be in A i+1 , so A i+1 ⊆ A i . Since the static bound is determined by the the set A i , and the key of u remain the same, so the static bound of u is non-decreasing.

After a node is removed, the search operation steped on the node should be able to continue its work. It should find the node still on the backbone. So we can put the following natural assumption:

Removed Unchanged Assumption(RUA): The successor pointers of a node remain unchanged when and after the node is removed.

A search path is sequence of nodes that are visited in order by a search operation, start from Root, it is all the nodes pointed by the pointer c. Consider a search path v 0 = Root, v 1 , • • • v n . Since the search operation may return at any node, there is some past state such that v i was a backbone node for each i ∈ [1, n]. Then based on these assumptions, we can prove the following tree version hindsight lemma[???]:

Lemma 5. Tree version Hindsight lemma

Assume RUA and SCA. Consider an execution trace σ 0 , σ 1 , • • • σ n . For 0 ≤ i ≤ j ≤ n, if there is a backbone link u → σ i v, and a link v → σ j w, then there is i ≤ k ≤ j, such that v → σ k w is a backbone link.

Proof. Look at the proof of generalized Hindsight lemma.

Lemma 6. Tree version temporal backbone lemma

Assume RUA and SCA. Given an execution trace T = (σ 0 , σ 1 , • • • , σ n ) and a node path N = {(u 0 , u 1 ), (u 1 , u 2 ), • • • (u m-1 , u m )}, such that there is a subsequence(may have duplicated terms) of execution trace

T s = {σ i 1 , • • • σ im }, such that (u 0 , u 1 ) is a backbone link in σ i 1 , and (u k-1 , u k ) is a link in σ i k , for all 1 ≤ k ≤ m.
Then there is another subsequence of execution trace T s = {σ j 1 , • • • σ jm } such that for all 1 ≤ k ≤ m -1, j k-1 ≤ j k ≤ i k , and N is a temporal backbone going through T s .

Proof. This lemma simply follows by applying the hindsight lemma m times.

For the above two lemmas, it is important to note that although we gave a proof for binary search trees, the argument is actually independent from the underlying data structure; They can be easily proved for circular linked lists or k-ary trees. This is another reason of why our method can be generalized.

A basic point is, the search path of a search operation is a temporal backbone. This serves as a reason why the find operation is correct and linearizable. If find operation actually find some node, it has to be on the tree at some past state between the invocation and return of the search operation.

Lemma 7. Assume the RUA,NRA and SCA. Consider an execution trace T = (σ 0 , σ 1 , • • • σ n ). If during this execution trace, there is an invocation to the search operation of a thread t, its search path is

N = u 0 , u 1 , • • • u m . Then there is a subsequence T s = {σ i 1 , • • • σ im }, such that N is a temporal backbone goes through T s .
Proof. The search path starts from Root, the first link it crosses is always a backbone link and all it crosses are links at that state. So obviously it satisfies all the conditions mentioned in the above lemma.

Our main result is the following temporal data expansion lemma. This is the core insight of our design and our proof. To state this lemma, we reconsider our definition of static bound S σ (u) of a backbone node u in a state σ. We want to extend it to also a removed node v. Since a removed node must be on the backbone at some past state, we denote τ the last state that v was on the backbone. The we define S σ (v) = S τ (v). Note this static bound will never change after a node is removed.

A simple lemma unifies the change of static bound of all nodes -removed and backbone. We call it the data expansion lemma.

Lemma 8. Assume the RUA, NRA, and SCA. Given an execution trace σ 0 , σ 1 , • • • σ n , then for each 0 ≤ i ≤ j ≤ n, if node u exists from state σ i , then we have

S σ i (u) ⊆ S σ j (u)
Now we can use it to prove the temporal data expansion lemma. Note now we need some refined analysis, so our execution traces in the next lemma does not only take account transitions of shared heap, but also local transitions. Especially, we call a computation step corresponding to the execution of c = c.rChild or c = c.lChild in the search operation a "crossing step".

Lemma 9. Temporal Data Expansion Lemma

Assume all the above assumptions, suppose a search path v 0 , v 1 , • • • v m is visited by a search operation in an execution trace σ 0 , σ 1 , • • • σ n . For simplicity we assume the search operation invoked at state σ 0 and return at σ n . We denote at state σ i , the search operation is visiting node v τ (i) (namely pointer c = v τ (i) ), then the searching bound s(v τ (i) ) of node v is contained in the static bound S σ i (v τ (i) ). Since the search key k always lies in the searching bound, we have

k ∈ s(v τ (i) ) ⊆ S σ i (v τ (i) )
Proof. We prove this lemma by induction. For i = 0, it is trivial. Now assume the s(v τ (k) ) ⊆ S σ k (v τ (k) ). We consider the computation step σ k , s, σ k+1 . There are 3 cases:

1. s is a crossing step. Then σ k = σ k+1 , and τ (k + 1) = τ (k) + 1. Again there are two cases in this situation. (1) Link L k = (v τ (k) , v τ (k)+1 ) is a backbone link in state σ k . This case is simple: following the link L k adds a same inequality on both static bound and search bound. For example, if L k is a left link, and denote K k the key of v τ (k) , write the set S k = x|x is a key, and x < K k . Then

s(v τ (k)+1 ) = s(v τ (k) ) ∩ S k , and S σ k (v τ (k)+1 ) = S σ k (v τ (k) ) ∩ S k . So we proved the relation still holds for k+1 in this case. (2) Link L k is not a backbone link in σ k . Still we have s(v τ (k)+1 ) = s(v τ (k) )∩S k , S k is additional constraint of node v τ (k)+1
, but the change of the static bound is more complicated. Since L k is on our search path, we know from the temporal backbone lemma that there is a past state such that L k is a backbone link. We denote σ l the last state satisfying this property. If in σ l+1 , both v τ (k) and v τ (k)+1 are removed, then we have

S σ k (v τ (k)+1 ) = S σ l (v τ (k)+1 ) = S σ l (v τ (k) ) ∩ S k = S σ k (v τ (k) ) ∩ S k
Otherwise, if in σ l+1 , only v τ (k) is removed, then

S σ k (v τ (k)+1 ) ⊇ S σ l (v τ (k)+1 ) = S σ l (v τ (k) ) ∩ S k = S σ k (v τ (k) ) ∩ S k
The first ⊇ is due to the data expansion lemma. So we also proved in this case, the relation hold for k + 1. Now we consider, branch 57 of add returnning true. We can easily check the local modification to the tree, changed the abstract value exactly according to its specification. All the nodes represents Abs(σ) and Abs (σ) is still on the tree, and either a node with key k is turned into unmarked, or a new unmarked node is inserted into the tree. Branch 97 of remove returning false is similar.

Limitations

The designing and proof of our algorithm suffer from several restrictions. First, it do need a set of complex theorems to give us intuition of what can be done and what cannot be done. An automatic tool can be used to guarantee the correctness of preserving the state and step invariants, but may be very hard to automatically devise these theorems. Also, we are studying a very specific class of linked data structures, the one which allows a "sequential" search operation. In this class of data structures, modifications must be local, and this prevent many important data structures to be designed this way.

Conclusions

Proving correctness of highly concurrent data structures is a hard task, because of the interference between threads usually flood the proof. On one hand, [START_REF] Peter | Verifying linearizability with hindsight[END_REF] shows that for some kind of linked list based algorithms, Hindsight lemma can be used to guarantee the correctness of the contains() operation. On the other hand, more complicated data structures such as trees usually lack of rigorous proofs, not to mention formal ones. For many complicated algorithms, purely thread modular proofs are hopeless to achieve.

We argue that some data structures can be designed rigorously with thread modular proofs in mind. This is the search-and-perform methodology. Our design pattern and the hindsight lemma and the data expansion lemma can be applied into more linked data structions, such as linked lists, external binary search trees, k-ary external search trees, or skip lists. It can be applied to several more general graph structures too. Although limited on a special class, the resulting data structures are highly concurrent and usually very effiecient, and the proofs are thread modular.

  Definition 1. A history H is an execution trace containing only invocations and responses. A sequential history is a history that for each invocation, follows by a corresponding response. A partial history H t of thread t w.r.t history H is the subsequence of H which is invoked by thread t. A history H is called well-formed when for every thread t, H t is sequential. A sequential specification S p is a set of sequential histories. Definition 2. Suppose H is a well formed history, it is linearizable with sequential history H S , if there is a map τ from operations in H to the same operations in H S that preserves real time order(Namely, if two operations t 1 , t 2 with the response of t 1 is before the invocation of t 2 , then τ (t 1 ) before τ (t 2 ) ), then H is linearizable w.r.t H S . If every execution of an algorithm is a linearizable history w.r.t a sequential history in its sequential specification S p , the algorithm is said to be linearizable w.r.t. S p .

Table 1 :

 1 Specification of Operations Precondition operation Postcondition

Assumptions and Theorems

We first derive several natural thread modular assumptions and requirements that is needed to implement the 3 operations with the methodology described above, and then we prove several important properties from these assumptions. Note that nothing in this section is algorithm specific. All tree algorithms satisfying these assumptions automatically satisfies the lemmas. Some lemmas can also be generalized easily to other data structures, although they may need a different proof.

First, we write its node representation, its search operation, and a find operation act as a user of search. In the sequential case, deleting a leaf node with a marked parent, we may need both its parent and grand parent, so returning three pointers is required. For convinient, we also assume that Root is a special node, with key -∞, and has only a right child.

Then we discuss some of the natural assumptions we would like to assume throughout the paper. Although these assumptions cannot be derived rigorously in some sense, they are all quite natural and simple assumptions, to make our search operation work correct. We clarify several terms here. For a state σ, a right/left link u → R/L σ v is a pair of nodes such that for u.rChild = v or u.lChild in state σ respectively. A link u → σ v is a right or left link. The state σ may be omitted when the link exists in multiple states and can be infered from the context. A backbone link is a link that can be reached by following a finite number of links start from the Root.

Then we try to establish some restrictions of the execution to make such a search operation can Second, it is natural to assume the key of nodes never change. Because changing the key of a backbone node, is equivalent to remove and add the node loggically. But this will take at least two steps, because we implement add and remove as two different operations. Changing the key of a removed node is compeletely unnecessary, because it is already removed.

Non-mutable Assumption(NMA): Key value of a node never changes. Second, at any state, the accessible part of the heap h 0 must be a valid instance of a binary search tree, because if not, a search operation would go wrong if it is the only thread that progresses, since search has no locking primitive, the inconsistency of the data structure is possible break the semantics of search. So we have the following natural assumption:

State Consistency Assumption(SCA): In each visible state, accessible heap h 0 satisfies state invariants above.

We assume a node can have two location states for a given state: if it's on the tree( can be accessed by following a sequence of links from Root), we call it a backbone node, else it's removed from the tree(is not on but was on the tree) ,we call it a removed node. We further assume after a node is removed, it cannot become backbone again. This is a quite natural assumption, since if we want to add a node, we may add a fresh copy instead of using the old one. Also, if a node has two branches and these two branches are not deleted in the next state, the node itself will not be removed, it is marked instead. The following assumption is based on this intuition, that we don't perform the operation that remove a internal node and merge its two branches, it is a "global" operation that would not be highly concurrent.

Node Removal Assumption(NRA): In one computation step σ 0 , s, σ 1 , if in states σ 0 ,nodes u, v 1 , v 2 are backbone nodes, and v 1 , v 2 lies on each left and right branches of u. If v 1 , v 2 remains backbone node in σ 1 , then u is also a backbone node in σ 1 .

On every consistent state σ, there is a natural partial order on the backbone nodes. u < v is equivalent to say that v is on the subtree rooted at u. We have the following order preserving lemma, which serves as an important restriction for lock free search: Lemma 3. (Order Preserving Lemma) We assume the NRA and CFA. For an heap execution trace σ 0 , σ 1 , • • • σ n , u, v are two backbone nodes in both σ 0 and σ n , then u < v in σ 0 if and only if u < v in σ n Proof. First, we know that removed nodes cannot become backbone again. So u, v are backbone nodes in every σ i . Then, we only have to prove the order of u and v are preserved in every computation step.We prove the sufficiency by contradiction, assume u < v in σ i but not in σ i+1 . Start a find operation for v at σ i , and it is the only process that progresses, until it reaches u. Now, another thread come in, and push the state to σ i+1 . v is still on the tree, but the find operation will not find it, because it is not on the subtree rooted at u now. This is a contradition.

Then we prove necessity by contradition, assume u < v in σ i+1 but not in σ i . Then in σ i , the two nodes must be in different branch of a tree rooted at a node u . Start two find operations, each for u and v, in σ i , when they reach node u , another thread take an effectful computation step, push it to state σ n+1 , while u is still a backbone node. Then the two find operation continuous, and they can both find their target. However, both right branch and left branch of node u can reach node v, this is a contradition.

Corollary 1. Any BST algorithm with rebalancing or rotation cannot use a search operation without locks or synchronization.

In the search operation, the pointers p and l are supposed to cross multiple links. We define the state just before the computation step of updating l as a crossing state. In an execution trace of the algorithm σ 0 , • • • σ k , let {u i } n i=1 be the sequence of nodes visited by c( sometimes called a search path). Usually, the search operation is based on the following mechanism: In the sequential case, when l arrives at a new node u j , j < n, it reads u j 's key and decide which way to go next. We denote V j the set of possible keys in the future search up to the arrival on the node u j . In the binary search tree example, V j = [l j , r j ] is an interval in the key universe. V j is determined by the search history, and V i ⊂ V j , for any i > j. We call V j the searching bound at node u j . Also, at each state σ, if u is a backbone node in σ, then there is another interval, I σ,u = [a σ,u , b σ,u ], it is the range of keys which should be in the subtree rooted at u in state σ. We call it the static bound of u in σ.

Now we want to look a bit about add operation. Consider one computation step, σ 0 , s, σ 1 . If a new node is physically presented in σ 1 , we know that s is the linearizability point of an add operation. And, we have the following natural assumption.

Adding Node Assumption(ANA):

Now, these assumption allows us to prove the following important static data expansion lemma, which is essential for the correctness of our algorithm. Note that this lemma is correct on various data structures, such as sorted linked lists and external search trees. Also this is essential Lemma 4. Assume all the above assumputions, we have for an execution trace σ 0 , σ 1 , σ 2 , • • • σ n , if u remain a backbone node in the execution, then the static bound of u is non-decreasing.

Proof. We only have to prove

) according to order preserving lemma, no nodes presented in state σ i but not in A i can be contained in A i+1 , and (2) the new node not presented in A i (if it exists) is a leaf node of σ i+1 , 2. s is a heap step. This is trivial, because for heap step τ (k+1) = τ (k). So the searching bound remain the same, but the static bound will not decrease, thanks to the data expansion lemma.

3. s is neither a heap step nor a crossing step, then both bound remains the same. So using induction, we've proved the lemma for all possible k.

The reason why the above lemmas are actually necessary for a correct implementation of a binary search tree algorithm is very intuitive. Because we want the search operation to be correct. Temporal backbone lemma guarantees that a "successful search" is correct and linearizable-all the node it finds is actually presented in the data structure in some past state, while temporal data expansion lemma guarantees a "failed search" is correct and meet our specification -if a key is not found in the data structure, it did not present in the data structure, and also, the place it returns is where it should be inserted.

These two theorems only need a few thread modular information, and have the potential to be applied to a wide range of search based concurrent data structures, such as k -ary search trees. Before designing a linked data structure, think about these two lemmas are quite helpful. They will give us an intuition of how the search operation behaves and why.

Invariants

In this section, we figure out clearly all the invariants needed to make the theorems proved in last section valid. As discussed in the last section, these invariants are natural and actually needed to make synchronization and retry free search possible.

Lemma 10. Invariants φ Ro , φ loop , δ e , δ Ro , δ sn , δ Re are enough to prove the tree version Hindsight and Backbone lemma.

Proof. Just revisit the proof of tree version Hindsight lemma.

Lemma 11. Invariants φ Ro , φ ∞ , φ loop , φ < , φ 1 , δ K , δ sn and δ Re , δ e , δ Ro are enough to prove the temporal data expansion lemma.

Proof. Just verify the invariants imply all the conditions of the temporal data expansion lemma.

Our algorithm is designed with the following idea in mind. For add() and remove() operation, the thread first invoke the search operation to look for the place where the modification really take place. An effectless operation, can be of 2 types: find operations and remove(k) operations find that k is not currently in the tree. In these two cases, the linearizability point is obviously, in the search operation. So we can prove their correctness before even to figure them out.

Lemma 12. Effectless operations are linearizable with respect to their sequential specifications.

Proof. All effectless operations invokes the search operation as procedure. Assume the search path

According to the temporal backbone lemma, we know that link L m = (v m-1 , v m ) was a backbone link in some past state. We denote σ d the last state the link is a backbone before the search crosses the link. (If it remains a backbone till the search crosses the link, we take the state exactly after the crossing.) We claim that σ d is the right linearizability point. This is easy to see: for a search operation actually "finds" a node with the search key (no matter the node is marked or not), in σ d , that node is on the backbone. If search operation doesn't see a key k in the tree, the node is not in the tree on σ d . We can prove this as follows:

From the temporal data-expansion lemma, we know that k ∈ S σ d (v m ). Namely, if k is presented in the tree, it should be found in the subtree rooted at node v m . However, we have δ sn and δ e , which tell us, if k is presented in that subtree, in σ d+1 and subsequent states, it should still be there, search operation should find it. So we know that node with key k does not exists in state σ d . So we can choose effectless operation in this way.

Implementation

Now come to our implementation phase. In this phase, we must design our procedures carefully preserving the invariants mentioned above. This is an easy task, because we can just put them into small atomic sections: (For simplicity we use xChild to represent right child pointer or left child pointer, and this can be computed from the key under consider.) Lemma 13. The above algorithm is correct with respect to the sequential specification.

Proof. It is easy to verify the invariants using seperation logic. This verification can be done in a purely thread modular way. The rest is to define the linearizability points of each operation. For add operation the linearizability point is the state before the execution of the last "atomic" section. The remove operation is a bit more complicated. If the remove opration returns at line 66, the linearizability point is already explainned in the above lemma. If it returns at line 97, we also define its linearizability point is the state before the exectuion of the last atomic section. For the contains operation, if it returns at line 27, its linearizability point is also defined in the lemma above. If it returns at 28, the linearizability point is the state exactly before the read of l->marked in line 28.

We have already proved the linearizability of branches of operations with linearizability points lies in the search operation. Now we prove those branches with linearizability points not in search operation is linearizable. For simplicity we call them effectful operations, also they don't always take effect. We consider two abstract functions on states, Abs(σ) and Abs (σ). Abs(σ) is the set of keys of all accessible nodes(no matter marked or not) in the tree. Abs (σ) is the set of keys of all unmarked nodes in the tree. First consider the line 28 branch of contains operation. If k ∈ Abs (σ) at its linearizability point σ, it will return true, or it will return false, thanks to invariant φ M , and the definition of Abs , we can see this is true.

Then we consider the branch of add which returns false at 57. It returns false if and only if l->marked==false. So write its linearizability point σ, it is easy to check k ∈ Abs(σ), it is exactly the same as its sequential specification. The branch 97 of remove operation returning false has exactly the same proof.