research-article

Open access

Progress of concurrent objects with partial methods

Authors:

Xinyu FengAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 20, Pages 1 - 31

https://doi.org/10.1145/3158108

Published: 27 December 2017 Publication History

Abstract

Various progress properties have been proposed for concurrent objects, such as wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom. However, none of them applies to concurrent objects with partial methods, i.e., methods that are supposed not to return under certain circumstances. A typical example is the lock_acquire method, which must not return when the lock has already been acquired.

In this paper we propose two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF), for concurrent objects with partial methods. We also design four patterns to write abstract specifications for PSF or PDF objects under strongly or weakly fair scheduling, so that these objects contextually refine the abstract specifications. Our Abstraction Theorem shows the equivalence between PSF (or PDF) and the progress-aware contextual refinement. Finally, we generalize the program logic LiLi to have a new logic to verify the PSF (or PDF) property and linearizability of concurrent objects.

Supplementary Material

WEBM File (concurrentobjectswithpartialmethods.webm)

Download
101.77 MB

References

[1]

Pontus Boström and Peter Müller. 2015. Modular Verification of Finite Blocking in Non-terminating Programs. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 639–663.

[2]

Cristiano Calcagno, Matthew J. Parkinson, and Viktor Vafeiadis. 2007. Modular Safety Checking for Fine-Grained Concurrency. In Proceedings of the 14th International Symposium on Static Analysis (SAS 2007). 233–248.

[3]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving Program Termination. Commun. ACM 54, 5 (2011), 88–98.

Digital Library

[4]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. 2016. Modular Termination Verification for Non-blocking Concurrency. In Proceedings of the 25th European Symposium on Programming Languages and Systems (ESOP 2016). 176–201.

Digital Library

[5]

Ivana Filipović, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang. 2009. Abstraction for Concurrent Objects. In Proceedings of the 18th European Symposium on Programming (ESOP 2009). 252–266.

Digital Library

[6]

Alexey Gotsman, Byron Cook, Matthew J. Parkinson, and Viktor Vafeiadis. 2009. Proving that Non-Blocking Algorithms Don’t Block. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009). 16–28.

Digital Library

[7]

Alexey Gotsman and Hongseok Yang. 2011. Liveness-Preserving Atomicity Abstraction. In Proceedings of the 38th International Conference on Automata, Languages and Programming (ICALP 2011). 453–465.

[8]

Alexey Gotsman and Hongseok Yang. 2012. Linearizability with Ownership Transfer. In Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR 2012). 256–271.

Digital Library

[9]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI 2016). 653–669.

[10]

Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann.

[11]

Maurice Herlihy and Nir Shavit. 2011. On the Nature of Progress. In Proceedings of the 15th International Conference on Principles of Distributed Systems (OPODIS 2011). 313–328.

Digital Library

[12]

Maurice Herlihy and Jeannette Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492.

Digital Library

[13]

Jan Hoffmann, Michael Marmar, and Zhong Shao. 2013. Quantitative Reasoning for Proving Lock-Freedom. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013). 124–133.

Digital Library

[14]

Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. 2015. Modular Termination Verification. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 664–688.

[15]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015). 637–650.

Digital Library

[16]

Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew J. Parkinson. 2017. Proving Linearizability Using Partial Orders. In Proceedings of the 26th European Symposium on Programming (ESOP 2017). 639–667.

Digital Library

[17]

Hongjin Liang and Xinyu Feng. 2013. Modular Verification of Linearizability with Non-Fixed Linearization Points. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2013). 459–470.

Digital Library

[18]

Hongjin Liang and Xinyu Feng. 2016. A Program Logic for Concurrent Objects Under Fair Scheduling. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016). 385–399.

Digital Library

[19]

Hongjin Liang and Xinyu Feng. 2017. Progress of Concurrent Objects with Partial Methods (Extended Version). Technical Report. https://cs.nju.edu.cn/hongjin/papers/popl18- partial- tr.pdf .

[20]

Hongjin Liang, Xinyu Feng, and Zhong Shao. 2014. Compositional Verification of Termination-preserving Refinement of Concurrent Programs. In Proceedings of the 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). 65:1–65:10.

Digital Library

[21]

Hongjin Liang, Jan Hoffmann, Xinyu Feng, and Zhong Shao. 2013. Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. In Proceedings of the 24th International Conference on Concurrency Theory (CONCUR 2013). 227–241.

Digital Library

[22]

John M. Mellor-Crummey and Michael L. Scott. 1991. Algorithms for Scalable Synchronization on Shared-memory Multiprocessors. ACM Trans. Comput. Syst. 9, 1 (1991), 21–65.

Digital Library

[23]

Gerhard Schellhorn, Oleg Travkin, and Heike Wehrheim. 2016. Towards a Thread-Local Proof Technique for Starvation Freedom. In Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016). 193–209.

Digital Library

[24]

Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In Proceedings of the 26th European Symposium on Programming (ESOP 2017). 909–936.

Digital Library

[25]

R. Kent Treiber. 1986. System Programming: Coping with Parallelism. Technical Report RJ 5118. IBM Almaden Research Center.

[26]

Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical Relations for Fine-Grained Concurrency. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013). 343–356.

Digital Library

Cited By

Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Kim JGu RShao Z(2024) SimplMMJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2023.103049147:COnline publication date: 17-Apr-2024
https://dl.acm.org/doi/10.1016/j.sysarc.2023.103049
Show More Cited By

Index Terms

Progress of concurrent objects with partial methods
1. Theory of computation
  1. Logic
    1. Hoare logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

A program logic for concurrent objects under fair scheduling
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying lock-freedom of non-blocking objects, much less efforts are focused on ...
A program logic for concurrent objects under fair scheduling
POPL '16

Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying lock-freedom of non-blocking objects, much less efforts are focused on ...
Progress of Concurrent Objects

Implementations of concurrent objects should guarantee linearizability and a progress property such as wait-freedom, lock-freedom, starvation-freedom, or deadlock-freedom. These progress properties describe conditions under which a method call is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 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 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: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Natural Science Foundation of China

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
2,690
Total Downloads

Downloads (Last 12 months)82
Downloads (Last 6 weeks)11

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Kim JGu RShao Z(2024) SimplMMJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2023.103049147:COnline publication date: 17-Apr-2024
https://dl.acm.org/doi/10.1016/j.sysarc.2023.103049
Kim JKoenig JChen HGu RShao Z(2024) ThreadAbsJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2023.103046147:COnline publication date: 17-Apr-2024
https://dl.acm.org/doi/10.1016/j.sysarc.2023.103046
Lee DCho MKim JMoon SSong YHur C(2023)Fair Operational SemanticsProceedings of the ACM on Programming Languages10.1145/35912537:PLDI(811-834)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591253
Qian ZZhong SSun GXing XJin Y(2023)A Formal Approach to Design and Security Verification of Operating Systems for Intelligent Transportation Systems Based on Object ModelIEEE Transactions on Intelligent Transportation Systems10.1109/TITS.2022.322438524:12(15459-15467)Online publication date: Dec-2023
https://doi.org/10.1109/TITS.2022.3224385
Hayes IJones CMeinicke L(2023)Specifying and Reasoning About Shared-Variable ConcurrencyTheories of Programming and Formal Methods10.1007/978-3-031-40436-8_5(110-135)Online publication date: 8-Sep-2023
https://doi.org/10.1007/978-3-031-40436-8_5
Gäher LSammler MSpies SJung RDang HKrebbers RKang JDreyer D(2022)Simuliris: a separation logic framework for verifying concurrent program optimizationsProceedings of the ACM on Programming Languages10.1145/34986896:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498689
D’Osualdo ESutherland JFarzan AGardner P(2021)TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent ProgramsACM Transactions on Programming Languages and Systems10.1145/347708243:4(1-134)Online publication date: 10-Nov-2021
https://dl.acm.org/doi/10.1145/3477082
Spies SGäher LGratzer DTassarotti JKrebbers RDreyer DBirkedal LFreund SYahav E(2021)Transfinite Iris: resolving an existential dilemma of step-indexed separation logicProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454031(80-95)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454031
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents