Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
- Submitting institution
-
The University of Surrey
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 9025839_5
- Type
- D - Journal article
- DOI
-
10.1007/978-3-030-50086-3_3
- Title of journal
- Formal Techniques for Distributed Objects, Components, and Systems;Lecture Notes in Computer Science
- Article number
- -
- First page
- 39-58
- Volume
- 12136
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- -
- Year of publication
- 2020
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper won the best paper award at FORTE 2020. Non-volatile memory (NVM) is a new memory technology that preserves memory contents even under a system crash. It improves system both stability and recoverability, thus there is substantial industry (e.g., Intel and Arm) interest across hardware and software. However, NVM also requires traditional notions of safety to be redefined. This paper is significant because it provides foundations for high-performance concurrent algorithms under NVM by developing the first formal notion of correctness for transactional memory, verifying a durable version of a software transactional memory algorithm with proofs mechanised in Isabelle/HOL.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -