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.
Supplemental Material
- 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 Scholar
- 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 ScholarCross Ref
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving Program Termination. Commun. ACM 54, 5 (2011), 88–98. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 Scholar
- Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann.Google Scholar
- 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 ScholarDigital Library
- Maurice Herlihy and Jeannette Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- R. Kent Treiber. 1986. System Programming: Coping with Parallelism. Technical Report RJ 5118. IBM Almaden Research Center.Google Scholar
- 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 ScholarDigital Library
Index Terms
Progress of concurrent objects with partial methods
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 LanguagesExisting 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 '16Existing 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