Design of an efficient thread-safe concurrent data structure is a balancing act between its implementation complexity and performance. Lock-based concurrent data structures, which are relatively easy to derive from their sequential counterparts and to prove thread-safe, suffer from poor throughput under even light multi-threaded workload. At the same time, lock-free concurrent structures allow for high throughput, but are notoriously difficult to get right and require careful reasoning to formally establish their correctness.
In this work, we explore a solution to this conundrum based on a relatively old idea of batch parallelism—an approach for designing high-throughput concurrent data structures via a simple insight: efficiently processing a batch of a priori known operations in parallel is easier than optimising performance for a stream of arbitrary asynchronous requests. Alas, batch-parallel structures have not seen wide practical adoption due to (i) the inconvenience of having to structure multi-threaded programs to explicitly group operations and (ii) the lack of a systematic methodology to implement batch-parallel structures as simply as lock-based ones.
We present OBatcher—a Multicore OCaml library that streamlines the design, implementation, and usage of batch-parallel structures. OBatcher solves the first challenge (how to use) by suggesting a new lightweight implicit batching design pattern that is built on top of generic asynchronous programming mechanisms. The second challenge (how to implement) is addressed by identifying a family of strategies for converting common sequential structures into the corresponding efficient batch-parallel versions, and by providing a library of functors that embody those strategies. We showcase OBatcher with a diverse set of benchmarks ranging from Red-Black and AVL trees to van Emde Boas trees, skip lists, and a thread-safe implementation of a Datalog solver. Our evaluation of all the implementations on large asynchronous workloads shows that (a) they consistently outperform the corresponding coarse-grained lock-based implementations—the only ones available in OCaml to date, and that (b) their throughput scales reasonably with the number of processors.
Thu 24 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | |||
16:00 20mTalk | Concurrent Data Structures Made Easy OOPSLA 2024 Callista Le Yale-NUS College, Kiran Gopinathan National University of Singapore, Lee Koon Wen Ahrefs, Seth Gilbert National University of Singapore, Ilya Sergey National University of Singapore DOI | ||
16:20 20mTalk | Automated Verification of Parametric Channel-Based Process Communication OOPSLA 2024 Georgian-Vlad Saioc Aarhus University, Julien Lange Royal Holloway, University of London, Anders Møller Aarhus University DOI | ||
16:40 20mTalk | Automated Robustness Verification of Concurrent Data Structure Libraries Against Relaxed Memory Models OOPSLA 2024 Kartik Nagar IIT Madras, Anmol Sahoo Purdue University, Romit Roy Chowdhury Chennai Mathematical Institute, Suresh Jagannathan Purdue University DOI | ||
17:00 20mTalk | Verified Lock-Free Session Channels with Linking OOPSLA 2024 DOI | ||
17:20 20mTalk | Scenario-based Proofs for Concurrent ObjectsRemote OOPSLA 2024 DOI |