期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

Formal Reasoning About Lazy-STM Programs 被引量：1

Formal Reasoning About Lazy-STM Programs
原文传递
导出
摘要 Transactional memory （TM） is an easy-using parallel programming model that avoids common problems associated with conventional locking techniques. Several researchers have proposed a large amount of alternative hardware and software TM implementations. However, few ones focus on formal reasoning about these TM programs. In this paper, we propose a framework at assembly level for reasoning about lazy software transactional memory （STM） programs. First, we give a software TM implementation based on lightweight locks. These locks axe also one part of the shared memory. Then we define the semantics of the model operationally, and the lightweight locks in transaction axe non-blocking, avoiding deadlocks among transactions. Finally we design a logic -- a combination of permission accounting in separation logic and concurrent separation logic -- to verify various properties of concurrent programs based on this machine model. The whole framework is formalized using a proof-carrying-code （PCC） framework. Transactional memory （TM） is an easy-using parallel programming model that avoids common problems associated with conventional locking techniques. Several researchers have proposed a large amount of alternative hardware and software TM implementations. However, few ones focus on formal reasoning about these TM programs. In this paper, we propose a framework at assembly level for reasoning about lazy software transactional memory （STM） programs. First, we give a software TM implementation based on lightweight locks. These locks axe also one part of the shared memory. Then we define the semantics of the model operationally, and the lightweight locks in transaction axe non-blocking, avoiding deadlocks among transactions. Finally we design a logic -- a combination of permission accounting in separation logic and concurrent separation logic -- to verify various properties of concurrent programs based on this machine model. The whole framework is formalized using a proof-carrying-code （PCC） framework.
作者 李勇 张昱 陈意云 付明
机构地区 School of Computer Science and Technology Software Security Laboratory
出处 《Journal of Computer Science & Technology》 SCIE EI CSCD 2010年第4期841-852,共12页 计算机科学技术学报（英文版）
基金 Supported by the National Natural Science Foundation of China under Grant Nos.60928004 and 90718026
关键词 program verification transactional memory （TM） proof-carrying-code permission accounting in separation logic program verification, transactional memory （TM）, proof-carrying-code, permission accounting in separation logic
分类号 TP181 [自动化与计算机技术—控制理论与控制工程]
  • 相关文献

参考文献27

  • 1Herlihy M, Moss J E B. Transactional memory: Architectural support for lock-free data structures. In Proc. the 20th Annual International Symposium on Computer Architecture (ISCA 1993), San Diego, US, May 1993, pp.289-300.
  • 2Hammond L, Wong V, Chen Met al. Transactional memory coherence and consistency. In Proc. the 31st Annual International Symposium on Computer Architecture ( ISCA 2004), Miinchen, Germany, Jun. 19-23, 2004, p.102.
  • 3Ananian C S, Asanovic K, Kuszmaul B C et al. Unbounded transactional memory. In Proc. the llth International Symposium on High-Performance Computer Architecture (HPCA 2005), San Francisco, US, Feb. 12-16, 2005, pp.316-327.
  • 4Moore K E, Grossman D. Log-based transactional memory. In Proc. The Twelfth International Symposium on High-Performance Computer Architecture, Austin, USA, Feb. 11-15, 2006, pp.254-265.
  • 5Shavit N, Touitou D. Software transactional memory. In Proc. the 14th Annual ACM Symposium on Principles of Distributed Computing ( PODC 1995), Ottawa, Canada, Aug. 20- 23, 1995, pp.204-213.
  • 6Harris T, Fraser K. Language support for lightweight transactions. In Proc. the 18th Annual ACM SIGPLAN Confersnce on Object-Oriented P'rograming, Systems, Languages, and Applications (OOPSLA 2003), Anaheim, USA, Oct. 26- 30, 2003, pp.388-402.
  • 7Saha B, Adl-Tabatabai A R, Hudson R L, Minh C C, Hertzberg B. McRT-STM: A high performance software trans- actional memory system for a multi-core runtime. In Proc. the Eleventh ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2006), New York, USA, Mar. 29-31, 2006, pp.187-197.
  • 8Herlihy M, Luchangco V, Moir M, Scherer W N III. Soft- ware transactional memory for dynamic-sized data structures. In Proc. the 22nd Annual Symposium on Principles of Dis- tributed Computing (PODC2003), Boston, USA, July 13-16, 2003, pp.92-101.
  • 9Dice D, Shalev O, Shavit N. Transactional locking II. In Proc. International Symposium on Distributed Computing, Stockholm, Sweden, Sept. 18-20, 2006, pp.194-208.
  • 10Felber P, Fetzer C, Riegel T. Dynamic performance tuning of word-based software transactional memory. III Proc. the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming ( PPoPP 2008), Salt Lake City, USA, Feb. 20-23, 2008, pp.237-246.

同被引文献12

  • 1杨军,葛海通,郑飞君,严晓浪.一种形式化验证方法:模型检验[J].浙江大学学报（理学版）,2006,33(4):403-407. 被引量：17
  • 2Hoare C A R.An Axiomatic Basis for Computer Programming[J].Communications of the ACM,1969,12 (10):576- 580.
  • 3Reynolds J C.Separation Logic: A Logic for Shared Mutable Data Structures [C]//Proc. of the LICS 2002.Copenhagen,2002:55-74.
  • 4Ashcroft E A.Proving Assertions about Parallel Programs [J].J.Comput.Syst.Sci,1975,10(1): 110-135.
  • 5Necula G C.Proof-Carrying Code [C]//Paris:The 24th ACM Symp on Principles of Programing Language,1997.
  • 6Appel A W.Foundational Proof-Carrying Code [C]//The 16th Annual IEEE Symp on Logic" in Computer Science, Boston,2001.
  • 7朱允敏,张丽伟,王生原等.面向多核处理器的低级并行程序验证[C]//全国软件与应用学术会议论文集,2008:282-287.
  • 8Rachid G,Michal K.Principles of Transactional Memory [M].Morgan & Claypool Publishers,2010.
  • 9Herlihy M,Moss J E.Transactional Memory: Architectural Support for Lock-free Data Structures[C]//Proceedings of the Twentieth International Symposium on Computer Architecture, 1993:289-300.
  • 10李隆,张昱,陈意云,李勇.Certifying Concurrent Programs Using Transactional Memory[J].Journal of Computer Science & Technology,2009,24(1):110-121. 被引量：1

引证文献1

Journal of Computer Science & Technology
2010年 第4期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部