A Compositional Method for Verifying Software Transactional Memory
Episode details
Episode description
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 three intuitive properties. The implementation-level proof consists of checking whether these properties are satisfied by the STM implementation. We were able to express each check as an assertion in a particular *sequential* program that mimics interference between threads. This is a key benefit, as it allowed the assertion checks to be carried out using the sequential program verifier Boogie. We demonstrated our approach on a model of the Bartok STM. Noteworthy additional work since the August 2007 MSR talk on this project includes the following: (i) A formal, algorithm-level model and semantics for programs using transactions. This model handles nested transactions, conflicts and rollbacks. (ii) The definition of pure
Watch also from the same channel
More episodes from this channel
You might be interested in
