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.
- PerSeVerE: Persistency semantics for verification under ext4
Proc. ACM Program. Lang. 5, POPL, Article 43 (January 2021)
- Persistent Owicki-Gries reasoning: A program logic for reasoning about persistent programs on Intel-x86.
Proc. ACM Program. Lang. 4, OOPSLA, Article 151 (November 2020)
- Persistency semantics of the Intel-x86 architecture.
Proc. ACM Program. Lang. 4, POPL, Article 11 (January 2020)
- Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models.
Proc. ACM Program. Lang. 3, OOPSLA, Article 137 (October 2019)
- Persistence semantics for weak memory: Integrating epoch persistency with the TSO memory model.
Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (November 2018)
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).