Search

Concurrent data structures provide fundamental building blocks for concurrent programming. Standard concurrent data structures may be extended by allowing a sequence of operations to be submitted as a batch for later execution. A sequence of such operations can then be executed more efficiently than the standard execution of one operation at a time. In this article, we develop a novel algorithmic extension to the prevalent FIFO queue data structure that exploits such batching scenarios. An implementation in C++ on a multicore demonstrates significant performance improvement of more than an order of magnitude (depending on the batch lengths and the number of threads) compared to previous queue implementations.

The Nearest neighbour search (NNS) is a fundamental problem in many application domains dealing with multidimensional data. In a concurrent setting, where dynamic modifications are allowed, a linearizable implementation of the NNS is highly desirable. This paper introduces the LockFree-kD-tree (LFkD-tree ): a lock-free concurrent kD-tree, which implements an abstract data type (ADT) that provides the operations Add , Remove , Contains , and NNS . Our implementation is linearizable. The operations in the LFkD-tree use single-word read and compare-and-swap ( ) atomic primitives, which are readily supported on available multi-core processors. We experimentally evaluate the LFkD-tree using several benchmarks comprising real-world and synthetic datasets. The experiments show that the presented design is scalable and achieves significant speed-up compared to the implementations of an existing sequential kD-tree and a recently proposed multidimensional indexing structure, PH-tree.

Concurrent key-value stores with range query support are crucial for the scalability and performance of many applications. Existing lock-free data structures of this kind use a fixed synchronization granularity. Using a fixed synchronization granularity in a concurrent key-value store with range query support is problematic as the best performing synchronization granularity depends on a number of factors that are difficult to predict, such as the level of contention and the number of items that are accessed by range queries. We present the first linearizable lock-free key-value store with range query support that dynamically adapts its synchronization granularity. This data structure is called the lock-free contention adapting search tree (LFCA tree). An LFCA tree automatically performs local adaptations of its synchronization granularity based on heuristics that take contention and the performance of range queries into account. We show that the operations of LFCA trees are linearizable, that the lookup operation is wait-free, and that the remaining operations (insert, remove and range query) are lock-free. Our experimental evaluation shows that LFCA trees achieve more than twice the throughput of related lock-free data structures in many scenarios. Furthermore, LFCA trees are able to perform substantially better than data structures with a fixed synchronization granularity over a wide range of scenarios due to their ability to adapt to the scenario at hand.

Verifying the correctness of concurrent software with subtle synchronization is notoriously challenging. We present the Anchor verifier, which is based on a new formalism for specifying synchronization disciplines that describes both (1) what memory accesses are permitted, and (2) how each permitted access commutes with concurrent operations of other threads (to facilitate reduction proofs). Anchor supports the verification of both lock-based blocking and cas-based non-blocking algorithms. Experiments on a variety concurrent data structures and algorithms show that Anchor significantly reduces the burden of concurrent verification.

In the recent past, devising algorithms for concurrent data structures has been driven by the need for scalability. Further, there is an increased traction across the industry towards power efficient concurrent data structure designs. In this context, we introduce a scalable and energy-efficient concurrent binary search tree with fatnodes (namely, FatCBST) , and present algorithms to perform basic operations on it. Unlike a single node with one value, a fatnode consists of a set of values. FatCBST minimizes structural changes while performing update operations on the tree. In addition, fatnodes help to exploit the spatial locality in the cache hierarchy and also reduce the height of the tree. FatCBST allows multiple threads to perform update operations on an existing fatnode simultaneously. Experimental results show that for low contention workloads as well as large set sizes, FatCBST scales well and also provides high performance-per-watt values as compared to the state-of-the-art implementations. For high contention workloads with small set sizes, FatCBST suffers from contention.

Today���s graph-based analytics tasks in domains such as blockchains, social networks, biological networks, and several others demand real-time data updates at high speed. The real-time updates are efficiently ingested if the data structure naturally supports dynamic addition and removal of both edges and vertices. These dynamic updates are best facilitated by concurrency in the underlying data structure. Unfortunately, the existing dynamic graph frameworks broadly refurbish the static processing models using approaches such as versioning and incremental computation. Consequently, they carry their original design traits such as high memory footprint and batch processing that do not honor the real-time changes. At the same time, multi-core processors-a natural setting for concurrent data structures-are now commonplace, and the analytics tasks are moving closer to data sources over lightweight devices. Thus, exploring a fresh design approach for real-time graph analytics is significant. This paper reports a novel concurrent graph data structure that provides breadth-first search, single-source shortest-path, and betweenness centrality with concurrent dynamic updates of both edges and vertices. We evaluate the proposed data structure theoretically - by an amortized analysis - and experimentally via a C++ implementation. The experimental results show that (a) our algorithm outperforms the current state-of-the-art by a throughput speed-up of up to three orders of magnitude in several cases, and (b) it offers up to 80x lighter memory-footprint compared to existing methods. The experiments include several counterparts: Stinger, Ligra and GraphOne. We prove that the presented concurrent algorithms are non-blocking and linearizable., LIPIcs, Vol. 217, 25th International Conference on Principles of Distributed Systems (OPODIS 2021), pages 20:1-20:25

The Industrial Internet of Things (IIoT) plays an important role in the development of smart factories. However, the existing IIoT systems are prone to suffering from single points of failure and unable to provide stable service. Meanwhile, with the increase of node scale and network quantity, the maintenance cost presents to be higher. Such a disadvantage can be effectively compensated by the features such as security, privacy, non-tamperability and distributed deployment supported by the blockchain. In this paper, first, an intelligent manufacturing security model based on blockchain was proposed. Due to the high power consumption and low throughput of the traditional blockchain, IoT devices with limited power consumption can not work independently. Therefore, in this paper, a new Merkle Patricia tree (MPT) was adopted to extend the blockchain structure and provide fast query of node status. Second, since the MPT does not support concurrent operation and the data operation performance deteriorates with high data volume, a lock-free concurrent and cache-based Merkle Patricia tree was proposed (CMPT) to support lock-free concurrent data operation, which can improve the data operation efficiency in multi-core system. The experimental results indicate that, compared with the original MPT, the CMPT proposed in this paper effectively reduced the time complexity of data insertion and data query and improved the speed of block construction and data query.

Modern big data processing platforms employ huge in-memory key-value (KV) maps. Their applications simultaneously drive high-rate data ingestion and large-scale analytics. These two scenarios expect KV-map implementations that scale well with both real-time updates and large atomic scans triggered by range queries. We present KiWi, the first atomic KV-map to efficiently support simultaneous large scans and real-time access. The key to achieving this is treating scans as first class citizens,and organizing the data structure around them. KiWi provides wait-free scans, whereas its put operations are lightweight and lock-free. It optimizes memory management jointly with data structure access.We implement KiWi and compare it to state-of-the-art solutions. Compared to other KV-maps providing atomic scans, KiWi performs either long scans or concurrent puts an order of magnitude faster. Its scans are twice as fast as non-atomic ones implemented via iterators in the Java skiplist.

We present a lock-free algorithm for concurrent manipulation of a binary search tree (BST) in an asynchronous shared memory system that supports search, insert, and delete operations. In addition to read and write instructions, our algorithm uses (single-word) compare-and-swap (CAS) and bit-test-and-set (BTS) read-modify-write (RMW) instructions, both of which are commonly supported by many modern processors including Intel 64 and AMD64. In contrast to most of the existing concurrent algorithms for a binary search tree, our algorithm is edge-based rather than node-based. When compared to other concurrent algorithms for a binary search tree, modify (insert and delete) operations in our algorithm (a) work on a smaller section of the tree, (b) execute fewer RMW instructions, or (c) use fewer dynamically allocated objects. In our experiments, our lock-free algorithm significantly outperformed all other algorithms for a concurrent binary search tree especially when the contention was high. We also describe modifications to our basic lock-free algorithm so that the amortized complexity of any operation in the modified algorithm can be bounded by the sum of the tree height and the point contention to within a constant factor while preserving the other desirable features of our algorithm.

Linked lists and other list-based sets are some of the most ubiquitous data structures in computer science. They are useful in their own right and are frequently used as building blocks in other data structures. A linked list can be “unrolled” to combine multiple keys in each node; this improves storage density and overall performance. This organization also allows an operation to skip over nodes which cannot contain a key of interest. This work introduces a new high-performance concurrent unrolled linked list with a lazy synchronization strategy. Most write operations under this strategy can complete by locking a single node. Experiments show up to 300% improvement over other concurrent list-based sets.

Modern data-driven applications require that databases support fast analytical queries while undergoing rapid updates---often referred to as Hybrid Transactional Analytical Processing (HTAP). Achieving fast queries and updates in a database management system (DBMS) is challenging since optimizations to improve analytical queries can cause overhead for updates. One solution is to use snapshot isolation (SI) for multi-version concurrency control (MVCC) to allow readers to make progress regardless of concurrent writers. In this paper, we propose the Parallel Binary Tree (P-Tree) index structure to achieve SI and MVCC for multicore in-memory HTAP DBMSs. At their core, P-Trees are based on pure (immutable) data structures that use path-copying for updates for fast multi-versioning. They support tree nesting to improve OLAP performance while still allowing for efficient updates. The data structure also enables parallel algorithms for bulk operations on indexes and their underlying tables. We evaluate P-Trees on OLTP and OLAP benchmarks, and compare them with state-of-the-art data structures and DBMSs. Our experiments show that P-Trees outperform many concurrent data structures for the YCSB workload, and is 4--9 x faster than existing DBMSs for analytical queries, while also achieving reasonable throughput for simultaneous transactional updates.

Universal constructions are attractive as they can turn a sequential implementation of any data structure into a concurrent implementation. However, existing universal constructions have limitations, such as imposing high copying overhead, or poor scalability on NUMA systems mainly due to their lack of NUMA-aware design principles. To overcome these limitations, this paper introduces CR, a universal construction that provides highly scalable updates on NUMA systems while offering fast read-side performance. CR achieves NUMA-awareness by utilizing delegation within a NUMA node and a global shared log to maintain the consistency of replicas of data structures across nodes. Using CR does not require expertise in concurrent data structure design. Our evaluation shows that CR has up to 11.2 times better performance compared to a state-of-the-art universal construction CX on our tested sequential data structures. To demonstrate the effectiveness and applicability of CR, we have applied CR to an in-memory database system. The database shows up to 18.1 times better performance compared to the original version.

Safe lock-free memory reclamation is a difficult problem. Existing solutions follow three basic methods (or their combinations): epoch based reclamation, hazard pointers, and optimistic reclamation. Epoch-based methods are fast, but do not guarantee lock-freedom. Hazard pointer solutions are lock-free but typically do not provide high performance. Optimistic methods are lock-free and fast, but previous optimistic methods did not go all the way. While reads were executed optimistically, writes were protected by hazard pointers. In this work we present a new reclamation scheme called version based reclamation (VBR), which provides a full optimistic solution to lock-free memory reclamation, obtaining lock-freedom and high efficiency. Speculative execution is known as a fundamental tool for improving performance in various areas of computer science, and indeed evaluation with a lock-free linked-list, hash-table and skip-list shows that VBR outperforms state-of-the-art existing solutions., LIPIcs, Vol. 209, 35th International Symposium on Distributed Computing (DISC 2021), pages 35:1-35:18

Linearizability is the de facto consistency condition for concurrent objects, widely used in theory and practice. Loosely speaking, linearizability classifies concurrent executions as correct if operations on shared objects appear to take effect instantaneously during the operation execution time. This paper calls attention to a somewhat-neglected aspect of linearizability: restrictions on how pending invocations are handled, an issue that has become increasingly important for software running on systems with non-volatile main memory. Interestingly, the original published definition of linearizability includes a typo (a symbol is missing a prime) that concerns exactly this issue. In this paper we point out the typo and provide an amendment to make the definition complete. We believe that pointing this typo out rigorously and proposing a fix is important and timely.

The Transactional Data Structure Library (TDSL) methodology improves the programmability and performance of concurrent software by making it possible for programmers to compose multiple concurrent data structure operations into coarse-grained transactions. Like transactional memory, TDSL enables arbitrarily many operations on arbitrarily many data structures to appear to other threads as a single atomic, isolated transaction. Like concurrent data structures, the individual operations on a TDSL data structure are optimized to avoid artificial contention. We introduce techniques for reducing false conflicts in TDSL implementations. Our approach allows expressing the postconditions of operations entirely via semantic properties, instead of through low-level structural properties. Our design is general enough to support lists, deques, ordered and unordered maps, and vectors. It supports richer programming interfaces than are available in existing TDSL implementations. It is also capable of precise memory management, which is necessary in low-level languages like C++.

We consider durable data structures for non-volatile main memory, such as the new Intel Optane memory architecture. Substantial recent work has concentrated on making concurrent data structures durable with low overhead, by adding a minimal number of blocking persist operations (i.e., flushes and fences). In this work we show that focusing on minimizing the number of persist instructions is important, but not enough. We show that access to flushed content is of high cost due to cache invalidation in current architectures. Given this finding, we present a design of the queue data structure that properly takes care of minimizing blocking persist operations as well as minimizing access to flushed content. The proposed design outperforms state-of-the-art durable queues. We start by providing a durable version of the Michael Scott queue (MSQ). We amend MSQ by adding a minimal number of persist instructions, fewer than in available durable queues, and meeting the theoretical lower bound on the number of blocking persist operations. We then proceed with a second amendment to this design, that eliminates accesses to flushed data. Evaluation shows that the second amendment yields substantial performance improvement, outperforming the state of the art and demonstrating the importance of reduced accesses to flushed content. The presented queues are durably linearizable and lock-free. Finally, we discuss the theoretical optimal number of accesses to flushed content., Code: https://github.com/galysela/DurableQueues

This paper focuses on a large class of concurrent data structures that we call pool-like objects (e.g., stack, double-ended queue, and queue). Performance and progress guarantee are two important characteristics for concurrent data structures. In the aspect of performance, weakening the internal order in a pool-like object is an effective technique to reduce the synchronization cost among threads accessing the object, but no objects with weakened internal order provide a progress guarantee as strong as wait-freedom. Meanwhile, wait-free algorithms tend to be inefficient, which is mainly attributed to the helping mechanisms. Based on the philosophy of existing helping mechanisms, a wait-free pool-like object with weakened internal order would suffer from unnecessary process of getting the latest object state and synchronization. This paper takes a state-of-the-art implementation of stacks with weakened internal order as an example, and transforms it into a highly-efficient wait-free stack named WF-TS-Stack. The transformation method includes a helping mechanism with state reuse and a relaxed removal scheme. In addition, we use a simple and effective scheme to further improve the performance of WF-TS-Stack in Non-Uniform Memory Access (NUMA) architectures. Our evaluation with representative benchmarks shows that WF-TS-Stack outperforms its original building blocks by up to 1.45× at maximum concurrency. We also discuss how to yield an efficient double-ended queue (deque) variant of WF-TS-Stack, because deque is a more generalized pool-like object.

Pipelining is a well-known technique to overlap loop iterations by partitioning the loop body into a sequence of stages. A large class of programs can be expressed as linear pipelines if data dependences only flow from earlier to later stages. Various pipelining techniques have been explored but reconciling load-balancing and efficient execution is still a challenge for two main reasons. First, partitioning of the loop body into stages that lead to load-balancing may depend on the data set as well as system properties, e.g., number of cores. Second, the configuration of the runtime system is far from obvious. In this article, we present Pipelight, a technique that achieves load-balancing for linear pipelines. Pipelight relies on a way of mapping stages onto threads that simplifies partitioning and enables the design of a lightweight algorithm for dynamic scheduling. Furthermore, Pipelight introduces a concurrent data structure that exploits the properties of data dependences presented in linear pipelines to provide efficient communication and synchronization. This data structure simplifies the configuration of the runtime system and makes Pipelight a practical solution. The evaluation on a 44-core system shows the efficiency of Pipelight for a set of programs selected from widely-used collections. Although Pipelight simplifies parallelization of linear pipelines, it performs similarly to the most efficient properly configured state-of-the-art technique. The price paid for the benefits of Pipelight is additional overhead for fine-grained loops. However, this overhead can be amortized successfully with chunking. To make Pipelight a promising solution, we propose a directive-based transformation for Pipelight, which is developed in a prototype source-to-source compiler. Consequently, Pipelight is an efficient and practical solution to achieve load-balancing for fine-grained linear pipelines.

Implementation of concurrent data structures in architectures that provide limited synchronization primitives is a critical challenge. Typical lock-based implementations suffer from well-known problems such as poor scalability and unfairness. In this paper, we propose a client-server based synchronization model that can be applied in data structures with low level of parallelism for distributed shared memory many-core systems that support also message-passing communication. Additionally, we utilize a programmable hardware accelerator with appropriate application interfaces to overcome the performance-flexibility dilemma. Experimental results show that the proposed work performs 20 $\times$ faster than the single lock model with 88 $\times$ less idle cycles and 7 $\times$ less power consumption.

Remote memory access (RMA) technique is a very attractive way for improving efficiency of high-performance computations (HPC) and simplifying parallel program development. However, coming up with efficient concurrent data structures for distributed environments with deep hierarchy, such as computer clusters and data centres, is challenging. We propose a novel approach to design distributed concurrent data structures. The core idea behind the approach is relaxation of the order of executed operations. For example, a relaxed priority queues only requires the elements returned by delete-min operation to be sufficiently close to the minimum. Similarly, in a relaxed queue or stack, the removed elements are close to the first or the last one, respectively. There are multiple evidences that, on most workloads, relaxed data structures outperform data structures with strict semantics and ensure acceptable degrees of operation reordering. In this work we approve our approach on the example of a distributed queue, evaluate its efficiency and compare it with the other implementations of distributed lists.

We propose a method called Node Replication (NR) to implement any concurrent data structure. The method takes a single-threaded implementation of a data structure and automatically transforms it into a concurrent (thread-safe) implementation. The result is designed to work well with and harness the power of modern servers, which are complex Non-Uniform Memory Access (NUMA) machines with many processor sockets and subtle performance characteristics. Using NR requires no expertise in concurrent data structure design, and the result is free of concurrency bugs. NR represents a paradigm shift of how concurrent algorithms are developed: rather than designing for a data structure, we design for the architecture.

Context Testing concurrent data structures remains a notoriously challenging task, due to the nondeterminism of multi-threaded tests and the exponential explosion on the number of thread schedules. Objective We propose an automated approach to generate a series of concurrent test cases in an adaptive manner, i.e., the next test cases are generated with the guarantee to discover the thread schedules that have not yet been activated by the previous test cases. Method Two diversity metrics are presented to induce such adaptive test cases from a static and a dynamic perspective, respectively. The static metric enforces the diversity in the program structures of the test cases; while the dynamic one enforces the diversity in their capabilities of exposing untested thread schedules. We implement three adaptive test generation approaches for C/C++ concurrent data structures, based on the state-of-the-art active testing engine Maple. Results We then report an empirical study with 9 real-world C/C++ concurrent data structures, which demonstrates the efficiency of our test generation approaches in terms of the number of thread schedules discovered, as well as the time and the number of tests required for testing a concurrent data structure. Conclusion Hence, by using diverse test cases derived from the static and dynamic perspectives, our adaptive test generation approaches can deliver a more efficient coverage of the thread schedules of the concurrent data structure under test.

Eliminating so-called “out-of-thin-air” (OOTA) results is an open problem with many existing programming language memory models including Java, C, and C++. OOTA behaviors are problematic in that they break both formal and informal modular reasoning about program behavior. Defining memory model semantics that are easily understood, allow existing optimizations, and forbid OOTA results remains an open problem. This paper explores two simple solutions to this problem that forbid OOTA results. One solution is targeted towards C/C++-like memory models in which racing operations are explicitly labeled as atomic operations and a second solution is targeted towards Java-like languages in which all memory operations may create OOTA executions. Our solutions provide a per-candidate execution criterion that makes it possible to examine a single execution and determine whether the memory model permits the execution. We implemented and evaluated both solutions in the LLVM compiler framework. Our results show that on an ARMv8 processor the first solution has no overhead on average and a maximum overhead of 6.3% on 43 concurrent data structures, and that the second solution has an average overhead of 3.1% and a maximum overhead of 17.6% on the SPEC CPU2006 C/C++ benchmarks.

This paper introduces MEDS, a modular and elastic framework that simplifies the development of high-performance concurrent data structures that support linearizable primitive (i.e., add, remove, contains) and bulk (e.g., range query) operations.

Dynamic Connectivity is a fundamental algorithmic graph problem, motivated by a wide range of applications to social and communication networks and used as a building block in various other algorithms, such as the bi-connectivity and the dynamic minimal spanning tree problems. In brief, we wish to maintain the connected components of the graph under dynamic edge insertions and deletions. In the sequential case, the problem has been well-studied from both theoretical and practical perspectives. However, much less is known about efficient concurrent solutions to this problem. This is the gap we address in this paper. We start from one of the classic data structures used to solve this problem, the Euler Tour Tree. Our first contribution is a non-blocking single-writer implementation of it. We leverage this data structure to obtain the first truly concurrent generalization of dynamic connectivity, which preserves the time complexity of its sequential counterpart, but is also scalable in practice. To achieve this, we rely on three main techniques. The first is to ensure that connectivity queries, which usually dominate real-world workloads, are non-blocking. The second non-trivial technique expands the above idea by making all queries that do not change the connectivity structure non-blocking. The third ingredient is applying fine-grained locking for updating the connected components, which allows operations on disjoint components to occur in parallel. We evaluate the resulting algorithm on various workloads, executing on both real and synthetic graphs. The results show the efficiency of each of the proposed optimizations; the most efficient variant improves the performance of a coarse-grained based implementation on realistic scenarios up to 6x on average and up to 30x when connectivity queries dominate.

We tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions. This requires an understanding of the data structure, its sequential behavior, thread interactions during concurrent execution and shared memory synchronization primitives. We mechanize this design process using automated commonsense reasoning. We assume that the data structure description is provided as axioms alongside the sequential code of its algebraic operations. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees. Knowledge in our case is expressed using Answer Set Programming (ASP), and we employ deduction and abduction -- just as humans do -- in the reasoning involved. ASP allows for succinct modeling of first order theories of pointer data structures, run-time thread interactions and shared memory synchronization. Our reasoner can systematically make the same judgments as a human reasoner, while constructing provably safe concurrent code. We present several reasoning challenges involved in transforming the sequential data structure into its equivalent concurrent version. All the reasoning tasks are encoded in ASP and our reasoner can make sound judgments to transform sequential code into concurrent code. To the best of our knowledge, our work is the first one to use commonsense reasoning to automatically transform sequential programs into concurrent code. We also have developed a tool that we describe that relies on state-of-the-art ASP solvers and performs the reasoning tasks involved to generate concurrent code., Comment: In Proceedings ICLP 2021, arXiv:2109.07914. arXiv admin note: substantial text overlap with arXiv:2011.04045

Concurrent correctness conditions formalize the notion of “seeming atomicity” in concurrent access to shared object state. For different sorts of objects (databases, concurrent data structures, software transactional memory) different sorts of correctness conditions have been proposed (serializability, linearizability, opacity). Decidability of concurrent correctness conditions studies two problems: the membership problem asks whether a single execution is correct; the correctness problem asks whether all executions of a given implementation are correct.

This paper presents a new relaxed balanced concurrent binary search tree using a single word compare and swap primitive, in which all operations are lock-free. Our design separates balancing actions from update operations and includes a lock-free balancing mechanism in addition to the insert, search, and relaxed delete operations. Search in our design is not affected by ongoing concurrent update operations or by the movement of nodes by tree restructuring operations. Our experiments show that our algorithm performs better than other state-of-the-art concurrent BSTs.

Correctness verification of a concurrent history is challenging and has been proven to be an NP-complete problem. The reason that verifying correctness cannot be solved in polynomial time is a consequence of the way correctness is defined. Traditional correctness conditions require a concurrent history to be equivalent to a legal sequential history. The worst case number of legal sequential histories for a concurrent history is O(n!) with respect to n methods invoked. Existing correctness verification tools improve the time complexity by either reducing the size of the possible legal sequential histories or improving the efficiency of generating the possible legal sequential histories. Further improvements to the time complexity of correctness verification can be achieved by changing the way correctness of concurrent programs is defined. In this paper, we present the first methodology to recast the correctness conditions in literature to be defined in vector space. The concurrent histories are represented as a set of method call vectors, and correctness is defined as properties over the set of vectors. The challenge with defining correctness in vector space is accounting for method call ordering and data structure semantics. We solve this challenge by incorporating a priority assignment scheme to the values of the method call vectors. Using our new definitions of concurrent correctness, we design a dynamic analysis tool that checks the vector space correctness of concurrent data structures in \(O(n^2)\) with respect to n method calls, a significant improvement over O(n!) time required to analyze legal sequential histories. We showcase our dynamic analysis tool by using it to check the vector space correctness of a variety of queues, stacks, and hashmaps.

This paper reports a new concurrent graph data structure that supports updates of both edges and vertices and queries: Breadth-first search, Single-source shortest-path, and Betweenness centrality. The operations are provably linearizable and non-blocking., LIPIcs, Vol. 209, 35th International Symposium on Distributed Computing (DISC 2021), pages 52:1-52:4

Multicopy search structures such as log-structured merge (LSM) trees are optimized for high insert/update/delete (collectively known as upsert) performance. In such data structures, an upsert on key $k$, which adds $(k,v)$ where $v$ can be a value or a tombstone, is added to the root node even if $k$ is already present in other nodes. Thus there may be multiple copies of $k$ in the search structure. A search on $k$ aims to return the value associated with the most recent upsert. We present a general framework for verifying linearizability of concurrent multicopy search structures that abstracts from the underlying representation of the data structure in memory, enabling proof-reuse across diverse implementations. Based on our framework, we propose template algorithms for a) LSM structures forming arbitrary directed acyclic graphs and b) differential file structures, and formally verify these templates in the concurrent separation logic Iris. We also instantiate the LSM template to obtain the first verified concurrent in-memory LSM tree implementation., Comment: Extended version of an article to appear in OOPSLA'21

Priority queues with parallel access are an attractive data structure for applications like prioritized online scheduling, discrete event simulation, or greedy algorithms. However, a classical priority queue constitutes a severe bottleneck in this context, leading to very small throughput. Hence, there has been significant interest in concurrent priority queues with relaxed semantics. We investigate the complementary quality criteria rank error (how close are deleted elements to the global minimum) and delay (for each element x, how many elements with lower priority are deleted before x). In this paper, we introduce MultiQueues as a natural approach to relaxed priority queues based on multiple sequential priority queues. Their naturally high theoretical scalability is further enhanced by using three orthogonal ways of batching operations on the sequential queues. Experiments indicate that MultiQueues present a very good performance-quality tradeoff and considerably outperform competing approaches in at least one of these aspects. We employ a seemingly paradoxical technique of "wait-free locking" that might be of more general interest to convert sequential data structures to relaxed concurrent data structures., LIPIcs, Vol. 204, 29th Annual European Symposium on Algorithms (ESA 2021), pages 81:1-81:17