Verifiably Correct Transactional Memory
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.
Publications
Jeffrey A
(2022)
The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
in Proceedings of the ACM on Programming Languages
Ranjan A
(2023)
Molecule generation toward target protein (SARS-CoV-2) using reinforcement learning-based graph neural network via knowledge graph.
in Network modeling and analysis in health informatics and bioinformatics
Wright D
(2023)
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies
in Formal Aspects of Computing
| Description | We found a solution to the longstanding 'thin-air' problem in C and C++, and we worked to establish this as the best solution to the problem. In this grant we focussed particularly on how to update reasoning principles to work with this very different paradigm of program behaviour. We made a standard way of proving code correct work with our new semantics. |
| Exploitation Route | Our solution to the thin-air problem is of relevance to anyone wishing to verify systems software, or who would like to write compiler optimisations. Our reasoning principle can underpin automated program analysis tools. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | The work developed on this grant has informed our discussions with the international standards organisation surrounding the long-standing thin-air problem. Conversations started with the ISO in 2010 and we have changed the C and C++ standards to fix small problems in several revisions of the standards since then. Covid has slowed down this process. |
| First Year Of Impact | 2010 |
| Sector | Digital/Communication/Information Technologies (including Software) |
| Description | International Standards Organisation (ISO) |
| Organisation | International Standards Organization |
| Country | Switzerland |
| Sector | Charity/Non Profit |
| PI Contribution | The work of this grant forms part of a continued partnership with the ISO seeking to help them refine the definition of concurrency in the C and C++ languages. The partnership started in 2009, and early contributions (before the start of this grant) suggested changes to the international standards of these two languages. These changes were accepted and became part of the official definitions of the languages. This process led to Batty becoming a voting member of the ISO's Workgroup 21 (WG21), responsible for the definition of the C++ language. This earlier work also brought to light a major problem in the definition of the language: the current specification fails to take into account the interaction of concurrency and dependency-removing compiler optimisations. Batty took these concerns to the ISO and helped them to understand that this problem could not be solved with a minor fix, and it was the underlying paradigm of of the concurrency definition that was at fault. WG21 formed Subgroup 1 (SG1) to discuss this and other issues related to the C++ concurrency definition. This grant funded the development of a new model of C++ concurrency called Modular Relaxed Dependencies (MRD). MRD solves the fundamental problems that we found in C++ by defining when a compiler can remove a dependency between two memory accesses, and when it cannot. It tightens the language definition to exclude behaviours that we showed make formal reasoning, like establishing security properties, impossible. MRD does have a significantly different underlying paradigm to the existing C++ memory definition, but we constructed it in such a way that it can be incorporated into the current definition with a surprisingly small list of changes. We presented MRD to SG1 at ISO meetings in Cologne (2019) and Belfast (2019), producing two white papers D1780R0 and D1780R1. These papers presented the workings of MRD and a concrete textual change to the C++ standard that implements MRD in the existing document. The change was complex yet concise and consisted of adding 2 new pages to the 1,622-page document. The committee found this to be palatable and were pleased to have a possible fix to a 10-year problem. SG1 voted unanimously to pursue the solution, recognising it as "the best path forward". Unfortunately, the pandemic caused an end to ISO meetings for some time in the next year. In response, we developed MRDer, an online tool that automatically evaluates MRD over small test programs. In our previous experience, our web tools have allowed ISO members to experiment with our models, and gain intuitions about the design decisions they embody. When meetings restarted online, we presented MRDer to SG1, and it was well received. We would like to push further for the incorporation of MRD into the C++ specification, but the online ISO meetings are sub optimal for this: the ones we have been to have had poor attendance, they were centred on discussing smaller issues, and the dynamics of the interactions seemed prone to confusion. We will return to this in 2021: momentum seems to be building to discuss more involved issues in the online meetings, and there is a chance of in-person meetings on the horizon. |
| Collaborator Contribution | The ISO act as gatekeepers for changes to the official definitions of the C and C++ languages. The ISO's SG1 is particularly influential in concurrency definitions, with many other languages adopting a minor extension of the C++ concurrency definition. SG1 is made up of global experts in concurrency who can provide us with feedback on our definitions. We received valuable and notably positive feedback 3 times from the committee at meetings at Belfast, Cologne and at an online meeting. The committee held a vote and unanimously recognised our technical solution to problems in the C++ specification as something they will pursue, and as the "the best path forward". |
| Impact | Two white papers at the ISO (despite being labelled as revisions, they have almost entirely different contents): D1780R0 -- Modular Relaxed Dependencies: A new approach to the Out-Of-Thin-Air Problem, 2019, Mark Batty, Simon Cooksey, Scott Owens, Anouk Paradis, Marco Paviotti, Daniel Wright D1780R1 -- Modular Relaxed Dependencies: A new approach to the Out-Of-Thin-Air Problem, 2019, Mark Batty, Simon Cooksey, Scott Owens, Anouk Paradis, Marco Paviotti, Daniel Wright The vote on the proposals made: Giroux, O (SG1 chair), 2019. ISO WG21 SG1 concurrency subgroup vote, unanimously approved: OOTA is a major problem for C++, modular relaxed dependencies is the best path forward we have seen, and we wish to continue to pursue this direction. |
| Start Year | 2018 |
| Title | Isabelle/HOL files for "Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies" |
| Description | Isabelle/HOL files for the paper "Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies". Tested for Isabelle 2022. |
| Type Of Technology | Software |
| Year Produced | 2022 |
| Open Source License? | Yes |
| URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Mechanised_Operational_Reasoning_for_C... |
| Description | Isabelle/HOL files for "Unifying Operational Weak Memory Verification: An Axiomatic Approach" to appear in ACM Transactions on Computational Logic. The proofs require Isabelle/HOL 2020. |
| Type Of Technology | Software |
| Year Produced | 2022 |
| Open Source License? | Yes |
| URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Unifying_Operational_Weak_Memory_Verif... |