PERSIST: A Semantic Foundation for Persistent Programming

Summary

Non-volatile memory (NVM) is an emerging technology that provides orders of magnitude faster access to persistent storage (which preserves its contents after a crash or a power failure) than hard disks.

While NVM is expected to radically change how we manage storage in applications, its programming model is standing on very shaky foundations. The persistency semantics of the mainstream architectures is unclear and full of counterintuitive behaviours. As a result, writing correct NVM programs is extremely difficult.

The project's goal is to develop a solid mathematical basis for determining the possible outcomes of persistent programs and reasoning about their correctness. More specifically, we aim to produce:

• Formal persistency models for mainstream hardware architectures,
• Formal persistency models for mainstream programming languages,
• Firmly-grounded higher-level abstractions to ease persistent programming, and
• Effective testing and verification techniques for persistent programs.

Project publications

• SPORE: Combining symmetry and partial order reduction.
  Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
  Proc. ACM Program. Lang. 8, PLDI, Article 219 (June 2024)
  [Paper] [More...]
• Enhancing GenMC's usability and performance.
  Michalis Kokologiannakis, Rupak Majumdar, Viktor Vafeiadis
  In TACAS 2024
  [Paper] [More...]
• Specifying and verifying persistent libraries.
  Leo Stefanesco, Azalea Raad, Viktor Vafeiadis
  In ESOP 2024
  [Paper]
• Optimal bounded partial order reduction.
  Iason Marmanis, Viktor Vafeiadis
  In FMCAD 2023, pp. 86–91 (October 2023)
  [Paper] [@TU Wien]
• Unblocking dynamic partial order reduction.
  Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
  In CAV 2023, pp. 230-250 (July 2023)
  [Paper] [@Springer] [Appendix] [Artifact @Zenodo]
• Reconciling preemption bounding with DPOR.
  Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis.
  In TACAS 2023 (April 2023)
  [Paper]
• Kater: Automating weak memory model metatheory and consistency checking.
  Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 7, POPL, Article 19 (January 2023)
  [Paper] [@ACM] [Artifact @Zenodo]
• The Path to Durable Linearizability.
  Emanuele D’Osualdo, Azalea Raad, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 7, POPL, Article 26 (January 2023)
  [Paper] [@ACM]
• SMT-based verification of persistency invariants of Px86 programs.
  Iason Marmanis, Viktor Vafeiadis.
  In VSTTE 2022 (October 2022)
  [Paper]
• Model checking for a multi-execution memory model.
  Evgenii Moiseenko, Michalis Kokologiannakis, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, OOPSLA2, Article 152 (October 2022)
  [Paper] [@ACM] [Artifact @Zenodo]
• Truly stateless, optimal dynamic partial order reduction.
  Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, POPL, Article 49 (January 2022)
  [Paper] [@ACM] [Artifact @Zenodo]
• Extending Intel-x86 consistency and persistency: Formalising the semantics of Intel-x86 memory types and non-temporal stores.
  Azalea Raad, Luc Maranget, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, POPL, Article 22 (January 2022)
  [Paper] [@ACM] [Artifact @Inria]
• Making weak memory models fair.
  Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 5, OOPSLA, Article 98 (October 2021)
  Distinguished paper award at OOPSLA'21
  [Paper] [@ACM] [@arXiv] [Artifact @Zenodo]
• Dynamic partial order reductions for spinloops.
  Michalis Kokologiannakis, Xiaowei Ren, Viktor Vafeiadis.
  In FMCAD 2021 (October 2021)
  [Paper] [@IEEE] [More...]
• The challenges of weak persistency.
  Viktor Vafeiadis.
  In CALCO 2021. LIPIcs 211, pp. 4:1–4:3 (September 2021)
  [Paper] [@Dagstuhl]
• GenMC: A model checker for weak memory models.
  Michalis Kokologiannakis, Viktor Vafeiadis.
  In CAV 2021 (July 2021)
  [Paper] [@Springer] [Artifact @Zenodo] [More...]
• BAM: Efficient model checking for barriers.
  Michalis Kokologiannakis, Viktor Vafeiadis.
  In NETYS 2021 (May 2021)
  [Paper]

Other relevant publications

• PerSeVerE: Persistency semantics for verification under ext4.
  Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 5, POPL, Article 43 (January 2021)
  [Paper] [@ACM] [More...]
• Persistent Owicki-Gries reasoning: A program logic for reasoning about persistent programs on Intel-x86.
  Azalea Raad, Ori Lahav, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 4, OOPSLA, Article 151 (November 2020)
  [Paper] [@ACM] [More...]
• Persistency semantics of the Intel-x86 architecture.
  Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 4, POPL, Article 11 (January 2020)
  [Paper] [@ACM] [More...]
• Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models.
  Azalea Raad, John Wickerson, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, OOPSLA, Article 137 (October 2019)
  [Paper] [@ACM] [More...]
• Persistence semantics for weak memory: Integrating epoch persistency with the TSO memory model.
  Azalea Raad, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (November 2018)
  [Paper] [@ACM] [More...]

This project is funded from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101003349).