Modular Verification of Linearizability with Non-Fixed Linearization Points Hongjin Liang Xinyu Feng University of Science and Technology of China lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn Abstract intended operation.When a thread A detects conflicts with another Locating linearization points (LPs)is an intuitive approach for thread B,A may access B's descriptor and help B finish its intended proving linearizability.but it is difficult to apply the idea in Hoare- operation first before finishing its own.In this case,B's operation style logic for formal program verification,especially for verify- takes effect at a step from A.Thus its LP should not be in its own ing algorithms whose LPs cannot be statically located in the code code,but in the code of thread A. In this paper,we propose a program logic with a lightweight in- Besides,in optimistic algorithms and lazy algorithms (e.g., strumentation mechanism which can verify algorithms with non- Heller et al.'s lazy set [13)).the LPs might depend on unpredictable fixed LPs,including the most challenging ones that use the help- future interleavings.In those algorithms,a thread may access the ing mechanism to achieve lock-freedom (as in HSY elimination- shared states as if no interference would occur,and validate the based stack),or have LPs depending on unpredictable future exe- accesses later.If the validation succeeds,it finishes the operation; cutions (as in the lazy set algorithm),or involve both features.We otherwise it rolls back and retries.Its LP is usually at a prior state also develop a thread-local simulation as the meta-theory of our access,but only if the later validation succeeds. logic,and show it implies contextual refinement,which is equiv- Reasoning about algorithms with non-fixed LPs has been a alent to linearizability.Using our logic we have successfully ver- long-standing problem.Most existing work either supports only ified various classic algorithms,some of which are used in the simple objects with static LPs in the implementation code (e.g..[2. java.util.concurrent package. 5,19,301).or lacks formal soundness arguments (e.g.,[321).In this paper,we propose a program logic for verification of linearizability Categories and Subject Descriptors D.2.4 [Software Engineer- with non-fixed LPs.For a concrete implementation of an object ing]:Software/Program Verification-Correctness proofs,Formal method,we treat the corresponding abstract atomic operation and methods;F.3.1 [Logics and Meanings of Programs]:Specifying the abstract state as auxiliary states,and insert auxiliary commands and Verifying and Reasoning about Programs at the LP to execute the abstract operation simultaneously with the concrete step.We verify the instrumented implementation in General Terms Theory,Verification an existing concurrent program logic (we will use LRG [8]in Keywords Concurrency;Rely-Guarantee Reasoning;Lineariz- this paper),but extend it with new logic rules for the auxiliary ability;Refinement;Simulation commands.We also give a new relational interpretation to the logic assertions,and show that at the LP,the step of the original concrete 1.Introduction implementation has the same effect as the abstract operation.We handle non-fixed LPs in the following way: Linearizability is a standard correctness criterion for concurrent ob- ject implementations [16].It requires the fine-grained implementa- To support the helping mechanism,we collect a pending thread tion of an object operation to have the same effect with an instanta- pool as auxiliary state,which is a set of threads and their neous atomic operation.To prove linearizability,the most intuitive abstract operations that might be helped.We allow the thread approach is to find a linearization point(LP)in the code of the im- that is currently being verified to use auxiliary commands to plementation,and show that it is the single point where the effect help execute the abstract operations in the pending thread pool of the operation takes place. For future-dependent LPs,we introduce a try-commit mecha- However,it is difficult to apply this idea when the LPs are not nism to reason with uncertainty.The try clause guesses whether fixed in the code of object methods.For a large class of lock- the corresponding abstract operation should be executed and free algorithms with helping mechanism (e.g.,HSY elimination- keeps all possibilities,while commit chooses a specific pos- based stack [14]),the LP of one method might be in the code sible case when we know which guess is correct later. of some other method.In these algorithms,each thread maintains Although our program logic looks intuitive,it is challenging to a descriptor recording all the information required to fulfill its prove that the logic is sound w.r.t.linearizability.Recent work has shown the equivalence between linearizability and contextual re- finement [5,9,10].The latter is often verified by proving simula- tions between the concrete implementation and the atomic opera- 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 tion [5].The simulation establishes some correspondence between the executions of the two sides,showing there exists one step in for profit or commercial advantage and that copies bear this notice and the full citation nthe first page.To copy otherwise,to republish,to post to redistribute the concrete execution that fulfills the abstract operation.Given the to lists,requires prior specific permission and/or a fee equivalence between linearizability and refinement,we would ex- PLDI'13,June 16-19,2013,Seattle,WA,USA pect the simulations to justify the soundness of the LP method and Copyright©2013ACM978-1-4503-2014-6/1306..s15.00 to serve as the meta-theory of our logic.However,existing thread- 459Modular Verification of Linearizability with Non-Fixed Linearization Points Hongjin Liang Xinyu Feng University of Science and Technology of China lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn Abstract Locating linearization points (LPs) is an intuitive approach for proving linearizability, but it is difficult to apply the idea in Hoare￾style logic for formal program verification, especially for verify￾ing algorithms whose LPs cannot be statically located in the code. In this paper, we propose a program logic with a lightweight in￾strumentation mechanism which can verify algorithms with non- fixed LPs, including the most challenging ones that use the help￾ing mechanism to achieve lock-freedom (as in HSY elimination￾based stack), or have LPs depending on unpredictable future exe￾cutions (as in the lazy set algorithm), or involve both features. We also develop a thread-local simulation as the meta-theory of our logic, and show it implies contextual refinement, which is equiv￾alent to linearizability. Using our logic we have successfully ver￾ified various classic algorithms, some of which are used in the java.util.concurrent package. 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; Rely-Guarantee Reasoning; Lineariz￾ability; Refinement; Simulation 1. Introduction Linearizability is a standard correctness criterion for concurrent ob￾ject implementations [16]. It requires the fine-grained implementa￾tion of an object operation to have the same effect with an instanta￾neous atomic operation. To prove linearizability, the most intuitive approach is to find a linearization point (LP) in the code of the im￾plementation, and show that it is the single point where the effect of the operation takes place. However, it is difficult to apply this idea when the LPs are not fixed in the code of object methods. For a large class of lock￾free algorithms with helping mechanism (e.g., HSY elimination￾based stack [14]), the LP of one method might be in the code of some other method. In these algorithms, each thread maintains a descriptor recording all the information required to fulfill its 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. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. PLDI’13, June 16–19, 2013, Seattle, WA, USA. Copyright c 2013 ACM 978-1-4503-2014-6/13/06. . . $15.00 intended operation. When a thread A detects conflicts with another thread B, A may access B’s descriptor and help B finish its intended operation first before finishing its own. In this case, B’s operation takes effect at a step from A. Thus its LP should not be in its own code, but in the code of thread A. Besides, in optimistic algorithms and lazy algorithms (e.g., Heller et al.’s lazy set [13]), the LPs might depend on unpredictable future interleavings. In those algorithms, a thread may access the shared states as if no interference would occur, and validate the accesses later. If the validation succeeds, it finishes the operation; otherwise it rolls back and retries. Its LP is usually at a prior state access, but only if the later validation succeeds. Reasoning about algorithms with non-fixed LPs has been a long-standing problem. Most existing work either supports only simple objects with static LPs in the implementation code (e.g., [2, 5, 19, 30]), or lacks formal soundness arguments (e.g., [32]). In this paper, we propose a program logic for verification of linearizability with non-fixed LPs. For a concrete implementation of an object method, we treat the corresponding abstract atomic operation and the abstract state as auxiliary states, and insert auxiliary commands at the LP to execute the abstract operation simultaneously with the concrete step. We verify the instrumented implementation in an existing concurrent program logic (we will use LRG [8] in this paper), but extend it with new logic rules for the auxiliary commands. We also give a new relational interpretation to the logic assertions, and show that at the LP, the step of the original concrete implementation has the same effect as the abstract operation. We handle non-fixed LPs in the following way: • To support the helping mechanism, we collect a pending thread pool as auxiliary state, which is a set of threads and their abstract operations that might be helped. We allow the thread that is currently being verified to use auxiliary commands to help execute the abstract operations in the pending thread pool. • For future-dependent LPs, we introduce a try-commit mecha￾nism to reason with uncertainty. The try clause guesses whether the corresponding abstract operation should be executed and keeps all possibilities, while commit chooses a specific pos￾sible case when we know which guess is correct later. Although our program logic looks intuitive, it is challenging to prove that the logic is sound w.r.t. linearizability. Recent work has shown the equivalence between linearizability and contextual re- finement [5, 9, 10]. The latter is often verified by proving simula￾tions between the concrete implementation and the atomic opera￾tion [5]. The simulation establishes some correspondence between the executions of the two sides, showing there exists one step in the concrete execution that fulfills the abstract operation. Given the equivalence between linearizability and refinement, we would ex￾pect the simulations to justify the soundness of the LP method and to serve as the meta-theory of our logic. However, existing thread- 459