Formal Reasoning About Lazy-STM Programs

被引:1
作者
Li, Yong [1 ]
Zhang, Yu
Chen, Yi-Yun
Fu, Ming
机构
[1] Univ Sci & Technol China, Sch Comp Sci & Technol, Hefei 230027, Peoples R China
基金
中国国家自然科学基金;
关键词
program verification; transactional memory (TM); proof-carrying-code; permission accounting in separation logic;
D O I
10.1007/s11390-010-9369-2
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
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 are also one part of the shared memory. Then we define the semantics of the model operationally, and the lightweight locks in transaction are 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.
引用
收藏
页码:841 / 852
页数:12
相关论文
共 26 条
[1]   Unbounded transactional memory [J].
Ananian, CS ;
Asanovic, K ;
Kuszmaul, BC ;
Leiserson, CE ;
Lie, S .
11TH INTERNATIONAL SYMPOSIUM ON HIGH-PERFORMANCE COMPUTER ARCHITECTURE, PROCEEDINGS, 2005, :316-327
[2]  
BORNAT R, 2005, POPL, P259
[3]   A Grainless Semantics for Parallel Programs with Shared Mutable Data [J].
Brookes, Stephen .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 155 :277-307
[4]  
Dice D., 2006, Proceedings of the International Symposium on Distributed Computing (DISC), P194, DOI DOI 10.1007/11864219_14
[5]   Dynamic Performance Tuning of Word-Based Software Transactional Memory [J].
Felber, Pascal ;
Fetzer, Christof ;
Riegel, Torvald .
PPOPP'08: PROCEEDINGS OF THE 2008 ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF PARALLEL PROGRAMMING, 2008, :237-245
[6]  
Feng X, 2006, ACM SIGPLAN NOTICES, V41, P401, DOI 10.1145/1133981.1134028
[7]  
FENG XY, 2005, P 2005 ACM INT C FUN, P254
[8]  
Hammond L, 2004, CONF PROC INT SYMP C, P102
[9]  
HARRIS T, 2003, P 18 ANN ACM SIGPLAN, P388, DOI DOI 10.1145/949305.949340
[10]  
Herlihy M., 2003, Proceedings of the twenty-second annual symposium on Principles of distributed computing, P92