A compositional method for verifying software transactional memory implementations

We present a compositional method for verifying software transactional memory (STM) implementations and its application to the Bartok STM. The method consists of two parts. The first is a generic, manual proof of serializability at the algorithm level for lazy-invalidate, write-in-place STM’s. The proof relies on three properties of program executions that the STM must ensure. The second part consists of proving that the Bartok STM implementation guarantees these properties and thus refines the algorithm-level description. We present a novel technique for expressing the properties required of the STM implementation as assertions in sequential programs that model certain interference scenarios. This is a key benefit, as it allows these properties to be checked using sequential program verification tools. Using our method, the Spec# language and the Boogie verification tool, we were able to detect an omission in the published pseudo-code for the STM implementation and “challenge bugs” extracted from earlier versions of the STM. We were also able to prove correct the most recent version of the implementation.