A Compositional Method for Verifying Software Transactional Memory

  • Serdar Tasiran | Koc University in Istanbul, Turkey

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:

  1. A formal, algorithm-level model and semantics for programs using transactions. This model handles nested transactions, conflicts and rollbacks.
  2. The definition of “pure serializability”, a correctness criterion for the kinds of programs described in (i).
  3. A lower-level semantics that is at the same level of granularity as the actual STM implementation. This semantics also describes STM implementation state transitions that are invisible to the programmer.
  4. A formalization of the desired relationship between implementation-level and algorithm-level executions. This includes translating sufficient conditions expressed at the algorithm-level to requirements at the implementation level.
  5. The identification of abstractions in modeling required to make the refinement proof and algorithm-level serializability proof go through.

Speaker Details

Serdar Tasiran received the B.S. degree in electrical engineering from Bilkent University, Ankara, Turkey in 1991 and the M.S. and Ph.D. degrees in electrical engineering and computer sciences from the University of California, Berkeley in 1995 and 1998. He was a research scientist with the Gigascale Systems Research Center (1998-2000), and the Systems Research Center (Compaq/HP Labs). Since 2003, he has been an assistant professor at Koc University, Istanbul, Turkey. He has had visiting appointments at Microsoft Research, EPFL, and MIT Research Laboratory for Electronics. Dr. Tasiran’s research focus is the application of formal and algorithmic methods to system verification and validation, particularly to concurrent software and hardware. His broader research interests include the synthesis, verification, performance analysis and optimization of hardware and software systems.

Watch Next