使用事务内存同步机制的并行程序验证的研究
|
摘要
近年来,随着超线程、多核体系结构等多线程技术的发展和广泛应用,计算机硬件已经提供了越来越高效的软件运行平台。但是要更好地利用这些平台的并行优势,计算机软件就需要具备更好地并行性,以充分利用多个处理器的性能。并行程序已经成为了软件开发的主流。然而要确保顺序程序的正确性已经是非常困难的了,要保证并行程序的正确性难度更甚。这是因为在并行程序中,程序员还需要处理共享数据的并发存取问题,确保数据在不同线程中的有效性。传统上,程序员使用锁的方式来管理并行程序中共享数据的并发存取。但是锁方式不仅难于推理,而且还容易出现死锁等导致程序进入异常执行状态的隐患。为减轻程序员开发并行程序的负担,提高软件开发的效率,近年的研究提出了使用事务内存同步机制来管理共享数据的并发存取。提供了事务内存同步机制的系统通过自动地管理数据的并发访问,免除了程序员在这方面的负担,也避免了死锁等锁机制的致命隐患。但是近年来围绕着事务内存同步机制的研究主要集中于提供事务内存同步机制的系统的各种实现策略及其性能的提高上,而对该同步机制在程序推理、形式验证及易于推理方面的研究甚少。
针对事务内存同步机制相关研究的现状,基于程序推理验证的研究成果,本文提出了一种推理方法以推理使用了事务内存同步机制的实现系统所提供的编程结构的程序。该推理方法基于众所周知的不变式证明(Invariance Proof)方法并对Hoare逻辑进行了扩展,通过指明共享数据上的不变式来约束多个线程间的并发访问,可靠、可行,并具备模块化验证的特点。同时,本文还专注于事务内存同步机制的语义研究,在携带证明的代码的研究的基础上,将所提出的推理方法形式化到遵循事务内存同步机制语义的Hoare风格的验证框架中,并证明了推理方法遵循事务内存同步机制的语义的可靠性。此外,本文还给出了推理验证的应用实例,展示了本文所提出的推理方法和验证框架的有效性。最后,本文通过详尽的比较,阐明了事务内存同步机制相对于传统的锁同步机制易推理的优点,展示了事务内存同步机制对程序推理的简化。
本文的主要特色和贡献为:
·本文提出了一种Hoare风格的推理方法,用于在事务内存同步机制的语义的高层抽象上推理源语言级的并行程序。
·本文也提出了一个携带证明的代码(Proof-Carrying Code)风格的验证框架,用于在事务内存同步机制的语义的底层实现上验证汇编级的并行程序,并证明了验证框架遵循事务内存同步机制的语义的可靠性。该验证框架的提出,填补了携带证明的代码的研究在事务内存同步机制方面的空白。
·本文在Coq定理证明辅助工具中完成了所提出的验证框架的可靠性证明,从而将验证框架中的验证推理系统从受信任计算基础中排除出去,使得本文的验证框架具有更高的可靠性。
·本文还通过详细的比较阐述了事务内存同步机制相对于锁同步机制的易推理的优势。
The multicore architecture, which has provided infrastructures of better performance, has become popular. To benefit from this growth in performance, programmers are required to develop multi-threaded programs. Whereas it is difficult to ensure correctness for sequential programs, it is even more so for concurrent programs due to the interaction between multiple threads. Traditionally, programmers use locks to achieve mutual exclusion on concurrent access to shared resources. But lock-based programming is difficult to reason about and may lead to problems such as deadlock. Transactional memory (TM) is proposed as an alternate concurrency-control mechanism to avoid many of the pitfalls of the lock-based one. TM systems manage data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound.
This dissertation presents a reasoning method for programs using TM and formalizes it into a Hoare-style verification framework. The reasoning method is based on invariance proof and Hoare-style reasoning and supports modular verification. The proof-carrying code (PCC) style framework is proved sound with respect to the TM semantics. And a comparison between lock-based reasoning and TM-based reasoning is presented and shows the convenience of the latter. This dissertation makes the following contributions:
It presents a Hoare-style reasoning method to reason about source-level programs using TM. Even though programming using transactions is supposed to reason about easily, there are subtle properties expected by multithreaded programs. To ensure such properties are correctly enforced in a concurrent program, programmers must reason about the behaviors of their programs thoroughly. This dissertation presents a method to perform such TM-based reasoning. And the presented reasoning is based on the same intended semantics of different TM systems: to provide a programming structure that executes atomically and in isolation. This makes the presented reasoning compatible with various TM systems that respect the same intended semantics.
It also presents a proof-carrying code style framework to certify the properties of assembly level programs using TM. The presented framework brings PCC into the brand-new TM area. The inference rules of the framework are proved sound with respect to the TM semantics. And examples are also given to illustrate the construction of the proofs for programs in the framework, demonstrating the effectiveness of the framework.
The presented framework addresses safety issues at assembly-level directly as PCC systems do. So the complicated and error-prone compilation and optimization do not need to be trusted. And the presented reasoning method is formalize into framework and is sound due to the soundness of the framework. All the work on the framework, including its soundness proof and examples, is mechanized in proof assistant Coq. This makes our work more reliable.
Through thorough comparison, it shows the convenience of TM-based reasoning over lock-based reasoning.
针对事务内存同步机制相关研究的现状,基于程序推理验证的研究成果,本文提出了一种推理方法以推理使用了事务内存同步机制的实现系统所提供的编程结构的程序。该推理方法基于众所周知的不变式证明(Invariance Proof)方法并对Hoare逻辑进行了扩展,通过指明共享数据上的不变式来约束多个线程间的并发访问,可靠、可行,并具备模块化验证的特点。同时,本文还专注于事务内存同步机制的语义研究,在携带证明的代码的研究的基础上,将所提出的推理方法形式化到遵循事务内存同步机制语义的Hoare风格的验证框架中,并证明了推理方法遵循事务内存同步机制的语义的可靠性。此外,本文还给出了推理验证的应用实例,展示了本文所提出的推理方法和验证框架的有效性。最后,本文通过详尽的比较,阐明了事务内存同步机制相对于传统的锁同步机制易推理的优点,展示了事务内存同步机制对程序推理的简化。
本文的主要特色和贡献为:
·本文提出了一种Hoare风格的推理方法,用于在事务内存同步机制的语义的高层抽象上推理源语言级的并行程序。
·本文也提出了一个携带证明的代码(Proof-Carrying Code)风格的验证框架,用于在事务内存同步机制的语义的底层实现上验证汇编级的并行程序,并证明了验证框架遵循事务内存同步机制的语义的可靠性。该验证框架的提出,填补了携带证明的代码的研究在事务内存同步机制方面的空白。
·本文在Coq定理证明辅助工具中完成了所提出的验证框架的可靠性证明,从而将验证框架中的验证推理系统从受信任计算基础中排除出去,使得本文的验证框架具有更高的可靠性。
·本文还通过详细的比较阐述了事务内存同步机制相对于锁同步机制的易推理的优势。
The multicore architecture, which has provided infrastructures of better performance, has become popular. To benefit from this growth in performance, programmers are required to develop multi-threaded programs. Whereas it is difficult to ensure correctness for sequential programs, it is even more so for concurrent programs due to the interaction between multiple threads. Traditionally, programmers use locks to achieve mutual exclusion on concurrent access to shared resources. But lock-based programming is difficult to reason about and may lead to problems such as deadlock. Transactional memory (TM) is proposed as an alternate concurrency-control mechanism to avoid many of the pitfalls of the lock-based one. TM systems manage data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound.
This dissertation presents a reasoning method for programs using TM and formalizes it into a Hoare-style verification framework. The reasoning method is based on invariance proof and Hoare-style reasoning and supports modular verification. The proof-carrying code (PCC) style framework is proved sound with respect to the TM semantics. And a comparison between lock-based reasoning and TM-based reasoning is presented and shows the convenience of the latter. This dissertation makes the following contributions:
It presents a Hoare-style reasoning method to reason about source-level programs using TM. Even though programming using transactions is supposed to reason about easily, there are subtle properties expected by multithreaded programs. To ensure such properties are correctly enforced in a concurrent program, programmers must reason about the behaviors of their programs thoroughly. This dissertation presents a method to perform such TM-based reasoning. And the presented reasoning is based on the same intended semantics of different TM systems: to provide a programming structure that executes atomically and in isolation. This makes the presented reasoning compatible with various TM systems that respect the same intended semantics.
It also presents a proof-carrying code style framework to certify the properties of assembly level programs using TM. The presented framework brings PCC into the brand-new TM area. The inference rules of the framework are proved sound with respect to the TM semantics. And examples are also given to illustrate the construction of the proofs for programs in the framework, demonstrating the effectiveness of the framework.
The presented framework addresses safety issues at assembly-level directly as PCC systems do. So the complicated and error-prone compilation and optimization do not need to be trusted. And the presented reasoning method is formalize into framework and is sound due to the soundness of the framework. All the work on the framework, including its soundness proof and examples, is mechanized in proof assistant Coq. This makes our work more reliable.
Through thorough comparison, it shows the convenience of TM-based reasoning over lock-based reasoning.
引文
Abadi M, Lamport L. 1993. Composing specifications[J]. ACM Trans. Program. Lang. Syst., 15(1):73-132.
Abadi M, Lamport L. 1995. Conjoining specifications[J]. ACM Trans. Program. Lang. Syst., 17(3):507-535.
Abadi M, Birrell A, Harris T, et al. 2008. Semantics of transactional memory and automatic mutual exclusion[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:63-74.
Ananian C S, Asanovic K, Kuszmaul B C, et al. 2005. Unbounded Transactional Memory [C]//HPCA '05: Proceedings of the 11th International Symposium on High-Performance Computer Architecture. Washington, DC, USA: IEEE Computer Society:316-327.
Appel A W. 2001. Foundational Proof-Carrying Code[C]//LICS '01: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:247-258.
Appel A W, Felty A P. 2000. A semantic model of types and machine instructions for proof-carrying code[C]//POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:243-253.
APT K R. 1981. Ten Years of Hoare's Logic: A Survey-Part I[J]. ACM Trans. Program. Lang. Syst., 3(4):431-483.
Bornat R, Calcagno C, O'Hearn P, et al. 2005. Permission accounting in separation logic[C]//POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:259-270.
Bowen J P. 1996. Formal Specification and Documentation using Z: A Case Study Approach[M].[S.1.]: International Thomson Computer Press.
Bowen J P, Franzle M, Olderog E R, et al. 1993. Developing Correct Systems[C]//Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland.[S.l.]: IEEE Computer Society Press: 176-187.
Brookes S. 2007. A semantics for concurrent separation logic[J]. Theor. Comput. Sci., 375(1-3):227-270.
Cau A, Collette P. 1996. Parallel composition of assumption-commitment specifications[J]. Acta Inf., 33(2):153-176.
Chaki S, Clarke E, Groce A, et al. 2004. Modular Verification of Software Components in C[J]. IEEE Trans. Softw. Eng., 30(6):388-402.
Chen J, Wu D, Appel A W, et al. 2003. A provably sound TAL for back-end optimization[C]//PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation. New York, NY, USA: ACM:208-219.
Clarke E M, Wing J M. 1996. Formal methods: state of the art and future directions[J]. ACM Comput. Surv., 28(4):626-643.
DAMRON P, Fedorova A, Lev Y, et al. 2006. Hybrid transactional memory[C]//ASPLOS-XII: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems. New York, NY, USA: ACM:336-346.
Demartini C, Iosif R, Sisto R. 1999. dSPIN: A Dynamic Extension of SPIN [C]//Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking. London, UK: Springer-Verlag: 261-276.
Feng X, Shao Z. 2005. Modular verification of concurrent assembly code with dynamic thread creation and termination[C]//ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:254-267.
Feng X, Shao Z, Vaynberg A, et al. 2006. Modular verification of assembly code with stack-based control abstractions[C]//PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:401-414.
Feng X, Ferreira R, Shao Z. 2007a. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning[C]//In Proc. 16th European Symposium on Programming (ESOP'07). Braga, Portugal: [s.n.] . Lecture Notes in Computer Science, vol. 4421.
Feng X, Ni Z, Shao Z, et al. 2007b. An open framework for foundational
proof-carrying code[C]//TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation. New York, NY, USA: ACM:67-78.
Feng X, Shao Z, Dong Y, et al. 2008. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads[C]//PLDI'08: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. Tucson, Arizona, USA: [s.n.] .
Flanagan C, Abadi M. 1999a. Object Types against Races[C]//CONCUR '99: Proceedings of the 10th International Conference on Concurrency Theory. London, UK: Springer-Verlag:288-303.
Flanagan C, Abadi M. 1999b. Types for Safe Locking[C]//Proceedings of the 8th European Symposium on Programming Languages and Systems.[S.l.]: Springer-Verlag:91-108.
Flanagan C, Qadeer S. 2003a. Thread-Modular Model Checking[C]//Proc. 10th SPIN workshop. [S.l.]: [s.n.] :213-224.
Flanagan C, Qadeer S. 2003b. A type and effect system for atomicity [C]//PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation. New York, NY, USA: ACM:338-349.
Flanagan C, Freund S N, Qadeer S. 2002. Thread-Modular Verification for Shared-Memory Programs[C]//ESOP '02: Proceedings of the 11th European Symposium on Programming Languages and Systems. London, UK: Springer-Verlag:262-277.
FLOYD R W. Assigning meanings to programs[C]//American Mathematical Society Symposium in Applied Mathematics. Providence, R.I.: [s.n.] , 19.
FRANCEZ N, Pnueli A. 1978. A proof method for cyclic programs[J]. Acta Informatica, 9:133-157.
Giannakopoulou D, P"s"reanu C S, Barringer H. 2002. Assumption Generation for Software Component Verification [C]//ASE '02: Proceedings of the 17th IEEE international conference on Automated software engineering. Washington, DC, USA: IEEE Computer Society:3.
Gray J, Reuter A. 1992. Transaction Processing: Concepts and Techniques[M]. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc.
Grossman D. 2003. Type-safe multithreading in cyclone[C]//TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in lan- guages design and implementation. New York, NY, USA: ACM:13-25.
Hamid N A, Shao Z, Trifonov V, et al. 2002. A Syntactic Approach to Foundational Proof-Carrying Code[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:89-100.
Hammond L, Wong V, Chen M, et al. 2004. Transactional Memory Coherence and Consistency[C]//ISCA '04: Proceedings of the 31st annual international symposium on Computer architecture. Washington, DC, USA: IEEE Computer Society:102.
Harris T, Fraser K. 2003. Language support for lightweight transac-tions[C]//OOPSLA '03: Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications. New York, NY, USA: ACM:388-402.
Harris T, Jones S P. 2006. Transactional memory with data invari-ants[C]//The First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT06). Ottawa, Canada: [s.n.] .
Harris T, Marlow S, Peyton-Jones S, et al. 2005. Composable memory transactions[C]//PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming. New York, NY, USA: ACM:48-60.
HAVELUND K, Pressburger T. 2000. Model Checking Java Programs using Java PathFinder[J]. Software Tools for Technology Transfer (STTT), 2(4): 72-84.
Henzinger T A, Qadeer S, Rajamani S K, et al. 2002. An assume-guarantee rule for checking simulation[J]. ACM Trans. Program. Lang. Syst., 24(1):51-64.
Henzinger T A, Jhala R, Majumdar R. 2004. Race checking by context inference[C]//PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation. New York, NY, USA: ACM:1-13.
Herlihy M, Moss J E B. 1993. Transactional memory: architectural support for lock-free data structures[C]//ISCA '93: Proceedings of the 20th annual international symposium on Computer architecture. New York, NY, USA: ACM:289-300.
Herlihy M, Luchangco V, Moir M, et al. 2003. Software transactional memory for dynamic-sized data structures[C]//PODC '03: Proceedings of the twenty-second annual symposium on Principles of distributed computing. New York, NY, USA: ACM:92-101.
HOARE C A R. 1969. An axiomatic basis for computer programming[J]. Coramun. ACM, 12(10):576-580.
HOLZMANN G J. 1995. Tutorial: Proving Properties of Concurrent System with SPIN[C]//CONCUR '95: Proceedings of the 6th International Conference on Concurrency Theory. London, UK: Springer-Verlag:453-455.
Igarashi A, Pierce B, Wadler P. 1999. Featherwieght Java: a minimal core calculus for Java and GJ[C]//OOPSLA '99: Proceedings of the 14th ACM SIG-PLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM:132-146.
Jones C B. 1983. Tentative steps toward a development method for interfering programs[J]. ACM Trans. Program. Lang. Syst., 5(4):596-619.
Lamport L. 1994. The temporal logic of actions[J]. ACM Trans. Program. Lang. Syst., 16(3):872-923.
Lamport L, Schneider F B. 1984. The "Hoare Logic" of CSP, and All That[J]. ACM Trans. Program. Lang. Syst., 6(2):281-296.
Li L, Li Y. 2007. Coq implementation for certifying concurrent programs using transactional memory [EB/OL]. http://ssg.ustcsz.edu.cn/ccac/index.html.
Liblit B. 2006. An Operational Semantics for LogTM[R].[S.l.]: University of Wisconsin-Madison. Version 1.0.
Lin C, Chen Y, Li L, et al. 2007. Garbage Collector Verification for Proof-Carrying Code[J]. Journal of Computer Science and Technology, 22(3):426-437.
Martin M, Blundell C, Lewis E. 2006. Subtleties of Transactional Memory Atomicity Semantics[J]. IEEE Comput. Archit. Lett., 5(2):17.
McCreight A, Shao Z, Lin C, et al. 2007. A general framework for certifying garbage collectors and their mutators[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:468-479.
MISRA J, Chandy K M. 1981. Proofs of networks of processes[J]. IEEE Transactions on Software Engineering, 7(7):417-426.
MOORE K E, Bobba J, Moravan M J, et al. 2006. LogTM: Log-based Transactional Memory[C]//Proceedings of the 12th International Symposium on High-Performance Computer Architecture. Austin, Texas, USA: IEEE Computer Society Press .254-265.
Moore K F, Grossman D. 2007. High-Level Small-Step Operational Semantics for Transactions[C]//2nd ACM SIGPLAN Workshop on Transactional Computing. [S.l.]: [s.n.] .
Moore K F, Grossman D. 2008. High-level small-step operational semantics for transactions[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:51-62.
Necula G C. 1997. Proof-carrying code[C]//POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:106-119.
Ni Z, Shao Z. 2006. Certified assembly programming with embedded code point-ers[C]//POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:320-333.
O'Hearn P W. 2007. Resources, concurrency, and local reasoning[J]. Theor. Comput. Sci., 375(1-3):271-307.
Ossefort M. 1983. Correctness Proofs of Communicating Processes: Three Illustrative Examples From the Literature[J]. ACM Trans. Program. Lang. Syst., 5(4).620-640.
Owicki S, Gries D. 1976. An axiomatic proof technique for parallel programs[J]. Acta Informatica, 6(4):319-340.
Paulin-Mohring C. 1993. Inductive Definitions in the system Coq - Rules and Properties[C]//TLCA '93: Proceedings of the International Conference on Typed Lambda Calculi and Applications. London, UK: Springer-Verlag:328-345.
Pnueli A. 1985. Logics and models of concurrent systems(123-144):In transition from global to modular temporal reasoning about programs[M]. New York, NY, USA: Springer-Verlag New York, Inc.
Reynolds J C. 2002. Separation Logic: A Logic for Shared Mutable Data Structures[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:55-74.
Saha B, Adl-Tabatabai A R, Hudson R L, et al. 2006. McRT-STM: a high performance software transactional memory system for a multi-core run-time[C]//PPoPP '06: Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. New York, NY, USA: ACM:187-197.
Scott M L. 2006. Sequential Specification of Transactional Memory Seman-tics[C]//Proceedings of the First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing. [S.l.]: [s.n.] .
Shavit N, Touitou D. 1995. Software transactional memory[C]//PODC '95: Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing. New York, NY, USA: ACM:204-213.
Shpeisman T, Menon V, Adl-Tabatabai A R, et al. 2007. Enforcing isolation and ordering in STM[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:78-88.
Spear M F, Marathe V J, Dalessandro L, et al. 2007. Privatization techniques for software transactional memory[C]//PODC '07: Proceedings of the twenty-sixth annual ACM symposium on Principles of distributed computing. New York, NY, USA: ACM:338-339.
Stark E W. 1985. A Proof Technique for Rely/Guarantee Proper-ties[C]//Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science. London, UK: Springer-Verlag:369-391.
Stirling C. 1988. A generalization of Owicki-Gries's Hoare logic for a concurrent while language[J]. Theor. Comput. Sci., 58(1-3):347-359.
Team C D. 2005. The Coq Proof Assistant Reference Manual v8.0[EB-OL].
Tennent R D. 1997. Foundations for Programming Languages by John C. Mitchell, MIT Press, 1996.[J]. J. Funct. Program., 7(6):667-668.
VITEK J, JAGANNATHAN S, Welc A, et al. 2004. A Semantic Framework for Designer Transactions[C] //Proceedings of the European Symposium on Programming. [S.l.]: Springer-Verlag. Lecture Notes in Computer Science, vol. 2986, Apr.
Xiang S, Chen Y, Lin C, et al. 2006. Modularly Certified Dynamic Storage Allocation in SCAP[C]//Proceedings of Sixth International Conference on Quality Software (QSIC'06). Beijing, China: IEEE Computer Society:321-328.
Xu Q, Cau A, Collette P. 1994. On Unifying Assumption-Commitment
Style Proof Rules for Concurrency[C]//CONCUR '94: Proceedings of the Concurrency Theory. London, UK: Springer-Verlag:267-282.
Yahav E. 2001. Verifying safety properties of concurrent Java programs using 3-valued logic[C]//POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:27-40.
Yu D, Shao Z. 2004. Verification of safety properties for concurrent assembly code[C]//ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:175-188.
Yu D, Hamid N A, Shao Z. 2004. Building certified libraries for PCC: dynamic storage allocation[J]. Sci. Comput. Program., 50(1-3):101-127.
Abadi M, Lamport L. 1995. Conjoining specifications[J]. ACM Trans. Program. Lang. Syst., 17(3):507-535.
Abadi M, Birrell A, Harris T, et al. 2008. Semantics of transactional memory and automatic mutual exclusion[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:63-74.
Ananian C S, Asanovic K, Kuszmaul B C, et al. 2005. Unbounded Transactional Memory [C]//HPCA '05: Proceedings of the 11th International Symposium on High-Performance Computer Architecture. Washington, DC, USA: IEEE Computer Society:316-327.
Appel A W. 2001. Foundational Proof-Carrying Code[C]//LICS '01: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:247-258.
Appel A W, Felty A P. 2000. A semantic model of types and machine instructions for proof-carrying code[C]//POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:243-253.
APT K R. 1981. Ten Years of Hoare's Logic: A Survey-Part I[J]. ACM Trans. Program. Lang. Syst., 3(4):431-483.
Bornat R, Calcagno C, O'Hearn P, et al. 2005. Permission accounting in separation logic[C]//POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:259-270.
Bowen J P. 1996. Formal Specification and Documentation using Z: A Case Study Approach[M].[S.1.]: International Thomson Computer Press.
Bowen J P, Franzle M, Olderog E R, et al. 1993. Developing Correct Systems[C]//Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland.[S.l.]: IEEE Computer Society Press: 176-187.
Brookes S. 2007. A semantics for concurrent separation logic[J]. Theor. Comput. Sci., 375(1-3):227-270.
Cau A, Collette P. 1996. Parallel composition of assumption-commitment specifications[J]. Acta Inf., 33(2):153-176.
Chaki S, Clarke E, Groce A, et al. 2004. Modular Verification of Software Components in C[J]. IEEE Trans. Softw. Eng., 30(6):388-402.
Chen J, Wu D, Appel A W, et al. 2003. A provably sound TAL for back-end optimization[C]//PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation. New York, NY, USA: ACM:208-219.
Clarke E M, Wing J M. 1996. Formal methods: state of the art and future directions[J]. ACM Comput. Surv., 28(4):626-643.
DAMRON P, Fedorova A, Lev Y, et al. 2006. Hybrid transactional memory[C]//ASPLOS-XII: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems. New York, NY, USA: ACM:336-346.
Demartini C, Iosif R, Sisto R. 1999. dSPIN: A Dynamic Extension of SPIN [C]//Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking. London, UK: Springer-Verlag: 261-276.
Feng X, Shao Z. 2005. Modular verification of concurrent assembly code with dynamic thread creation and termination[C]//ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:254-267.
Feng X, Shao Z, Vaynberg A, et al. 2006. Modular verification of assembly code with stack-based control abstractions[C]//PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:401-414.
Feng X, Ferreira R, Shao Z. 2007a. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning[C]//In Proc. 16th European Symposium on Programming (ESOP'07). Braga, Portugal: [s.n.] . Lecture Notes in Computer Science, vol. 4421.
Feng X, Ni Z, Shao Z, et al. 2007b. An open framework for foundational
proof-carrying code[C]//TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation. New York, NY, USA: ACM:67-78.
Feng X, Shao Z, Dong Y, et al. 2008. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads[C]//PLDI'08: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. Tucson, Arizona, USA: [s.n.] .
Flanagan C, Abadi M. 1999a. Object Types against Races[C]//CONCUR '99: Proceedings of the 10th International Conference on Concurrency Theory. London, UK: Springer-Verlag:288-303.
Flanagan C, Abadi M. 1999b. Types for Safe Locking[C]//Proceedings of the 8th European Symposium on Programming Languages and Systems.[S.l.]: Springer-Verlag:91-108.
Flanagan C, Qadeer S. 2003a. Thread-Modular Model Checking[C]//Proc. 10th SPIN workshop. [S.l.]: [s.n.] :213-224.
Flanagan C, Qadeer S. 2003b. A type and effect system for atomicity [C]//PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation. New York, NY, USA: ACM:338-349.
Flanagan C, Freund S N, Qadeer S. 2002. Thread-Modular Verification for Shared-Memory Programs[C]//ESOP '02: Proceedings of the 11th European Symposium on Programming Languages and Systems. London, UK: Springer-Verlag:262-277.
FLOYD R W. Assigning meanings to programs[C]//American Mathematical Society Symposium in Applied Mathematics. Providence, R.I.: [s.n.] , 19.
FRANCEZ N, Pnueli A. 1978. A proof method for cyclic programs[J]. Acta Informatica, 9:133-157.
Giannakopoulou D, P"s"reanu C S, Barringer H. 2002. Assumption Generation for Software Component Verification [C]//ASE '02: Proceedings of the 17th IEEE international conference on Automated software engineering. Washington, DC, USA: IEEE Computer Society:3.
Gray J, Reuter A. 1992. Transaction Processing: Concepts and Techniques[M]. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc.
Grossman D. 2003. Type-safe multithreading in cyclone[C]//TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in lan- guages design and implementation. New York, NY, USA: ACM:13-25.
Hamid N A, Shao Z, Trifonov V, et al. 2002. A Syntactic Approach to Foundational Proof-Carrying Code[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:89-100.
Hammond L, Wong V, Chen M, et al. 2004. Transactional Memory Coherence and Consistency[C]//ISCA '04: Proceedings of the 31st annual international symposium on Computer architecture. Washington, DC, USA: IEEE Computer Society:102.
Harris T, Fraser K. 2003. Language support for lightweight transac-tions[C]//OOPSLA '03: Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications. New York, NY, USA: ACM:388-402.
Harris T, Jones S P. 2006. Transactional memory with data invari-ants[C]//The First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT06). Ottawa, Canada: [s.n.] .
Harris T, Marlow S, Peyton-Jones S, et al. 2005. Composable memory transactions[C]//PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming. New York, NY, USA: ACM:48-60.
HAVELUND K, Pressburger T. 2000. Model Checking Java Programs using Java PathFinder[J]. Software Tools for Technology Transfer (STTT), 2(4): 72-84.
Henzinger T A, Qadeer S, Rajamani S K, et al. 2002. An assume-guarantee rule for checking simulation[J]. ACM Trans. Program. Lang. Syst., 24(1):51-64.
Henzinger T A, Jhala R, Majumdar R. 2004. Race checking by context inference[C]//PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation. New York, NY, USA: ACM:1-13.
Herlihy M, Moss J E B. 1993. Transactional memory: architectural support for lock-free data structures[C]//ISCA '93: Proceedings of the 20th annual international symposium on Computer architecture. New York, NY, USA: ACM:289-300.
Herlihy M, Luchangco V, Moir M, et al. 2003. Software transactional memory for dynamic-sized data structures[C]//PODC '03: Proceedings of the twenty-second annual symposium on Principles of distributed computing. New York, NY, USA: ACM:92-101.
HOARE C A R. 1969. An axiomatic basis for computer programming[J]. Coramun. ACM, 12(10):576-580.
HOLZMANN G J. 1995. Tutorial: Proving Properties of Concurrent System with SPIN[C]//CONCUR '95: Proceedings of the 6th International Conference on Concurrency Theory. London, UK: Springer-Verlag:453-455.
Igarashi A, Pierce B, Wadler P. 1999. Featherwieght Java: a minimal core calculus for Java and GJ[C]//OOPSLA '99: Proceedings of the 14th ACM SIG-PLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM:132-146.
Jones C B. 1983. Tentative steps toward a development method for interfering programs[J]. ACM Trans. Program. Lang. Syst., 5(4):596-619.
Lamport L. 1994. The temporal logic of actions[J]. ACM Trans. Program. Lang. Syst., 16(3):872-923.
Lamport L, Schneider F B. 1984. The "Hoare Logic" of CSP, and All That[J]. ACM Trans. Program. Lang. Syst., 6(2):281-296.
Li L, Li Y. 2007. Coq implementation for certifying concurrent programs using transactional memory [EB/OL]. http://ssg.ustcsz.edu.cn/ccac/index.html.
Liblit B. 2006. An Operational Semantics for LogTM[R].[S.l.]: University of Wisconsin-Madison. Version 1.0.
Lin C, Chen Y, Li L, et al. 2007. Garbage Collector Verification for Proof-Carrying Code[J]. Journal of Computer Science and Technology, 22(3):426-437.
Martin M, Blundell C, Lewis E. 2006. Subtleties of Transactional Memory Atomicity Semantics[J]. IEEE Comput. Archit. Lett., 5(2):17.
McCreight A, Shao Z, Lin C, et al. 2007. A general framework for certifying garbage collectors and their mutators[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:468-479.
MISRA J, Chandy K M. 1981. Proofs of networks of processes[J]. IEEE Transactions on Software Engineering, 7(7):417-426.
MOORE K E, Bobba J, Moravan M J, et al. 2006. LogTM: Log-based Transactional Memory[C]//Proceedings of the 12th International Symposium on High-Performance Computer Architecture. Austin, Texas, USA: IEEE Computer Society Press .254-265.
Moore K F, Grossman D. 2007. High-Level Small-Step Operational Semantics for Transactions[C]//2nd ACM SIGPLAN Workshop on Transactional Computing. [S.l.]: [s.n.] .
Moore K F, Grossman D. 2008. High-level small-step operational semantics for transactions[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:51-62.
Necula G C. 1997. Proof-carrying code[C]//POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:106-119.
Ni Z, Shao Z. 2006. Certified assembly programming with embedded code point-ers[C]//POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:320-333.
O'Hearn P W. 2007. Resources, concurrency, and local reasoning[J]. Theor. Comput. Sci., 375(1-3):271-307.
Ossefort M. 1983. Correctness Proofs of Communicating Processes: Three Illustrative Examples From the Literature[J]. ACM Trans. Program. Lang. Syst., 5(4).620-640.
Owicki S, Gries D. 1976. An axiomatic proof technique for parallel programs[J]. Acta Informatica, 6(4):319-340.
Paulin-Mohring C. 1993. Inductive Definitions in the system Coq - Rules and Properties[C]//TLCA '93: Proceedings of the International Conference on Typed Lambda Calculi and Applications. London, UK: Springer-Verlag:328-345.
Pnueli A. 1985. Logics and models of concurrent systems(123-144):In transition from global to modular temporal reasoning about programs[M]. New York, NY, USA: Springer-Verlag New York, Inc.
Reynolds J C. 2002. Separation Logic: A Logic for Shared Mutable Data Structures[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:55-74.
Saha B, Adl-Tabatabai A R, Hudson R L, et al. 2006. McRT-STM: a high performance software transactional memory system for a multi-core run-time[C]//PPoPP '06: Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. New York, NY, USA: ACM:187-197.
Scott M L. 2006. Sequential Specification of Transactional Memory Seman-tics[C]//Proceedings of the First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing. [S.l.]: [s.n.] .
Shavit N, Touitou D. 1995. Software transactional memory[C]//PODC '95: Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing. New York, NY, USA: ACM:204-213.
Shpeisman T, Menon V, Adl-Tabatabai A R, et al. 2007. Enforcing isolation and ordering in STM[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:78-88.
Spear M F, Marathe V J, Dalessandro L, et al. 2007. Privatization techniques for software transactional memory[C]//PODC '07: Proceedings of the twenty-sixth annual ACM symposium on Principles of distributed computing. New York, NY, USA: ACM:338-339.
Stark E W. 1985. A Proof Technique for Rely/Guarantee Proper-ties[C]//Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science. London, UK: Springer-Verlag:369-391.
Stirling C. 1988. A generalization of Owicki-Gries's Hoare logic for a concurrent while language[J]. Theor. Comput. Sci., 58(1-3):347-359.
Team C D. 2005. The Coq Proof Assistant Reference Manual v8.0[EB-OL].
Tennent R D. 1997. Foundations for Programming Languages by John C. Mitchell, MIT Press, 1996.[J]. J. Funct. Program., 7(6):667-668.
VITEK J, JAGANNATHAN S, Welc A, et al. 2004. A Semantic Framework for Designer Transactions[C] //Proceedings of the European Symposium on Programming. [S.l.]: Springer-Verlag. Lecture Notes in Computer Science, vol. 2986, Apr.
Xiang S, Chen Y, Lin C, et al. 2006. Modularly Certified Dynamic Storage Allocation in SCAP[C]//Proceedings of Sixth International Conference on Quality Software (QSIC'06). Beijing, China: IEEE Computer Society:321-328.
Xu Q, Cau A, Collette P. 1994. On Unifying Assumption-Commitment
Style Proof Rules for Concurrency[C]//CONCUR '94: Proceedings of the Concurrency Theory. London, UK: Springer-Verlag:267-282.
Yahav E. 2001. Verifying safety properties of concurrent Java programs using 3-valued logic[C]//POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:27-40.
Yu D, Shao Z. 2004. Verification of safety properties for concurrent assembly code[C]//ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:175-188.
Yu D, Hamid N A, Shao Z. 2004. Building certified libraries for PCC: dynamic storage allocation[J]. Sci. Comput. Program., 50(1-3):101-127.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |