Modern society depends on storing and accessing vast quantities of data, at ever-increasing speeds. This global data reliance is underpinned by fast and reliable storage solutions. To meet our conflicting desiderata of fast and persistent data, storage hardware is traditionally divided into two categories: fast, byte-addressable memory (e.g. RAM) that is volatile (it loses its contents after a crash, e.g. power loss); and slow, block-addressable storage (e.g. hard disks) that is persistent (its contents survive crashes). However, advances in cutting-edge non-volatile memory (NVM) render this dichotomy obsolete by combining the strengths of both: NVM provides fast, byte-addressable access as with DRAM, while ensuring persistence across crashes as with hard disks.

NVM (persistent memory) has recently become commercially available through products such as Intel Optane which already has a larger capacity than DRAM, its access latency and throughput are within an order of magnitude of DRAM and 2-3 orders of magnitude better than hard disks. With DRAM scalability increasingly becoming an obstacle, NVM is expected to grow in importance and to complement or even supplant DRAM in the near future, which will inevitably lead to substantial changes in software and its engineering.

Existing persistency research has made commendable strides in several directions:

• Architecture (low-level) persistency models: The two major mainstream architectures (Intel-x86 in desk-top/server computing and ARMv8 for mobile/embedded computing) provide support for NVM programming via instructions for managing and flushing the cache, with their persistency semantics recently formalised.
• Libraries: Existing work includes several persistent libraries and data structures. Most notably, PMDK is an industry-backed library by Intel, providing low-level NVM primitives and a few persistent data structures.
• Verification: Verifying persistent code has recently attracted the attention of the formal methods community; with the proliferation of persistency architectures this area will undoubtedly grow in importance and popularity.

All in all, persistent programming and persistency semantics are highly active research areas; nevertheless, there are several directions in which the existing work on persistency is lacking, leading to a research gap, including:

• Persistency validation and testing: Although the existing formal persistency models of mainstream architectures are a good starting point, they have a key limitation in that they lack validation: they were devised after discussions with processor architects, but were not checked against existing hardware implementations. This is a significant gap: closely related work on testing processor consistency semantics revealed errors in prior models, bugs in deployed hardware implementations, and even led to changes in the official architecture specifications.
• Language (high-level) persistency models: There is currently no high-level support for persistent programming in mainstream languages such as C/C++ and Rust. Specifically, there are currently only a handful of academic proposals for high-level persistency which suffer two main drawbacks: they cannot be implemented efficiently and lack verified implementations. For instance, they rely on primitives such as persistent fences to enforce persist-ordering on writes. However, such primitives may not be efficiently implementable on mainstream architectures, and thus may not be supported by architecture vendors in the foreseeable future. As such, these proposals cannot currently be reasonably implemented on existing hardware, thus lacking compilation schemes.
• Persistent libraries and data structures: With a few notable exceptions such as PMDK, there is currently little work on implementing persistent libraries and data structures. The main drawback of PMDK and similar (less-developed) libraries is that they lack formal specifications, and given the current lack of testing infrastructure for persistency, it is unclear if their implementations are correct.
• General correctness conditions for persistency: A key challenge in verifying persistent implementations is defining a general correctness condition for persistent libraries. The only existing such condition is durable linearisability, a simple extension of the well-known linearisability criterion to persistency. Although a useful starting point, durable linearisability has a key drawback: it presupposes strong consistency and does not cater to the more realistic weak consistency setting. As such, durable linearisability is too strong and is not suitable for verifying libraries implemented in mainstream languages (e.g. C/C++) with weak consistency guarantees.

In this Dagstuhl Seminar we aim to take the first steps to close this gap by bringing together a diverse group of world-renowned researchers on formal concurrency and persistency semantics and leading industry practitioners including chief hardware architects, concurrent software developers and experts on programming language design and standards. The seminar is structured along the four topics above to facilitate an interdisciplinary interchange between the theory and practice of persistency, thereby fostering the development of rigorous foundations for persistent programming.

Creative Commons BY 3.0 DE

Hans-J. Boehm, Ori Lahav, and Azalea Raad