Dagstuhl Seminar 23412
Formal Methods for Correct Persistent Programming
( Oct 08 – Oct 11, 2023 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/23412
Organizers
- Ori Lahav (Tel Aviv University, IL)
- Azalea Raad (Imperial College London, GB)
- Joseph Tassarotti (New York University, US)
- Viktor Vafeiadis (MPI-SWS - Kaiserslautern, DE)
Contact
- Michael Gerke (for scientific matters)
- Simone Schilke (for administrative matters)
Schedule
Many systems and applications need to store data in a durable way. Historically, durable storage devices had considerably higher latency than volatile random-access memory (RAM) and provided interfaces with larger, coarser access granularity. To achieve acceptable performance, applications requiring durable storage were structured to account for these characteristics. However, in recent years, novel storage systems, such as non-volatile memory (NVM), have emerged that provide durability along with performance and access granularity much closer to RAM. This provides the opportunity for applications to achieve durability with much lower latencies.
However, taking full advantage of that opportunity involves restructuring applications to make proper use of these new devices. Doing so requires care because bugs in these parts of applications can cause permanent data loss. Moreover, non-volatile memory interacts in subtle ways with caches and other parts of modern memory hierarchies, making it challenging for programmers to write correct code.
One promising approach to address this challenge is to develop formal methods techniques to certify the absence of bugs in programs using non-volatile memory. This Dagstuhl Seminar brought together experts in non-volatile memory, relaxed memory, concurrency, and formal methods to explore the application of formal methods to programming with persistent memory. Since this subfield involves deep theoretical work, but is also very dependent on technological developments, the participants of the seminar were from a spectrum of backgrounds ranging from theory of verification to hardware specification, design, and testing.
The seminar included a series of talks and discussions, some of which were unplanned additions prompted by topics or misunderstandings identified during earlier parts of the seminar. The addition of these unplanned talks proved beneficial, adding a dynamic element to the event. We decided to forgo smaller break-out sessions based on the feeling that much of the seminar's value was in discussions that spanned from theoretical to practical, drawing on the full range of participants' expertise.
Several recurring themes arose in the talks and following discussions:
- Correctness Criteria and Specifications for Persistent Objects: A number of correctness criteria have been proposed for concurrent objects that persistently store data. Many of these definitions are adaptations of the classical notion of linearizability. However, we discussed ways in which these existing definitions can have surprising consequences when objects are implemented in the setting of weak memory. A related topic was the appropriate guarantees that transactional interfaces should provide, as certain strong guarantees may prevent efficient implementations.
- Liveness: Our discussions revealed a lack of consensus on assumptions that can be made from existing architectures concerning liveness properties, underscoring the need for further research in this area.
- Future of NVM and Related Technologies: NVM remains an emerging technology, and manufacturers continue to announce large changes in plans for future product lines. We discussed the ramifications of these changes and how techniques for the semantics and verification of certain forms of NVM might apply to other persistency models. Moreover, we identified the need for generic verification methods, which would lend themselves more easily to ongoing changes in the exact semantics of the underlying memory system. Indeed, several talks suggested modular approaches for verification, that, to some extent, take the memory model as an input. Related technologies, including Remote Direct Memory Access (RDMA) and Compute Express Link (CXL), were discussed, focusing on the appropriate abstractions and semantics of interfaces for these devices, and challenges with testing these devices.
We believe that these issues will be an important focus in research on formal methods for persistent memory in the future.
Creative Commons BY 4.0
Ori Lahav, Azalea Raad, Joseph Tassarotti, and Viktor Vafeiadis
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?
Ori Lahav, Azalea Raad, Joseph Tassarotti, and Viktor Vafeiadis
- Guillaume Ambal (Imperial College London, GB) [dblp]
- Parosh Aziz Abdulla (Uppsala University, SE) [dblp]
- Mark Batty (University of Kent - Canterbury, GB) [dblp]
- Michael D. Bond (Ohio State University - Columbus, US) [dblp]
- Ahmed Bouajjani (Université Paris Cité, FR) [dblp]
- Paulo Emílio de Vilhena (Imperial College London, GB) [dblp]
- Brijesh Dongol (University of Surrey - Guildford, GB) [dblp]
- Michal Friedman (ETH Zürich, CH) [dblp]
- Ohad Kammar (University of Edinburgh, GB) [dblp]
- Jeehoon Kang (KAIST - Daejeon, KR) [dblp]
- Vasileios Klimis (Queen Mary University of London, GB)
- Michalis Kokologiannakis (MPI-SWS - Kaiserslautern, DE) [dblp]
- Ori Lahav (Tel Aviv University, IL) [dblp]
- Anton Podkopaev (JetBrains - Amsterdam, NL) [dblp]
- Hernán Ponce de León (Huawei Technologies - München, DE) [dblp]
- Azalea Raad (Imperial College London, GB) [dblp]
- Alastair Reid (Intel - London, GB) [dblp]
- Michael Scott (University of Rochester, US) [dblp]
- Léo Stefanesco (MPI-SWS - Kaiserslautern, DE) [dblp]
- Milijana Surbatovich (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Joseph Tassarotti (New York University, US) [dblp]
- Viktor Vafeiadis (MPI-SWS - Kaiserslautern, DE) [dblp]
- Haris Volos (University of Cyprus - Nicosia, CY) [dblp]
- Heike Wehrheim (Universität Oldenburg, DE) [dblp]
Related Seminars
- Dagstuhl Seminar 21462: Foundations of Persistent Programming (2021-11-14 - 2021-11-17) (Details)
Classification
- Distributed / Parallel / and Cluster Computing
- Programming Languages
Keywords
- non-volatile-memory
- persistency
- verification
- formal methods
- concurrency
