Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations HONGJIN LIANG,XINYU FENG and MING FU,University of Science and Technology of China 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 sequen- tial 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 transfor. mations. In this paper,we propose a Rely-Guarantee-based Simulation(RGSim)to verify concurrent program transformations.The relation 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 compositional w.r.t.parallel composi- tions as long as the constraints are satisfied.Also,RGSim does not require semantics preservation under all environments,and can incorporate the assumptions about environments made by specific program transfor. mations in the form of rely/guarantee conditions.We use RGSim to reason about optimizations and prove atomicity of concurrent objects.We also propose 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 Engineeringl:Software/Program Verification-Cor- rectness proofs,Formal methods;F.3.1 [Logics and Meanings of Programs):Specifying and Verifying and Reasoning about Programs General Terms:Theory,Verification Additional Key Words and Phrases:Concurrency,Program Transformation,Rely-Guarantee Reasoning, Simulation ACM Reference Format: Liang,H.,Feng,X.,and Fu,M.2014.Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations.ACM Trans.Program.Lang.Syst.V,N,Article A (January YYYY), 53 pages. D0I:http/dx.doi.org10.1145/0000000.0000000 This work is supported in part by grants from National Natural Science Foundation of China(NSFC)under Grant Nos.61379039,61229201,61103023 and 91318301,Program for New Century Excellent Talents in Universities(Grant No.NCET-2010-0984).and the Fundamental Research Funds for the Central Universi- ties(Grant No.WK0110000031). Author's addresses:H.Liang,X.Feng and M.Fu,School of Computer Science and Technology,University of Science and Technology of China,Hefei,Anhui 230026,China;Suzhou Institute for Advanced Study, University of Science and Technology of China,Suzhou,Jiangsu 215123,China. Emails:H.Liang,Ihj1018@mail.ustc.edu.cn;X.Feng (corresponding author),xyfeng@ustc.edu.cn;and M.Fu,fuming@ustc.edu.cn Permission to make digital or hard copies of part or all 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 show this notice on the first page or initial screen of a display along with the full citation.Copyrights for components of this work owned by others than ACM must be honored.Abstracting with credit is per- mitted.To copy otherwise,to republish,to post on servers,to redistribute to lists,or to use any component of this work in other works requires prior specific permission and/or a fee.Permissions may be requested from Publications Dept.,ACM,Inc.,2 Penn Plaza,Suite 701,New York,NY 10121-0701 USA,fax +1(212) 869-0481,or permissions@acm.org YYYY ACM 0164-0925/YYYY/01-ARTA $15.00 D0I:http/dk.doi.org10.1145/0000000.0000000 ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY.A Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations HONGJIN LIANG, XINYU FENG and MING FU, University of Science and Technology of China 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 sequen￾tial 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 transfor￾mations. In this paper, we propose a Rely-Guarantee-based Simulation (RGSim) to verify concurrent program transformations. The relation 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 compositional w.r.t. parallel composi￾tions as long as the constraints are satisfied. Also, RGSim does not require semantics preservation under all environments, and can incorporate the assumptions about environments made by specific program transfor￾mations in the form of rely/guarantee conditions. We use RGSim to reason about optimizations and prove atomicity of concurrent objects. We also propose 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 Engineering]: Software/Program Verification – Cor￾rectness proofs, Formal methods; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms: Theory, Verification Additional Key Words and Phrases: Concurrency, Program Transformation, Rely-Guarantee Reasoning, Simulation ACM Reference Format: Liang, H., Feng, X., and Fu, M. 2014. Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations. ACM Trans. Program. Lang. Syst. V, N, Article A (January YYYY), 53 pages. DOI:http://dx.doi.org/10.1145/0000000.0000000 This work is supported in part by grants from National Natural Science Foundation of China (NSFC) under Grant Nos. 61379039, 61229201, 61103023 and 91318301, Program for New Century Excellent Talents in Universities (Grant No. NCET-2010-0984), and the Fundamental Research Funds for the Central Universi￾ties (Grant No. WK0110000031). Author’s addresses: H. Liang, X. Feng and M. Fu, School of Computer Science and Technology, University of Science and Technology of China, Hefei, Anhui 230026, China; Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou, Jiangsu 215123, China. Emails: H. Liang, lhj1018@mail.ustc.edu.cn; X. Feng (corresponding author), xyfeng@ustc.edu.cn; and M. Fu, fuming@ustc.edu.cn. Permission to make digital or hard copies of part or all 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 show this notice on the first page or initial screen of a display along with the full citation. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is per￾mitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works requires prior specific permission and/or a fee. Permissions may be requested from Publications Dept., ACM, Inc., 2 Penn Plaza, Suite 701, New York, NY 10121-0701 USA, fax +1 (212) 869-0481, or permissions@acm.org. ⃝c YYYY ACM 0164-0925/YYYY/01-ARTA $15.00 DOI:http://dx.doi.org/10.1145/0000000.0000000 ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY