skip to main content
research-article
Open Access

Progress of concurrent objects with partial methods

Authors Info & Claims
Published:27 December 2017Publication History
Skip Abstract Section

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.

Skip Supplemental Material Section

Supplemental Material

concurrentobjectswithpartialmethods.webm

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.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarCross RefCross Ref
  3. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving Program Termination. Commun. ACM 54, 5 (2011), 88–98. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarCross RefCross Ref
  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. Google ScholarGoogle ScholarDigital LibraryDigital 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.Google ScholarGoogle Scholar
  10. Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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 .Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital 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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. R. Kent Treiber. 1986. System Programming: Coping with Parallelism. Technical Report RJ 5118. IBM Almaden Research Center.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Progress of concurrent objects with partial methods

          Recommendations

          Comments

          Login options

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

          Sign in

          Full Access

          • 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 about this article.

            Request Permissions

            Check for updates

            Qualifiers

            • research-article

          PDF Format

          View or Download as a PDF file.

          PDF

          eReader

          View online with eReader.

          eReader