skip to main content
research-article
Open access

A Scalable, Correct Time-Stamped Stack

Published: 14 January 2015 Publication History

Abstract

Concurrent data-structures, such as stacks, queues, and deques, often implicitly enforce a total order over elements in their underlying memory layout. However, much of this order is unnecessary: linearizability only requires that elements are ordered if the insert methods ran in sequence. We propose a new approach which uses timestamping to avoid unnecessary ordering. Pairs of elements can be left unordered if their associated insert operations ran concurrently, and order imposed as necessary at the eventual removal.
We realise our approach in a new non-blocking data-structure, the TS (timestamped) stack. Using the same approach, we can define corresponding queue and deque data-structures. In experiments on x86, the TS stack outperforms and outscales all its competitors -- for example, it outperforms the elimination-backoff stack by factor of two. In our approach, more concurrency translates into less ordering, giving less-contended removal and thus higher performance and scalability. Despite this, the TS stack is linearizable with respect to stack semantics.
The weak internal ordering in the TS stack presents a challenge when establishing linearizability: standard techniques such as linearization points work well when there exists a total internal order. We present a new stack theorem, mechanised in Isabelle, which characterises the orderings sufficient to establish stack semantics. By applying our stack theorem, we show that the TS stack is indeed linearizable. Our theorem constitutes a new, generic proof technique for concurrent stacks, and it paves the way for future weakly ordered data-structure designs.

Supplementary Material

ZIP File (popl008.zip)
A Scalable, Correct Time-Stamped Stack We provide an appendix and two artifacts: * A proof in Isabelle/HOL of the Stack Theorem (Theorem 1 in our paper). * The TS stack, a concurrent stack written in C, along with implementations of several other algorithms for comparison purposes.
MPG File (p233-sidebyside.mpg)

References

[1]
Y. Afek and A. Morrison. Fast concurrent queues for x86 processors. In phPPoPP. ACM, 2013.
[2]
H. Attiya, R. Guerraoui, D. Hendler, P. Kuznetsov, M. Michael, and M. Vechev. Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. In phPOPL, 2011.
[3]
G. Bar-Nissan, D. Hendler, and A. Suissa. A dynamic elimination-combining stack algorithm. In phOPODIS, 2011.
[4]
M. Batty, M. Dodds, and A. Gotsman. Library abstraction for C/C
[5]
concurrency. In phPOPL, 2013.
[6]
}scalComputational Systems Group, University of Salzburg. Scal framework. URL http://scal.cs.uni-salzburg.at.
[7]
M. Gorelik and D. Hendler. Brief announcement: an asymmetric flat-combining based queue algorithm. In phPODC, 2013.
[8]
A. Haas, C. Kirsch, M. Lippautz, and H. Payer. How FIFO is your concurrent FIFO queue? In phRACES. ACM, 2012.
[9]
A. Haas, T. Henzinger, C. Kirsch, M. Lippautz, H. Payer, A. Sezgin, and A. Sokolova. Distributed queues in shared memory--multicore performance and scalability through quantitative relaxation. In phCF. ACM, 2013.
[10]
D. Hendler, N. Shavit, and L. Yerushalmi. A scalable lock-free stack algorithm. In phSPAA. ACM, 2004.
[11]
D. Hendler, I. Incze, N. Shavit, and M. Tzafrir. Flat combining and the synchronization-parallelism tradeoff. In phSPAA, 2010.
[12]
Henzinger, Payer, and Sezgin}Henzinger13bT. Henzinger, H. Payer, and A. Sezgin. Replacing competition with cooperation to achieve scalable lock-free FIFO queues. Technical Report IST-2013--124-v1
[13]
1, IST Austria, 2013\natexlaba.
[14]
Henzinger, Sezgin, and Vafeiadis}Henzinger13T. A. Henzinger, A. Sezgin, and V. Vafeiadis. Aspect-oriented linearizability proofs. In phCONCUR, 2013\natexlabb.
[15]
M. Herlihy and N. Shavit. phThe Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., 2008.
[16]
M. Herlihy and J. Wing. Linearizability: a correctness condition for concurrent objects. phTOPLAS, 12 (3), 1990.
[17]
M. Hoffman, O. Shalev, and N. Shavit. The baskets queue. In phOPODIS. Springer, 2007.
[18]
Intel. Intel 64 and ia-32 architectures software developer's manual, volume 3b: System programming guide, part 2, 2013. URL http://download.intel.com/products/processor/manual/253669.pdf.
[19]
L. Lamport. Time, clocks, and the ordering of events in a distributed system. phCommunications ACM, 21, July 1978.
[20]
M. Michael and M. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In phPODC. ACM, 1996.
[21]
H. H. Nguyen and M. Rinard. Detecting and eliminating memory leaks using cyclic memory allocation. In phISMM. ACM, 2007.
[22]
W. Ruan, Y. Liu, and M. Spear. Boosting timestamp-based transactional memory by exploiting hardware cycle counters. In phTRANSACT, 2013.
[23]
P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. phCommun. ACM, 53 (7), 2010.
[24]
R. Treiber. Systems programming: Coping with parallelism. Technical Report RJ5118, IBM Almaden Research Center, April 1986.

Cited By

View all
  • (2024)A Conflict-Resilient Lock-Free Linearizable Calendar QueueACM Transactions on Parallel Computing10.1145/363516311:1(1-32)Online publication date: 11-Mar-2024
  • (2023)A general approach for supporting nonblocking data structures on distributed-memory systemsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2022.11.006173(48-60)Online publication date: Mar-2023
  • (2023)VeriLin: A Linearizability Checker for Large-Scale Concurrent ObjectsTheoretical Aspects of Software Engineering10.1007/978-3-031-35257-7_12(202-220)Online publication date: 4-Jul-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. concurrent stack
  2. linearizability
  3. timestamps
  4. verification

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)203
  • Downloads (Last 6 weeks)33
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)A Conflict-Resilient Lock-Free Linearizable Calendar QueueACM Transactions on Parallel Computing10.1145/363516311:1(1-32)Online publication date: 11-Mar-2024
  • (2023)A general approach for supporting nonblocking data structures on distributed-memory systemsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2022.11.006173(48-60)Online publication date: Mar-2023
  • (2023)VeriLin: A Linearizability Checker for Large-Scale Concurrent ObjectsTheoretical Aspects of Software Engineering10.1007/978-3-031-35257-7_12(202-220)Online publication date: 4-Jul-2023
  • (2022)Parameterized verification of systems with component identities, using view abstractionInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00648-024:2(287-324)Online publication date: 26-Feb-2022
  • (2021)Nonblocking Data Structures for Distributed-Memory Machines: Stacks as an Example2021 29th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)10.1109/PDP52278.2021.00012(9-17)Online publication date: Mar-2021
  • (2019)Fast Wait-Free Construction for Pool-Like Objects with Weakened Internal Order: Stacks as an ExampleIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2018.288904830:7(1596-1612)Online publication date: 1-Jul-2019
  • (2019)Towards Relaxed Concurrent Data Structures on Distributed Memory Computer Systems2019 International Multi-Conference on Industrial Engineering and Modern Technologies (FarEastCon)10.1109/FarEastCon.2019.8934183(1-6)Online publication date: Oct-2019
  • (2019)Implementation and Analysis of Distributed Relaxed Concurrent Queues in Remote Memory Access ModelProcedia Computer Science10.1016/j.procs.2019.02.101150:C(654-662)Online publication date: 1-Jan-2019
  • (2019)A mechanized refinement proof of the Chase---Lev deque using a proof systemComputing10.1007/s00607-018-0635-4101:1(59-74)Online publication date: 1-Jan-2019
  • (2018)FA-Stack: A Fast Array-Based Stack with Wait-Free Progress GuaranteeIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2017.277012129:4(843-857)Online publication date: 1-Apr-2018
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media