The size of a data structure (i.e., the number of elements in it) is a widely used property of a data set.
However, for concurrent programs, obtaining a correct size efficiently is non-trivial. In fact, the literature does not offer a mechanism to obtain a correct (linearizable) size of a concurrent data set without resorting to inefficient solutions, such as taking a full snapshot of the data structure to count the elements, or acquiring one global lock in all update and size operations. This paper presents a methodology for adding a concurrent linearizable size operation to sets and dictionaries with a relatively low performance overhead. Theoretically, the proposed size operation is wait-free with asymptotic complexity linear in the number of threads (independently of data-structure size). Practically, we evaluated the performance overhead by adding size to various concurrent data structures in Java$-$a skip list, a hash table and a tree. The proposed linearizable size operation executes faster by orders of magnitude compared to the existing option of taking a snapshot, while incurring a throughput loss of $1%-20%$ on the original data structure's operations.
Sat 10 DecDisplayed time zone: Auckland, Wellington change
13:30 - 15:00
|C4: verified transactional objects
Mohsen Lesani University of California at Riverside, Li-yao Xia University of Pennsylvania, Anders Kaseorg Massachusetts Institute of Technology, Christian J. Bell MIT CSAIL, Adam Chlipala Massachusetts Institute of Technology, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of PennsylvaniaDOI
|Veracity: Declarative Multicore Programming with Commutativity
Adam Chen Stevens Institute of Technology, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, Jared Pincus Stevens Institute of TechnologyDOI