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 serializability", a correctness criterion for the kinds of programs described in (i).
(iii) 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.
(iv) 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.
(v) The identification of abstractions in modeling required to make the refinement proof and algorithm-level serializability proof go through.
Speaker(s):
Serdar Tasiran, teaching at the Koc University in Istanbul, Turkey
|
