PaperlayerView exact revision on arXiv

Source-linked AI summary

A General Technique for Non-blocking Trees

Trevor Brown, Faith Ellen, Eric Ruppert

arXiv:1712.06687v1cs.DC

TL;DR

Fine-grained non-blocking balanced BSTs have been difficult to prove correct, while coarse-grained transactional approaches limit concurrency. The paper gives a general tree-update template using LLX, SCX, and VLX, and applies it to a chromatic tree whose Java implementation rivals or outperforms leading concurrent dictionaries.

  • Problem

    Existing concurrent balanced BST implementations either relied on coarse-grained transactions that limit concurrency or lacked rigorous correctness proofs.

    Source: §1 · p. 1

  • Method

    The paper provides a template for provably correct non-blocking down-tree updates and demonstrates it with a chromatic tree implementation.

    Source: Our Contributions · p. 2, §7 · p. 17

  • Results

    The chromatic tree implementation rivals or outperforms other data structures across tested workloads and contention levels, with the relaxed AVL implementation’s performance indistinguishable from Chromatic6 after allowing more path violations before rebalancing.

    Source: §6 · pp. 16–17, §7 · p. 17

  • Takeaways & Limitations

    The template supports efficient concurrent implementations of down-tree structures, and a relaxed-balance AVL implementation was produced in less than a week by a first-year undergraduate using the cited materials.

    Source: §7 · p. 17

    The experiments use random operation sequences, which may leave unrebalanced BSTs balanced with high probability and therefore do not evaluate balanced trees’ worst-case sequence guarantees.

    Source: §6 · p. 17

Abstract

from arXiv · show

We describe a general technique for obtaining provably correct, non-blocking implementations of a large class of tree data structures where pointers are directed from parents to children. Updates are permitted to modify any contiguous portion of the tree atomically. Our non-blocking algorithms make use of the LLX, SCX and VLX primitives, which are multi-word generalizations of the standard LL, SC and VL primitives and have been implemented from single-word CAS. To illustrate our technique, we describe how it can be used in a fairly straightforward way to obtain a non-blocking implementation of a chromatic tree, which is a relaxed variant of a red-black tree. The height of the tree at any time is $O(c+ \log n)$, where $n$ is the number of keys and $c$ is the number of updates in progress. We provide an experimental performance analysis which demonstrates that our Java implementation of a chromatic tree rivals, and often significantly outperforms, other leading concurrent dictionaries.

1 Introduction

The paper addresses the difficulty of proving fine-grained, non-blocking balanced search trees correct by proposing a general down-tree update technique. It applies the technique to a chromatic tree and reports strong performance against concurrent dictionaries.

1 Introduction

  • Earlier concurrent balanced BST implementations either used coarse-grained transactions that limit concurrency or lacked rigorous correctness proofs.The paper presents its technique as a way to develop provably correct balanced BSTs with fine-grained synchronization.Source: §1 · p. 1
  • The technique targets localized updates, which modify a small number of nearby nodes and can be freely interleaved in some data structures.Relaxed-balance structures such as chromatic trees split insertion or deletion and rebalancing into localized updates.Source: §1 · p. 1

Our Contributions

  • The template makes updates to down-tree data structures atomic, linearizable, and non-blocking while handling process coordination, so designers can reason about updates as atomic steps.It supports updates that modify any connected subgraph.Source: Our Contributions · pp. 1–2
  • The chromatic tree is a provably correct, non-blocking balanced BST with fine-grained synchronization and height O(c + log n), where c is in-progress insertions and deletions.It is a relaxed-balanced version of a red-black tree.Source: Our Contributions · p. 2
  • The implementation also supports queries that ignore concurrent updates, including ordinary BST search, and describes successor queries that interact properly with template updates.The paper notes that ignoring updates makes searches very fast.Source: Our Contributions · p. 2
  • With 128 threads, the chromatic tree outperforms Java’s non-blocking skiplist by 13% to 156%, a lock-based AVL tree by 63% to 224%, and an STM red-black tree by 13 to 134 times.The comparisons span a variety of workloads, contention levels, and thread counts.Source: Our Contributions · p. 2

2 Related Work

Prior non-blocking tree work includes unbalanced BSTs, balanced trees with limited concurrency, and fine-grained structures whose correctness arguments were incomplete or complex. Relaxed-balance trees offer localized updates that can be interleaved, and the paper applies its template to chromatic and relaxed AVL trees.

2 Related Work

  • Several non-blocking BST, k-ary tree, and Patricia-trie implementations were not balanced, allowing height Θ(n) for n keys.Their approaches included cooperative techniques and edge marking.Source: §2 · p. 2
  • A prior wait-free tree technique required every operation, including read-only searches, to copy a root-to-node path and change the root pointer.It also required an extra level of indirection for each child pointer.Source: §2 · p. 2
  • Prior wait-free red-black-tree approaches retained limited update concurrency, while STM implementations used large transactions and provided only obstruction-freedom.The wait-free approach could allow searches to read paths, but updates still had to copy paths.Source: §2 · p. 2
  • Fine-grained non-blocking balanced-tree proposals had difficult correctness support: one offered only a brief justification, while another had a long, complex proof.The cited examples were a B-tree/skip-list hybrid and a B+tree.Source: §2 · p. 2
  • Chromatic trees split insertion, deletion, and rebalancing into interleavable localized updates; an amortized constant number of rebalancing steps per operation suffices to restore balance.The paper also implemented a relaxed AVL tree, for which an amortized logarithmic number of rebalancing steps per operation suffices.Source: §2 · p. 3
  • Other relaxed AVL designs require different rebalancing budgets, including an amortized linear number of steps per insertion or deletion in the node-oriented tree of Bougé et al.Existing implementations described here used locking or STM; a non-blocking implementation of Bougé’s tree had not appeared.Source: §2 · p. 3

3 LLX, SCX and VLX Primitives

LLX, SCX, and VLX extend LL, SC, and VL to operate on multi-field records and can be implemented from single-word CAS. The template uses these primitives to coordinate updates and support correctness and progress arguments.

3 LLX, SCX and VLX Primitives

  • LLX, SCX, and VLX generalize LL, SC, and VL and are implemented from single-word CAS, encapsulating much of the template’s proof complexity.Their design balances ease of use with efficient implementation.Source: §3 · pp. 3–4
  • LLX attempts to snapshot a record’s mutable fields; SCX atomically changes one field and finalizes records in its removal set, while VLX validates a set of records.A finalized record’s mutable fields cannot be changed by later SCXs, and LLX returns Finalized rather than a snapshot.Source: §3 · p. 3
  • Before SCX or VLX, a process must LLX every record in its sequence; the operation succeeds only if those records remain unchanged since the linked snapshots.VLX can obtain a snapshot of a set of records; primitive failures are limited in ways used to build non-blocking structures.Source: §3 · p. 3
  • The implementation relies on constraints that avoid ABA and order SCX sequences consistently after changes stop; the tree update template satisfies these constraints naturally.The cited implementation guarantees a linearization of modifying SCXs and successful LLX and VLX operations under the constraints.Source: §3 · p. 4
  • The tree has a permanent entry record, and the template finalizes a record if and only if an SCX removes it.The LLX/SCX implementation then provides properties about snapshots, newly linked records, and records reached by following pointers.Source: §3 · p. 4
  • Each node adds a descriptor pointer and a bit, and a completed update’s descriptor can use three machine words; the described implementation assumes garbage collection.The passage notes that this assumption can be eliminated using a memory-reclamation scheme.Source: §3 · p. 4

4 Tree Update Template

The tree update template replaces a connected subgraph through one atomic child-pointer update, using LLX to inspect records and SCX to validate and commit. Its postconditions support correctness and progress proofs for implementations that follow the template.

4 Tree Update Template

  • A successful update atomically replaces a connected old subgraph with a new one by changing a single child pointer; removed nodes are finalized and new nodes are added.The replaced portion may implement changes such as BST insertion or red-black-tree rotation.Source: §4 · pp. 4–6
  • Nodes use mutable child pointers and immutable other fields; changing immutable data requires creating a new copy of the node.The template’s SCX-Arguments and Result functions are computed from locally available information.Source: §4 · pp. 5–6
  • The update reads a path and performs LLXs on a sequence of nodes, then invokes SCX to change the child pointer and finalize removed nodes.LLX failure or finalization aborts the attempted update; Figure 1 depicts removed nodes R, new nodes N, and fringe nodes FN.Source: §4 · pp. 5–6, Figure 1 · p. 5
  • SCX-Arguments must select sequences and fields satisfying the postconditions, so an SCX fails if relevant records changed since their LLXs.The new connected tree is rooted at new; postconditions constrain removed nodes, fringe nodes, and newly allocated nodes.Source: §4 · pp. 6–7
  • PC8 orders V sequences consistently with a fixed traversal during periods without structural SCXs; PC9 requires the removed-subgraph fringe to match the new-subgraph fringe.These conditions let the update preserve fringe nodes while replacing the selected connected portion.Source: §4 · p. 7

4.1 Correctness and Progress

  • The correctness proof shows that successful SCXs replace connected subgraphs, remove and finalize R, add N, and never reinsert removed nodes.It also establishes that template updates satisfy primitive preconditions and preserve the tree structure.Source: §4.1 · p. 7
  • Some queries can use reads alone: the cited properties support linearizable queries, and Get is implemented by ordinary BST search to a leaf.The figure distinguishes empty and non-empty tree states.Source: §4.1 · pp. 7–8, Figure 4 · p. 8
  • Each template update is wait-free, and if updates are performed infinitely often, successful updates occur infinitely often.The proof establishes that each process can receive Finalized from LLX on a given record at most once, supporting this progress result.Source: §4.1 · p. 8

5 Application: Chromatic Trees

The application uses a chromatic tree—a relaxed red-black tree whose localized updates can be interleaved—to implement an ordered dictionary. It combines search and update procedures with violation cleanup, whose rules support a height bound and non-blocking progress.

5 Application: Chromatic Trees

  • Chromatic trees replace red-black colors with integer weights, permitting red-red and overweight violations while preserving equal weight sums on root-to-leaf paths.The chosen rebalancing steps do not increase violations, can be applied in any order, and eventually restore a red-black tree; their amortized count is at most three per insertion and one per deletion.Source: §5 · p. 9

5.1 Implementation

  • Get, Insert, and Delete search to a leaf; updates make a localized change and invoke Cleanup when they create a violation.Search reads child pointers and returns the leaf, parent, and grandparent; Get returns the value only when the leaf key matches.Source: §5.1 · p. 9

5.2 The rebalancing algorithm

  • Cleanup searches for the key and applies localized rebalancing while a violation remains on its search path, avoiding auxiliary violation queues.The VIOL rule ensures a rebalancing step either eliminates a violation or leaves it on the relevant search path; a concurrent search therefore does not miss it.Source: §5.2 · pp. 13–14

5.3 Proving a bound on the height of the tree

  • The tree has height O(c + log n), where c is the number of insertions and deletions in progress.The number of violations is bounded by c; eliminating each violation reduces height by at most one, and a tree without violations has red-black-tree height.Source: §5.3 · p. 14

5.4 Correctness and Progress

  • Get can be linearized at a time its reached leaf was on the search path, and the implementation is non-blocking under the rebalancing-step bound.Updates that modify the tree linearize at their SCX; at most 3i + d rebalancing steps follow i insertions and d deletions.Source: §5.4 · p. 14

5.5 Successor queries

  • Successor uses LLX to read search paths and VLX to validate the path between candidate leaves before returning the next key.If an LLX or VLX fails, Successor restarts; a successful VLX supplies the query's linearization point.Source: §5.5 · p. 14

5.6 Allowing more violations

  • Deferring Cleanup until a search path has more than k violations reduces rebalancing steps, with height O(k + c + log n).The paper notes that slightly higher search costs can benefit update-heavy workloads; Figure 8 plots throughput against thread count on a 2-socket SPARC T2+ with 128 hardware threads.Source: §5.6 · p. 15, Figure 8 · p. 15

6 Experimental Results

The experiments compare Chromatic and Chromatic6 with concurrent ordered dictionaries across operation mixes, key ranges, and thread counts. Chromatic6 generally rivals or outperforms competitors, though the tests use random operation sequences.

6 Experimental Results

  • The tests cover 0i-0d, 20i-10d, and 50i-50d operation mixes across key ranges [0, 10^2), [0, 10^4), and [0, 10^6), varying contention.Each configuration used five trials measuring aggregate throughput for five seconds, after an untimed prefilling phase.Source: §6 · p. 16
  • Chromatic6 rivals or outperforms competing data structures across the reported graphs, with only limited exceptions under high contention.At high contention it trails SkipList for 50i-50d and AVL-D for 0i-0d; under moderate contention it significantly outperforms competitors in 50i-50d and 20i-10d.Source: §6 · pp. 16–17
  • Chromatic6 nearly always outperforms Chromatic, except that Chromatic is slightly better for all-query workloads.Chromatic6 has slightly greater average leaf depth because it is prefilled with its own insertion and deletion algorithms.Source: §6 · p. 16
  • Figure 9 compares single-threaded throughput with Java’s sequential RBT for key range [0, 10^6), demonstrating relatively small overhead from the technique.The caption identifies the measure and baseline but does not provide specific throughput values.Source: Figure 9 · p. 17, §6 · p. 17
  • The experiments use random sequences, which can leave unrebalanced BSTs balanced with high probability and give them lower overhead.The authors call for better experiments to evaluate balanced BSTs.Source: §6 · p. 17

7 Conclusion

The paper presents a template for non-blocking down-tree data structures and demonstrates it with a chromatic tree. It also reports that a relaxed-balance AVL implementation was produced quickly and reached Chromatic6-level performance after allowing more violations.

7 Conclusion

  • The template yields non-blocking implementations for down-tree data structures, and the paper demonstrates it with a chromatic tree.The authors state that their chromatic tree is the first provably correct, non-blocking balanced BST with fine-grained synchronization, to their knowledge.Source: §7 · p. 17
  • A first-year undergraduate produced a Java relaxed-balance AVL implementation in less than a week using and this paper.Its performance was slightly below Chromatic, but became indistinguishable from Chromatic6 after allowing more violations on a path before rebalancing.Source: §7 · p. 17
  • The authors hope the work encourages development of more relaxed-balance sequential data structures, whose concurrent implementations can use the template.Source: §7 · p. 17

A Primitives

LLX, SCX, and VLX coordinate reads, updates, and validation on data records. Their stated properties specify the values operations observe and conditions under which operations make progress.

A Primitives

  • VLX(V) returns true only if no SCX has modified any record in V since the process’s last LLX.Source: A Primitives · p. 20
  • Before SCX or VLX, a process must perform a linked LLX on every record in its sequence V.A linked LLX returns neither Fail nor Finalized, and no intervening LLX, SCX, or VLX by that process may involve the record.Source: A Primitives · p. 20
  • The specification linearizes successful LLXs, SCXs, VLXs, and reads so reads and LLXs return the latest values stored by preceding SCXs.An LLX returns Finalized exactly when linearized after an SCX that finalized its record.Source: A Primitives · p. 20
  • A terminating LLX begun after a successful SCX that finalized its record, or after an LLX returned Finalized, returns Finalized.Source: A Primitives · p. 20
  • If operations continue indefinitely, operations succeed infinitely often; SCX and VLX each have the stated progress guarantees when invoked infinitely often.Infinitely many SCX invocations specifically imply infinitely many successful SCXs.Source: A Primitives · p. 20

B Proof for Tree Update Template

The proof establishes that tree-update SCX operations satisfy their required conditions and preserve the tree’s structure, then derives linearizability and progress guarantees. Its results depend on stated constraints, including that every SCX is performed by a tree-update operation.

B.1 Additional properties of LLX/SCX/VLX

  • LLX snapshots and linearized SCX insertions establish record membership, while the path lemma relates observed pointers to configurations in the execution.The path lemma also gives a configuration in which the final record’s mutable field contains an observed value.Source: §B.1 · p. 21

B.2 Correctness of the tree update template

  • The proof’s tree-update results apply under Constraint 7: every SCX invocation must be performed by a tree-update operation.The proof also invokes Constraint 3 and the tree-update template’s other conditions when deriving its invariants.Source: §B.2 · p. 21
  • The proof reasons about LLX, SCX, and VLX through their relative linearization order, without requiring knowledge of a particular implementation’s linearization points.A non-terminating SCX invocation can still modify the data structure and is linearized when it does.Source: §B.2 · p. 21
  • Every linearized SCX replaces a connected subgraph with another, adds exactly the records in N, removes exactly those in R, and preserves a tree rooted at root.The proof establishes this invariant by induction on execution steps.Source: §B.2 · pp. 21, 23
  • Tree-update SCX invocations satisfy the primitive’s preconditions, including linked LLXs and the required conditions on the replaced subgraph.The proof verifies the SCX preconditions and uses the tree-update constraints to establish the required graph properties.Source: §B.2 · pp. 21–22
  • The concurrent tree and the atomic execution of tree updates have the same state at every time, and each update returns its atomic-execution value.The theorem linearizes each successful tree update at its linearized SCX invocation.Source: §B.2 · pp. 23–24
  • A removed data-record cannot be added back, because every added record is newly created and absent before its SCX linearizes.This non-reinsertion property supports the proof that a process performs at most one LLX of a given record returning Finalized during tree-update operations.Source: §B.2 · pp. 24–25
  • Tree-update operations are wait-free, and infinitely many such operations imply infinitely many successes.The wait-free result relies on wait-free LLX and SCX implementations, finite local computations, and Condition eventually returning True; the success result uses the stated constraints.Source: §B.2 · pp. 24–25

C.1 Pseudocode

Dictionary updates search for a location, perform a tree-template pointer update, and then clean up any resulting violation. Cleanup uses rebalancing transformations, while successor queries validate the path between leaves.

C.1 Pseudocode

  • Insert and Delete search for an update location, use TryInsert or TryDelete to swing a pointer, and invoke Cleanup when needed.Insert1 adds an absent key, Insert2 replaces the leaf for an existing key’s value, and Delete removes a key.Source: §C.1 · pp. 25–26
  • Figure 10 contrasts the initial tree with a non-empty tree and places the node weights on the right.Sentinel nodes use weight one.Source: Figure 10 · p. 25, §C.1 · p. 25
  • Cleanup searches from the root toward a leaf, fixing encountered violations with a rebalancing step selected by a weight-based decision tree.The rebalancing transformations are slight modifications of those in, with symmetric mirror-image versions except for BLK.Source: §C.1 · p. 26
  • Successor searches for a leaf and, when needed, finds its in-order successor, then uses VLX to verify the connecting path has not changed.Predecessor can be implemented similarly.Source: §C.1 · p. 26

C.2 Correctness of chromatic trees

The correctness argument shows that chromatic-tree updates preserve the required tree structure and establishes search-path properties for reasoning about searches during concurrent rebalancing. It proves that Get, Insert, Delete, and Successor form a linearizable ordered dictionary, using a BST invariant and linearization points within each terminating operation.

C.2 Correctness of chromatic trees

  • Insert and delete follow the tree-update template, while rebalance either follows it or returns early without performing an SCX.This allows the authors to apply the template’s results to show that SCXs perform the Figure 11 transformations atomically.Source: §C.2 · p. 26
  • The tree rooted at root always has the required empty or nonempty shape, and the algorithms do not access fields of Nil nodes.The proof uses the update-template property to show that SCXs preserve the root shape and that LLX calls receive non-Nil nodes.Source: §C.2 · p. 33
  • A node that remains in the data structure and was on key k’s search path stays on that path as the tree changes.The proof checks that each possible tree modification preserves the relevant path through the SCX fringe set; the lemmas follow an approach similar to.Source: §C.2 · p. 34
  • If a root-based BST search for k reaches a node, that node was on k’s search path in an earlier configuration during the search.This property addresses searches that visit nodes no longer in the tree while concurrent updates occur.Source: §C.2 · p. 34
  • The tree rooted at the left child of root remains a BST because successful SCXs preserve the invariant across root changes, rebalancing, deletes, and inserts.For Insert1, the insertion point remains on the search path when its child pointer changes.Source: §C.2 · pp. 34–35
  • Each terminating operation has an in-operation linearization point: updates use successful SCXs, while Get and some Successor cases use search-path times, LLX, or VLX.Get and unsuccessful Delete use times when the reached leaf was on the key’s search path; Successor also has cases linearized at LLX or successful VLX.Source: §C.2 · p. 35
  • The chromatic search tree is a linearizable implementation of an ordered dictionary supporting Get, Insert, Delete, and Successor.The proof shows that rebalancing preserves the stored key-value set and that linearized inserts and deletes maintain the dictionary’s contents.Source: §C.2 · p. 35
  • Get returns the value at the reached leaf when it contains the key and returns ⊥ otherwise; the described Successor cases return the correct successor.The Successor proof covers an empty tree, a leaf found on the search path, and a successor validated by VLX.Source: §C.2 · p. 35

C.3 Progress

The proof establishes that chromatic-tree operations are non-blocking by ruling out an execution in which processes keep taking steps but no operation completes. It handles query-only and update-including executions separately.

C.3 Progress

  • If TryRebalance is invoked infinitely often, it follows the tree update template infinitely often.An invocation returning at either of the specified lines must overlap a tree-changing update; otherwise the tree would violate its chromatic invariant.Source: §C.3 · p. 36
  • Theorem 22 establishes non-blocking operations by ruling out an execution where processes keep taking steps but none complete.The proof divides this case into executions with queries only and executions that include Insert or Delete.Source: §C.3 · p. 36
  • When only queries continue, the absence of SCXs eventually lets all LLXs and VLXs succeed, so the queries terminate.Source: §C.3 · p. 36
  • When updates continue, infinitely many template-following calls succeed, forcing infinitely many rebalancing steps; bounds these steps until no further rebalancing applies.Source: §C.3 · p. 36

C.4 Bounding the chromatic tree’s height

The chromatic tree’s height is O(log n + c), where n is the number of keys and c is the number of incomplete Insert and Delete operations. The bound follows by limiting violations to pending updates and relating tree height to the height of a red-black tree obtained by rebalancing.

C.4 Bounding the chromatic tree’s height

  • An injective mapping assigns each violation to a process in a cleanup phase whose key’s search path contains that violation.The invariant also requires that each assigned process satisfy one of the stated conditions on its location, parent, or search path.Source: §C.4 · p. 37
  • The number of violations is bounded by the number of incomplete Insert and Delete operations.Each such operation can create one violation and does not terminate until the violation it created is destroyed.Source: §C.4 · pp. 36, 40
  • The proof relates chromatic-tree height to weighted height and then to the height of a red-black tree produced by eliminating violations.The stated bounds are h(root) ≤ 2wh(root) + c, wh(root) ≤ wh(rootT) + c, and wh(rootT) ≤ h(rootT).Source: §C.4 · pp. 40–41
  • O(log n + c) bounds the tree height for n keys and c incomplete Insert and Delete operations.The bound includes the two dummy nodes at the top of the tree.Source: §C.4 · p. 41
Loading 1712.06687v1…