In this short article, I will discuss the concept of linearizability and demonstrate that ConcurrentLinkedDeque in Java is non-linearizable by using Lincheck, a tool for testing concurrent data structures. You can find the code of the test on GitHub.
Table of Contents
What is Linearizability?
Linearizability is a consistency condition for concurrent operations. It ensures that even though operations may be executed concurrently, they appear to take effect instantaneously at some point between their start and end time.
Imagine you’re working with a shared object, like a queue or a stack. Linearizability ensures that every operation on this object looks as if it happened in a single, indivisible instant, even if behind the scenes, multiple threads are accessing it simultaneously.
Why Should You Care?
In the world of concurrent programming, achieving correctness is tricky. Without a clear consistency model, your code could behave unpredictably, leading to subtle bugs that are hard to reproduce and fix. Linearizability provides a strong guarantee that can simplify reasoning about your concurrent programs. Note that the absence of linearizability doesn’t imply that the data structures are incorrect. But it is an important property that you should take into consideration when building programs or libraries.
ConcurrentLinkedDeque in Java is non-linearizable
ConcurrentLinkedDeque is a concurrent deque based on linked nodes. You can insert and remove elements from both ends. In addition, it is thread-safe, which means that multiple threads can safely access, remove, and add elements to the queue.
But ConcurrentLinkedDeque is non-linearizable, which was revealed by Lincheck, a framework for testing concurrent algorithms on JVM.
Below is the code for the test written in Kotlin. The test uses Lincheck service annotations:
class ConcurrentLinkedDequeTest {
private val deque = ConcurrentLinkedDeque<Int>()
@Operation
fun addFirst(e: Int) = deque.addFirst(e)
@Operation
fun addLast(e: Int) = deque.addLast(1)
@Operation
fun pollFirst() = deque.pollFirst()
@Operation
fun pollLast() = deque.pollLast()
@Operation
fun peekFirst() = deque.peekFirst()
@Operation
fun peekLast() = deque.peekLast()
@Test
fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
}If we run the test, it “fails,” which means that the data structure is not linearizable. As you can see on the screenshot below, Lincheck provides not only the scenario on which ConcurrentLinkedDeque works incorrectly but also a detailed interleaving trace that leads to this error.
First, we need to understand why this execution is non-linearizable. For peekLast() to return "1", it should happen before pollFirst(). In this case, addFirst(0) is also completed before pollFirst(), so pollFirst() should return "0"; however, it returns "1" on the diagram.
But how does it happen? Let’s analyze the execution trace provided by Lincheck.
The underlying data structure forms a doubly linked list, with head and tail pointers approximating its first and last nodes. Initially, "head" and "tail" point to a logically removed (Node.item == null) node.
Then, addLast(1) is called, and the element “1” is added to the end of the linked list; “head’ and “tail” remain unchanged.
After that, the pollFirst() operation starts, finding the first node with a non-null value. However, the thread gets preempted right before extracting the element “1” from “Node#1.”
The execution switches to the second thread.
The addFirst(0) operation adds “0” to the beginning of the linked list; “head” and “tail” still remain unchanged (and this is fine, just consider them oracles).
Then, peekLast() reads the last element and returns “1”. Note that the concurrent pollFirst() is about to extract it, while "1" is no longer the first element.
The pollFirst() operation atomically replaces “1” with “null” in “Node#2.item”, accidentally extracting an element that is no longer the first. The current implementation finds the first non-null node and extracts the element from it, but the whole world may change in between.
Finally, the algorithm tries to unlink the extracted node from the linked list, but this part does not affect correctness.
Conclusion
There’s an issue in the JDK Bug System documenting this behavior of ConcurrentLinkedDeque. As the official documentation states:
We believe (without full proof) that all single-element Deque operations that operate directly at the two ends of the Deque (e.g., addFirst, peekLast, pollLast) are linearizable (see Herlihy and Shavit's book). However, some combinations of operations are known not to be linearizable. In particular, when an addFirst(A) is racing with pollFirst() removing B, it is possible for an observer iterating over the elements to observe first [A B C] and then [A C], even though no interior removes are ever performed. Nevertheless, iterators behave reasonably, providing the "weakly consistent" guarantees.
