Verifiably Correct Transactional Memory
Lead Research Organisation:
University of Surrey
Department Name: Computing Science
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.
Organisations
Publications
Ahmadi S
(2022)
Proving Memory Access Violations in Isabelle/HOL
Bila E
(2020)
Modularising Verification Of Durable Opacity
Bila E
(2022)
Modularising Verification Of Durable Opacity
in Logical Methods in Computer Science
Dalvandi M
(2019)
Towards deductive verification of C11 programs with Event-B and ProB
| Description | We have developed a series of new logics to reason about concurrent programs over advanced memory models. This, includes a programming language (C/C++) and a non-volatile memory (persistent x86) developed by Intel. We have used these logics to verify complex concurrent programs. This work will ultimately enable development of more trustworthy programs. We have tackled both concurrent objects (e.g., as implemented in Facebook's Folly library) and transactional memory libraries. |
| Exploitation Route | Our logic can be used as a basis to prove other (more complex) concurrent programs. Our modular technique allows program composition and library development. We have tackled both concurrent objects (e.g., as implemented in Facebook's Folly library) and transactional memory libraries. |
| Sectors | Digital/Communication/Information Technologies (including Software) Education |
| Description | Arm hardware now includes a transactional memory extension. https://developer.arm.com/documentation/102873/0100 Although their developments occurred independently from our work, the PIs were involved in discussions with Arm engineers during the development process. |
| First Year Of Impact | 2022 |
| Sector | Digital/Communication/Information Technologies (including Software) |
| Impact Types | Economic |
| Description | Amazon Gift |
| Amount | £100,000 (GBP) |
| Organisation | Amazon.com |
| Sector | Private |
| Country | United States |
| Start | 09/2020 |
| Description | Design and verification of correct, efficient and secure concurrent systems |
| Amount | $460,000 (AUD) |
| Funding ID | DP190102142 |
| Organisation | Australian Research Council |
| Sector | Public |
| Country | Australia |
| Start | 01/2019 |
| End | 12/2021 |
| Description | FACT: Faithful Composition of Trust |
| Amount | £204,000 (GBP) |
| Organisation | National Cyber Security Centre |
| Sector | Public |
| Country | United Kingdom |
| Start | 09/2019 |
| End | 03/2021 |
| Description | Persistent Safety and Security |
| Amount | £78,000 (GBP) |
| Organisation | The Research Institute on Verified Trustworthy Software Systems |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 09/2019 |
| End | 03/2023 |
| Description | SACRED-MA: Safe And seCure REmote Direct Memory Access |
| Amount | £466,480 (GBP) |
| Funding ID | EP/X037142/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 08/2023 |
| End | 08/2026 |
| Description | Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT) |
| Amount | £416,971 (GBP) |
| Funding ID | EP/X015149/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 08/2023 |
| End | 02/2027 |
| Description | Transactional Memory Security |
| Amount | £31,063 (GBP) |
| Organisation | National Cyber Security Centre |
| Sector | Public |
| Country | United Kingdom |
| Start | 01/2021 |
| End | 03/2021 |
| Title | Implementing and Verifying Release-Acquire Transactional Memory (Artifact) |
| Description | Supplementary files for the paper "Implementing and Verifying Release-Acquire Transactional Memory". The upload includes: Isabelle/HOL files for all proofs. The proofs have been developed/tested on Isabelle/HOL 2021-1. C++ implementations of TML-SC and TML-RA |
| Type Of Technology | Software |
| Year Produced | 2022 |
| Impact | None to report |
| URL | https://zenodo.org/record/6899918 |
| 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 |
| Impact | None to report. The artifact is a mechanised proof. |
| URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Mechanised_Operational_Reasoning_for_C... |
| Title | Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" |
| Description | Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" accepted to SAC 2023. The theories have been tested on Isabelle 2022. |
| Type Of Technology | Software |
| Year Produced | 2022 |
| Open Source License? | Yes |
| URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Ownership-Based_Owicki-Gries_Reasoning... |
| Description | FDR models for the SEFM 2021 paper "Checking Opacity and Durable Opacity with FDR" |
| Type Of Technology | Software |
| Year Produced | 2021 |
| Impact | None to report. The artifact is a mechanised proof. |
| URL | https://figshare.com/articles/software/FDR_models_for_Checking_Opacity_and_Durable_Opacity_with_FDR_... |
| Description | Isabelle files for "Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL".The proofs require Isabelle/HOL 2020. |
| Type Of Technology | Software |
| Year Produced | 2021 |
| Impact | None to report. The artifact is a mechanised proof. |
| URL | https://figshare.com/articles/software/Isabelle_Files_for_Integrating_Owicki-Gries_for_C11-Style_Mem... |