extended-abstract

Brief Announcement: Linearizability: A Typo

Authors:

Gal Sela,

Maurice Herlihy,

Erez PetrankAuthors Info & Claims

PODC'21: Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing

Pages 561 - 564

https://doi.org/10.1145/3465084.3467944

Published: 23 July 2021 Publication History

Get Access

Abstract

Linearizability is the de facto consistency condition for concurrent objects, widely used in theory and practice. Loosely speaking, linearizability classifies concurrent executions as correct if operations on shared objects appear to take effect instantaneously during the operation execution time. This paper calls attention to a somewhat-neglected aspect of linearizability: restrictions on how pending invocations are handled, an issue that has become increasingly important for software running on systems with non-volatile main memory. Interestingly, the original published definition of linearizability includes a typo (a symbol is missing a prime) that concerns exactly this issue. In this paper we point out the typo and provide an amendment to make the definition complete. We believe that pointing this typo out rigorously and proposing a fix is important and timely.

Supplementary Material

MP4 File (PODC21-119ba.mp4)

Linearizability: A Typo - Gal Sela, Maurice Herlihy and Erez Petrank. Linearizability is the de facto consistency condition for concurrent objects, widely used in theory and practice. Loosely speaking, linearizability classifies concurrent executions as correct if operations on shared objects appear to take effect instantaneously during the operation execution time. This paper calls attention to a somewhat-neglected aspect of linearizability: restrictions on how pending invocations are handled, an issue that has become increasingly important for software running on systems with non-volatile main memory. Interestingly, the original published definition of linearizability includes a typo (a symbol is missing a prime) that concerns exactly this issue. In this paper we point out the typo and provide an amendment to make the definition complete. We believe that pointing this typo out rigorously and proposing a fix is important and timely. (The paper appears at https://doi.org/10.1145/3465084.3467944)

Download
22.14 MB

References

[1]

Marcos K Aguilera and Svend Frølund. 2003. Strict linearizability and the power of aborting. Technical Report HPL-2003--241 (2003). https://hpl.hp.com/techreports/2003/HPL-2003--241.html

Google Scholar

[2]

Ryan Berryhill, Wojciech Golab, and Mahesh Tripunitara. 2015. Robust shared objects for non-volatile main memory. In OPODIS. https://doi.org/10.4230/LIPIcs.OPODIS.2015.20

Crossref

Google Scholar

[3]

Rachid Guerraoui and Ron R Levy. 2004. Robust emulations of shared memory in a crash-recovery model. In ICDCS. https://doi.org/10.1109/ICDCS.2004.1281605

Crossref

Google Scholar

[4]

Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A correctness condition for concurrent objects. TOPLAS, Vol. 12, 3 (1990). https://doi.org/10.1145/78969.78972

Crossref

Google Scholar

[5]

Joseph Izraelevitz, Hammurabi Mendes, and Michael L Scott. 2016. Linearizability of persistent memory objects under a full-system-crash failure model. In DISC. https://doi.org/10.1007/978-3-662-53426-7_23

Crossref

Google Scholar

[6]

Gal Sela, Maurice Herlihy, and Erez Petrank. 2021. Linearizability: A typo. arXiv preprint (2021).

Google Scholar

Cited By

View all

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Dalvandi SDongol B(2022)Implementing and verifying release-acquire transactional memory in C11Proceedings of the ACM on Programming Languages10.1145/35633526:OOPSLA2(1817-1844)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563352
Sela GPetrank E(2022)Concurrent sizeProceedings of the ACM on Programming Languages10.1145/35633006:OOPSLA2(345-372)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563300

Index Terms

Brief Announcement: Linearizability: A Typo

Recommendations

Brief Announcement: Proust: A Design Space for Highly-Concurrent Transactional Data Structures
PODC '17: Proceedings of the ACM Symposium on Principles of Distributed Computing

Most STM systems are poorly equipped to support libraries of concurrent data structures. One reason is that they typically detect conflicts by tracking transactions' read sets and write sets, an approach that often leads to false conflicts. A second is ...
Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability
PODC '23: Proceedings of the 2023 ACM Symposium on Principles of Distributed Computing

This paper studies the problem of verifying linearizability at runtime, where one seeks for a concurrent algorithm for verifying that the current execution of a given concurrent shared object implementation is linearizable. It shows that it is ...
Concurrent Size (Abstract)
HOPC'24: Proceedings of the 2024 ACM Workshop on Highlights of Parallel Computing

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PODC'21: Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing

July 2021

590 pages

ISBN:9781450385480

DOI:10.1145/3465084

General Chair:
Avery Miller
University of Manitoba, Canada
,
Program Chair:
Keren Censor-Hillel
Technion, Israel

Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 July 2021

Check for updates

Author Tags

Qualifiers

Extended-abstract

Funding Sources

The United States - Israel BSF

Conference

PODC '21

Sponsor:

PODC '21: ACM Symposium on Principles of Distributed Computing

July 26 - 30, 2021

Virtual Event, Italy

Acceptance Rates

Overall Acceptance Rate 740 of 2,477 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
208
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)4

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Dalvandi SDongol B(2022)Implementing and verifying release-acquire transactional memory in C11Proceedings of the ACM on Programming Languages10.1145/35633526:OOPSLA2(1817-1844)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563352
Sela GPetrank E(2022)Concurrent sizeProceedings of the ACM on Programming Languages10.1145/35633006:OOPSLA2(345-372)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563300

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Brief Announcement: Proust: A Design Space for Highly-Concurrent Transactional Data Structures

Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

Concurrent Size (Abstract)