A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations Hongjin Liang Xinyu Feng Ming Fu School of Computer Science and Technology,University of Science and Technology of China Hefei.Anhui 230026.China Ihj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn fumingOustc.edu.cn Abstract Correctness of compilation and optimizations of concurrent Verifying program transformations usually requires proving that programs.In this most natural program transformation verifica- the resulting program(the target)refines or is equivalent to the tion problem,every compilation phase does a program transfor- original one (the source).However,the refinement relation between mation T,which needs to preserve the semantics of the inputs individual sequential threads cannot be preserved in general with Atomicity of concurrent objects.A concurrent object or library the presence of parallel compositions,due to instruction reordering provides a set of methods that allow clients to manipulate the and the different granularities of atomic operations at the source shared data structure with abstract atomic behaviors [15].Their and the target.On the other hand,the refinement relation defined correctness can be reduced to the correctness of the transforma- based on fully abstract semantics of concurrent programs assumes tion from abstract atomic operations to concrete and executable arbitrary parallel environments,which is too strong and cannot be programs in a concurrent context. satisfied by many well-known transformations. Verifying implementations of software transactional memory In this paper,we propose a Rely-Guarantee-based Simulation (STM).Many languages supporting STM provide a high-level (RGSim)to verify concurrent program transformations.The rela- atomic block atomicC,so that programmers can assume the tion is parametrized with constraints of the environments that the atomicity of the execution of C.Atomic blocks are imple- source and the target programs may compose with.It considers the mented using some STM protocol (e.g.,TL2 [111)that allows interference between threads and their environments,thus is less very fine-grained interleavings.Verifying that the fine-grained permissive than relations over sequential programs.It is composi- program respects the semantics of atomic blocks gives us the tional w.rt.parallel compositions as long as the constraints are sat- correctness of the STM implementation. isfied.Also,RGSim does not require semantics preservation under Correctness of concurrent garbage collectors (GCs).High- all environments,and can incorporate the assumptions about en- level garbage-collected languages (e.g.,Java)allow program- vironments made by specific program transformations in the form mers to work at an abstract level without knowledge of the un- of rely/guarantee conditions.We use RGSim to reason about opti- derlying GC algorithm.However,the concrete and executable mizations and prove atomicity of concurrent objects.We also pro- low-level program involves interactions between the mutators pose a general garbage collector verification framework based on and the collector.If we view the GC implementation as a trans- RGSim,and verify the Boehm et al.concurrent mark-sweep GC. formation from high-level mutators to low-level ones with a Categories and Subject Descriptors D.2.4 [Software Engineer- concrete GC thread,the GC safety can be reduced naturally to ing]:Software/Program Verification-Correctness proofs,Formal the semantics preservation of the transformation. methods;F.3.1 [Logics and Meanings of Programs]:Specifying To verify the correctness of a program transformation T,we and Verifying and Reasoning about Programs follow Leroy's approach [19]and define a refinement relation General Terms Theory,Verification between the target and the source programs,which says the target has no more observable behaviors than the source.Then we can Keywords Concurrency,Program Transformation,Rely-Guarantee formalize the correctness of the transformation as follows: Reasoning.Simulation Correct(T)≌C,C.C=T(C)=→CgC. (1.1) 1. Introduction That is,for any source program C acceptable by T.T(C)is Many verification problems can be reduced to verifying program a refinement of C.When the source and the target are shared- transformations,i.e.,proving the target program of the transforma- state concurrent programs,the refinement needs to satisfy the tion has no more observable behaviors than the source.Below we following requirements to support effective proof of Correct(T): give some typical examples in concurrent settings: Since the target T(C)may be in a different language from the source,the refinement should be general and independent of the language details. Permission to make digital or hard copies of all or part of this work for personal or To verify fine-grained implementations of abstract operations classroom use is granted without fee provided that copies are not made or distributed the refinement should support different views of program states for profit or commercial advantage and that copies bear this notice and the full citation and different granularities of state accesses at the source and the on the first page.To copy otherwisc.to republish,to post toredistribute to lists,requires prior specific permission and/or a fee. target levels. POPL'12.January 25-27.2012.Philadelphia,PA,USA. When T is syntax-directed (and it is usually the case for par- Copyright©2012ACM978-1-4503-1083-3/1201..s10.00 allel compositions,i.e.,T(CC)=T(C)T(C)).a com 455A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations Hongjin Liang Xinyu Feng Ming Fu School of Computer Science and Technology, University of Science and Technology of China Hefei, Anhui 230026, China lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn fuming@ustc.edu.cn Abstract Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be preserved in general with the presence of parallel compositions, due to instruction reordering and the different granularities of atomic operations at the source and the target. On the other hand, the refinement relation defined based on fully abstract semantics of concurrent programs assumes arbitrary parallel environments, which is too strong and cannot be satisfied by many well-known transformations. In this paper, we propose a Rely-Guarantee-based Simulation (RGSim) to verify concurrent program transformations. The rela￾tion is parametrized with constraints of the environments that the source and the target programs may compose with. It considers the interference between threads and their environments, thus is less permissive than relations over sequential programs. It is composi￾tional w.r.t. parallel compositions as long as the constraints are sat￾isfied. Also, RGSim does not require semantics preservation under all environments, and can incorporate the assumptions about en￾vironments made by specific program transformations in the form of rely/guarantee conditions. We use RGSim to reason about opti￾mizations and prove atomicity of concurrent objects. We also pro￾pose a general garbage collector verification framework based on RGSim, and verify the Boehm et al. concurrent mark-sweep GC. 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, Program Transformation, Rely-Guarantee Reasoning, Simulation 1. Introduction Many verification problems can be reduced to verifying program transformations, i.e., proving the target program of the transforma￾tion has no more observable behaviors than the source. Below we give some typical examples in concurrent settings: 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. POPL’12, January 25–27, 2012, Philadelphia, PA, USA. Copyright c 2012 ACM 978-1-4503-1083-3/12/01. . . $10.00 • Correctness of compilation and optimizations of concurrent programs. In this most natural program transformation verifica￾tion problem, every compilation phase does a program transfor￾mation T, which needs to preserve the semantics of the inputs. • Atomicity of concurrent objects. A concurrent object or library provides a set of methods that allow clients to manipulate the shared data structure with abstract atomic behaviors [15]. Their correctness can be reduced to the correctness of the transforma￾tion from abstract atomic operations to concrete and executable programs in a concurrent context. • Verifying implementations of software transactional memory (STM). Many languages supporting STM provide a high-level atomic block atomic{C}, so that programmers can assume the atomicity of the execution of C. Atomic blocks are imple￾mented using some STM protocol (e.g., TL2 [11]) that allows very fine-grained interleavings. Verifying that the fine-grained program respects the semantics of atomic blocks gives us the correctness of the STM implementation. • Correctness of concurrent garbage collectors (GCs). High￾level garbage-collected languages (e.g., Java) allow program￾mers to work at an abstract level without knowledge of the un￾derlying GC algorithm. However, the concrete and executable low-level program involves interactions between the mutators and the collector. If we view the GC implementation as a trans￾formation from high-level mutators to low-level ones with a concrete GC thread, the GC safety can be reduced naturally to the semantics preservation of the transformation. To verify the correctness of a program transformation T, we follow Leroy’s approach [19] and define a refinement relation between the target and the source programs, which says the target has no more observable behaviors than the source. Then we can formalize the correctness of the transformation as follows: Correct(T) ∀C, C. C = T(C) =⇒ C C . (1.1) That is, for any source program C acceptable by T, T(C) is a refinement of C. When the source and the target are shared￾state concurrent programs, the refinement needs to satisfy the following requirements to support effective proof of Correct(T): • Since the target T(C) may be in a different language from the source, the refinement should be general and independent of the language details. • To verify fine-grained implementations of abstract operations, the refinement should support different views of program states and different granularities of state accesses at the source and the target levels. • When T is syntax-directed (and it is usually the case for par￾allel compositions, i.e., T(C C ) = T(C) T(C )), a com- 455