-
Non-Blocking Doubly-Linked Lists with Good Amortized Complexity
Authors:
Niloufar Shafiei
Abstract:
We present a new non-blocking doubly-linked list implementation for an asynchronous shared-memory system. It is the first such implementation for which an upper bound on amortized time complexity has been proved. In our implementation, operations access the list via cursors. Each cursor is associated with an item in the list and is local to a process. The implementation supports two update operati…
▽ More
We present a new non-blocking doubly-linked list implementation for an asynchronous shared-memory system. It is the first such implementation for which an upper bound on amortized time complexity has been proved. In our implementation, operations access the list via cursors. Each cursor is associated with an item in the list and is local to a process. The implementation supports two update operations, insertBefore and delete, and two move operations, moveRight and moveLeft. An insertBefore(c, x) operation inserts an item x into the list immediately before the cursor c's location. A delete(c) operation removes the item at the cursor c's location and sets the cursor to the next item in the list. The move operations move the cursor one position to the right or left. The update operations use single-word Compare&Swap instructions. The move operations only read shared memory and never change the state of the data structure. If all update operations modify different parts of the list, they run completely concurrently. Let cp(op) be the maximum number of active cursors at any one time during the operation op. The amortized complexity of each update operation op is O(cp(op)) and each move operation is O(1). We have written a detailed correctness proof and amortized analysis of our implementation.
△ Less
Submitted 8 August, 2014;
originally announced August 2014.
-
Non-blocking Patricia Tries with Replace Operations
Authors:
Niloufar Shafiei
Abstract:
This paper presents a non-blocking Patricia trie implementation for an asynchronous shared-memory system using Compare&Swap. The trie implements a linearizable set and supports three update operations: insert adds an element, delete removes an element and replace replaces one element by another. The replace operation is interesting because it changes two different locations of tree atomically. If…
▽ More
This paper presents a non-blocking Patricia trie implementation for an asynchronous shared-memory system using Compare&Swap. The trie implements a linearizable set and supports three update operations: insert adds an element, delete removes an element and replace replaces one element by another. The replace operation is interesting because it changes two different locations of tree atomically. If all update operations modify different parts of the trie, they run completely concurrently. The implementation also supports a wait-free find operation, which only reads shared memory and never changes the data structure. Empirically, we compare our algorithms to some existing set implementations.
△ Less
Submitted 14 March, 2013;
originally announced March 2013.
-
jpf-concurrent: An extension of Java PathFinder for java.util.concurrent
Authors:
Mateusz Ujma,
Nastaran Shafiei
Abstract:
One of the main challenges when verifying multi-threaded Java applications is the state space explosion problem. Due to thread interleavings, the number of states that the model checker has to verify can grow rapidly and impede the feasibility of verification. In the Java language, the source of thread interleavings can be the system under test as well as the Java Development Kit (JDK) itself. In…
▽ More
One of the main challenges when verifying multi-threaded Java applications is the state space explosion problem. Due to thread interleavings, the number of states that the model checker has to verify can grow rapidly and impede the feasibility of verification. In the Java language, the source of thread interleavings can be the system under test as well as the Java Development Kit (JDK) itself. In our paper, we propose a method to minimize the state space explosion problem for applications verified under the Java PathFinder (JPF) model checker. Our method is based on abstracting the state of the application to a smaller domain and implementing application behavior using the Model Java Interface (MJI) of JPF. To show the capabilities of our approach, we have created a JPF extension called jpf-concurrent which abstracts classes from the Java Concurrency Utilities. Several benchmarks proved the usefulness of our approach. In all cases, our implementation was faster than the JDK implementation when running under the JPF model checker. Moreover, our implementation led to significantly smaller state spaces.
△ Less
Submitted 30 April, 2012;
originally announced May 2012.
