Loading...
Please wait, while we are loading the content...
Similar Documents
Chapter 9 Towards a Verified Implementation of Software Transactional
| Content Provider | CiteSeerX |
|---|---|
| Author | Hu, Liyang Hutton, Graham |
| Abstract | 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, using subtle optimisation techniques to execute multiple concurrent transactions efficiently, which is essential to the viability of the programming model. 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, 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 formalisation. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Stm Haskell Correctness Theorem Transactional Memory Multiple Concurrent Transaction Verified Implementation Subtle Optimisation Technique First Step High-level Semantics Software Transactional Simple High-level Model Idealised Concurrent Language Haskell Program Coverage Much Interest Programming Model Stop-the-world Semantics Low-level Implementation |
| Content Type | Text |
| Resource Type | Article |
