Verifiably Correct Transactional Memory

Lead Research Organisation: University of Surrey
Department Name: Computing Science

Abstract

Multi-core computing architectures have become ubiquitous over the last decade. This has been driven by the demand for continual performance improvements to cope with the ever-increasing sophistication of applications, combined with physical limitations on chip designs, whereby speedup via higher clock speeds has become infeasible. The inherent parallelism that multi-core architectures entail offers great technical opportunities, however, exploiting these opportunities presents a number of technical challenges.

To ensure correctness, concurrent programs must be properly synchronised, but synchronisation invariably introduces sequential bottlenecks, causing performance to suffer. Fully exploiting the potential for concurrency requires optimisations to consider executions at low levels of abstraction, e.g., the underlying memory model, compiler optimisations, cache-coherency protocols etc. The complexity of such considerations means that checking correctness with a high degree of confidence is extremely difficult. Concurrency bugs have specifically been attributed to disasters such as a power blackout in north eastern USA, Nasdaq's botched IPO of Facebook shares, and the near failure of NASA's Mars Pathfinder mission. Other safety-critical errors have manifested from using low-level optimisations, e.g., the double-checked locking bug and the Java Parker bug.

This project improves programmability of concurrent programs through the use of transactional memory (TM), which is a concurrency mechanism that makes low-level optimisations available to general application programmers. TM is an adaptation of transactions from databases. TM operations are highly concurrent (which improves efficiency), yet manage synchronisation on behalf of a programmer to provide an illusion of atomicity. Thus, by using TM, the focus of a programmer switches from what should be made atomic, as opposed to how atomicity should be guaranteed. This means concurrent systems can be developed in a layered manner (enabling a separation of concerns).

The attractive set of features that TM promises means that TM implementations are increasingly being incorporated into mainstream systems (hardware and software). Since the adaptation of transactions from database theory in the mid 1990s, software TM implementations are now available for all major programming languages. Recent advances include experimental features in compilers such as G++ 4.7 that directly enable compilation of transactional code; standardisation work to include TM within C++ is ongoing. There is extensive research interest in hybrid TM within both academia and industry to make best use of, for example, TM features in Intel's Haswell/Broadwell and IBM's Blue Gene/Q processors.

The high level of complexity, yet wide-scale applicability of TM means that implementations must be formally verified to ensure dependability and reliability.

This project addresses some of the main challenges surrounding TM, and takes the key steps necessary to facilitate wide-scale adoption. Namely, we deliver theoretical advances in our understanding of TM correctness; methodological advances in verification techniques for TM; and pragmatic advances via the development of application-aware TM designs. Verification tools will support each of these steps. We therefore set the following objectives:

O1. Develop foundations for TM correctness (atomicity and interaction guarantees) under different execution models and relate these to client correctness.
O2. Mechanically verify correctness of TM implementations, and develop principled proof techniques.
O3. Design TM implementations that provide better performance under current and future multi-core hardware.
O4. Develop tool support to simplify mechanised verification of TM and automated checking of client programs that use them.

Overall, we will improve the dependability, performance, and flexibility of TM implementations.
 
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 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 Transactional Memory Security
Amount £31,063 (GBP)
Organisation National Cyber Security Centre 
Sector Public
Country United Kingdom
Start 01/2021 
End 03/2021
 
Description FDR models for the SEFM 2021 paper "Checking Opacity and Durable Opacity with FDR" 
Type Of Technology  
Year Produced 2021 
Open Source License? Yes  
URL https://figshare.com/articles/software/FDR_models_for_Checking_Opacity_and_Durable_Opacity_with_FDR_...
 
Description FDR models for the SEFM 2021 paper "Checking Opacity and Durable Opacity with FDR" 
Type Of Technology  
Year Produced 2021 
Open Source License? Yes  
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  
Year Produced 2021 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_Files_for_Integrating_Owicki-Gries_for_C11-Style_Mem...
 
Description Isabelle files for "Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL".The proofs require Isabelle/HOL 2020. 
Type Of Technology  
Year Produced 2021 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_Files_for_Integrating_Owicki-Gries_for_C11-Style_Mem...
 
Description Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. 
Type Of Technology  
Year Produced 2022 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_files_for_View-Based_Owicki-Gries_Reasoning_for_Pers...
 
Description Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. 
Type Of Technology  
Year Produced 2022 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_files_for_View-Based_Owicki-Gries_Reasoning_for_Pers...
 
Description Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. 
Type Of Technology  
Year Produced 2022 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_files_for_View-Based_Owicki-Gries_Reasoning_for_Pers...