Foundations and Trends in Programming Languages：Progress of Concurrent Objects

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 ex￾plicit 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 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 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 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

1 Introduction A concurrent object consists of shared data and a set of methods which provide an interface for client threads to access the shared data.Lineariz- ability (Herlihy and Wing,1990)has been used as a standard definition of the correctness of concurrent object implementations.It describes safety and functionality,but has no requirement about termination of object methods.Various progress properties,such as wait-freedom,lock- freedom,starvation-freedom and deadlock-freedom,have been proposed to specify termination of object methods.In their textbook Herlihy and Shavit (2008)give a systematic introduction of these properties. Although program termination has been an obvious notion for sequential programs,it becomes much more complex in a concurrent setting.Termination of a method call in a thread is affected not only by the sequential behavior of the method code,but also by interference from the environment.Different implementations of the concurrent object methods have different tolerance of the interference.That's why we need these different progress properties. We give two implementations of a simple counter object in Figure 1.1. The variable x (line 0)is the object data implementing the counter. Figure 1.1(a)and (b)are two different implementations of the inc 284

1 Introduction A concurrent object consists of shared data and a set of methods which provide an interface for client threads to access the shared data. Lineariz￾ability (Herlihy and Wing, 1990) has been used as a standard definition of the correctness of concurrent object implementations. It describes safety and functionality, but has no requirement about termination of object methods. Various progress properties, such as wait-freedom, lock￾freedom, starvation-freedom and deadlock-freedom, have been proposed to specify termination of object methods. In their textbook Herlihy and Shavit (2008) give a systematic introduction of these properties. Although program termination has been an obvious notion for sequential programs, it becomes much more complex in a concurrent setting. Termination of a method call in a thread is affected not only by the sequential behavior of the method code, but also by interference from the environment. Different implementations of the concurrent object methods have different tolerance of the interference. That’s why we need these different progress properties. We give two implementations of a simple counter object in Figure 1.1. The variable x (line 0) is the object data implementing the counter. Figure 1.1(a) and (b) are two different implementations of the inc 284

285 0 int x;//object data 1 inc(){ 2 local t,done :=false; 8 inc(){ 3 while(!done){ 9 lock(); 4 t:=x; 10 X:=X+1; 5 done :cas(&x,t,t+1); 11 unlock(); 6 12J 7 (a) (b) Figure 1.1:Implementations of the counter object. method,which increments the counter.Figure 1.1(a)shows an optimistic implementation.It takes a snapshot t of the counter (line 4).The atomic compare-and-swap(cas)command (line 5)compares the current value of x with t.If they are equal,it atomically sets x to t+1 and returns true.Otherwise it does nothing and returns false,and the method has to run another round of the loop to roll back and retry the process. Figure 1.1(b)is a lock-based implementation,where the update of the shared variable x is protected by a lock.Here we omit the implementation of locks,which will be discussed later. The different implementations of the inc method have different progress properties.We can consider the following client program to see their difference.The formal definitions of progress properties will be discussed later in Section 5. inc()while(true){inc(); If we use the optimistic version in Figure 1.1(a),the call of inc()in the left thread may never terminates because the cas command at line 5 may always fail due to the infinite number of calls of inc()in the right thread.However,whenever we suspend the execution of the right thread,the inc()in the left eventually terminates.Therefore we call Figure 1.1(a)a non-blocking implementation.Also,since at least one of the call of inc()in the whole program terminates,this is a lock-free implementation

285 0 int x; //object data 1 inc(){ 2 local t, done := false; 3 while(!done){ 4 t := x; 5 done := cas(&x, t, t+1); 6 } 7 } 8 inc(){ 9 lock(); 10 x := x+1; 11 unlock(); 12 } (a) (b) Figure 1.1: Implementations of the counter object. method, which increments the counter. Figure 1.1(a) shows an optimistic implementation. It takes a snapshot t of the counter (line 4). The atomic compare-and-swap (cas) command (line 5) compares the current value of x with t. If they are equal, it atomically sets x to t+1 and returns true. Otherwise it does nothing and returns false, and the method has to run another round of the loop to roll back and retry the process. Figure 1.1(b) is a lock-based implementation, where the update of the shared variable x is protected by a lock. Here we omit the implementation of locks, which will be discussed later. The different implementations of the inc method have different progress properties. We can consider the following client program to see their difference. The formal definitions of progress properties will be discussed later in Section 5. inc() k while(true){ inc(); } If we use the optimistic version in Figure 1.1(a), the call of inc() in the left thread may never terminates because the cas command at line 5 may always fail due to the infinite number of calls of inc() in the right thread. However, whenever we suspend the execution of the right thread, the inc() in the left eventually terminates. Therefore we call Figure 1.1(a) a non-blocking implementation. Also, since at least one of the call of inc() in the whole program terminates, this is a lock-free implementation

286 Introduction If we use the lock-based inc in Figure 1.1(b),whether the call of inc()in the left thread terminates or not depends on the implemen- tation of the lock.If the lock implementation is fair,the inc()on the left always terminates,otherwise it may always fail to acquire the lock and may never terminate.In both cases,if we suspend the right thread when it is executing line 10,the inc()on the left cannot terminate because it can never acquire the lock (which has been taken by the suspended right thread).So we say the lock-based implementation of inc is blocking.The termination of a method call relies on both the lock algorithm and the fairness of scheduling. The goal of this tutorial is to help the reader understand the various 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.We also introduce a program logic LiLi to formally verify progress properties. 1.1 General Motivation 1.1.1 Progress-Aware Abstraction Progress properties describe conditions under which method calls are guaranteed to successfully complete in an execution.For example,lock- freedom guarantees that "infinitely often some method call finishes in a finite number of steps"(Herlihy and Shavit,2008).They are difficult to use in a modular and layered program verification because they fail to describe how the progress properties affect clients. In a modular verification of client threads,the concrete implemen- tation II of the object methods should be replaced by an abstraction (or specification)II'that consists of equivalent methods.The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses II instead of II'.In particular,we are interested in systematically studying whether the termination of a client using the abstract methods II'will be preserved when using an implementation II with some progress guarantee

286 Introduction If we use the lock-based inc in Figure 1.1(b), whether the call of inc() in the left thread terminates or not depends on the implemen￾tation of the lock. If the lock implementation is fair, the inc() on the left always terminates, otherwise it may always fail to acquire the lock and may never terminate. In both cases, if we suspend the right thread when it is executing line 10, the inc() on the left cannot terminate because it can never acquire the lock (which has been taken by the suspended right thread). So we say the lock-based implementation of inc is blocking. The termination of a method call relies on both the lock algorithm and the fairness of scheduling. The goal of this tutorial is to help the reader understand the various 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. We also introduce a program logic LiLi to formally verify progress properties. 1.1 General Motivation 1.1.1 Progress-Aware Abstraction Progress properties describe conditions under which method calls are guaranteed to successfully complete in an execution. For example, lock￾freedom guarantees that “infinitely often some method call finishes in a finite number of steps” (Herlihy and Shavit, 2008). They are difficult to use in a modular and layered program verification because they fail to describe how the progress properties affect clients. In a modular verification of client threads, the concrete implemen￾tation Π of the object methods should be replaced by an abstraction (or specification) Π0 that consists of equivalent methods. The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses Π instead of Π0 . In particular, we are interested in systematically studying whether the termination of a client using the abstract methods Π0 will be preserved when using an implementation Π with some progress guarantee

1.1.General Motivation 287 Previous work on verifying the safety of concurrent objects (e.g., Filipovic et al.,2009;Liang and Feng,2013)has shown that linearizabil- ity-a standard safety criterion for concurrent objects-and contextual refinement are equivalent.Informally,an implementation II is a con- textual refinement of a(more abstract)implementation II',if every observable behavior of any client program using II can also be observed when the client uses II'instead.To obtain equivalence to linearizability, the observable behaviors include I/O events but not divergence (i.e., non-termination).Recently,Gotsman and Yang(2011)showed that a client program that diverges using a linearizable and lock-free object must also diverge when using the abstract operations instead.Their work reveals a connection between lock-freedom and a form of contex- tual refinement which preserves termination as well as safety properties. It is unclear how other progress guarantees affect termination of client programs and how they are related to contextual refinements. This tutorial studies four commonly used progress properties (wait- freedom,lock-freedom,starvation-freedom and deadlock-freedom)and their relationships to contextual refinements.We show that,when progress properties are taken into account,one may have the corre- sponding progress-aware contextual refinement to reestablish the equiv- alence.We give different abstract specifications II'for different progress properties.The equivalence results allow us to build abstractions for linearizable objects so that safety and progress of the client code can be reasoned about at a more abstract level. 1.1.2 Program Logic for Progress Verification Recent program logics for verifying concurrent objects either prove only linearizability and ignore the issue of termination (e.g.,Derrick et al, 2011;Liang and Feng,2013;Turon et al.,2013a;Vafeiadis,2008),or aim for non-blocking progress properties (e.g.,da Rocha Pinto et al., 2016;Gotsman et al.,2009;Hoffmann et al.,2013;Liang et al.,2014), which cannot be applied to blocking algorithms that progress only under fair scheduling.The fairness assumption introduces complicated interdependencies among progress properties of threads,making it incredibly more challenging to verify the lock-based algorithms than

1.1. General Motivation 287 Previous work on verifying the safety of concurrent objects (e.g., Filipović et al., 2009; Liang and Feng, 2013) has shown that linearizabil￾ity—a standard safety criterion for concurrent objects—and contextual refinement are equivalent. Informally, an implementation Π is a con￾textual refinement of a (more abstract) implementation Π0 , if every observable behavior of any client program using Π can also be observed when the client uses Π0 instead. To obtain equivalence to linearizability, the observable behaviors include I/O events but not divergence (i.e., non-termination). Recently, Gotsman and Yang (2011) showed that a client program that diverges using a linearizable and lock-free object must also diverge when using the abstract operations instead. Their work reveals a connection between lock-freedom and a form of contex￾tual refinement which preserves termination as well as safety properties. It is unclear how other progress guarantees affect termination of client programs and how they are related to contextual refinements. This tutorial studies four commonly used progress properties (wait￾freedom, lock-freedom, starvation-freedom and deadlock-freedom) and their relationships to contextual refinements. We show that, when progress properties are taken into account, one may have the corre￾sponding progress-aware contextual refinement to reestablish the equiv￾alence. We give different abstract specifications Π0 for different progress properties. The equivalence results allow us to build abstractions for linearizable objects so that safety and progress of the client code can be reasoned about at a more abstract level. 1.1.2 Program Logic for Progress Verification Recent program logics for verifying concurrent objects either prove only linearizability and ignore the issue of termination (e.g., Derrick et al., 2011; Liang and Feng, 2013; Turon et al., 2013a; Vafeiadis, 2008), or aim for non-blocking progress properties (e.g., da Rocha Pinto et al., 2016; Gotsman et al., 2009; Hoffmann et al., 2013; Liang et al., 2014), which cannot be applied to blocking algorithms that progress only under fair scheduling. The fairness assumption introduces complicated interdependencies among progress properties of threads, making it incredibly more challenging to verify the lock-based algorithms than

288 Introduction their non-blocking counterparts.We will explain the challenges in detail in Subsection 7.1. It is important to note that,although there has been much work on deadlock detection or deadlock-freedom verification (e.g.,Boyapati et al.,2002;Leino et al.,2010;Williams et al.,2005),deadlock-freedom is often defined as a safety property,which ensures the lack of circular waiting for locks.It does not prevent live-lock or non-termination inside the critical section.Another limitation of this kind of work is that it often assumes built-in lock primitives,and lacks support of ad-hoc synchronization (e.g.,mutual exclusion achieved using spin-locks implemented by the programmers).The deadlock-freedom we discuss in this tutorial is a liveness property and its definition does not rely on built-in lock primitives.We discuss more related work on liveness verification in Section 8. In this tutorial we introduce LiLi,a new rely-guarantee style logic for concurrent objects.It unifies verification of linearizability,wait- freedom,lock-freedom,starvation-freedom and deadlock-freedom in one framework (the name LiLi stands for Linearizability and Liveness). In particular,it supports verification of both mutex-based pessimistic algorithms (including fine-grained ones such as lock-coupling lists)and optimistic ones such as optimistic lists and lazy lists.The unified approach allows us to prove in the same logic,for instance,the lock- coupling list algorithm is starvation-free if we use fair locks,e.g.,ticket locks (Mellor-Crummey and Scott,1991),and is deadlock-free if regular test-and-set based spin locks (Herlihy and Shavit,2008)are used. 1.1.3 Concurrent Objects with Partial Methods However,none of the aforementioned progress-related results applies to concurrent objects with partial methods!A method is partial if it is 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.Concurrent objects with partial methods simply do not satisfy any of the aforementioned progress properties,and people do not know how to give progress-aware abstract specifications for them either.The existing studies on progress properties and progress-aware

288 Introduction their non-blocking counterparts. We will explain the challenges in detail in Subsection 7.1. It is important to note that, although there has been much work on deadlock detection or deadlock-freedom verification (e.g., Boyapati et al., 2002; Leino et al., 2010; Williams et al., 2005), deadlock-freedom is often defined as a safety property, which ensures the lack of circular waiting for locks. It does not prevent live-lock or non-termination inside the critical section. Another limitation of this kind of work is that it often assumes built-in lock primitives, and lacks support of ad-hoc synchronization (e.g., mutual exclusion achieved using spin-locks implemented by the programmers). The deadlock-freedom we discuss in this tutorial is a liveness property and its definition does not rely on built-in lock primitives. We discuss more related work on liveness verification in Section 8. In this tutorial we introduce LiLi, a new rely-guarantee style logic for concurrent objects. It unifies verification of linearizability, wait￾freedom, lock-freedom, starvation-freedom and deadlock-freedom in one framework (the name LiLi stands for Linearizability and Liveness). In particular, it supports verification of both mutex-based pessimistic algorithms (including fine-grained ones such as lock-coupling lists) and optimistic ones such as optimistic lists and lazy lists. The unified approach allows us to prove in the same logic, for instance, the lock￾coupling list algorithm is starvation-free if we use fair locks, e.g., ticket locks (Mellor-Crummey and Scott, 1991), and is deadlock-free if regular test-and-set based spin locks (Herlihy and Shavit, 2008) are used. 1.1.3 Concurrent Objects with Partial Methods However, none of the aforementioned progress-related results applies to concurrent objects with partial methods! A method is partial if it is 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. Concurrent objects with partial methods simply do not satisfy any of the aforementioned progress properties, and people do not know how to give progress-aware abstract specifications for them either. The existing studies on progress properties and progress-aware