TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


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

Contact

Shared Documents

Schedule

Motivation

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?
Copyright Ori Lahav, Azalea Raad, Joseph Tassarotti, and Viktor Vafeiadis

Participants

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