client thread may acquire the lock).It gives us the full correctness References of the TTAS lock.As an optimization of TAS lock,it preserves the [1]N.Benton.Simple relational correctness proofs for static analyses and behaviors on both functionality and termination of the latter. program transformations.In POPL,pages 14-25,2004. [2]S.Doherty,L.Groves,V.Luchangco,and M.Moir.Formal verifica- 7.Related Work and Conclusion tion of a practical lock-free queue algorithm.In FORTE,pages 97- Hoffmann et al.[7]propose a program logic to verify lock-freedom 114.2004. of concurrent objects.They reason about termination quantitatively [3]X.Feng.Local rely-guarantee reasoning.In POPL,pages 315-327. by introducing tokens,and model the environment's interference 2009. over the current thread's termination in terms of token transfer.The [4]I.Filipovic.P.O'Hearn,N.Rinetzky.and H.Yang.Abstraction idea is simple and natural,but their logic has very limited support for concurrent objects.Theor.Comput.Sci.,411(51-52):4379-4398. of local reasoning.One needs to know the total number of tokens 2010. needed by each thread (which may have multiple while loops)and [5]A.Gotsman.B.Cook.M.J.Parkinson,and V.Vafeiadis.Proving that the (fixed)number of threads,to calculate the number of tokens for non-blocking algorithms don't block.In POPL,pages 16-28,2009. a thread to lose or initially own.This requirement also disallows [6]M.Herlihy and N.Shavit.The Art of Multiprocessor Programming. their logic to reason about programs with infinite nondeterminism. Morgan Kaufmann,2008. Here we allow a thread to set its effect bit in R/G without knowing [7]J.Hoffmann,M.Marmar,and Z.Shao.Quantitative reasoning for the details of other threads;and other threads can determine by proving lock-freedom.In L/CS.pages 124-133.2013. themselves how many tokens they gain.We also introduce the [8]C.B.Jones.Tentative steps toward a development method for inter- HIDE-W rule to hide the number of tokens and to support infinite fering programs.ACM Trans.Program.Lang.Syst.,5(4):596-619. nondeterminism.Another key difference is that our logic supports 1983. verification of refinement,which is not supported by their logic. [9]X.Leroy.A formally verified compiler back-end.J.Autom.Reason., Gotsman et al.[5]propose program logic and tools to verify 43:363-446.December2009. lock-freedom.Their approach is more heavyweight in that they [10]H.Liang and X.Feng.Modular verification of linearizability with need temporal assertions in the rely/guarantee conditions to spec- non-fixed linearization points.In PLDI.pages 459-470,2013. ify interference between threads,and the rely/guarantee conditions [11]H.Liang,X.Feng,and M.Fu.A rely-guarantee-based simulation for need to be specified iteratively in multiple rounds to break circu- verifying concurrent program transformations.In POPL,pages 455- lar reliance on progress.Moreover,their work relies on third-party 468.2012. tools to check termination of individual threads as closed sequential [12]H.Liang.J.Hoffmann,X.Feng,and Z.Shao.Characterizing progress programs.Therefore they do not have a set of self-contained pro- gram logic rules and a coherent meta-theory as we do.Like Hoff- properties of concurrent objects via contextual refinements.In CON. CUR,pages227-241,2013. mann et al.[7].they do not support refinement verification either. [13]H.Liang,X.Feng,and Z.Shao.Compositional verification of As we explained in Sec.1,none of recent work on general termination-preserving refinement of concurrent programs(extended refinement verification of concurrent programs [11,21,22]and version).Technical report,Univ.of Science and Technology of China on verifying linearizability of concurrent objects [10,23](which May 2014.http://kyhcs.ustcsz.edu.cn/relconcur/rgsimt. can be viewed as a specialized refinement problem)preserves [14]M.M.Michael and M.L.Scott.Simple,fast.and practical non- termination.Seveik et al.equipped their simulation proofs for blocking and blocking concurrent queue algorithms.In PODC,pages CompCertTSO [17]with a well-founded order,following the 267-275.1996. CompCert approach.Their approach is similar to our second at- [15]M.Parkinson,R.Bornat,and C.Calcagno.Variables as resource in tempt explained in Sec.2.thus cannot be applied to prove lock- Hoare logics.In LICS.pages 137-146.2006. freedom of concurrent objects. [16]W.N.Scherer III.D.Lea.and M.L.Scott.Scalable synchronous Conclusion and future work.We propose a new compositional queues.In PPoPP,pages 147-156,2006. simulation RGSim-T to verify termination-preserving refinement [17]J.Sevefk.V.Vafeiadis.F.Z.Nardelli,S.Jagannathan,and P.Sewell between concurrent programs.We also give a rely/guarantee pro- CompCertTSO:A verified compiler for relaxed-memory concurrency gram logic as a proof theory for the simulation.Our logic is the first J.ACM.60(3):22.2013. to support compositional verification of termination-preserving re- [18]T.A.L.Sewell,M.O.Myreen,and G.Klein.Translation validation finement.The simulation and logic are general.They can be used for a verified os kernel.In PLDI,pages 471-482,2013. to verify both correctness of optimizations(where the source may [19]K.Stolen.A method for the development of totally correct shared- not necessarily terminate)and lock-freedom of concurrent objects. state parallel programs.In CONCUR.pages 510-525,1991. As future work,we would like to further extend them with the tech [20]R.K.Treiber.System programming:coping with parallelism.Tech- niques of pending thread pools and speculations [10]to verify ob nical Report RJ 5118,IBM Almaden Research Center,1986. jects with non-fixed linearization points.We also hope to explore [21]A.Turon,D.Dreyer,and L.Birkedal.Unifying refinement and hoare- the possibility of building tools to automate the verification. style reasoning in a logic for higher-order concurrency.In /CFP,pages 377-390.2013. Acknowledgments [22]A.Turon,J.Thamsborg,A.Ahmed,L.Birkedal,and D.Dreyer. We thank anonymous referees for their suggestions and com- Logical relations for fine-grained concurrency.In POPL,pages 343- ments.This work is supported in part by China Scholarship Coun- 356.2013. cil,National Natural Science Foundation of China (NSFC)under [23]V.Vafeiadis.Modular fine-grained concurrency verification.PhD Grant Nos.61229201,61379039 and 91318301.and the National thesis,University of Cambridge,Computer Laboratory,2008. Hi-Tech Research and Development Program of China(Grant [24]V.Vafeiadis.Concurrent separation logic and operational semantics No.2012AA010901).It is also supported in part by DARPA In MFPS,pages 335-351,2011. grants FA8750-10-2-0254 and FA8750-12-2-0293,ONR grant [25]H.Yang.Relational separation logic.Theoretical Computer Science N000141210478,and NSF grants 0915888 and 1065451.Any 375:308-334.2007. opinions,findings,and conclusions contained in this document are those of the authors and do not reflect the views of these agenciesclient thread may acquire the lock). It gives us the full correctness of the TTAS lock. As an optimization of TAS lock, it preserves the behaviors on both functionality and termination of the latter. 7. Related Work and Conclusion Hoffmann et al. [7] propose a program logic to verify lock-freedom of concurrent objects. They reason about termination quantitatively by introducing tokens, and model the environment’s interference over the current thread’s termination in terms of token transfer. The idea is simple and natural, but their logic has very limited support of local reasoning. One needs to know the total number of tokens needed by each thread (which may have multiple while loops) and the (fixed) number of threads, to calculate the number of tokens for a thread to lose or initially own. This requirement also disallows their logic to reason about programs with infinite nondeterminism. Here we allow a thread to set its effect bit in R/G without knowing the details of other threads; and other threads can determine by themselves how many tokens they gain. We also introduce the HIDE-W rule to hide the number of tokens and to support infinite nondeterminism. Another key difference is that our logic supports verification of refinement, which is not supported by their logic. Gotsman et al. [5] propose program logic and tools to verify lock-freedom. Their approach is more heavyweight in that they need temporal assertions in the rely/guarantee conditions to spec￾ify interference between threads, and the rely/guarantee conditions need to be specified iteratively in multiple rounds to break circu￾lar reliance on progress. Moreover, their work relies on third-party tools to check termination of individual threads as closed sequential programs. Therefore they do not have a set of self-contained pro￾gram logic rules and a coherent meta-theory as we do. Like Hoff￾mann et al. [7], they do not support refinement verification either. As we explained in Sec. 1, none of recent work on general refinement verification of concurrent programs [11, 21, 22] and on verifying linearizability of concurrent objects [10, 23] (which can be viewed as a specialized refinement problem) preserves termination. Sevˇc´ık et al. equipped their simulation proofs for ˇ CompCertTSO [17] with a well-founded order, following the CompCert approach. Their approach is similar to our second at￾tempt explained in Sec. 2, thus cannot be applied to prove lock￾freedom of concurrent objects. Conclusion and future work. We propose a new compositional simulation RGSim-T to verify termination-preserving refinement between concurrent programs. We also give a rely/guarantee pro￾gram logic as a proof theory for the simulation. Our logic is the first to support compositional verification of termination-preserving re- finement. The simulation and logic are general. They can be used to verify both correctness of optimizations (where the source may not necessarily terminate) and lock-freedom of concurrent objects. As future work, we would like to further extend them with the tech￾niques of pending thread pools and speculations [10] to verify ob￾jects with non-fixed linearization points. We also hope to explore the possibility of building tools to automate the verification. Acknowledgments We thank anonymous referees for their suggestions and com￾ments. This work is supported in part by China Scholarship Coun￾cil, National Natural Science Foundation of China (NSFC) under Grant Nos. 61229201, 61379039 and 91318301, and the National Hi-Tech Research and Development Program of China (Grant No. 2012AA010901). It is also supported in part by DARPA grants FA8750-10-2-0254 and FA8750-12-2-0293, ONR grant N000141210478, and NSF grants 0915888 and 1065451. Any opinions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies. References [1] N. Benton. Simple relational correctness proofs for static analyses and program transformations. In POPL, pages 14–25, 2004. [2] S. Doherty, L. Groves, V. Luchangco, and M. Moir. Formal verifica￾tion of a practical lock-free queue algorithm. In FORTE, pages 97– 114, 2004. [3] X. Feng. Local rely-guarantee reasoning. In POPL, pages 315–327, 2009. [4] I. Filipovic, P. O’Hearn, N. Rinetzky, and H. Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51-52):4379–4398, 2010. [5] A. Gotsman, B. Cook, M. J. Parkinson, and V. Vafeiadis. Proving that non-blocking algorithms don’t block. In POPL, pages 16–28, 2009. [6] M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008. [7] J. Hoffmann, M. Marmar, and Z. Shao. Quantitative reasoning for proving lock-freedom. In LICS, pages 124–133, 2013. [8] C. B. Jones. Tentative steps toward a development method for inter￾fering programs. ACM Trans. Program. Lang. Syst., 5(4):596–619, 1983. [9] X. Leroy. A formally verified compiler back-end. J. Autom. Reason., 43:363–446, December 2009. [10] H. Liang and X. Feng. Modular verification of linearizability with non-fixed linearization points. In PLDI, pages 459–470, 2013. [11] H. Liang, X. Feng, and M. Fu. A rely-guarantee-based simulation for verifying concurrent program transformations. In POPL, pages 455– 468, 2012. [12] H. Liang, J. Hoffmann, X. Feng, and Z. Shao. Characterizing progress properties of concurrent objects via contextual refinements. In CON￾CUR, pages 227–241, 2013. [13] H. Liang, X. Feng, and Z. Shao. Compositional verification of termination-preserving refinement of concurrent programs (extended version). Technical report, Univ. of Science and Technology of China, May 2014. http://kyhcs.ustcsz.edu.cn/relconcur/rgsimt. [14] M. M. Michael and M. L. Scott. Simple, fast, and practical non￾blocking and blocking concurrent queue algorithms. In PODC, pages 267–275, 1996. [15] M. Parkinson, R. Bornat, and C. Calcagno. Variables as resource in Hoare logics. In LICS, pages 137–146, 2006. [16] W. N. Scherer III, D. Lea, and M. L. Scott. Scalable synchronous queues. In PPoPP, pages 147–156, 2006. [17] J. Sevˇc´ık, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell. ˇ CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM, 60(3):22, 2013. [18] T. A. L. Sewell, M. O. Myreen, and G. Klein. Translation validation for a verified os kernel. In PLDI, pages 471–482, 2013. [19] K. Stølen. A method for the development of totally correct shared￾state parallel programs. In CONCUR, pages 510–525, 1991. [20] R. K. Treiber. System programming: coping with parallelism. Tech￾nical Report RJ 5118, IBM Almaden Research Center, 1986. [21] A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and hoare￾style reasoning in a logic for higher-order concurrency. In ICFP, pages 377–390, 2013. [22] A. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer. Logical relations for fine-grained concurrency. In POPL, pages 343– 356, 2013. [23] V. Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, Computer Laboratory, 2008. [24] V. Vafeiadis. Concurrent separation logic and operational semantics. In MFPS, pages 335–351, 2011. [25] H. Yang. Relational separation logic. Theoretical Computer Science, 375:308–334, 2007