Maintaining memory order dependencies through LLVM optimisation passes.
Lead Research Organisation:
University of Kent
Department Name: Sch of Computing
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
People |
ORCID iD |
| Mark Batty (Primary Supervisor) | |
| Simon Cooksey (Student) |
Publications
Cooksey S J
(2019)
PrideMM: Second Order Model Checking for Memory Consistency Models
Paviotti M
(2020)
Modular Relaxed Dependencies in Weak Memory Concurrency
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/R513246/1 | 30/09/2018 | 29/09/2023 | |||
| 1773013 | Studentship | EP/R513246/1 | 30/09/2016 | 30/03/2020 | Simon Cooksey |
| Description | The mathematical complexity of simulating how multi-threaded programs work is higher than we expected. To better understand these programs, complex mathematical models have been derived. These models are often impenetrable, even by experts. It was identified early on in this project that to succeed in critiquing and further develop these models that they must be executable and scrutable. Building fast software to evaluate many small programs under each model gives intuitions about the mechanisms that each artefact provides, as well as giving a coarse grained (but useful) set of points for comparison. |
| Exploitation Route | Further development of complex models can be achieved using our findings. |
| Sectors | Aerospace Defence and Marine Digital/Communication/Information Technologies (including Software) Electronics Energy |
| Description | I have been involved with developing industry specifications for memory consistency models which will be published as general technical documentation for all programmers. |
| First Year Of Impact | 2018 |
| Sector | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Electronics,Energy |
| Impact Types | Societal |
| Description | Attendance at ISO C/C++ Meetings (SG1). |
| Geographic Reach | Multiple continents/international |
| Policy Influence Type | Membership of a guideline committee |
| Description | Fixing the thin-air problem: ISO disemination |
| Amount | £60,458 (GBP) |
| Organisation | The Research Institute on Verified Trustworthy Software Systems |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 03/2020 |
| End | 03/2021 |
| Description | PrideMM web interface |
| Amount | £41,000 (GBP) |
| Organisation | The Research Institute on Verified Trustworthy Software Systems |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 07/2018 |
| End | 03/2019 |
| Description | Programming Lanugages Mentoring Workshop grant |
| Amount | £750 (GBP) |
| Organisation | Association for Computing Machinery |
| Sector | Charity/Non Profit |
| Country | United States |
| Start | 01/2017 |
| End | 01/2017 |
| Description | Industrial Research Internship |
| Organisation | NVIDIA |
| Country | Global |
| Sector | Private |
| PI Contribution | Provided mathematical modelling of industrial hardware specifications. |
| Collaborator Contribution | Industrial internship to work on research related to my thesis. |
| Impact | Submitted a paper to leading academic conference. |
| Start Year | 2018 |
| Title | MRDer |
| Description | Evaluator for first denotational semantics of C/C++ which forbids thin-air executions. |
| Type Of Technology | Software |
| Year Produced | 2019 |
| Impact | Part of work published at ESOP 2020. |
| Title | PrideMM |
| Description | Evaluates small programs, called litmus tests, under a cutting edge mathematical model of concurrency. |
| Type Of Technology | Software |
| Year Produced | 2018 |
| Impact | Contributed to a paper seen at TACAS 2019. Cited by James Riely and Alan Jeffery in 2019 Journal version of Event Structures Work. Drove further development of more simple Thin-Air free memory models. |
| Description | Speaking at ISO/WG21/SG1 standards meeting |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | Described cutting edge research into memory consistency models, and agreed strategy for developing this model further. WG21 agreed that our work shows promise as a future direction for the international standard of C++ concurrency and would like to see more. |
| Year(s) Of Engagement Activity | 2019,2020 |
| URL | https://github.com/cplusplus/papers/issues/554 |