Compiling concurrency correctly: verifying software transactional memory
Publication Date
June 15, 2013
Creator
Abstract
Concurrent programming is notoriously difficult, but with multi-core processors becoming the norm, is now a reality that every programmer must face. Concurrency has traditionally been managed using low-level mutual exclusion /locks/, which are error-prone and do not naturally support the compositional style of programming that is becoming indispensable for today's large-scale software projects.
A novel, high-level approach that has emerged in recent years is that of /software transactional memory/ (STM), which avoids the need for explicit locking, instead presenting the programmer with a declarative approach to concurrency. However, its implementation is much more complex and subtle, and ensuring its correctness places significant demands on the compiler writer.
This thesis considers the problem of formally verifying an implementation of STM. Utilising a minimal language incorporating only the features that we are interested in studying, we first explore various STM design choices, along with the issue of compiler correctness via the use of automated testing tools. Then we outline a new approach to concurrent compiler correctness using the notion of bisimulation, implemented using the Agda theorem prover. Finally, we show how bisimulation can be used to establish the correctness of a low-level implementation of software transactional memory.
Item Type
ethesis
Thesis Type
PhD
Supervisors
Subjects (LC)
Associated Schools / Departments
School of Computer Science (UK)
eprints ID
13348
UoN Repository URI
Except where otherwise noted, this item's license is described as
File(s)![Thumbnail Image]()
Name
hu-thesis.pdf
Type
Full-text
Description
Examined. Thesis
Size
944.8 KB
Format
Adobe PDF
Checksum ()