正在加载图片...
120 J.Comput.Sci.Technol.,Jan.2009,Vol.24,No.1 plan to study the violations in implementations of TM [14 Moore K F,Grossman D.High-level small-step operational systems in more depth and define a more flexible pro semantics for transactions.In Proc.the 95th ACM Sym- gramming model for supporting transactional memory. posium on Principles of Programming Languages,San Fran- cisco,USA,Jan.2008,pp.51-62. [15 Abadi M,Birrell A,Harris T,Isard M.Semantics of transac- tional memory and automatic mutual exclusion.In Proc.the References 35th ACM Symposium on Principles of Programming Lan- guages,San Francisco,USA,Jan.2008,pp.63-74. [1]C Scott Ananian,Krste Asanovic,Bradley C Kuszmaul, [16]Necula G C.Proof-carrying code.In Proc.the 24th ACM Charles E Leiserson,Sean Lie.Unbounded transactional SIGPLAN-SIGACT Symposium on Principles of Program- memory.In Proc.the Eleventh International Symposium ming Languages (POPL '97),Paris,France,ACM Press, on High-Performance Computer Architecture,San Francisco. 1997,pp.106-119. USA,Fb.2005,pp.316-327. [17]Appel A W.Foundational proof-carrying code.In Proc.the [2]Hammond L,Wong V,Chen M,Carlstrom B D,Davis J D, 16th Annual IEEE Symposium on Logic in Computer Science Hertzberg B,Prabhu M K,Wijaya H,Kozyrakis C,Olukotun (LICS'01),Boston,USA,IEEE Computer Society,Jun.2001, K.Transactional memory coherence and consistency.In Proc pp.247-258. the 31st Annual International Symposium on Computer Ar [18 Yu D,Hamid N A,Shao Z.Building certified libraries for chitecture,Miinchen,Germany,IEEE Computer Society,Jun. PCC:Dynamic storage allocation.Science of Computer Pro- 2004,p.102. gramming,2004,50(1-3):101-127. [3]Herlihy M,Moss J E B.Transactional memory:Architec- [19]Feng X,Shao Z,Vaynberg A,Xiang S,Ni Z.Modular ver- tural support for lock-free data structures.In Proc.the 20th ification of assembly code with stack-based control abstrac- Annual International Symposium on Computer Architecture, tions.In Proc.2006 ACM SIGPLAN Conference on Pro- San Diego,USA,May 1993,pp.289-300. gramming Language Design and Implementation(PLDI'06). Ottawa,Canada,Jun.2006,pp.401-414. [4)Moore K E,Bobba J,Moravan M J,Hill M D,Wood D A.LogTM:Log-based transactional memory.In Proc.the [20 Ni Z,Shao Z.Certified assembly programming with embed- 12th International Symposium on High-Performance Com- ded code pointers.In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Program- puter Architecture,Austin,USA,Feb.2006,pp.254-265. ming Languages (POPL'06),Charleston,South Carolina, 5]Harris T,Fraser K.Language support for lightweight trans USA,ACM Press,2006,pp.320-333. actions.In Proc.the 18th Annual ACM SIGPLAN Conf. Object-Oriented Programming,Systems,Languages,and Ap- [21]Yu D,Shao Z.Verification of safety properties for concur- rent assembly code.In Proc.the 9th ACM SIGPLAN Inter- plications,Anaheim,USA,Oct.2003,pp.388-402. [6]Harris T,Herlihy M,Marlow S,Peyton-Jones S.Composable national Conference on Functional Programming (ICFP'04). Snowbird,Utah,Sept.2004,pp.175-188. memory transactions.In Proc.the 10th ACM SIGPLAN Symposium on Principles and Practice of Parallel Program- [22]Feng X,Shao Z.Modular verification of concurrent assem bly code with dynamic thread creation and termination.In ming,Chicago,USA,Jun.2005,pp.48-60. Proc.the 10th ACM SIGPLAN International Conference on [7]Herlihy M,Luchangco V,Moir M,Scherer III W N.Soft- Functional Programming (ICFP'05),Tallinn,Estonia,ACM ware transactional memory for dynamic-sized data structures. Press,Sept.2005,pp.254-267. In Proc.the Twenty-Second Annual Symposium on Prin. [23]The Cog proof assistant reference manual.The Cog release ciples of Distributed Computing (PODC '03).Boston.Mas- v8.0,Cog Development Team,Oct.2005. sachusetts,USA,ACM Press,2003,pp.92-101. [24]Colin Blundell,E Christopher Lewis,Milo M K Martin.Sub- 8]Shavit N,Touitou D.Software transactional memory.In Proc. tleties of transactional memory atomicity semantics.Com the 14th ACM Symposium on Principles of Distributed Com- puter Architecture Letters,Nov.2006,5(2):17. puting,Ottawa,Canada,Aug.1995,pp.204-213. [25 Spear M F,Marathe V J,Dalessandro L.Scott M L.Pri- 9]Kumar S,Chu M,Hughes C J,Kundu P,Nguyen A.Hybrid vatization techniques for software transactional memory.In transactional memory.In Proc.the 11th ACM SIGPLAN Proc.the 26th ACM Symposium on Principles of Distributed Symposium on Principles and Practice of Parallel Program- Computing(PODC),Portland,USA,Aug.2007,pp.338-339. ming,New York,USA,Mar.2006,pp.209-220. [26]Tatiana Shpeisman,Vijay Menon,Ali-Reza Adl-Tabatabai. 10]Bratin Saha,Ali-Reza Adl-Tabatabai,Richard L Hudson,Chi Steven Balensiefer,Dan Grossman,Richard L Hudson. Cao Minh,Benjamin Hertzberg.McRT-STM:A high perfor- Katherine F Moore,Bratin Saha.Enforcing isolation and mance software transactional memory system for a multi-core ordering in STM.In Proc.the 2007 ACM SIGPLAN Confer- runtime.In Proc.the 11th ACM SIGPLAN Symp.Prin- ence on Programming Language Design and Implementation ciples and Practice of Parallel Programming (PPoPP '06), (PLDI'07),San Diego,California,USA,ACM Press,2007, New York,USA,Mar.2006,pp.187-197. Pp.78-88. [11]Vitek J,Jagannathan S,Welc A,Hosking A L.A semantic [27 Reynolds J C.Separation logic:A logic for shared mutable framework for designer transactions.In Proc.the 13th Euro- data structures.In Proc.the 17th Annual IEEE Symposium pean Symposium on Programming,Barcelona,Spain,Lecture on Logic in Computer Science (LICS'02),Copenhagen,Den- Notes in Computer Science 2986,Springer-Verlag,Apr.2004, mark,IEEE Computer Society,2002,pp.55-74. pp.249-263. 28]Li L,Zhang Y,Chen YY,Li Y.Certifying concurrent pro- [12]Ben Liblit.An operational semantics for LogTM.Version grams using transactional memory (documents and Cog im- 1.0,Technical Report 1571,University of Wisconsin-Madison, plementation).Aug.2007,http://ssg.ustcsz.edu.cn/ccac/. Aug.2006. [29]Floyd R W.Assigning meanings to programs.In Proc.the [13]Moore K F,Grossman D.High-level small-step operational se- Symposium on Applied Math.,American Mathematical Soci- mantics for transactions.In Proc.the 2nd ACM SIGPLAN ety (ed.),Providence,R.I.,1967,Vol.19,pp.19-31. Workshop on Transactional Computing,Portland,USA,Aug. [30 Hoare C A R.An axiomatic basis for computer programming. 2007. Communications of the ACM,Oct.1969,12(10):576-580.120 J. Comput. Sci. & Technol., Jan. 2009, Vol.24, No.1 plan to study the violations in implementations of TM systems in more depth and define a more flexible programming model for supporting transactional memory. References [1] C Scott Ananian, Krste Asanovic, Bradley C Kuszmaul, Charles E Leiserson, Sean Lie. Unbounded transactional memory. In Proc. the Eleventh International Symposium on High-Performance Computer Architecture, San Francisco, USA, Feb. 2005, pp.316–327. [2] Hammond L, Wong V, Chen M, Carlstrom B D, Davis J D, Hertzberg B, Prabhu M K, Wijaya H, Kozyrakis C, Olukotun K. Transactional memory coherence and consistency. In Proc. the 31st Annual International Symposium on Computer Architecture, M¨unchen, Germany, IEEE Computer Society, Jun. 2004, p.102. [3] Herlihy M, Moss J E B. Transactional memory: Architectural support for lock-free data structures. In Proc. the 20th Annual International Symposium on Computer Architecture, San Diego, USA, May 1993, pp.289–300. [4] Moore K E, Bobba J, Moravan M J, Hill M D, Wood D A. LogTM: Log-based transactional memory. In Proc. the 12th International Symposium on High-Performance Computer Architecture, Austin, USA, Feb. 2006, pp.254–265. [5] Harris T, Fraser K. Language support for lightweight transactions. In Proc. the 18th Annual ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications, Anaheim, USA, Oct. 2003, pp.388–402. [6] Harris T, Herlihy M, Marlow S, Peyton-Jones S. Composable memory transactions. In Proc. the 10th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Chicago, USA, Jun. 2005, pp.48–60. [7] Herlihy M, Luchangco V, Moir M, Scherer III W N. Software transactional memory for dynamic-sized data structures. In Proc. the Twenty-Second Annual Symposium on Principles of Distributed Computing (PODC ’03), Boston, Massachusetts, USA, ACM Press, 2003, pp.92–101. [8] Shavit N, Touitou D. Software transactional memory. In Proc. the 14th ACM Symposium on Principles of Distributed Computing, Ottawa, Canada, Aug. 1995, pp.204–213. [9] Kumar S, Chu M, Hughes C J, Kundu P, Nguyen A. Hybrid transactional memory. In Proc. the 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, New York, USA, Mar. 2006, pp.209–220. [10] Bratin Saha, Ali-Reza Adl-Tabatabai, Richard L Hudson, Chi Cao Minh, Benjamin Hertzberg. McRT-STM: A high performance software transactional memory system for a multi-core runtime. In Proc. the 11th ACM SIGPLAN Symp. Principles and Practice of Parallel Programming (PPoPP ’06), New York, USA, Mar. 2006, pp.187–197. [11] Vitek J, Jagannathan S, Welc A, Hosking A L. A semantic framework for designer transactions. In Proc. the 13th European Symposium on Programming, Barcelona, Spain, Lecture Notes in Computer Science 2986, Springer-Verlag, Apr. 2004, pp.249–263. [12] Ben Liblit. An operational semantics for LogTM. Version 1.0, Technical Report 1571, University of Wisconsin–Madison, Aug. 2006. [13] Moore K F, Grossman D. High-level small-step operational semantics for transactions. In Proc. the 2nd ACM SIGPLAN Workshop on Transactional Computing, Portland, USA, Aug. 2007. [14] Moore K F, Grossman D. High-level small-step operational semantics for transactions. In Proc. the 35th ACM Symposium on Principles of Programming Languages, San Francisco, USA, Jan. 2008, pp.51–62. [15] Abadi M, Birrell A, Harris T, Isard M. Semantics of transactional memory and automatic mutual exclusion. In Proc. the 35th ACM Symposium on Principles of Programming Languages, San Francisco, USA, Jan. 2008, pp.63–74. [16] Necula G C. Proof-carrying code. In Proc. the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’97), Paris, France, ACM Press, 1997, pp.106–119. [17] Appel A W. Foundational proof-carrying code. In Proc. the 16th Annual IEEE Symposium on Logic in Computer Science (LICS’01), Boston, USA, IEEE Computer Society, Jun. 2001, pp.247–258. [18] Yu D, Hamid N A, Shao Z. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 2004, 50 (1-3): 101–127. [19] Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’06), Ottawa, Canada, Jun. 2006, pp.401–414. [20] Ni Z, Shao Z. Certified assembly programming with embedded code pointers. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06), Charleston, South Carolina, USA, ACM Press, 2006, pp.320–333. [21] Yu D, Shao Z. Verification of safety properties for concurrent assembly code. In Proc. the 9th ACM SIGPLAN International Conference on Functional Programming (ICFP’04), Snowbird, Utah, Sept. 2004, pp.175–188. [22] Feng X, Shao Z. Modular verification of concurrent assembly code with dynamic thread creation and termination. In Proc. the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP’05), Tallinn, Estonia, ACM Press, Sept. 2005, pp.254–267. [23] The Coq proof assistant reference manual. The Coq release v8.0, Coq Development Team, Oct. 2005. [24] Colin Blundell, E Christopher Lewis, Milo M K Martin. Subtleties of transactional memory atomicity semantics. Computer Architecture Letters, Nov. 2006, 5(2): 17. [25] Spear M F, Marathe V J, Dalessandro L, Scott M L. Privatization techniques for software transactional memory. In Proc. the 26th ACM Symposium on Principles of Distributed Computing (PODC), Portland, USA, Aug. 2007, pp.338–339. [26] Tatiana Shpeisman, Vijay Menon, Ali-Reza Adl-Tabatabai, Steven Balensiefer, Dan Grossman, Richard L Hudson, Katherine F Moore, Bratin Saha. Enforcing isolation and ordering in STM. In Proc. the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’07), San Diego, California, USA, ACM Press, 2007, pp.78–88. [27] Reynolds J C. Separation logic: A logic for shared mutable data structures. In Proc. the 17th Annual IEEE Symposium on Logic in Computer Science (LICS’02), Copenhagen, Denmark, IEEE Computer Society, 2002, pp.55–74. [28] Li L, Zhang Y, Chen Y Y, Li Y. Certifying concurrent programs using transactional memory (documents and Coq implementation). Aug. 2007, http://ssg.ustcsz.edu.cn/ccac/. [29] Floyd R W. Assigning meanings to programs. In Proc. the Symposium on Applied Math., American Mathematical Society (ed.), Providence, R.I., 1967, Vol.19, pp.19–31. [30] Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, Oct. 1969, 12(10): 576–580