PI: Brijesh Dongol, Co-I: Francois Dupressoir, PhD Students: Elena Vila, Mikhail Semenyuk, University of Surrey, Co-I, John Derrick, University of Sheffield

Computing architectures have recently shifted towards new persistent or non-volatile memory technologies (NVRAM), whose state is preserved even in case of a system crash or loss of power.

  • NVRAM closes the latency gap between different forms of storage and has the potential to vastly improve system speed and stability in systems ranging from personal devices to large data clusters.
  • Rebooting from persistent memory can leave the system in an unsafe/insecure state, as persistent me-mory writes are controlled by the system and the programmer, introducing several research challenges.
  • Information must be persisted in the correct order (in case of a system crash), and moreover, any secrets stored in persistent storage must not be available to unauthorised parties.
  • Our focus is the rigorous development of concurrent programs in systems that use persistent memory.

Our main aim is to develop correctness conditions, programming abstractions and verification methods that enable developers to build safe and secure persistent memory systems. To support scalability, we focus on verified libraries implementing concurrent objects, which form basic software components developers can re-use. To future-proof our results, we conduct our research in the context of cutting-edge techniques on weak memory semantics and associated verification methodologies (including mechanisation in the Isabelle/HOL theorem prover), software libraries (including concurrent objects and transactional memory), and security verification techniques.

We work across the hardware/software interface and consider the impact of low-level read/write primitives on high-level concurrency abstractions. In particular, the work is being conducted in the context of weak memory models for both programming languages (C/C++11) and hardware (Intel-TSO, ARM).

To better understand the atomicity requirements and associated safety properties for NVRAM-based systems, we have developed verification methods for concurrent objects (e.g., stacks, queues). For software transactional memory, we have developed a new notion of atomicity (called durable opacity) and the associated verification techniques.

We are developing high-level logics for reasoning about systems that combine persistency with relaxed accesses from weak memory, forming the first step towards program verification. We are also investigating the interaction between concurrency abstractions and hyper-properties, including within our recent VETSS small grant. Our current works are mechanised within the Isabelle/HOL and KIV theorem provers.

PUBLICATIONS. [1] J. Derrick, S. Doherty, B. Dongol, H. Wehrheim, G. Schellhorn, “Verifying Correctness of Persi-stent Concurrent Data Structures: A Sound and Complete Method.”, Formal Aspects of Computing (2021). [2] E. Bila, J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, H. Wehrheim, “Modularising Verification of Durable Opacity.” (under review). [3] E. Bila, S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, H. Wehrheim, “Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.” FORTE 2020, best paper award.

RELATED GRANTS. VeTSS small grant on Transactional Memory Security (£30k). EPSRC Cross Research Institute Grant on Verifiably Correct Swarm Attestation (£514k): Brijesh Dongol (PI), Santanu Dash (co-I), Helen Treharne (co-I) and Liqun Chen (co-I), with project partners Arm, Thales, NTU, and SRI.

IMPACT. Software correctness and security are two fundamental properties that need to be addressed as systems transition to using Non-Volatile Memory (NVM). While program logics, design patterns, and libraries exist for traditional weak-consistent memory, these techniques have to be revised and adapted in the context of NVM. Arm believes that progress on methodologies to guarantee correctness and security of NVM programs is of paramount importance to realize the benefits of NVM. – Gustavo Petri, Staff Research Engineer, Arm Research –