verification framework is inspired by McCreight et al.[22],who of Systems (TACAS'10),volume 6015 of Lecture Notes in Computer propose a framework for separate verification of stop-the-world and Science,pages 296-311.Springer,March 2010. incremental GCs and their mutators,but their framework does not [13]I.Filipovic,P.O'Hear,N.Rinetzky,and H.Yang.Abstraction handle concurrency. for concurrent objects.In Proc.18th European Symp.on Prog. (ESOP'09),volume 5502 of Lecture Notes in Computer Science,pages Conclusion and future work.We propose RGSim to verify con- 252-266.Springer.March 2009. current program transformations.By describing explicitly the inter- [14]D.S.Gladstein and M.Wand.Compiler correctness for concur- ference with environments,RGSim is compositional,and can sup- rent languages.In Proc.Ist Int'l Conf.on Coordination Languages port many widely-used transformations.We have applied RGSim and Models (COORDINATION'96).volume 1061 of Lecture Notes in to reason about optimizations,prove atomicity of fine-grained con- Computer Science.pages 231-248.Springer.April 1996. current algorithms and verify concurrent garbage collectors.In the [15]M.Herlihy and N.Shavit.The Art of Multiprocessor Programming future,we would like to further test its applicability with more ap- Morgan Kaufmann,April 2008. plications,such as verifying STM implementations and compilers. [16]C.-K.Hur and D.Dreyer.A Kripke logical relation between ML and It is also interesting to explore the possibility of building tools to assembly.In Proc.38th ACM Symp.on Principles of Prog.Lang. automate the verification process. (POPL'11),pages 133-146.ACM Press,January 2011. [17]C.B.Jones.Tentative steps toward a development method for inter- Acknowledgments fering programs.ACM Trans.Program.Lang.Syst..5(4):596-619. 1983. We would like to thank Matthew Parkinson and anonymous ref- [18]K.Kapoor,K.Lodaya,and U.Reddy.Fine-grained concurrency with erees for their suggestions and comments on earlier versions of separation logic.J.Philosophical Logic,40(5):583-632,2011. this paper.This work is supported in part by grants from National Natural Science Foundation of China (NSFC)under Grant No. [19]X.Leroy.A formally verified compiler back-end.J.Autom.Reason., 43(4):363-446.December2009. 60928004.61073040 and 61103023.Xinyu Feng is also supported in part by NSFC under Grant No.90818019,by Program for New [20]H.Liang.X.Feng,and M.Fu. A rely-guarantee-based simulation for verifying Century Excellent Talents in Universities (NCET).and by the Fun- concurrent program transforma- tions. Technical report (with Coq implementation).Uni- damental Research Funds for the Central Universities. versity of Science and Technology of China.October 2011. http://kyhcs.ustcsz.edu.cn/relconcur/rgsim. References [21]A.Lochbihler.Verifying a compiler for java threads.In Proc.20th European Symp.on Prog.(ESOP'10),volume 6012 of Lecture Notes [1]M.Abadi and G.Plotkin.A model of cooperative threads.In Proc. in Computer Science,pages 427-447.Springer,March 2010. 36th ACM Symp.on Principles of Prog.Lang.(POPL'09),pages 29- 40.ACM Press,January 2009. [22]A.McCreight,Z.Shao,C.Lin,and L.Li.A general framework for certifying garbage collectors and their mutators.In Proc.2007 ACM [2]K.Barabash,O.Ben-Yitzhak,I.Goft,E.K.Kolodner,V.Leikehman. Conf.on Prog.Lang.Design and Impl.(PLDI'07),pages 468-479. Y.Ossia,A.Owshanko,and E.Petrank.A parallel,incremental ACM Press,June 2007. mostly concurrent garbage collector for servers.ACM Trans.Program. Lang.yst.,27(6):1097-1146.2005. [23]M.Parkinson,R.Bornat,and C.Calcagno.Variables as resource in Hoare logics.In Proc.2Ith IEEE Symp.on Logic In Computer Science [3]N.Benton.Simple relational correctness proofs for static analyses and (L/CS'06),pages 137-146.IEEE Computer Society,August 2006. program transformations.In Proc.3Ith ACM Symp.on Principles of Prog.Lang.(POPL'04),pages 14-25.ACM Press,January 2004. [24]D.Pavlovic,P.Pepper,and D.R.Smith.Formal derivation of con- current garbage collectors.In Proc.10th Int'l Conf.on Mathematics [4]N.Benton and C.-K.Hur.Biorthogonality.step-indexing and compiler of Program Construction (MPC'10),volume 6120 of Lecture Notes in correctness.In Proc.14th ACM Int'l Conf.on Functional Prog. Computer Science,pages 353-376.Springer.June 2010. (ICFP'09),pages 97-108.ACM Press,September 2009 [25]J.Seveik,V.Vafeiadis,F.Z.Nardelli,S.Jagannathan,and P.Sewell. [5]H.-J.Boehm.Threads cannot be implemented as a library.In Proc. Relaxed-memory concurrency and verified compilation.In Proc.38th 2005 ACM Conf.on Prog.Lang.Design and Impl.(PLDI05),pages ACM Symp.on Principles of Prog.Lang.(POPL'11),pages 43-54 261-268.ACM Press,June 2005 ACM Press,January 2011. [6]H.-J.Boehm and S.V.Adve.Foundations of the C++concurrency [26]R.K.Treiber.System programming:coping with parallelism.Tech- memory model.In Proc.2008 ACM Conf.on Prog.Lang.Design and nical Report RJ 5118,IBM Almaden Research Center,1986. Impl(PLDI'08),pages 68-78.ACM Press.June 2008. [27]A.Turon and M.Wand.A separation logic for refining concurrent [7]H.-J.Boehm,A.J.Demers,and S.Shenker.Mostly parallel garbage objects.In Proc.38th ACM Symp.on Principles of Prog.Lang. collection.In Proc.1991 ACM Conf.on Prog.Lang.Design and Impl. (POPL'11),pages 247-258.ACM Press,January 2011. (PLDI'91).pages 157-164.ACM Press,June 1991. [28]V.Vafeiadis.Modular fine-grained concurrency verification.Techni- [8]S.D.Brookes.Full abstraction for a shared-variable parallel language cal Report UCAM-CL-TR-726,University of Cambridge,Computer 1 nf.Comp.,127(2):145-163,1996. Laboratory,July 2008. [9]S.Burckhardt,M.Musuvathi,and V.Singh.Verifying local transfor- [29]V.Vafeiadis and M.J.Parkinson.A marriage of rely/guarantee and mations on relaxed memory models.In Proc.19th Int'l Conf.on Com- separation logic.In Proc.18th Int'l Conf.on Concurrency Theory piler Construction (CC'10),volume 6011 of Lecture Notes in Com- (CONCUR'07),volume 4703,pages 256-271.Springer,2007 puter Science,pages 104-123.Springer,March 2010. [30]M.T.Vechev.E.Yahav,and D.F.Bacon.Correctness-preserving [10]Cog Development Team.The Cog proof assistant reference manual. derivation of concurrent garbage collection algorithms.In Proc.2006 The Cog release v8.3,October 2010. ACM Conf.on Prog.Lang.Design and Impl.(PLDI'06).pages 341- (11]D.Dice,O.Shalev,and N.Shavit.Transactional locking II.In 353.ACM Press.June 2006. Proc.20th Int'l Symp.on Distributed Computing (DISC'06),volume [31]M.Wand.Compiler correctness for parallel languages.In Proc.Conf. 4167 of Lecture Notes in Computer Science,pages 194-208.Springer, on Functional Prog.Lang.and Computer Architecture (FPCA'95), September 2006. pages 120-134.ACM Press,June 1995. [12]T.Elmas,S.Qadeer,A.Sezgin,O.Subasi,and S.Tasiran.Simplifying [32]H.Yang.Relational separation logic.Theoretical Computer Science, linearizability proofs with reduction and abstraction.In Proc./6th 375(1-3):308-334.2007 Int'l Conf.on Tools and Algorithms for the Construction and Analysis 468verification framework is inspired by McCreight et al. [22], who propose a framework for separate verification of stop-the-world and incremental GCs and their mutators, but their framework does not handle concurrency. Conclusion and future work. We propose RGSim to verify con￾current program transformations. By describing explicitly the inter￾ference with environments, RGSim is compositional, and can sup￾port many widely-used transformations. We have applied RGSim to reason about optimizations, prove atomicity of fine-grained con￾current algorithms and verify concurrent garbage collectors. In the future, we would like to further test its applicability with more ap￾plications, such as verifying STM implementations and compilers. It is also interesting to explore the possibility of building tools to automate the verification process. Acknowledgments We would like to thank Matthew Parkinson and anonymous ref￾erees for their suggestions and comments on earlier versions of this paper. This work is supported in part by grants from National Natural Science Foundation of China (NSFC) under Grant No. 60928004, 61073040 and 61103023. Xinyu Feng is also supported in part by NSFC under Grant No. 90818019, by Program for New Century Excellent Talents in Universities (NCET), and by the Fun￾damental Research Funds for the Central Universities. References [1] M. Abadi and G. Plotkin. A model of cooperative threads. In Proc. 36th ACM Symp. on Principles of Prog. Lang. (POPL’09), pages 29– 40. ACM Press, January 2009. [2] K. Barabash, O. Ben-Yitzhak, I. Goft, E. K. Kolodner, V. Leikehman, Y. Ossia, A. Owshanko, and E. Petrank. A parallel, incremental, mostly concurrent garbage collector for servers. ACM Trans. Program. Lang. Syst., 27(6):1097–1146, 2005. [3] N. Benton. Simple relational correctness proofs for static analyses and program transformations. In Proc. 31th ACM Symp. on Principles of Prog. Lang. (POPL’04), pages 14–25. ACM Press, January 2004. [4] N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In Proc. 14th ACM Int’l Conf. on Functional Prog. (ICFP’09), pages 97–108. ACM Press, September 2009. [5] H.-J. Boehm. Threads cannot be implemented as a library. In Proc. 2005 ACM Conf. on Prog. Lang. Design and Impl. (PLDI’05), pages 261–268. ACM Press, June 2005. [6] H.-J. Boehm and S. V. Adve. Foundations of the C++ concurrency memory model. In Proc. 2008 ACM Conf. on Prog. Lang. Design and Impl. (PLDI’08), pages 68–78. ACM Press, June 2008. [7] H.-J. Boehm, A. J. Demers, and S. Shenker. Mostly parallel garbage collection. In Proc. 1991 ACM Conf. on Prog. Lang. Design and Impl. (PLDI’91), pages 157–164. ACM Press, June 1991. [8] S. D. Brookes. Full abstraction for a shared-variable parallel language. Inf. Comput., 127(2):145–163, 1996. [9] S. Burckhardt, M. Musuvathi, and V. Singh. Verifying local transfor￾mations on relaxed memory models. In Proc. 19th Int’l Conf. on Com￾piler Construction (CC’10), volume 6011 of Lecture Notes in Com￾puter Science, pages 104–123. Springer, March 2010. [10] Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.3, October 2010. [11] D. Dice, O. Shalev, and N. Shavit. Transactional locking II. In Proc. 20th Int’l Symp. on Distributed Computing (DISC’06), volume 4167 of Lecture Notes in Computer Science, pages 194–208. Springer, September 2006. [12] T. Elmas, S. Qadeer, A. Sezgin, O. Subasi, and S. Tasiran. Simplifying linearizability proofs with reduction and abstraction. In Proc. 16th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10), volume 6015 of Lecture Notes in Computer Science, pages 296–311. Springer, March 2010. [13] I. Filipovic, P. O’Hearn, N. Rinetzky, and H. Yang. Abstraction ´ for concurrent objects. In Proc. 18th European Symp. on Prog. (ESOP’09), volume 5502 of Lecture Notes in Computer Science, pages 252–266. Springer, March 2009. [14] D. S. Gladstein and M. Wand. Compiler correctness for concur￾rent languages. In Proc. 1st Int’l Conf. on Coordination Languages and Models (COORDINATION’96), volume 1061 of Lecture Notes in Computer Science, pages 231–248. Springer, April 1996. [15] M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, April 2008. [16] C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In Proc. 38th ACM Symp. on Principles of Prog. Lang. (POPL’11), pages 133–146. ACM Press, January 2011. [17] C. B. Jones. Tentative steps toward a development method for inter￾fering programs. ACM Trans. Program. Lang. Syst., 5(4):596–619, 1983. [18] K. Kapoor, K. Lodaya, and U. Reddy. Fine-grained concurrency with separation logic. J. Philosophical Logic, 40(5):583–632, 2011. [19] X. Leroy. A formally verified compiler back-end. J. Autom. Reason., 43(4):363–446, December 2009. [20] H. Liang, X. Feng, and M. Fu. A rely-guarantee-based simulation for verifying concurrent program transforma￾tions. Technical report (with Coq implementation), Uni￾versity of Science and Technology of China, October 2011. http://kyhcs.ustcsz.edu.cn/relconcur/rgsim. [21] A. Lochbihler. Verifying a compiler for java threads. In Proc. 20th European Symp. on Prog. (ESOP’10), volume 6012 of Lecture Notes in Computer Science, pages 427–447. Springer, March 2010. [22] A. McCreight, Z. Shao, C. Lin, and L. Li. A general framework for certifying garbage collectors and their mutators. In Proc. 2007 ACM Conf. on Prog. Lang. Design and Impl. (PLDI’07), pages 468–479. ACM Press, June 2007. [23] M. Parkinson, R. Bornat, and C. Calcagno. Variables as resource in Hoare logics. In Proc. 21th IEEE Symp. on Logic In Computer Science (LICS’06), pages 137–146. IEEE Computer Society, August 2006. [24] D. Pavlovic, P. Pepper, and D. R. Smith. Formal derivation of con￾current garbage collectors. In Proc. 10th Int’l Conf. on Mathematics of Program Construction (MPC’10), volume 6120 of Lecture Notes in Computer Science, pages 353–376. Springer, June 2010. [25] J. Sev ˇ cˇ´ık, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell. Relaxed-memory concurrency and verified compilation. In Proc. 38th ACM Symp. on Principles of Prog. Lang. (POPL’11), pages 43–54. ACM Press, January 2011. [26] R. K. Treiber. System programming: coping with parallelism. Tech￾nical Report RJ 5118, IBM Almaden Research Center, 1986. [27] A. Turon and M. Wand. A separation logic for refining concurrent objects. In Proc. 38th ACM Symp. on Principles of Prog. Lang. (POPL’11), pages 247–258. ACM Press, January 2011. [28] V. Vafeiadis. Modular fine-grained concurrency verification. Techni￾cal Report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory, July 2008. [29] V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In Proc. 18th Int’l Conf. on Concurrency Theory (CONCUR’07), volume 4703, pages 256–271. Springer, 2007. [30] M. T. Vechev, E. Yahav, and D. F. Bacon. Correctness-preserving derivation of concurrent garbage collection algorithms. In Proc. 2006 ACM Conf. on Prog. Lang. Design and Impl. (PLDI’06), pages 341– 353. ACM Press, June 2006. [31] M. Wand. Compiler correctness for parallel languages. In Proc. Conf. on Functional Prog. Lang. and Computer Architecture (FPCA’95), pages 120–134. ACM Press, June 1995. [32] H. Yang. Relational separation logic. Theoretical Computer Science, 375(1-3):308–334, 2007. 468