Semantics for Persistent Memory

Summary

Non-volatile memory (NVM) is emerging as a technology that may significantly impact the computing landscape in the near future. NVM ensures durability of data across power failures (i.e., as hard drives do) at a performance close to that of conventional volatile memory (RAM). Nevertheless, NVM is quite difficult to use correctly because of data caches: the writes do not persist to memory immediately when performed by a program and may further be reordered. In order to ensure that writes are propagated to memory in the correct order and that all writes have persisted to memory, the programmers have to use special barrier and cache flushing instructions.

This project is primarily concerned with the formalization of the semantics of such instructions and their interaction with the weak consistency model followed by each architecture. In addition, we develop correctness conditions for programs running over persistent memory and techniques to prove such programs correct.

Papers

• Persistency semantics of the Intel-x86 architecture.
  Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis.
  Proc. ACM Program. Lang. 4, POPL, Article 11 (January 2020)
  [Paper] [Appendix] [@ACM] [Talk video]
• Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models.
  Azalea Raad, John Wickerson, and Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, OOPSLA, Article 135 (October 2019)
  [Paper] [Appendix] [@ACM] [Slides] [Talk video]
• Persistence semantics for weak memory: Integrating epoch persistency with the TSO memory model.
  Azalea Raad and Viktor Vafeiadis.
  Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (November 2018)
  [Paper] [@ACM] [Appendix] [Slides] [Talk video] [Webpage]

People

• Azalea Raad (Imperial College London, formely MPI-SWS)
• John Wickerson (Imperial College London)
• Viktor Vafeiadis (MPI-SWS)