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.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.
