Thu 24 Oct 2024 16:00 - 16:20 at IBR East - Concurrency Chair(s): Alex Potanin

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 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
ConcurrencyOOPSLA 2024 at IBR East
Chair(s): Alex Potanin Australian National University
16:00
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
Verified Lock-Free Session Channels with Linking
OOPSLA 2024
Thomas Somers Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen
DOI
17:20
20m
Talk
Scenario-based Proofs for Concurrent ObjectsRemote
OOPSLA 2024
Constantin Enea LIX, CNRS, Ecole Polytechnique, Eric Koskinen Stevens Institute of Technology
DOI