Practical and Formal Infrastructure for Nonvolatile Memory

April 4, 2019

Joseph Izraelevitz


Practical and Formal Infrastructure for Nonvolatile Memory

Time:   10:45am
Location:   Meeting room 302 (Mountain View), level 3

For decades, programmers have interacted with persistent storage via a well-defined block-based API, namely, that of the file system. However, it is expected that byte-addressable nonvolatile memory (NVM) will soon be commonplace, potentially transforming main memory into a storage device. This transition forces fundamental changes in how to reason about and manage persistent storage. The possibility that programmers may wish for data in main memory to survive program runs and even system crashes suggests the need to reassess design decisions at all levels of the system stack.

This talk will discuss how system architecture and formal foundations are changing to meet the demands of NVM at all scales. At a formal level, we explore what it means for a program to be “correct” on a machine with NVM. At the hardware level, extensions of memory consistency control the ordering and timing of writes into persistence. At the library level, data structures are transformed to be consistent not only in the face of concurrent access, but also in the wake of crashes. Finally, at the compiler and language level, extensions to transactional memory give programmers the ability to ensure that complex changes to persistent state are not only isolated and consistent, but also failure atomic and durable. We conclude by discussing the second-order effects of these changes and how we expect the software ecosystem will mutate after NVM has become deeply integrated into the stack.