Formal reasoning about lazy-STM programs
Authors
Yong Li
Yu Zhang
Yiyun Chen
Ming Fu
Abstract
Transactional memory(TM) is an easy-using parallel programming model that avoids common problems associated with conventional locking techniques. Several researchers have proposed alternative hardware and software TM implementations. However, few ones focus on formal reasoning about programs using TM system. In this paper, we propose a framework at assembly level for reasoning about concurrent programs using a lazy-STM system.
First, we give a software TM implementation based on storable locks. Then we define the semantics of the model operationally, and the synchronization constructs in transaction are light-weight and non-blocking, and it will not lead to deadlocks in transaction. Finally we devise 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.
Published
- Paper Draft
- Coq implementation