Liyang on the intartubes

Towards a Verified Implementation of Software Transactional Memory

Liyang HU and Graham Hutton. Proceedings of the Symposium on Trends in Functional Programming, Nijmegen, The Nether­lands, May 2008.

In recent years there has been much interest in the idea of concurrent programming using transactional memory, for ex­am­ple 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 im­p­le­men­ta­tion is rather more complex, using subtle optimisation tech­ni­ques to execute multiple concurrent transactions effi­cient­ly, which is essential to the viability of the pro­gram­ming model.

In this article, we take the first steps towards a formally ve­ri­fied implementation of transactional memory. In par­ti­cu­lar, we present a stripped-down, idealised concurrent lan­gua­ge inspired by STM Haskell, and show how a low-level im­p­le­men­ta­tion of this language can be justified with respect to a high-level semantics, by means of a compiler and its cor­rect­ness theorem, mechanically tested using QuickCheck and the HPC (Haskell Program Coverage) toolkit. The use of these tools proved to be invaluable in the development of our for­ma­li­sa­tion.

[Paper] [BibTeX]