| Implementing Software Transactional Memory, Correctly (2008) | |||||||||||||||
Abstract | |||||||||||||||
| In recent years there has been much interest in the idea of concurrent programming using transactional memory, for example as provided in STM Haskell. While programmers are provided with a simple high-level model of transactions in terms of a stop-the-world semantics, the low-level implementation is rather more complex, involving subtle techniques that allow multiple transactions to execute concurrently. In this article, we take the first steps towards a formally verified implementation of transactional memory. In particular, we present a stripped-down, idealised concurrent language inspired by STM Haskell, and show how a low-level implementation of this language can be justified with respect to a high-level semantics, by means of a compiler and its correctness theorem, validated using QuickCheck and HPC. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||