Compiling concurrency correctly: verifying software transactional memory
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 composition...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2013
|
| Online Access: | https://eprints.nottingham.ac.uk/13348/ |
| _version_ | 1848791711972589568 |
|---|---|
| author | Hu, Liyang |
| author_facet | Hu, Liyang |
| author_sort | Hu, Liyang |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:32:52Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-13348 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T18:32:52Z |
| publishDate | 2013 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-133482025-02-28T19:37:01Z https://eprints.nottingham.ac.uk/13348/ Compiling concurrency correctly: verifying software transactional memory Hu, Liyang 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. 2013-06-15 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en cc_by_nc_sa https://eprints.nottingham.ac.uk/13348/1/hu-thesis.pdf Hu, Liyang (2013) Compiling concurrency correctly: verifying software transactional memory. PhD thesis, University of Nottingham. |
| spellingShingle | Hu, Liyang Compiling concurrency correctly: verifying software transactional memory |
| title | Compiling concurrency correctly: verifying software transactional memory |
| title_full | Compiling concurrency correctly: verifying software transactional memory |
| title_fullStr | Compiling concurrency correctly: verifying software transactional memory |
| title_full_unstemmed | Compiling concurrency correctly: verifying software transactional memory |
| title_short | Compiling concurrency correctly: verifying software transactional memory |
| title_sort | compiling concurrency correctly: verifying software transactional memory |
| url | https://eprints.nottingham.ac.uk/13348/ |