A common theme of computing applications is the need to persist their data to durable storage. The landscape of durable storage options and requirements, however, has changed significantly in recent years. Novel storage systems, such as non-volatile memory (NVM), combine the performance characteristics of RAM with the durability guarantees of disks, while novel deployment contexts, such as intermittent computing, require durability at a much finer gain because of frequent power failures.

These new characteristics and requirements provide us an opportunity to redesign and improve the performance of the key components of file systems, databases, and other storage systems that must store data durably. Such redesign, however, is by no means easy because many aspects of these novel systems are challenging to use correctly. For instance, NVM writes are made persistent at a much finer granularity than conventional disk writes and in a way that may contradict program order. This requires programmers to carefully structure their software, and failure to do so can leave data in an inconsistent and irrecoverable state if a system crashes.

Formal methods techniques, such as program logics, static analysis, theorem proving, model checking, and fuzzing, can be used to prevent such errors, and have already been applied to verify toy programs with durable storage requirements. However, existing formal methods are not yet able to handle the full complexity and range of uses needed for realistic systems.

Building upon recent formal semantic models and frameworks for NVM, this Dagstuhl Seminar will bring together experts in verification, formal methods, programming language semantics, and persistent memory to explore new formal verification techniques for persistent memory. We seek to enable conversations and solutions cutting across different sub-communities in verification (e.g., program logics and model checking) and between different instances of persistency (e.g., non-volatile memory and durable disk storage).

This seminar will cover several concrete research challenges, including:

• How do the recent changes in NVM technology and its deployment affect scientific work in this area?
• How can we relax and generalise the notion of correctness for persistent programs?
• How can we bridge the gap between existing persistency models and those assumed by verification tools?
• What are the trade-offs between expressive, comprehensive and scalable persistency verification techniques?
• How can we import and adapt existing verification techniques from other domains to persistency?

Creative Commons BY 4.0

Ori Lahav, Azalea Raad, Joseph Tassarotti, and Viktor Vafeiadis