Transactional memory （TM） is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle data races between threads automatically so ...Transactional memory （TM） is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle 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. In this paper, we focus on the semantics of transactional memory and present a proof-carrying code （PCC） system for reasoning about programs using TM . We formalize our reasoning with respect to the TM semantics, prove its soundness, and use examples to demonstrate its effectiveness.展开更多
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 hard...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.展开更多
基金Supported by the National Natural Science Foundation of China under Grant Nos.60673126 and 90718026, and Intel China Research Center.
文摘Transactional memory （TM） is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle 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. In this paper, we focus on the semantics of transactional memory and present a proof-carrying code （PCC） system for reasoning about programs using TM . We formalize our reasoning with respect to the TM semantics, prove its soundness, and use examples to demonstrate its effectiveness.
基金Supported by the National Natural Science Foundation of China under Grant Nos.60928004 and 90718026
文摘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.
