Foundations and TrendsR in Programming Languages Progress of Concurrent Objects 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.D0l:10.1561/2500000041. 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 This article may be used only for the purpose of research,teaching. now and/or private study.Commercial use or systematic downloading (by robots or other automatic processes)is prohibited without ex- the essence of knowledge plicit Publisher approval. Boston-Delft
Foundations and Trends R in Programming Languages Progress of Concurrent Objects Suggested Citation: Hongjin Liang and Xinyu Feng (2020), “Progress of Concurrent Objects”, Foundations and Trends R in Programming Languages: Vol. 5, No. 4, pp 282–414. DOI: 10.1561/2500000041. 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 This article may be used only for the purpose of research, teaching, and/or private study. Commercial use or systematic downloading (by robots or other automatic processes) is prohibited without explicit Publisher approval. Boston — Delft
Contents 1 Introduction 284 1.1 General Motivation.......·..···· ··。 286 1.2 Overview....... 289 2 Background 291 2.1 Linearizability.... .·.291 2.2 Progress Properties.··· 293 2.3 Contextual Refinement and Abstraction Theorems.....297 2.4 Verifying Progress Properties................303 3 Basic Technical Settings 313 3.1 The Language················ 313 3.2 Execution Traces and Fairness of Scheduling.·:····· 319 4 Linearizability and Contextual Refinement 322 4.1 Linearizability 322 4.2 Contextual Refinement and Abstraction····. 324 5 Progress Properties 325 5.1 Progress for Objects with Total Methods Only.······ 325 5.2 Progress for Objects with Partial Methods..··.··.·327
Contents 1 Introduction 284 1.1 General Motivation . . . . . . . . . . . . . . . . . . . . . 286 1.2 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . 289 2 Background 291 2.1 Linearizability . . . . . . . . . . . . . . . . . . . . . . . . 291 2.2 Progress Properties . . . . . . . . . . . . . . . . . . . . . 293 2.3 Contextual Refinement and Abstraction Theorems . . . . . 297 2.4 Verifying Progress Properties . . . . . . . . . . . . . . . . 303 3 Basic Technical Settings 313 3.1 The Language . . . . . . . . . . . . . . . . . . . . . . . . 313 3.2 Execution Traces and Fairness of Scheduling . . . . . . . . 319 4 Linearizability and Contextual Refinement 322 4.1 Linearizability . . . . . . . . . . . . . . . . . . . . . . . . 322 4.2 Contextual Refinement and Abstraction . . . . . . . . . . 324 5 Progress Properties 325 5.1 Progress for Objects with Total Methods Only . . . . . . . 325 5.2 Progress for Objects with Partial Methods . . . . . . . . . 327
6 Progress-Aware Abstraction 331 6.1 Overview of Our Results..················ 331 6.2 Formalizing Progress-Aware Contextual Refinements.... 334 6.3 Abstraction for Wait-Free and Lock-Free Objects 337 6.4 Abstraction for Starvation-Free and Deadlock-Free Objects 341 6.5 Abstraction for PSF and PDF Objects........... 342 7 Verifying Progress of Concurrent Objects 349 7.1 Challenges and Key ldeas.·.··· 349 7.2 The Program Logic LiLi...... 356 7.3 Soundness 385 7.4 Examples...···· 387 8 Related Work 397 8.1 Progress Properties and Abstraction 397 8.2 Verification.......··············· 398 8.3 Comparison with TaDA-Live ....... 401 9 Conclusion and Future Work 406 Acknowledgements 409 References 410
6 Progress-Aware Abstraction 331 6.1 Overview of Our Results . . . . . . . . . . . . . . . . . . . 331 6.2 Formalizing Progress-Aware Contextual Refinements . . . . 334 6.3 Abstraction for Wait-Free and Lock-Free Objects . . . . . 337 6.4 Abstraction for Starvation-Free and Deadlock-Free Objects 341 6.5 Abstraction for PSF and PDF Objects . . . . . . . . . . . 342 7 Verifying Progress of Concurrent Objects 349 7.1 Challenges and Key Ideas . . . . . . . . . . . . . . . . . . 349 7.2 The Program Logic LiLi . . . . . . . . . . . . . . . . . . . 356 7.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . 385 7.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . 387 8 Related Work 397 8.1 Progress Properties and Abstraction . . . . . . . . . . . . 397 8.2 Verification . . . . . . . . . . . . . . . . . . . . . . . . . . 398 8.3 Comparison with TaDA-Live . . . . . . . . . . . . . . . . 401 9 Conclusion and Future Work 406 Acknowledgements 409 References 410
Progress of Concurrent Objects Hongjin Liangl and Xinyu Feng2 1State Key Laboratory for Novel Software Technology,Nanjing University;China;hongjin@nju.edu.cn 2State Key Laboratory for Novel Software Technology,Nanjing University,China;ryfeng@nju.edu.cn ABSTRACT Implementations of concurrent objects should guarantee lin- earizability 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 fair- ness 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 cer- tain 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 concur- rent 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, Hongjin Liang and Xinyu Feng(2020),"Progress of Concurrent Objects",Founda- tions and Trends in Programming Languages:Vol.5,No.4,pp 282-414.DOI: 10.1561/2500000041
Progress of Concurrent Objects Hongjin Liang1 and Xinyu Feng2 1State Key Laboratory for Novel Software Technology, Nanjing University, China; hongjin@nju.edu.cn 2State Key Laboratory for Novel Software Technology, Nanjing University, China; xyfeng@nju.edu.cn 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, Hongjin Liang and Xinyu Feng (2020), “Progress of Concurrent Objects”, Foundations and Trends R in Programming Languages: Vol. 5, No. 4, pp 282–414. DOI: 10.1561/2500000041
283 when verifying clients of the objects,we can soundly re- place the concrete object implementations with their ab- stractions,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 re- fine 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
283 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 re- fine their abstractions. Finally, we introduce a rely-guarantee style program logic LiLi for verifying linearizability and progress together for concurrent objects. It unifies threadmodular reasoning about all the six progress properties (wait-freedom, lock-freedom, starvation-freedom, deadlockfreedom, PSF and PDF) in one framework. We have successfully applied LiLi to verify starvation-freedom or deadlock-freedom of representative algorithms such as lockcoupling lists, optimistic lists and lazy lists, and PSF or PDF of lock algorithms