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)
Dagstuhl Reports
As part of the mandatory documentation, participants are asked to submit their talk abstracts, working group results, etc. for publication in our series Dagstuhl Reports via the Dagstuhl Reports Submission System.
- Upload (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
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
- 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
