Foundations and Trends® in Programming Languages > Vol 5 > Issue 4

Progress of Concurrent Objects

Hongjin Liang, State Key Laboratory for Novel Software Technology, Nanjing University, China, hongjin@nju.edu.cn Xinyu Feng, State Key Laboratory for Novel Software Technology, Nanjing University, China, xyfeng@nju.edu.cn
 
Suggested Citation
Hongjin Liang and Xinyu Feng (2020), "Progress of Concurrent Objects", Foundations and TrendsĀ® in Programming Languages: Vol. 5: No. 4, pp 282-414. http://dx.doi.org/10.1561/2500000041

Publication Date: 18 May 2020
© 2020 Hongjin Liang and Xinyu Feng
 
Subjects
Program Logic,  Program Verification
 

Free Preview:

Download extract

Share

Download article
In this article:
1. Introduction
2. Background
3. Basic Technical Settings
4. Linearizability and Contextual Refinement
5. Progress Properties
6. Progress-Aware Abstraction
7. Verifying Progress of Concurrent Objects
8. Related Work
9. Conclusion and Future Work
Acknowledgements
References

Abstract

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 guaranteed to complete. However, they fail to describe how clients are affected, making it difficult to utilize them in layered and modular program verification. Also we lack verification techniques for starvation-free or deadlock-free objects. They are challenging to verify because the fairness assumption introduces complicated interdependencies among progress of threads. Even worse, none of the existing results 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 tutorial we examine the progress properties of concurrent objects. We formulate each progress property (together with linearizability as a basic correctness requirement) in terms of contextual refinement. This essentially gives us progress-aware abstraction for concurrent objects. Thus, when verifying clients of the objects, we can soundly replace the concrete object implementations with their abstractions, achieving modular verification. For concurrent objects with partial methods, we formulate two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF). We also design four patterns to write abstractions for PSF or PDF objects under strongly or weakly fair scheduling, so that these objects contextually refine their abstractions. Finally, we introduce a rely-guarantee style program logic LiLi for verifying linearizability and progress together for concurrent objects. It unifies thread-modular reasoning about all the six progress properties (wait-freedom, lock-freedom, starvation-freedom, deadlock-freedom, PSF and PDF) in one framework. We have successfully applied LiLi to verify starvation-freedom or deadlock-freedom of representative algorithms such as lock-coupling lists, optimistic lists and lazy lists, and PSF or PDF of lock algorithms.

DOI:10.1561/2500000041
ISBN: 978-1-68083-672-1
146 pp. $95.00
Buy book (pb)
 
ISBN: 978-1-68083-673-8
146 pp. $140.00
Buy E-book (.pdf)
Table of contents:
1. Introduction
2. Background
3. Basic Technical Settings
4. Linearizability and Contextual Refinement
5. Progress Properties
6. Progress-Aware Abstraction
7. Verifying Progress of Concurrent Objects
8. Related Work
9. Conclusion and Future Work
Acknowledgements
References

Progress of Concurrent Objects

Implementations of concurrent objects in programming languages should guarantee linearizability and a progress property. These progress properties describe conditions under which a method call is guaranteed to complete. However, they fail to describe how clients are affected, making it difficult to utilize them in layered and modular program verification. Even worse, none of the existing results applies to concurrent objects with partial methods.

Progress of Concurrent Objects examines the progress properties of concurrent objects. It formulates each progress property in terms of contextual refinement so that, when verifying clients of the objects, concrete object implementations can be replaced with their abstractions with certainty, achieving modular verification. For concurrent objects with partial methods, two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF) are described. Finally, a rely-guarantee style program logic LiLi for verifying linearizability and progress together for concurrent objects is introduced.

This tutorial is intended for use by researchers and students. It surveys the current state of the topic and introduces the reader to recent advances in a tutorial style that makes the topic accessible to newcomers to the field.

 
PGL-041