Compositional Verification of Termination-Preserving Refinement of Concurrent Programs Hongjin Liangt Xinyu Fengt Zhong Shaot University of Science and Technology of China +Yale University lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn zhong.shao@yale.edu Abstract should termination of the source be preserved too by the target?If Many verification problems can be reduced to refinement verifica- yes,how to verify such refinement? Preservation of termination is an indispensable requirement tion.However,existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination.al- in many refinement applications.For instance,compilation and lowing a diverging program to trivially refine any programs,or is optimizations are not allowed to transform a terminating source difficult to apply in compositional thread-local reasoning.In this program to a diverging (non-terminating)target.Also,implemen- paper,we first propose a new simulation technique,which estab- tations of concurrent data structures are often expected to have lishes termination-preserving refinement and is a congruence with progress guarantees (e.g.,lock-freedom and wait-freedom)in ad- respect to parallel composition.We then give a proof theory for the dition to linearizability.The requirements are equivalent to some simulation,which is the first Hoare-style concurrent program logic contextual refinements that preserve the termination of client pro- supporting termination-preserving refinement proofs.We show two grams [12]. key applications of our logic,i.e.,verifying linearizability and lock- Most existing approaches for verifying concurrent program freedom together for fine-grained concurrent objects,and verifying refinement,including simulations (e.g.,[11]),logical relations full correctness of optimizations of concurrent algorithms. (e.g..[221),and refinement logics (e.g.,[211).do not reason about the preservation of termination.As a result,a program that Categories and Subject Descriptors D.2.4 [Software Engineer- does an infinite loop without generating any external events,e.g ing]:Software/Program Verification-Correctness proofs,Formal while true do skip,would trivially refine any source program methods;F.3.1 [Logics and Meanings of Programs]:Specifying (just like that it trivially satisfies partial correctness in Hoare logic). and Verifying and Reasoning about Programs Certainly this kind of refinement is not acceptable in the applica- General Terms Theory,Verification tions mentioned above. CompCert [9]addresses the problem by introducing a well- Keywords Concurrency,Refinement,Termination Preservation, founded order in the simulation,but it works only for sequential Rely-Guarantee Reasoning.Simulation programs.It is difficult to apply this idea to do thread-local ver- ification of concurrent program refinement,which enables us to 1.Introduction know Ti Il T2 S1 ll S2 by proving T1 S1 and T2E S2 Verifying refinement between programs is the crux of many ver- In practice,the termination preservation in the refinement proofs of ification problems.For instance.reasoning about compilation or individual threads could be easily broken by the interference from their environments (i.e.,other threads running in parallel).For in- program transformations requires proving that every target pro- gram is a refinement of its source [9].In concurrent settings,re- stance,a method call of a lock-free data structure (e.g.,Treiber cent work [4.12]shows that the correctness of concurrent data stack)may never terminate when other threads call the methods structures and libraries can be characterized via some forms of con- and update the shared memory infinitely often.As we will explain in Sec.2,the key challenge here is to effectively specify the en textual refinements,i.e.,every client that calls the concrete library vironments'effects on the termination preservation of individual methods should refine the client with some abstract atomic oper- ations.Verification of concurrent garbage collectors [11]and OS threads.As far as we know,no previous work can use "composi- kernels [18]can also be reduced to refinement verification. tional"thread-local reasoning to verify termination-preserving re- finement between(whole)concurrent programs. Refinement from the source program S to the target T,written as T S,requires that T have no more observable behaviors In this paper,we first propose novel rely/guarantee conditions than S.Usually observable behaviors include the traces of external which can effectively specify the interference over the termina- tion properties between a thread and its environment.Traditional events such as 1/O operations and runtime errors.The question is rely/guarantee conditions [8]are binary relations of program states and they specify the state updates.We extend them with a boolean tag indicating whether a state update may let the thread or its envi- 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 ronment make more moves for profit or commercial advantage and that copies bear this notice and the full citation With the help of our new rely/guarantee conditions,we then on the first page.Copyrights for components of this work owned by others than ACM propose a new simulation RGSim-T,and a new Hoare-style pro- must be honored.Abstracting with credit is permitted.To copy otherwise.or republish gram logic,both of which support compositional verification to post on servers or to redistribute to lists,requires prior specific permission and/or a of termination-preserving refinement of concurrent programs fee.Request permissions from permissions@acm.org. Our work is based on our previous compositional simulation RGSim [11](which unfortunately cannot preserve termination), http:/ldk.doi.org/10.1145/2603088.2603123 and is inspired by Hoffmann et al.'s program logic for lock-Compositional Verification of Termination-Preserving Refinement of Concurrent Programs Hongjin Liang† Xinyu Feng† Zhong Shao‡ †University of Science and Technology of China ‡Yale University lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn zhong.shao@yale.edu Abstract Many verification problems can be reduced to refinement verifica￾tion. However, existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination, al￾lowing a diverging program to trivially refine any programs, or is difficult to apply in compositional thread-local reasoning. In this paper, we first propose a new simulation technique, which estab￾lishes termination-preserving refinement and is a congruence with respect to parallel composition. We then give a proof theory for the simulation, which is the first Hoare-style concurrent program logic supporting termination-preserving refinement proofs. We show two key applications of our logic, i.e., verifying linearizability and lock￾freedom together for fine-grained concurrent objects, and verifying full correctness of optimizations of concurrent algorithms. 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, Refinement, Termination Preservation, Rely-Guarantee Reasoning, Simulation 1. Introduction Verifying refinement between programs is the crux of many ver￾ification problems. For instance, reasoning about compilation or program transformations requires proving that every target pro￾gram is a refinement of its source [9]. In concurrent settings, re￾cent work [4, 12] shows that the correctness of concurrent data structures and libraries can be characterized via some forms of con￾textual refinements, i.e., every client that calls the concrete library methods should refine the client with some abstract atomic oper￾ations. Verification of concurrent garbage collectors [11] and OS kernels [18] can also be reduced to refinement verification. Refinement from the source program S to the target T , written as T ⊑ S, requires that T have no more observable behaviors than S. Usually observable behaviors include the traces of external events such as I/O operations and runtime errors. The question is, 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. CSL-LICS 2014, July 14–18, 2014, Vienna, Austria. Copyright c 2014 ACM 978-1-4503-2886-9. . . $15.00. http://dx.doi.org/10.1145/2603088.2603123 should termination of the source be preserved too by the target? If yes, how to verify such refinement? Preservation of termination is an indispensable requirement in many refinement applications. For instance, compilation and optimizations are not allowed to transform a terminating source program to a diverging (non-terminating) target. Also, implemen￾tations of concurrent data structures are often expected to have progress guarantees (e.g., lock-freedom and wait-freedom) in ad￾dition to linearizability. The requirements are equivalent to some contextual refinements that preserve the termination of client pro￾grams [12]. Most existing approaches for verifying concurrent program refinement, including simulations (e.g., [11]), logical relations (e.g., [22]), and refinement logics (e.g., [21]), do not reason about the preservation of termination. As a result, a program that does an infinite loop without generating any external events, e.g. while true do skip, would trivially refine any source program (just like that it trivially satisfies partial correctness in Hoare logic). Certainly this kind of refinement is not acceptable in the applica￾tions mentioned above. CompCert [9] addresses the problem by introducing a well￾founded order in the simulation, but it works only for sequential programs. It is difficult to apply this idea to do thread-local ver￾ification of concurrent program refinement, which enables us to know T1 k T2 ⊑ S1 k S2 by proving T1 ⊑ S1 and T2 ⊑ S2. In practice, the termination preservation in the refinement proofs of individual threads could be easily broken by the interference from their environments (i.e., other threads running in parallel). For in￾stance, a method call of a lock-free data structure (e.g., Treiber stack) may never terminate when other threads call the methods and update the shared memory infinitely often. As we will explain in Sec. 2, the key challenge here is to effectively specify the en￾vironments’ effects on the termination preservation of individual threads. As far as we know, no previous work can use “composi￾tional” thread-local reasoning to verify termination-preserving re- finement between (whole) concurrent programs. In this paper, we first propose novel rely/guarantee conditions which can effectively specify the interference over the termina￾tion properties between a thread and its environment. Traditional rely/guarantee conditions [8] are binary relations of program states and they specify the state updates. We extend them with a boolean tag indicating whether a state update may let the thread or its envi￾ronment make more moves. With the help of our new rely/guarantee conditions, we then propose a new simulation RGSim-T, and a new Hoare-style pro￾gram logic, both of which support compositional verification of termination-preserving refinement of concurrent programs. Our work is based on our previous compositional simulation RGSim [11] (which unfortunately cannot preserve termination), and is inspired by Hoffmann et al.’s program logic for lock-