research-article

Proving Lock-Freedom Easily and Automatically

Authors:

Viktor VafeiadisAuthors Info & Claims

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

Pages 119 - 127

https://doi.org/10.1145/2676724.2693179

Published: 13 January 2015 Publication History

Abstract

Lock-freedom is a liveness property satisfied by most non-blocking concurrent algorithms. It ensures that at any point at least one thread is making progress towards termination; so the system as a whole makes progress. As a global property, lock-freedom is typically shown by global proofs or complex iterated arguments. We show that this complexity is not needed in practice. By introducing simple loop depth counters into the programs, we can reduce proving lock-freedom to checking simple local properties on those counters. We have implemented the approach in Cave and report on our findings.

References

[1]

Robert Colvin and Brijesh Dongol. Verifying lock-freedom using well-founded orders. In ICTAC 2007: 4th International Colloquium on Theoretical Aspects of Computing, pages 124--138, 2007.

Digital Library

[2]

Robert Colvin and Brijesh Dongol. A general technique for proving lock-freedom. Sci. Comput. Program., 74 (3): 143--165, 2009.

Digital Library

[3]

Simon Doherty, Lindsay Groves, Victor Luchangco, and Mark Moir. Formal verification of a practical lock-free queue algorithm. In FORTE 2014: Formal Techniques for Networked and Distributed Systems, volume 3235 of phLecture Notes in Computer Science, pages 97--114. Springer, 2004. 10.1007/978-3-540-30232-2_7.

[4]

Alexey Gotsman, Byron Cook, Matthew J. Parkinson, and Viktor Vafeiadis. Proving that non-blocking algorithms don't block. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009), pages 16--28. ACM, 2009. 10.1145/1480881.1480886.

Digital Library

[5]

Danny Hendler, Nir Shavit, and Lena Yerushalmi. A scalable lock-free stack algorithm. J. Parallel Distrib. Comput., 70 (1): 1--12, 2010. 10.1016/j.jpdc.2009.08.011.

Digital Library

[6]

Maurice Herlihy. Wait-free synchronization. ACM Transactions on Programming Languages and Systems (TOPLAS), 13 (1): 124--149, 1991.

Digital Library

[7]

Maurice Herlihy and Nir Shavit. The art of multiprocessor programming. Morgan Kaufmann, 2008. ISBN 978-0-12-370591-4.

Digital Library

[8]

Maurice P. Herlihy, Victor Luchangco, and Mark Moir. Obstruction-free synchronization: Double-ended queues as an example. In Proceedings of the 23rd International Conference on Distributed Computing Systems (ICDCS 2003), pages 522--529. IEEE, 2003.

Digital Library

[9]

Jan Hoffmann, Michael Marmar, and Zhong Shao. Quantitative reasoning for proving lock-freedom. In Proceedings of the 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS), pages 124--133. IEEE, 2013.

Digital Library

[10]

Hongjin Liang, Xinyu Feng, and Zhong Shao. Compositional verification of termination-preserving refinement of concurrent programs. In Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014). ACM, 2014.

Digital Library

[11]

Henry Massalin and Calton Pu. A lock-free multiprocessor os kernel. ACM SIGOPS Operating Systems Review, 26 (2): 108, 1992.

[12]

Maged M. Michael and Michael L. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In PODC 1996: 15th Annual ACM Symposium on Principles of Distributed Computing, pages 267--275. ACM, 1996. 10.1145/248052.248106.

Digital Library

[13]

R. K. Treiber. Systems programming: Coping with parallelism. Technical Report Technical Report RJ 5118, IBM Almaden Research Center, April 1986.

[14]

Viktor Vafeiadis. Automatically proving linearizability. In CAV 2010: 22nd Int. Conference on Computer Aided Verification, pages 450--464. Springer, 2010.

Digital Library

[15]

Viktor Vafeiadis. RGSep action inference. In VMCAI 2010: 11th Int. Conference on Verification, Model Checking, and Abstract Interpretation, pages 345--361. Springer, 2010.

Digital Library

[16]

Viktor Vafeiadis and Matthew J. Parkinson. A marriage of rely/guarantee and separation logic. InCONCUR 2007: 18th International Conference on Concurrency Theory, volume 4703 of Lecture Notes in Computer Science, pages 256--271. Springer, 2007. 10.1007/978-3-540-74407-8_18.

Digital Library

Cited By

Koval NKhalanskiy DAlistarh D(2023)CQS: A Formally-Verified Framework for Fair and Abortable SynchronizationProceedings of the ACM on Programming Languages10.1145/35912307:PLDI(244-266)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591230
Pani TWeissenbacher GZuleger F(2021)Rely-guarantee bound analysis of parameterized concurrent shared-memory programsFormal Methods in System Design10.1007/s10703-021-00370-8Online publication date: 6-Apr-2021
https://doi.org/10.1007/s10703-021-00370-8
Peterson CCook VDechev D(2019)Practical Progress Verification of Descriptor-Based Non-Blocking Data Structures2019 IEEE 27th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS)10.1109/MASCOTS.2019.00019(83-93)Online publication date: Oct-2019
https://doi.org/10.1109/MASCOTS.2019.00019
Show More Cited By

Index Terms

Proving Lock-Freedom Easily and Automatically
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation

Recommendations

Separating Lock-Freedom from Wait-Freedom
PODC '18: Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing

A long-standing open question has been whether lock-freedom and wait-freedom are fundamentally different progress conditions, namely, can the former be provided in situations where the latter cannot? This paper answers the question in the affirmative, ...
Quantitative Reasoning for Proving Lock-Freedom
LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science

This article describes a novel quantitative proof technique for the modular and local verification of lock-freedom. In contrast to proofs based on temporal rely-guarantee requirements, this new quantitative reasoning method can be directly integrated in ...
Static lock capabilities for deadlock freedom
TLDI '12: Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation

We present a technique --- lock capabilities --- for statically verifying that multithreaded programs with locks will not deadlock. Most previous work on deadlock prevention requires a strict total order on all locks held simultaneously by a thread, but ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

January 2015

192 pages

ISBN:9781450332965

DOI:10.1145/2676724

Program Chairs:
Xavier Leroy
Inria Paris-Rocquencourt, France
,
Alwen Tiu
Nanyang Technological University, Singapore

Copyright © 2015 ACM.

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 the author(s) 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].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Seventh Framework Programme

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 13 - 14, 2015

Mumbai, India

Acceptance Rates

CPP '15 Paper Acceptance Rate 18 of 26 submissions, 69%;

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
167
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 27 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Koval NKhalanskiy DAlistarh D(2023)CQS: A Formally-Verified Framework for Fair and Abortable SynchronizationProceedings of the ACM on Programming Languages10.1145/35912307:PLDI(244-266)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591230
Pani TWeissenbacher GZuleger F(2021)Rely-guarantee bound analysis of parameterized concurrent shared-memory programsFormal Methods in System Design10.1007/s10703-021-00370-8Online publication date: 6-Apr-2021
https://doi.org/10.1007/s10703-021-00370-8
Peterson CCook VDechev D(2019)Practical Progress Verification of Descriptor-Based Non-Blocking Data Structures2019 IEEE 27th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS)10.1109/MASCOTS.2019.00019(83-93)Online publication date: Oct-2019
https://doi.org/10.1109/MASCOTS.2019.00019
Pani TWeissenbacher GZuleger F(2018)Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms2018 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2018.8603020(1-9)Online publication date: Oct-2018
https://doi.org/10.23919/FMCAD.2018.8603020

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten