A Compositional Method for Verifying Software Transactional Memory

We present a method for verifying software transactional memory (STM) implementations. We decompose the problem by viewing STM descriptions at two levels: algorithm-level descriptions and actual implementations. The proof of serializability of the algorithm-level description, which is generic and performed manually, is separated from the proof that the implementation is a correct refinement of the algorithm-level description, which is checked mechanically. In the algorithm-level proof for a lazy-invalidate, write-in-place STM, we model a program composed with an abstract STM, and devise a sufficient condition for serializability expressed as ...