并发程序精化验证及其应用
|
摘要
许多程序验证问题都可以被归结为精化验证,即证明一个较具体的程序不会比一个较抽象的程序产生更多的行为。本文发掘了在并发环境下精化验证的应用场景,并提出若干种可以支持这些精化应用实例的验证技术。具体来说,本文在理解和验证并发程序精化方面做出了如下贡献。
首先,本文提出了一种基于依赖/保证的模拟关系RGSim,作为并发程序精化的通用验证手段。这一新颖的模拟关系将线程和并发环境之间的交互作为参数,从而获得可组合性,支持模块化验证。同时,它将精化应用中对并发环境的特定前提参数化,因而具有较好的灵活性和实用性。我们应用RGSim验证了并发环境下的几种程序优化。此外,我们还将并发垃圾收集器的验证归结为精化验证,并提出一种基于RGSim的通用验证框架。使用这一框架,我们验证了Boehm等人提出的并发的标记-清扫垃圾收集算法。
其次,本文提出了一种霍尔风格的程序逻辑,用于高效地、模块化地验证并发对象的线性一致性。这是并发程序精化验证的一种重要应用。作为该程序逻辑的一部分,我们提出了一种轻量的辅助代码插桩机制。我们的程序逻辑支持可线性化点不固定的并发算法,这些算法的验证难度很大。具体包括：使用帮助机制的无锁算法(如HSY栈),可线性化点依赖未来不确定执行的算法(如懒惰集合算法),以及同时有这两种特性的算法(如RDCSS算法)。我们还扩展了模拟关系RGSim以支持可线性化点不固定的程序,新的模拟关系保证了我们的程序逻辑的可靠性,它可以蕴涵一种上下文精化关系,该精化关系与线性一致性等价。我们应用这一程序逻辑验证了12个著名的并发算法,其中两个算法已经在Java并发包java.util.concurrent中使用。
最后,本文展示了一个用精化关系刻画并发对象完整正确性(包括线性一致性以及各种进展性性质)的统一框架。我们证明了对于满足线性一致性的并发对象,每种进展性性质等价于一种特定的对终止性敏感的上下文精化关系。我们用上下文精化关系统一了并发对象的线性一致性和所有常见的进展性性质,包括无等待性、无锁性、无阻碍性、无饥饿性和无死锁性。根据这一结果,对于任何使用并发对象操作的客户端程序,我们可以模块化地验证该客户端程序的安全性和终止性。另一方面,它也告诉我们,有希望借鉴已有的验证上下文精化的技术来同时验证线性一致性和进展性性质。
Many verification problems can be reduced to refinement verification, i.e., proving that a concrete program has no more behaviors than a more abstract program. This dis-sertation explores the applications of refinement verification of concurrent programs, and proposes compositional verification techniques that support these applications. It makes several contributions to understanding and verifying concurrent program refine-ment.
First, it shows a Rely-Guarantee-based Simulation (RGSim) as a general proof technique for concurrent program refinement. The novel simulation relation is param-eterized with the interference between threads and their parallel environments. It is compositional and supports modular verification. RGSim can incorporate the assump-tions about environments made by specific refinement applications, thus is flexible and practical. We apply RGSim to reason about optimizations in parallel contexts. We also reduce the verification of concurrent garbage collectors (GCs) to refinement verifica-tion, and propose a general GC verification framework based on RGSim. Using the framework, we verify the Boehm et al. concurrent mark-sweep GC algorithm.
Second, it shows a Hoare-style program logic for modular and effective verifica-tion of linearizability of concurrent objects, which is an important application of con-current program refinement verification. Our logic with a lightweight instrumentation mechanism supports objects with non-fixed linearization points (LPs), including the most challenging ones that use the helping mechanism to achieve lock-freedom (as in HSY elimination-based stack), or have LPs depending on unpredictable future execu-tions (as in the lazy set algorithm), or involve both features (as in the RDCSS algo-rithm). We generalize RGSim with the support for non-fixed LPs as the meta-theory of our logic, and show it implies a contextual refinement which is equivalent to lineariz-ability. Using our logic we successfully verify12well-known algorithms, two of which are in the java. util. concurrent package.
Finally, it shows a unified framework that characterizes the full correctness (i.e., linearizability and progress properties) of concurrent objects via contextual refinements. We prove that for linearizable objects, each progress property is equivalent to a certain form of termination-sensitive contextual refinement. The framework unifies lineariz-ability and all the five most common progress properties:wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, and deadlock-freedom. It enables modular verification of safety and liveness properties of client programs, and also makes it pos-sible to borrow ideas from existing proof methods for contextual refinements to verify linearizability and a progress property together.
首先,本文提出了一种基于依赖/保证的模拟关系RGSim,作为并发程序精化的通用验证手段。这一新颖的模拟关系将线程和并发环境之间的交互作为参数,从而获得可组合性,支持模块化验证。同时,它将精化应用中对并发环境的特定前提参数化,因而具有较好的灵活性和实用性。我们应用RGSim验证了并发环境下的几种程序优化。此外,我们还将并发垃圾收集器的验证归结为精化验证,并提出一种基于RGSim的通用验证框架。使用这一框架,我们验证了Boehm等人提出的并发的标记-清扫垃圾收集算法。
其次,本文提出了一种霍尔风格的程序逻辑,用于高效地、模块化地验证并发对象的线性一致性。这是并发程序精化验证的一种重要应用。作为该程序逻辑的一部分,我们提出了一种轻量的辅助代码插桩机制。我们的程序逻辑支持可线性化点不固定的并发算法,这些算法的验证难度很大。具体包括：使用帮助机制的无锁算法(如HSY栈),可线性化点依赖未来不确定执行的算法(如懒惰集合算法),以及同时有这两种特性的算法(如RDCSS算法)。我们还扩展了模拟关系RGSim以支持可线性化点不固定的程序,新的模拟关系保证了我们的程序逻辑的可靠性,它可以蕴涵一种上下文精化关系,该精化关系与线性一致性等价。我们应用这一程序逻辑验证了12个著名的并发算法,其中两个算法已经在Java并发包java.util.concurrent中使用。
最后,本文展示了一个用精化关系刻画并发对象完整正确性(包括线性一致性以及各种进展性性质)的统一框架。我们证明了对于满足线性一致性的并发对象,每种进展性性质等价于一种特定的对终止性敏感的上下文精化关系。我们用上下文精化关系统一了并发对象的线性一致性和所有常见的进展性性质,包括无等待性、无锁性、无阻碍性、无饥饿性和无死锁性。根据这一结果,对于任何使用并发对象操作的客户端程序,我们可以模块化地验证该客户端程序的安全性和终止性。另一方面,它也告诉我们,有希望借鉴已有的验证上下文精化的技术来同时验证线性一致性和进展性性质。
Many verification problems can be reduced to refinement verification, i.e., proving that a concrete program has no more behaviors than a more abstract program. This dis-sertation explores the applications of refinement verification of concurrent programs, and proposes compositional verification techniques that support these applications. It makes several contributions to understanding and verifying concurrent program refine-ment.
First, it shows a Rely-Guarantee-based Simulation (RGSim) as a general proof technique for concurrent program refinement. The novel simulation relation is param-eterized with the interference between threads and their parallel environments. It is compositional and supports modular verification. RGSim can incorporate the assump-tions about environments made by specific refinement applications, thus is flexible and practical. We apply RGSim to reason about optimizations in parallel contexts. We also reduce the verification of concurrent garbage collectors (GCs) to refinement verifica-tion, and propose a general GC verification framework based on RGSim. Using the framework, we verify the Boehm et al. concurrent mark-sweep GC algorithm.
Second, it shows a Hoare-style program logic for modular and effective verifica-tion of linearizability of concurrent objects, which is an important application of con-current program refinement verification. Our logic with a lightweight instrumentation mechanism supports objects with non-fixed linearization points (LPs), including the most challenging ones that use the helping mechanism to achieve lock-freedom (as in HSY elimination-based stack), or have LPs depending on unpredictable future execu-tions (as in the lazy set algorithm), or involve both features (as in the RDCSS algo-rithm). We generalize RGSim with the support for non-fixed LPs as the meta-theory of our logic, and show it implies a contextual refinement which is equivalent to lineariz-ability. Using our logic we successfully verify12well-known algorithms, two of which are in the java. util. concurrent package.
Finally, it shows a unified framework that characterizes the full correctness (i.e., linearizability and progress properties) of concurrent objects via contextual refinements. We prove that for linearizable objects, each progress property is equivalent to a certain form of termination-sensitive contextual refinement. The framework unifies lineariz-ability and all the five most common progress properties:wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, and deadlock-freedom. It enables modular verification of safety and liveness properties of client programs, and also makes it pos-sible to borrow ideas from existing proof methods for contextual refinements to verify linearizability and a progress property together.
引文
[I]Leroy X. A Formally Verified Compiler Back-end. J. Autom. Reason.,2009,43(4):363-446.
-[2] Hoare C A R. Proof of Correctness of Data Representations. Acta Inf.,1972,1(4):271-281.
[3]Herlihy M, Shavit N. The Art of Multiprocessor Programming. Morgan Kaufmann, April,2008.
[4]Herlihy M P, Wing J M. Linearizability:A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst.,1990,12(3):463-492.
[5]Filipovic I, O'Hearn P, Rinetzky N, et al. Abstraction for concurrent objects. Theor. Comput. Sci.,2010, 411(51-52):4379-4398.
[6]Dice D, Shalev O, Shavit N. Transactional Locking II. Proceedings of DISC, Berlin, Heidelberg:Springer, 2006.194-208.
[7]Klein G, Andronick J, Elphinstone K, et al. seL4:Formal Verification of an Operating-system Kernel. Commun. ACM,2010,53(6):107-115.
'[8] He J, Hoare C A R, Sanders J W. Data Refinement Refined. Proceedings of ESOP. Springer,1986.187-196.
[9]Abadi M, Lamport L. The Existence of Refinement Mappings. Theor. Comput. Sci.,1991,82(2):253-284.
[10]Treiber R K. System programming:coping with parallelism. Technical Report RJ 5118, IBM Almaden Re-search Center,1986.
[11]Brookes S D. Full Abstraction for a Shared-Variable Parallel Language. Inf. Comput.,1996,127(2):145-163.
[12]Hur C K, Dreyer D. A Kripke Logical Relation Between ML and Assembly. Proceedings of POPL, New York, NY, USA:ACM Press,2011.133-146.
[13]Abadi M, Plotkin G. A model of cooperative threads. Proceedings of POPL, New York, NY, USA:ACM Press, 2009.29-40.
[14]Amit D, Rinetzky N, Reps T, et al. Comparison Under Abstraction for Verifying Linearizability. Proceedings of CAV, Berlin, Heidelberg:Springer,2007.477-490.
[15]Vafeiadis V. Modular fine-grained concurrency verification. Technical Report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory, July,2008.
[16]Derrick J, Schellhom G, Wehrheim H. Mechanically Verified Proof Obligations for Linearizability. ACM Trans. Program. Lang. Syst.,2011,33(1):4:1-4:43.
[17]Turon A J, Thamsborg J, Ahmed A, et al. Logical Relations for Fine-grained Concurrency. Proceedings of POPL, New York, NY, USA:ACM Press,2013.343-356.
[18]Hendler D, Shavit N, Yerushalmi L. A Scalable Lock-free Stack Algorithm. Proceedings of SPAA, New York, NY, USA:ACM Press,2004.206-215.
[19]Heller S, Herlihy M, Luchangco V, et al. A Lazy Concurrent List-based Set Algorithm. Proceedings of OPODIS, Berlin, Heidelberg:Springer,2006.3-16.
[20]Turon A, Wand M. A separation logic for refining concurrent objects. Proceedings of POPL, New York, NY, USA:ACM Press,2011.247-258.
[21]Gotsman A, Yang H. Liveness-preserving atomicity abstraction. Proceedings of ICALP. Springer,2011. 453-465.
[22]Jones C B. Tentative Steps Toward a Development Method for Interfering Programs. ACM Trans. Program. Lang. Syst,1983,5(4):596-619.
[23]Boehm H J, Demers A J, Shenker S. Mostly Parallel Garbage Collection. Proceedings of PLDI, New York, NY, USA:ACM Press,1991.157-164.
[24]Feng X. Local rely-guarantee reasoning. Proceedings of POPL, New York, NY, USA:ACM Press,2009. 315-327.
[25]Boehm H J. Threads cannot be implemented as a library. Proceedings of PLDI, New York, NY, USA:ACM Press,2005.261-268.
[26]Boehm H J, Adve S V. Foundations of the C++ concurrency memory model. Proceedings of PLDI, New York, NY, USA:ACM Press,2008.68-78.
[27]Benton N. Simple relational correctness proofs for static analyses and program transformations. Proceedings of POPL, New York, NY, USA:ACM Press,2004.14-25.
[28]Sevcik J, Vafeiadis V, Nardelli F Z, et al. Relaxed-Memory Concurrency and Verified Compilation. Proceedings of POPL, New York, NY, USA:ACM Press,2011.43-54.
[29]Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.3,2010. http: //coq.inria.fr.
[30]Liang H, Feng X, Fu M. A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transforma-tions. Technical report (with Coq implementation), University of Science and Technology of China, October, 2011. http://kyhcs.ustcsz.edu.cn/relconcur/rgsim.
[31]Reynolds J C. Separation Logic:A Logic for Shared Mutable Data Structures. Proceedings of LICS, Wash-ington, DC, USA:IEEE Computer Society,2002.55-74.
[32]Turon A, Dreyer D, Birkedal L. Unifying Refinement and Hoare-style Reasoning in a Logic for Higher-order Concurrency. Proceedings of ICFP'13, New York, NY, USA:ACM Press,2013.377-390.
[33]Yang H. Relational separation logic. Theor. Comput. Sci.,2007,375(1-3):308-334.
[34]Wand M. Compiler Correctness for Parallel Languages. Proceedings of FPCA, New York, NY, USA:ACM Press,1995.120-134.
[35]Gladstein D S, Wand M. Compiler Correctness for Concurrent Languages. Proceedings of COORDINATION, volume 1061 of Lecture Notes in Computer Science. Springer,1996.231-248.
[36]Lochbihler A. Verifying a Compiler for Java Threads. Proceedings of ESOP, Berlin, Heidelberg:Springer, 2010.427-447.
[37]Burckhardt S, Musuvathi M, Singh V. Verifying Local Transformations on Relaxed Memory Models. Proceed-ings of CC/ETAPS, Berlin, Heidelberg:Springer,2010.104-123.
[38]Barabash K, Ben-Yitzhak O, Goft I, et al. A parallel, incremental, mostly concurrent garbage collector for servers. ACM Trans. Program. Lang. Syst.,2005,27(6):1097-1146.
[39]Parkinson M, Bornat R, Calcagno C. Variables as Resource in Hoare Logics. Proceedings of LICS, Washington, DC, USA:IEEE Computer Society,2006.137-146.
[40]Vechev M T, Yahav E, Bacon D F. Correctness-Preserving Derivation of Concurrent Garbage Collection Al-gorithms. Proceedings of PLDI, New York, NY, USA:ACM Press,2006.341-353.
[41]Pavlovic D, Pepper P, Smith D R. Formal derivation of concurrent garbage collectors. Proceedings of MPC, 2010.353-376.
[42]Kapoor K, Lodaya K, Reddy U. Fine-grained concurrency with Separation Logic. J. Philosophical Logic,2011, 40(5):583-632.
[43]McCreight A, Shao Z, Lin C, et al. A General Framework for Certifying Garbage Collectors and Their Mutators. Proceedings of PLDI, New York, NY, USA:ACM Press,2007.468-479.
[44]O'Hearn P W. Resources, Concurrency, and Local Reasoning. Theor. Comput. Sci.,2007,375(1-3):271-307.
[45]Qadeer S, Sezgin A, Tasiran S. Back and Forth:Prophecy Variables for Static Verification of Concurrent Programs. Technical Report MSR-TR-2009-142, Microsoft, October,2009.
[46]Harris T L, Fraser K, Pratt I A. A Practical Multi-word Compare-and-Swap Operation. Proceedings of DISC, London, UK, UK:Springer,2002.265-279.
[47]Colvin R, Groves L, Luchangco V, et al. Formal verification of a lazy concurrent list-based set algorithm. Proceedings of CAV. Springer,2006.475-488.
[48]Lynch N A, Vaandrager F W. Forward and Backward Simulations:I. Untimed Systems. Inf. Comput.,1995, 121(2):214-233.
[49]Doherty S, Groves L, Luchangco V, et al. Formal Verification of a Practical Lock-Free Queue Algorithm. Proceedings of FORTE. Springer,2004.97-114.
[50]Gotsman A, Yang H. Linearizability with Ownership Transfer. Proceedings of CONCUR. Springer,2012. 256-271.
[51]O'Hearn P W, Yang H, Reynolds J C. Separation and Information Hiding. Proceedings of POPL, New York, NY, USA:ACM Press,2004.268-280.
[52]Vafeiadis V. Concurrent Separation Logic and Operational Semantics. Proceedings of MFPS. Elsevier Science Publishers Ltd.,2011.335-351.
[53]Liang H, Feng X. Modular Verification of Linearizability with Non-Fixed Linearization Points. Technical report, University of Science and Technology of China, March,2013. http://kyhcs.ustcsz.edu.cn/ relconcur/lin.
[54]Michael M M, Scott M L. Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algo-rithms. Proceedings of PODC, New York, NY, USA:ACM Press,1996.267-275.
[55]Harris T L. A Pragmatic Implementation of Non-blocking Linked-Lists. Proceedings of DISC, London, UK, UK:Springer,2001.300-314.
[56]Michael M M. High Performance Dynamic Lock-free Hash Tables and List-based Sets. Proceedings of SPAA, New York, NY, USA:ACM Press,2002.73-82.
[57]Vafeiadis V. Automatically Proving Linearizability. Proceedings of CAV. Springer,2010.450-464.
[58]O'Hearn P W, Rinetzky N, Vechev M T, et al. Verifying Linearizability with Hindsight. Proceedings of PODC. ACM Press,2010.85-94.
[59]Derrick J, Schellhorn G, Wehrheim H. Verifying Linearisability with Potential Linearisation Points. Proceed-ings of FM. Springer,2011.323-337.
[60]Schellhorn G, Wehrheim H, Derrick J. How to Prove Algorithms Linearisable. Proceedings of CAV. Springer, 2012.243-259.
[61]Elmas T, Qadeer S, Sezgin A, et al. Simplifying Linearizability Proofs with Reduction and Abstraction. Pro-ceedings of TACAS, Berlin, Heidelberg:Springer,2010.296-311.
[62]Liu Y, Chen W, Liu Y A, et al. Model Checking Linearizability via Refinement. Proceedings of FM. Springer; 2009.321-337.
[63]Vechev M T, Yahav E, Yorsh G. Experience with Model Checking Linearizability. Proceedings of SPIN. Springer,2009.261-278.
[64]Herlihy M. Wait-free Synchronization. ACM Trans. Program. Lang. Syst.,1991,13(1):124-149.
[65]Aspnes J, Herlihy M. Wait-free Data Structures in the Asynchronous PRAM Model. Proceedings of SPAA, New York, NY, USA:ACM,1990.340-349.
[66]Herlihy M, Luchangco V, Moir M. Obstruction-Free Synchronization:Double-Ended Queues as an Example. Proceedings of ICDCS, Washington, DC, USA:IEEE Computer Society,2003.522-529.
[67]Lamport L. A New Solution of Dijkstra's Concurrent Programming Problem. Commun. ACM,1974, 17(8):453-455.
[68]Herlihy M, Shavit N. On the Nature of Progress. Proceedings of OPODIS. Springer,2011.313-328.
[69]Fossati L, Honda K, Yoshida N. Intensional and extensional characterisation of global progress in the π-calculus. Proceedings of CONCUR. Springer,2012.287-301.
[70]Petrank E, Musuvathi M, Steesngaard B. Progress Guarantee for Parallel Programs via Bounded Lock-freedom. Proceedings of PLDI, New York, NY, USA:ACM Press,2009.144-154.
[71]Dongol B. Formalising Progress Properties of Non-blocking Programs. Proceedings of ICFEM,2006.284-303.
[72]Liang H, Hoffmann J, Feng X, et al. Characterizing Progress Properties of Concurrent Objects via Contex-tual Refinements. Technical report, University of Science and Technology of China, April,2013. http: //kyhcs.ustcsz.edu.cn/relconcur/prog.
-[2] Hoare C A R. Proof of Correctness of Data Representations. Acta Inf.,1972,1(4):271-281.
[3]Herlihy M, Shavit N. The Art of Multiprocessor Programming. Morgan Kaufmann, April,2008.
[4]Herlihy M P, Wing J M. Linearizability:A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst.,1990,12(3):463-492.
[5]Filipovic I, O'Hearn P, Rinetzky N, et al. Abstraction for concurrent objects. Theor. Comput. Sci.,2010, 411(51-52):4379-4398.
[6]Dice D, Shalev O, Shavit N. Transactional Locking II. Proceedings of DISC, Berlin, Heidelberg:Springer, 2006.194-208.
[7]Klein G, Andronick J, Elphinstone K, et al. seL4:Formal Verification of an Operating-system Kernel. Commun. ACM,2010,53(6):107-115.
'[8] He J, Hoare C A R, Sanders J W. Data Refinement Refined. Proceedings of ESOP. Springer,1986.187-196.
[9]Abadi M, Lamport L. The Existence of Refinement Mappings. Theor. Comput. Sci.,1991,82(2):253-284.
[10]Treiber R K. System programming:coping with parallelism. Technical Report RJ 5118, IBM Almaden Re-search Center,1986.
[11]Brookes S D. Full Abstraction for a Shared-Variable Parallel Language. Inf. Comput.,1996,127(2):145-163.
[12]Hur C K, Dreyer D. A Kripke Logical Relation Between ML and Assembly. Proceedings of POPL, New York, NY, USA:ACM Press,2011.133-146.
[13]Abadi M, Plotkin G. A model of cooperative threads. Proceedings of POPL, New York, NY, USA:ACM Press, 2009.29-40.
[14]Amit D, Rinetzky N, Reps T, et al. Comparison Under Abstraction for Verifying Linearizability. Proceedings of CAV, Berlin, Heidelberg:Springer,2007.477-490.
[15]Vafeiadis V. Modular fine-grained concurrency verification. Technical Report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory, July,2008.
[16]Derrick J, Schellhom G, Wehrheim H. Mechanically Verified Proof Obligations for Linearizability. ACM Trans. Program. Lang. Syst.,2011,33(1):4:1-4:43.
[17]Turon A J, Thamsborg J, Ahmed A, et al. Logical Relations for Fine-grained Concurrency. Proceedings of POPL, New York, NY, USA:ACM Press,2013.343-356.
[18]Hendler D, Shavit N, Yerushalmi L. A Scalable Lock-free Stack Algorithm. Proceedings of SPAA, New York, NY, USA:ACM Press,2004.206-215.
[19]Heller S, Herlihy M, Luchangco V, et al. A Lazy Concurrent List-based Set Algorithm. Proceedings of OPODIS, Berlin, Heidelberg:Springer,2006.3-16.
[20]Turon A, Wand M. A separation logic for refining concurrent objects. Proceedings of POPL, New York, NY, USA:ACM Press,2011.247-258.
[21]Gotsman A, Yang H. Liveness-preserving atomicity abstraction. Proceedings of ICALP. Springer,2011. 453-465.
[22]Jones C B. Tentative Steps Toward a Development Method for Interfering Programs. ACM Trans. Program. Lang. Syst,1983,5(4):596-619.
[23]Boehm H J, Demers A J, Shenker S. Mostly Parallel Garbage Collection. Proceedings of PLDI, New York, NY, USA:ACM Press,1991.157-164.
[24]Feng X. Local rely-guarantee reasoning. Proceedings of POPL, New York, NY, USA:ACM Press,2009. 315-327.
[25]Boehm H J. Threads cannot be implemented as a library. Proceedings of PLDI, New York, NY, USA:ACM Press,2005.261-268.
[26]Boehm H J, Adve S V. Foundations of the C++ concurrency memory model. Proceedings of PLDI, New York, NY, USA:ACM Press,2008.68-78.
[27]Benton N. Simple relational correctness proofs for static analyses and program transformations. Proceedings of POPL, New York, NY, USA:ACM Press,2004.14-25.
[28]Sevcik J, Vafeiadis V, Nardelli F Z, et al. Relaxed-Memory Concurrency and Verified Compilation. Proceedings of POPL, New York, NY, USA:ACM Press,2011.43-54.
[29]Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.3,2010. http: //coq.inria.fr.
[30]Liang H, Feng X, Fu M. A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transforma-tions. Technical report (with Coq implementation), University of Science and Technology of China, October, 2011. http://kyhcs.ustcsz.edu.cn/relconcur/rgsim.
[31]Reynolds J C. Separation Logic:A Logic for Shared Mutable Data Structures. Proceedings of LICS, Wash-ington, DC, USA:IEEE Computer Society,2002.55-74.
[32]Turon A, Dreyer D, Birkedal L. Unifying Refinement and Hoare-style Reasoning in a Logic for Higher-order Concurrency. Proceedings of ICFP'13, New York, NY, USA:ACM Press,2013.377-390.
[33]Yang H. Relational separation logic. Theor. Comput. Sci.,2007,375(1-3):308-334.
[34]Wand M. Compiler Correctness for Parallel Languages. Proceedings of FPCA, New York, NY, USA:ACM Press,1995.120-134.
[35]Gladstein D S, Wand M. Compiler Correctness for Concurrent Languages. Proceedings of COORDINATION, volume 1061 of Lecture Notes in Computer Science. Springer,1996.231-248.
[36]Lochbihler A. Verifying a Compiler for Java Threads. Proceedings of ESOP, Berlin, Heidelberg:Springer, 2010.427-447.
[37]Burckhardt S, Musuvathi M, Singh V. Verifying Local Transformations on Relaxed Memory Models. Proceed-ings of CC/ETAPS, Berlin, Heidelberg:Springer,2010.104-123.
[38]Barabash K, Ben-Yitzhak O, Goft I, et al. A parallel, incremental, mostly concurrent garbage collector for servers. ACM Trans. Program. Lang. Syst.,2005,27(6):1097-1146.
[39]Parkinson M, Bornat R, Calcagno C. Variables as Resource in Hoare Logics. Proceedings of LICS, Washington, DC, USA:IEEE Computer Society,2006.137-146.
[40]Vechev M T, Yahav E, Bacon D F. Correctness-Preserving Derivation of Concurrent Garbage Collection Al-gorithms. Proceedings of PLDI, New York, NY, USA:ACM Press,2006.341-353.
[41]Pavlovic D, Pepper P, Smith D R. Formal derivation of concurrent garbage collectors. Proceedings of MPC, 2010.353-376.
[42]Kapoor K, Lodaya K, Reddy U. Fine-grained concurrency with Separation Logic. J. Philosophical Logic,2011, 40(5):583-632.
[43]McCreight A, Shao Z, Lin C, et al. A General Framework for Certifying Garbage Collectors and Their Mutators. Proceedings of PLDI, New York, NY, USA:ACM Press,2007.468-479.
[44]O'Hearn P W. Resources, Concurrency, and Local Reasoning. Theor. Comput. Sci.,2007,375(1-3):271-307.
[45]Qadeer S, Sezgin A, Tasiran S. Back and Forth:Prophecy Variables for Static Verification of Concurrent Programs. Technical Report MSR-TR-2009-142, Microsoft, October,2009.
[46]Harris T L, Fraser K, Pratt I A. A Practical Multi-word Compare-and-Swap Operation. Proceedings of DISC, London, UK, UK:Springer,2002.265-279.
[47]Colvin R, Groves L, Luchangco V, et al. Formal verification of a lazy concurrent list-based set algorithm. Proceedings of CAV. Springer,2006.475-488.
[48]Lynch N A, Vaandrager F W. Forward and Backward Simulations:I. Untimed Systems. Inf. Comput.,1995, 121(2):214-233.
[49]Doherty S, Groves L, Luchangco V, et al. Formal Verification of a Practical Lock-Free Queue Algorithm. Proceedings of FORTE. Springer,2004.97-114.
[50]Gotsman A, Yang H. Linearizability with Ownership Transfer. Proceedings of CONCUR. Springer,2012. 256-271.
[51]O'Hearn P W, Yang H, Reynolds J C. Separation and Information Hiding. Proceedings of POPL, New York, NY, USA:ACM Press,2004.268-280.
[52]Vafeiadis V. Concurrent Separation Logic and Operational Semantics. Proceedings of MFPS. Elsevier Science Publishers Ltd.,2011.335-351.
[53]Liang H, Feng X. Modular Verification of Linearizability with Non-Fixed Linearization Points. Technical report, University of Science and Technology of China, March,2013. http://kyhcs.ustcsz.edu.cn/ relconcur/lin.
[54]Michael M M, Scott M L. Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algo-rithms. Proceedings of PODC, New York, NY, USA:ACM Press,1996.267-275.
[55]Harris T L. A Pragmatic Implementation of Non-blocking Linked-Lists. Proceedings of DISC, London, UK, UK:Springer,2001.300-314.
[56]Michael M M. High Performance Dynamic Lock-free Hash Tables and List-based Sets. Proceedings of SPAA, New York, NY, USA:ACM Press,2002.73-82.
[57]Vafeiadis V. Automatically Proving Linearizability. Proceedings of CAV. Springer,2010.450-464.
[58]O'Hearn P W, Rinetzky N, Vechev M T, et al. Verifying Linearizability with Hindsight. Proceedings of PODC. ACM Press,2010.85-94.
[59]Derrick J, Schellhorn G, Wehrheim H. Verifying Linearisability with Potential Linearisation Points. Proceed-ings of FM. Springer,2011.323-337.
[60]Schellhorn G, Wehrheim H, Derrick J. How to Prove Algorithms Linearisable. Proceedings of CAV. Springer, 2012.243-259.
[61]Elmas T, Qadeer S, Sezgin A, et al. Simplifying Linearizability Proofs with Reduction and Abstraction. Pro-ceedings of TACAS, Berlin, Heidelberg:Springer,2010.296-311.
[62]Liu Y, Chen W, Liu Y A, et al. Model Checking Linearizability via Refinement. Proceedings of FM. Springer; 2009.321-337.
[63]Vechev M T, Yahav E, Yorsh G. Experience with Model Checking Linearizability. Proceedings of SPIN. Springer,2009.261-278.
[64]Herlihy M. Wait-free Synchronization. ACM Trans. Program. Lang. Syst.,1991,13(1):124-149.
[65]Aspnes J, Herlihy M. Wait-free Data Structures in the Asynchronous PRAM Model. Proceedings of SPAA, New York, NY, USA:ACM,1990.340-349.
[66]Herlihy M, Luchangco V, Moir M. Obstruction-Free Synchronization:Double-Ended Queues as an Example. Proceedings of ICDCS, Washington, DC, USA:IEEE Computer Society,2003.522-529.
[67]Lamport L. A New Solution of Dijkstra's Concurrent Programming Problem. Commun. ACM,1974, 17(8):453-455.
[68]Herlihy M, Shavit N. On the Nature of Progress. Proceedings of OPODIS. Springer,2011.313-328.
[69]Fossati L, Honda K, Yoshida N. Intensional and extensional characterisation of global progress in the π-calculus. Proceedings of CONCUR. Springer,2012.287-301.
[70]Petrank E, Musuvathi M, Steesngaard B. Progress Guarantee for Parallel Programs via Bounded Lock-freedom. Proceedings of PLDI, New York, NY, USA:ACM Press,2009.144-154.
[71]Dongol B. Formalising Progress Properties of Non-blocking Programs. Proceedings of ICFEM,2006.284-303.
[72]Liang H, Hoffmann J, Feng X, et al. Characterizing Progress Properties of Concurrent Objects via Contex-tual Refinements. Technical report, University of Science and Technology of China, April,2013. http: //kyhcs.ustcsz.edu.cn/relconcur/prog.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |