A Program Logic for Concurrent Objects under Fair Scheduling Hongjin Liang Xinyu Feng School of Computer Science and Technology Suzhou Institute for Advanced Study University of Science and Technology of China Ihj1018@ustc.edu.cn xyfengOustc.edu.cn Abstract In addition to linearizability,a safety property,object imple- Existing work on verifying concurrent objects is mostly concerned mentations are expected to also satisfy progress properties.The with safety only,e.g.,partial correctness or linearizability.Although non-blocking progress properties,such as wait-freedom and lock- there has been recent work verifying lock-freedom of non-blocking freedom which have been studied a lot (e.g..[5,10,16,24]).guar- antee the termination of the method calls independently of how the objects,much less efforts are focused on deadlock-freedom and threads are scheduled.Unfortunately these properties are too strong starvation-freedom,progress properties of blocking objects.These properties are more challenging to verify than lock-freedom because to be satisfied by algorithms with blocking synchronization.For clients using lock-based objects,a delay of a thread holding a lock they allow the progress of one thread to depend on the progress of will block other threads requesting the lock.Thus their progress another,assuming fair scheduling. relies on the assumption that every thread holding the lock will We propose LiLi,a new rely-guarantee style program logic for eventually be scheduled to release it.This assumption requires fair verifying linearizability and progress together for concurrent objects under fair scheduling.The rely-guarantee style logic unifies thread- scheduling,i.e.,every thread gets eventually executed.As summa- modular reasoning about both starvation-freedom and deadlock rized by Herlihy and Shavit [14].there are two desirable progress freedom in one framework.It also establishes progress-aware properties for blocking algorithms,both assuming fair scheduling: abstraction for concurrent objects,which can be applied when Deadlock-freedom:In each fair execution,there always exists verifying safety and liveness of client code.We have successfully some method call that can finish.It disallows the situation in applied the logic to verify starvation-freedom or deadlock-freedom which multiple threads requesting locks are waiting for each of representative algorithms such as ticket locks,queue locks,lock- other to release the locks in hand.It ensures the absence of coupling lists,optimistic lists and lazy lists. livelock.but not starvation. Categories and Subject Descriptors D.2.4 [Software Engineer- Starvation-freedom:Every method call should finish in fair ing]:Software/Program Verification-Correctness proofs,Formal executions.It requires that every thread attempting to acquire methods;F.3.1 [Logics and Meanings of Programs]:Specifying a lock should eventually succeed and in the end release the and Verifying and Reasoning about Programs lock.Starvation-freedom is stronger than deadlock-freedom. Nevertheless it can often be achieved by using fair locks [13]. General Terms Theory,Verification Recent program logics for verifying concurrent objects either Keywords Concurrency,Progress,Program Logic,Rely-Guarantee prove only linearizability and ignore the issue of termination (e.g.,[6, Reasoning,Refinement 21,30,311),or aim for non-blocking progress properties(e.g.,[5. 10,16,24]),which cannot be applied to blocking algorithms that progress only under fair scheduling.The fairness assumption intro- 1.Introduction duces complicated interdependencies among progress properties of A concurrent object or library provides a set of methods that al- threads,making it incredibly more challenging to verify the lock- low multiple client threads to manipulate the shared data structure. based algorithms than their non-blocking counterparts.We will Blocking synchronization (i.e..mutual exclusion locks),as a straight explain the challenges in detail in Sec.2. forward technique to ensure exclusive accesses and to control the It is important to note that,although there has been much work interference,has been widely-used in object implementations to on deadlock detection or deadlock-freedom verification (e.g.,[4,20. achieve linearizability,which ensures the object methods behave as 32]),deadlock-freedom is often defined as a safety property,which atomic operations in a concurrent setting. 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 Permission to make digital or hard copies of all or part of this work for classroom use is granted without fee wided that are not made or distribut achieved using spin-locks implemented by the programmers).The for profit or commercial advantage and that copic sbear this notice and the full citati deadlock-freedom we discuss in this paper is a liveness property and on the first page.Copyrights for components of this work owned by others than AC must be honored.Abstracting with credit is permitted.To copy otherwise,or republish. its definition does not rely on built-in lock primitives.We discuss to post on servers or to redistribute to lists,requires prior specific permission and/or a more related work on liveness verification in Sec.8. fee.Request permissions from Permissions@acm.org. In this paper we propose LiLi,a new rely-guarantee style logic POPL'/6,January 20-22,2016,St.Petersburg,FL.USA for concurrent objects under fair scheduling.LiLi is the first program logic that unifies verification of linearizability,starvation-freedom and deadlock-freedom in one framework (the name LiLi stands for 385A Program Logic for Concurrent Objects under Fair Scheduling Hongjin Liang Xinyu Feng School of Computer Science and Technology & Suzhou Institute for Advanced Study University of Science and Technology of China lhj1018@ustc.edu.cn xyfeng@ustc.edu.cn Abstract Existing 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 deadlock-freedom and starvation-freedom, progress properties of blocking objects. These properties are more challenging to verify than lock-freedom because they allow the progress of one thread to depend on the progress of another, assuming fair scheduling. We propose LiLi, a new rely-guarantee style program logic for verifying linearizability and progress together for concurrent objects under fair scheduling. The rely-guarantee style logic unifies thread￾modular reasoning about both starvation-freedom and deadlock￾freedom in one framework. It also establishes progress-aware abstraction for concurrent objects, which can be applied when verifying safety and liveness of client code. We have successfully applied the logic to verify starvation-freedom or deadlock-freedom of representative algorithms such as ticket locks, queue locks, lock￾coupling lists, optimistic lists and lazy lists. Categories and Subject Descriptors D.2.4 [Software Engineer￾ing]: Software/Program Verification – Correctness proofs, Formal methods; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Theory, Verification Keywords Concurrency, Progress, Program Logic, Rely-Guarantee Reasoning, Refinement 1. Introduction A concurrent object or library provides a set of methods that al￾low multiple client threads to manipulate the shared data structure. Blocking synchronization (i.e., mutual exclusion locks), as a straight￾forward technique to ensure exclusive accesses and to control the interference, has been widely-used in object implementations to achieve linearizability, which ensures the object methods behave as atomic operations in a concurrent setting. In addition to linearizability, a safety property, object imple￾mentations are expected to also satisfy progress properties. The non-blocking progress properties, such as wait-freedom and lock￾freedom which have been studied a lot (e.g., [5, 10, 16, 24]), guar￾antee the termination of the method calls independently of how the threads are scheduled. Unfortunately these properties are too strong to be satisfied by algorithms with blocking synchronization. For clients using lock-based objects, a delay of a thread holding a lock will block other threads requesting the lock. Thus their progress relies on the assumption that every thread holding the lock will eventually be scheduled to release it. This assumption requires fair scheduling, i.e., every thread gets eventually executed. As summa￾rized by Herlihy and Shavit [14], there are two desirable progress properties for blocking algorithms, both assuming fair scheduling: • Deadlock-freedom: In each fair execution, there always exists some method call that can finish. It disallows the situation in which multiple threads requesting locks are waiting for each other to release the locks in hand. It ensures the absence of livelock, but not starvation. • Starvation-freedom: Every method call should finish in fair executions. It requires that every thread attempting to acquire a lock should eventually succeed and in the end release the lock. Starvation-freedom is stronger than deadlock-freedom. Nevertheless it can often be achieved by using fair locks [13]. Recent program logics for verifying concurrent objects either prove only linearizability and ignore the issue of termination (e.g., [6, 21, 30, 31]), or aim for non-blocking progress properties (e.g., [5, 10, 16, 24]), which cannot be applied to blocking algorithms that progress only under fair scheduling. The fairness assumption intro￾duces complicated interdependencies among progress properties of threads, making it incredibly more challenging to verify the lock￾based algorithms than their non-blocking counterparts. We will explain the challenges in detail in Sec. 2. It is important to note that, although there has been much work on deadlock detection or deadlock-freedom verification (e.g., [4, 20, 32]), 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 paper is a liveness property and its definition does not rely on built-in lock primitives. We discuss more related work on liveness verification in Sec. 8. In this paper we propose LiLi, a new rely-guarantee style logic for concurrent objects under fair scheduling. LiLi is the first program logic that unifies verification of linearizability, starvation-freedom and deadlock-freedom in one framework (the name LiLi stands for 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 Permissions@acm.org. POPL’16, January 20–22, 2016, St. Petersburg, FL, USA c 2016 ACM. 978-1-4503-3549-2/16/01...$15.00 http://dx.doi.org/10.1145/2837614.2837635 385